CakeML:fa3ffad93124487cb6181834a9cf54c77dc6c6df
Adjust compilerXXProgScript whole_prog_spec proofs
#515 (opentheory-reader)
Merging into:48b96e8ed899928f3fa40f6f2237bb33e9ea8c25
Merge pull request #512 from CakeML/translator-module-ctors
HOL:b440d91de4ea0da60e3ebf207c5accaaf9892bf6
Fix ParseDatatype bug when parsing Datatype syntax
Machine:demi
Claimed job
Reusing HOL
Starting developers/bin
Finished developers/bin 6s 923MB
Starting semantics/ffi
Finished semantics/ffi 16s 303MB
Starting semantics
Finished semantics 1m46s 967MB
Starting semantics/proofs
Finished semantics/proofs 3m53s 1GB
Starting basis/pure
Finished basis/pure 1m13s 662MB
Starting translator
Finished translator 1m35s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m09s 1GB
Starting characteristic
Finished characteristic 3m36s 1GB
Starting translator/monadic
Finished translator/monadic 2m03s 1GB
Starting basis
Finished basis 23m21s 2GB
Starting compiler/inference
Finished compiler/inference 1m55s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 42s 1GB
Starting compiler/backend/gc
FAILED: compiler/backend/gc
]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/machine-code/multiword]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/balanced_bst]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/l3-machine-code/common]0;Holmake: ~/cakeml/regression-worker/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
Starting work on temporal_stateTheory
temporal_stateTheory OK
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
Starting work on asmTheory
asmTheory OK
Starting work on asmSemTheory
asmSemTheory OK
Starting work on asmPropsTheory
asmPropsTheory OK
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
Starting work on heap
heap OK
Starting work on backend_commonTheory
Starting work on db_varsTheory
Starting work on jsonLangTheory
Starting work on labLangTheory
labLangTheory OK
Starting work on lab_filterTheory
jsonLangTheory OK
Starting work on reachabilityTheory
db_varsTheory OK
Starting work on exportTheory
backend_commonTheory OK
Starting work on closLangTheory
lab_filterTheory OK
Starting work on stackLangTheory
exportTheory OK
Starting work on flatLangTheory
stackLangTheory OK
Starting work on wordLangTheory
closLangTheory OK
Starting work on bviTheory
bviTheory OK
Starting work on dataLangTheory
flatLangTheory OK
Starting work on bvi_letTheory
dataLangTheory OK
Starting work on data_liveTheory
reachabilityTheory OK
Starting work on data_simpTheory
wordLangTheory OK
Starting work on data_spaceTheory
bvi_letTheory OK
Starting work on bvi_tailrecTheory
data_simpTheory OK
Starting work on bvlTheory
bvlTheory OK
Starting work on bvl_constTheory
data_liveTheory OK
Starting work on bvl_jumpTheory
bvl_jumpTheory OK
Starting work on clos_annotateTheory
data_spaceTheory OK
Starting work on bvi_to_dataTheory
clos_annotateTheory OK
Starting work on clos_callTheory
bvi_to_dataTheory OK
clos_callTheory OK
Starting work on clos_knownTheory
Starting work on clos_mtiTheory
clos_mtiTheory OK
Starting work on clos_numberTheory
clos_numberTheory OK
Starting work on word_bignumTheory
bvi_tailrecTheory OK
Starting work on word_allocTheory
clos_knownTheory OK
Starting work on clos_to_bvlTheory
word_bignumTheory OK
Starting work on word_instTheory
clos_to_bvlTheory OK
Starting work on word_removeTheory
word_removeTheory OK
Starting work on word_simpTheory
word_instTheory OK
Starting work on patLangTheory
patLangTheory OK
Starting work on flat_to_patTheory
flat_to_patTheory OK
Starting work on lab_to_targetTheory
lab_to_targetTheory OK
Starting work on pat_to_closTheory
word_simpTheory OK
Starting work on displayLangTheory
displayLangTheory OK
Starting work on flat_elimTheory
pat_to_closTheory OK
Starting work on flat_exh_matchTheory
word_allocTheory OK
Starting work on word_to_wordTheory
flat_exh_matchTheory OK
Starting work on flat_reorder_matchTheory
word_to_wordTheory OK
Starting work on flat_uncheck_ctorsTheory
flat_elimTheory OK
Starting work on stack_namesTheory
flat_reorder_matchTheory OK
Starting work on stack_removeTheory
flat_uncheck_ctorsTheory OK
Starting work on source_to_flatTheory
stack_namesTheory OK
Starting work on word_to_stackTheory
stack_removeTheory OK
Starting work on clos_letopTheory
source_to_flatTheory OK
Starting work on presLangTheory
clos_letopTheory OK
Starting work on clos_ticksTheory
presLangTheory OK
Starting work on word_elimTheory
clos_ticksTheory OK
word_elimTheory OK
word_to_stackTheory OK
bvl_constTheory FAILED! <Signal 9>
]0;Holmake: .