OverviewCakeML:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
Stop assuming term eqtype in ml_monad_translatorBase
HOL:f6cebae5343aba271ecb51708ac30766ab496ee4
Git-Ignore Thm-sig.sml (new name for what was Thm.sig)
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 22MB
Starting developers/bin
Finished developers/bin 33s 143MB
Starting semantics/ffi
Finished semantics/ffi 32s 509MB
Starting semantics
Finished semantics 1m28s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m54s 1GB
Starting basis/pure
Finished basis/pure 3m32s 789MB
Starting translator
Finished translator 1m33s 1GB
Starting compiler/parsing
Finished compiler/parsing 57s 1GB
Starting characteristic
Finished characteristic 4m15s 1GB
Starting translator/monadic
Finished translator/monadic 1m22s 1GB
Starting basis
FAILED: basis
]0;Holmake: pure]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: pure]0;Holmake: ~/regression/cakeml-737/misc]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-737/misc]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f6cebae5343aba271ecb51708ac30766ab496ee4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-737/misc]0;Holmake: ~/regression/cakeml-737/developers]0;Holmake: ~/regression/cakeml-737/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-737/misc]0;Holmake: ~/regression/cakeml-737/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-737/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-737/misc]0;Holmake: ~/regression/cakeml-737/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-737/characteristic]0;Holmake: ~/regression/cakeml-737/compiler/parsing]0;Holmake: ~/regression/cakeml-737/semantics]0;Holmake: ~/regression/cakeml-737/semantics/ffi]0;Holmake: ~/regression/cakeml-737/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-737/semantics]0;Holmake: ~/regression/cakeml-737/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-737/compiler/parsing]0;Holmake: ~/regression/cakeml-737/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-737/characteristic]0;Holmake: ~/regression/cakeml-737/semantics/proofs]0;Holmake: ~/regression/cakeml-737/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-737/characteristic]0;Holmake: ~/regression/cakeml-737/translator]0;Holmake: ~/regression/cakeml-737/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-737/characteristic]0;Holmake: ~/regression/cakeml-737/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-737/translator/monadic]0;Holmake: ~/regression/cakeml-737/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-737/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-737/translator/monadic]0;Holmake: ~/regression/cakeml-737/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-737/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