OverviewCakeML:c2e2c5c2f7953ae5aff38252a9fb13eb3eb519c5
fix translator/ for record name issues from HOL
HOL:07333a55d32781dee415b101c776bae67ef23606
Fix Unicode violations in recent commit
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 121MB
Starting developers/bin
Finished developers/bin 5s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 301MB
Starting semantics
Finished semantics 1m25s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m31s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 398MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m11s 1GB
Starting basis/pure
Finished basis/pure 53s 1GB
Starting translator
Finished translator 3m18s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m09s 2GB
Starting characteristic
Finished characteristic 5m42s 3GB
Starting translator/monadic
Finished translator/monadic 1m48s 2GB
Starting basis
FAILED: basis
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md real: 0s user: 0s OK
Starting work on runtimeFFITheory
MarshallingTheory real: 11s user: 11s OK
Starting work on fsFFITheory
runtimeFFITheory real: 12s user: 11s OK
Starting work on basis_ffi.o
basis_ffi.o real: 0s user: 0s OK
clFFITheory real: 14s user: 13s OK
RuntimeProgTheory real: 22s user: 21sFAIL<1>
error in quse /home/myreen/regression/cakeml-1521/characteristic/cfLetAutoLib.sml : HOL_ERR {message = "\"sem_env_c\" not found in theory \"semanticPrimitives\"", origin_function = "prim_mk_const", origin_structure = "Term"}
error in load $(CAKEMLDIR)/characteristic/cfLetAutoLib : HOL_ERR {message = "\"sem_env_c\" not found in theory \"semanticPrimitives\"", origin_function = "prim_mk_const", origin_structure = "Term"}
error in load $(CAKEMLDIR)/characteristic/cfLib : HOL_ERR {message = "\"sem_env_c\" not found in theory \"semanticPrimitives\"", origin_function = "prim_mk_const", origin_structure = "Term"}
error in load $(CAKEMLDIR)/basis/basisFunctionsLib : HOL_ERR {message = "\"sem_env_c\" not found in theory \"semanticPrimitives\"", origin_function = "prim_mk_const", origin_structure = "Term"}
error in load /home/myreen/regression/cakeml-1521/basis/RuntimeProgScript : HOL_ERR {message = "\"sem_env_c\" not found in theory \"semanticPrimitives\"", origin_function = "prim_mk_const", origin_structure = "Term"}
Uncaught exception: HOL_ERR {message = "\"sem_env_c\" not found in theory \"semanticPrimitives\"", origin_function = "prim_mk_const", origin_structure = "Term"}
fsFFITheory M-KILLED