CakeML:3307d9840e93caaed0969c033bf55b654361b12a
Fix examples/array_searchProg for HOL's change to MEM_DROP thms
HOL:8a1dd56be791249751d00e89a4f65bc95edcb755
Announce add_strliteral_form in release notes
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 37MB
Starting developers/bin
Finished developers/bin 3s 144MB
Starting semantics/ffi
Finished semantics/ffi 32s 501MB
Starting semantics
Finished semantics 1m28s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m55s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 5s 312MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 1m45s 881MB
Starting basis/pure
Finished basis/pure 3m29s 617MB
Starting translator
Finished translator 1m39s 1GB
Starting compiler/parsing
Finished compiler/parsing 56s 2GB
Starting characteristic
Finished characteristic 5m09s 1GB
Starting translator/monadic
Finished translator/monadic 1m25s 1GB
Starting basis
Finished basis 16m49s 2GB
Starting compiler/inference
Finished compiler/inference 1m47s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 57s 1GB
Starting compiler/backend/gc
FAILED: compiler/backend/gc
]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
Starting work on multiwordTheory
multiwordTheory OK
Starting work on mc_multiwordTheory
mc_multiwordTheory OK
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-935/basis/pure]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/balanced_bst]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-935/basis/pure]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-935/basis/pure]0;Holmake: ~/regression/cakeml-935/misc]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-935/misc]0;Holmake: ~/regression/cakeml-935/developers]0;Holmake: ~/regression/cakeml-935/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-935/misc]0;Holmake: ~/regression/cakeml-935/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-935/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-935/misc]0;Holmake: ~/regression/cakeml-935/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-935/basis/pure]0;Holmake: ~/regression/cakeml-935/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-935/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-935/semantics]0;Holmake: ~/regression/cakeml-935/semantics/ffi]0;Holmake: ~/regression/cakeml-935/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-935/semantics]0;Holmake: ~/regression/cakeml-935/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-935/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-935/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-935/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-935/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: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8a1dd56be791249751d00e89a4f65bc95edcb755/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
Starting work on tripleTheory
Starting work on stateTheory
tripleTheory OK
stateTheory OK
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
Starting work on README.md
README.md OK
asmTheory OK
Starting work on asmSemTheory
asmSemTheory OK
Starting work on asmPropsTheory
asmPropsTheory OK
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-935/semantics/proofs]0;Holmake: ~/regression/cakeml-935/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
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 exportTheory
db_varsTheory OK
Starting work on README.md
README.md OK
backend_commonTheory OK
Starting work on closLangTheory
Starting work on stackLangTheory
lab_filterTheory OK
Starting work on flatLangTheory
exportTheory OK
Starting work on lab_to_targetTheory
stackLangTheory OK
Starting work on wordLangTheory
closLangTheory OK
Starting work on bviTheory
flatLangTheory OK
Starting work on dataLangTheory
bviTheory OK
Starting work on bvi_letTheory
wordLangTheory OK
Starting work on bvi_tailrecTheory
lab_to_targetTheory OK
Starting work on bvlTheory
dataLangTheory OK
Starting work on data_liveTheory
bvi_letTheory OK
Starting work on data_simpTheory
bvlTheory OK
Starting work on data_spaceTheory
data_simpTheory OK
Starting work on bvl_constTheory
data_liveTheory OK
Starting work on bvl_jumpTheory
data_spaceTheory OK
Starting work on bvi_to_dataTheory
bvl_jumpTheory OK
Starting work on clos_annotateTheory
clos_annotateTheory OK
Starting work on clos_callTheory
bvi_to_dataTheory OK
Starting work on clos_fvsTheory
bvi_tailrecTheory OK
Starting work on clos_letopTheory
clos_callTheory OK
Starting work on clos_ticksTheory
clos_fvsTheory OK
Starting work on clos_labelsTheory
clos_letopTheory OK
Starting work on clos_mtiTheory
clos_ticksTheory OK
Starting work on clos_knownTheory
clos_labelsTheory OK
Starting work on clos_numberTheory
clos_mtiTheory OK
Starting work on word_bignumTheory
clos_numberTheory OK
Starting work on word_allocTheory
bvl_constTheory OK
Starting work on bvl_handleTheory
bvl_handleTheory OK
Starting work on bvl_inlineTheory
clos_knownTheory OK
Starting work on clos_to_bvlTheory
word_bignumTheory OK
Starting work on word_instTheory
bvl_inlineTheory OK
Starting work on bvl_to_bviTheory
clos_to_bvlTheory OK
Starting work on word_removeTheory
word_instTheory OK
Starting work on word_simpTheory
word_removeTheory OK
Starting work on patLangTheory
patLangTheory OK
Starting work on flat_to_patTheory
bvl_to_bviTheory OK
Starting work on pat_to_closTheory
word_allocTheory OK
Starting work on displayLangTheory
flat_to_patTheory OK
Starting work on flat_elimTheory
displayLangTheory OK
Starting work on flat_exh_matchTheory
pat_to_closTheory OK
Starting work on flat_reorder_matchTheory
word_simpTheory OK
Starting work on word_to_wordTheory
flat_elimTheory OK
Starting work on flat_uncheck_ctorsTheory
flat_exh_matchTheory OK
Starting work on stack_namesTheory
flat_reorder_matchTheory OK
Starting work on stack_removeTheory
word_to_wordTheory OK
Starting work on data_to_wordTheory
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 word_elimTheory
source_to_flatTheory OK
Starting work on presLangTheory
word_elimTheory OK
word_to_stackTheory OK
data_to_wordTheory FAILED! <1>
Saved definition __ "Compare1_code_def"
Saved definition __ "Compare_code_def"
Saved definition __ "Equal1_code_def"
Exception raised at Parse.Absyn:
at line 710, character 55:
Lexical error - Character "" is a lexical error
error in quse /home/myreen/regression/cakeml-935/compiler/backend/data_to_wordScript.sml : HOL_ERR {message = "at line 710, character 55:\nLexical error - Character \"\226\" is a lexical error", origin_function = "Absyn", origin_structure = "Parse"}
error in load data_to_wordScript : HOL_ERR {message = "at line 710, character 55:\nLexical error - Character \"\226\" is a lexical error", origin_function = "Absyn", origin_structure = "Parse"}
Uncaught exception: HOL_ERR {message = "at line 710, character 55:\nLexical error - Character \"\226\" is a lexical error", origin_function = "Absyn", origin_structure = "Parse"}
presLangTheory M-KILLED
]0;Holmake: .