OverviewCakeML: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
Building HOL
Starting developers
Finished developers 0s 30MB
Starting developers/bin
Finished developers/bin 33s 142MB
Starting semantics/ffi
Finished semantics/ffi 33s 436MB
Starting semantics
Finished semantics 1m27s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m52s 971MB
Starting basis/pure
Finished basis/pure 3m32s 783MB
Starting translator
Finished translator 1m33s 1GB
Starting compiler/parsing
Finished compiler/parsing 56s 1GB
Starting characteristic
Finished characteristic 4m06s 1GB
Starting translator/monadic
Finished translator/monadic 1m24s 1GB
Starting basis
FAILED: basis
]0;Holmake: pure]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular]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/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: pure]0;Holmake: ~/regression/cakeml-729/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-729/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-729/misc]0;Holmake: ~/regression/cakeml-729/developers]0;Holmake: ~/regression/cakeml-729/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-729/misc]0;Holmake: ~/regression/cakeml-729/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-729/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-729/misc]0;Holmake: ~/regression/cakeml-729/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-729/characteristic]0;Holmake: ~/regression/cakeml-729/compiler/parsing]0;Holmake: ~/regression/cakeml-729/semantics]0;Holmake: ~/regression/cakeml-729/semantics/ffi]0;Holmake: ~/regression/cakeml-729/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-729/semantics]0;Holmake: ~/regression/cakeml-729/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-729/compiler/parsing]0;Holmake: ~/regression/cakeml-729/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-729/characteristic]0;Holmake: ~/regression/cakeml-729/semantics/proofs]0;Holmake: ~/regression/cakeml-729/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-729/characteristic]0;Holmake: ~/regression/cakeml-729/translator]0;Holmake: ~/regression/cakeml-729/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-729/characteristic]0;Holmake: ~/regression/cakeml-729/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-729/translator/monadic]0;Holmake: ~/regression/cakeml-729/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-729/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-729/translator/monadic]0;Holmake: ~/regression/cakeml-729/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-729/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