OverviewCakeML:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
Stop assuming term eqtype in ml_monad_translatorBase
HOL:f535214bfea72da93f045caf3e8a2e2a485bed6f
Add theory presenting abstract view of computation states
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 35MB
Starting developers/bin
Finished developers/bin 34s 204MB
Starting semantics/ffi
Finished semantics/ffi 7s 216MB
Starting semantics
Finished semantics 1m15s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m52s 937MB
Starting basis/pure
Finished basis/pure 43s 677MB
Starting translator
Finished translator 1m36s 1GB
Starting compiler/parsing
Finished compiler/parsing 56s 2GB
Starting characteristic
Finished characteristic 4m11s 1GB
Starting translator/monadic
Finished translator/monadic 1m22s 1GB
Starting basis
FAILED: basis
]0;Holmake: pure]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: pure]0;Holmake: ~/regression/cakeml-728/misc]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-728/misc]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f535214bfea72da93f045caf3e8a2e2a485bed6f/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-728/misc]0;Holmake: ~/regression/cakeml-728/developers]0;Holmake: ~/regression/cakeml-728/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-728/misc]0;Holmake: ~/regression/cakeml-728/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-728/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-728/misc]0;Holmake: ~/regression/cakeml-728/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-728/characteristic]0;Holmake: ~/regression/cakeml-728/compiler/parsing]0;Holmake: ~/regression/cakeml-728/semantics]0;Holmake: ~/regression/cakeml-728/semantics/ffi]0;Holmake: ~/regression/cakeml-728/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-728/semantics]0;Holmake: ~/regression/cakeml-728/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-728/compiler/parsing]0;Holmake: ~/regression/cakeml-728/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-728/characteristic]0;Holmake: ~/regression/cakeml-728/semantics/proofs]0;Holmake: ~/regression/cakeml-728/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-728/characteristic]0;Holmake: ~/regression/cakeml-728/translator]0;Holmake: ~/regression/cakeml-728/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-728/characteristic]0;Holmake: ~/regression/cakeml-728/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-728/translator/monadic]0;Holmake: ~/regression/cakeml-728/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-728/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-728/translator/monadic]0;Holmake: ~/regression/cakeml-728/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-728/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