Overview

Job 730

CakeML:62cb1c63146009d550cace769499732f81cc45b3
  Stop assuming term eqtype in cfLetAutoLib
#618 (monadic-trans-cleanup)
Merging into:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
  Stop assuming term eqtype in ml_monad_translatorBase
HOL:45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1
  Testing for src/Boolify
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  22MB
 Starting developers/bin
 Finished developers/bin                                          33s 142MB
 Starting semantics/ffi
 Finished semantics/ffi                                            7s 227MB
 Starting semantics
 Finished semantics                                             1m15s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m50s   1GB
 Starting basis/pure
 Finished basis/pure                                              43s 634MB
 Starting translator
 Finished translator                                            1m33s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        56s   2GB
 Starting characteristic
 Finished characteristic                                        4m08s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m22s   1GB
 Starting basis
 Finished basis                                                16m18s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m43s   1GB
 Starting compiler/backend/reg_alloc
 FAILED: compiler/backend/reg_alloc
]0;Holmake: ~/regression/cakeml-730/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-730/misc]0;Holmake: ~/regression/cakeml-730/developers]0;Holmake: ~/regression/cakeml-730/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-730/misc]0;Holmake: ~/regression/cakeml-730/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-730/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-730/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-730/misc]0;Holmake: ~/regression/cakeml-730/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-730/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-730/semantics]0;Holmake: ~/regression/cakeml-730/semantics/ffi]0;Holmake: ~/regression/cakeml-730/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-730/semantics]0;Holmake: ~/regression/cakeml-730/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-730/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-730/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-730/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-730/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Starting work on reg_allocTheory
Starting work on parmoveTheory
Starting work on README.md
README.md                                           OK
reg_allocTheory                            FAILED! <1>
      val ... = ... in mk_comb (case_tm, error_fun) end
 /home/myreen/regression/cakeml-730/translator/monadic/monad_base/ml_monadBaseLib.sml:539: error: Type error in function application.
    Function: List.foldl add_fun case_tm : ''a list -> term
    Argument: funs : term list
    Reason: Can't unify ''a to term (Requires equality type)
 Found near List.foldl add_fun case_tm funs
 error in quse /home/myreen/regression/cakeml-730/translator/monadic/monad_base/ml_monadBaseLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/translator/monadic/monad_base/ml_monadBaseLib : Fail "Static Errors"
 error in load reg_allocScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
parmoveTheory                                 M-KILLED