CakeML:0bca5648f09015518a7629441ff5c3e6174e3731
Fix some things downstream of the tap changes.
#526 (explorer)
Merging into:306e73e0ef0314393ecdbb996b50cf799375f15d
Use Git's -C option
HOL:2a42da875092fdec35e1cd69454995735c890117
Merge pull request #590 from binghe/PSL.fix
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 40s 912MB
Starting semantics/ffi
Finished semantics/ffi 40s 385MB
Starting semantics
Finished semantics 1m31s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m49s 1GB
Starting basis/pure
Finished basis/pure 3m40s 808MB
Starting translator
Finished translator 1m10s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m46s 1GB
Starting characteristic
Finished characteristic 2m30s 1GB
Starting translator/monadic
Finished translator/monadic 1m27s 1GB
Starting basis
Finished basis 17m23s 3GB
Starting compiler/inference
Finished compiler/inference 1m46s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 48s 1GB
Starting compiler/backend/gc
FAILED: compiler/backend/gc
]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/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: ../../../basis/pure]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/balanced_bst]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/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: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/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
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
bvi_letTheory OK
Starting work on data_spaceTheory
data_simpTheory OK
Starting work on bvi_tailrecTheory
wordLangTheory 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
clos_callTheory OK
Starting work on clos_knownTheory
bvi_to_dataTheory OK
Starting work on clos_mtiTheory
clos_mtiTheory OK
Starting work on clos_numberTheory
bvi_tailrecTheory OK
Starting work on word_bignumTheory
clos_knownTheory OK
Starting work on word_allocTheory
bvl_constTheory OK
Starting work on bvl_handleTheory
bvl_handleTheory OK
Starting work on bvl_inlineTheory
word_bignumTheory OK
Starting work on word_instTheory
bvl_inlineTheory OK
Starting work on bvl_to_bviTheory
word_instTheory OK
Starting work on word_removeTheory
word_removeTheory OK
Starting work on word_simpTheory
bvl_to_bviTheory OK
Starting work on patLangTheory
patLangTheory OK
Starting work on flat_to_patTheory
word_allocTheory OK
Starting work on lab_to_targetTheory
word_simpTheory OK
Starting work on word_to_wordTheory
word_to_wordTheory OK
Starting work on data_to_wordTheory
lab_to_targetTheory OK
Starting work on pat_to_closTheory
flat_to_patTheory OK
Starting work on displayLangTheory
displayLangTheory OK
Starting work on flat_elimTheory
pat_to_closTheory OK
Starting work on flat_exh_matchTheory
flat_elimTheory OK
Starting work on flat_reorder_matchTheory
flat_exh_matchTheory OK
Starting work on flat_uncheck_ctorsTheory
flat_uncheck_ctorsTheory OK
Starting work on stack_namesTheory
flat_reorder_matchTheory OK
Starting work on source_to_flatTheory
stack_namesTheory OK
Starting work on stack_removeTheory
source_to_flatTheory OK
Starting work on presLangTheory
stack_removeTheory OK
Starting work on word_to_stackTheory
presLangTheory OK
Starting work on clos_letopTheory
word_to_stackTheory OK
Starting work on clos_ticksTheory
clos_letopTheory OK
Starting work on word_elimTheory
clos_ticksTheory OK
word_elimTheory OK
data_to_wordTheory OK
Starting work on stack_allocTheory
stack_allocTheory OK
Starting work on stack_to_labTheory
stack_to_labTheory OK