OverviewCakeML:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
Stop assuming term eqtype in ml_monad_translatorBase
HOL:04268f2f08fa23acd6991def865b123616cfe6bc
Define a genlist that collects results of fn that may fail
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 30MB
Starting developers/bin
Finished developers/bin 31s 206MB
Starting semantics/ffi
Finished semantics/ffi 33s 493MB
Starting semantics
Finished semantics 1m30s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m54s 1GB
Starting basis/pure
Finished basis/pure 3m31s 719MB
Starting translator
Finished translator 1m35s 1GB
Starting compiler/parsing
Finished compiler/parsing 56s 1GB
Starting characteristic
Finished characteristic 4m10s 1GB
Starting translator/monadic
Finished translator/monadic 1m24s 1GB
Starting basis
FAILED: basis
]0;Holmake: pure]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: pure]0;Holmake: ~/regression/cakeml-743/misc]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-743/misc]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-04268f2f08fa23acd6991def865b123616cfe6bc/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-743/misc]0;Holmake: ~/regression/cakeml-743/developers]0;Holmake: ~/regression/cakeml-743/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-743/misc]0;Holmake: ~/regression/cakeml-743/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-743/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-743/misc]0;Holmake: ~/regression/cakeml-743/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-743/characteristic]0;Holmake: ~/regression/cakeml-743/compiler/parsing]0;Holmake: ~/regression/cakeml-743/semantics]0;Holmake: ~/regression/cakeml-743/semantics/ffi]0;Holmake: ~/regression/cakeml-743/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-743/semantics]0;Holmake: ~/regression/cakeml-743/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-743/compiler/parsing]0;Holmake: ~/regression/cakeml-743/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-743/characteristic]0;Holmake: ~/regression/cakeml-743/semantics/proofs]0;Holmake: ~/regression/cakeml-743/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-743/characteristic]0;Holmake: ~/regression/cakeml-743/translator]0;Holmake: ~/regression/cakeml-743/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-743/characteristic]0;Holmake: ~/regression/cakeml-743/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-743/translator/monadic]0;Holmake: ~/regression/cakeml-743/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-743/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-743/translator/monadic]0;Holmake: ~/regression/cakeml-743/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/basis[0m
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
MarshallingTheory OK
Starting work on fsFFITheory
runtimeFFITheory OK
Starting work on README.md
README.md OK
Starting work on basis_ffi.o
basis_ffi.o OK
clFFITheory OK
RuntimeProgTheory FAILED! <1>
fun ...
fun ...
...
...
end
error in quse /home/myreen/regression/cakeml-743/characteristic/cfLetAutoLib.sml : Fail "Static Errors"
error in load $(CAKEMLDIR)/characteristic/cfLetAutoLib : Fail "Static Errors"
error in load $(CAKEMLDIR)/characteristic/cfLib : Fail "Static Errors"
error in load RuntimeProgScript : Fail "Static Errors"
Uncaught exception: Fail "Static Errors"
fsFFITheory M-KILLED