CakeML Regression Test

Job 526

CakeML:5efe316d210e9a836e219b67008d1267a7cb185f
  Restore translation of explorer components. [Oct 10 10:39:58]
#526 (explorer)
Merging into:2ce1a84a603f5e9acdd2601314dd649077ede745
  Use modules in bootstrap translation. [Oct 11 13:44:11]
HOL:32537a5663e731a4d41cf53adf51cc27b71a0e97
  Get temporal_deep/src/model_check to build by fixing Holmakefile [Oct 11 22:55:58]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 12 14:45:02 Claimed job
Oct 12 14:45:25 Building HOL
Oct 12 14:55:07 Starting developers/bin
Oct 12 14:56:18 Finished developers/bin                                        1m10s 913MB
Oct 12 14:56:19 Starting semantics/ffi
Oct 12 14:56:59 Finished semantics/ffi                                           39s 363MB
Oct 12 14:57:00 Starting semantics
Oct 12 14:58:32 Finished semantics                                             1m31s 938MB
Oct 12 14:58:33 Starting semantics/proofs
Oct 12 15:01:20 Finished semantics/proofs                                      2m46s   1GB
Oct 12 15:01:20 Starting basis/pure
Oct 12 15:05:06 Finished basis/pure                                            3m45s 836MB
Oct 12 15:05:07 Starting translator
Oct 12 15:08:20 Finished translator                                            3m12s   1GB
Oct 12 15:08:20 Starting compiler/parsing
Oct 12 15:09:49 Finished compiler/parsing                                      1m28s   2GB
Oct 12 15:09:50 Starting characteristic
Oct 12 15:12:36 Finished characteristic                                        2m45s   1GB
Oct 12 15:12:37 Starting translator/monadic
Oct 12 15:14:10 Finished translator/monadic                                    1m32s   1GB
Oct 12 15:14:11 Starting basis
Oct 12 15:32:10 Finished basis                                                17m58s   3GB
Oct 12 15:32:11 Starting compiler/inference
Oct 12 15:33:56 Finished compiler/inference                                    1m44s   1GB
Oct 12 15:33:57 Starting compiler/backend/reg_alloc
Oct 12 15:34:49 Finished compiler/backend/reg_alloc                              51s   1GB
Oct 12 15:34:50 Starting compiler/backend/gc
Oct 16 07:54:40 FAILED: compiler/backend/gc
]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
Starting work on multiwordTheory
multiwordTheory                                                              OK
Starting work on mc_multiwordTheory
mc_multiwordTheory                                                           OK
]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]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/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-32537a5663e731a4d41cf53adf51cc27b71a0e97/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
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/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
Starting work on asmTheory
asmTheory                                                                    OK
Starting work on asmSemTheory
asmSemTheory                                                                 OK
Starting work on asmPropsTheory
asmPropsTheory                                                               OK
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
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
stackLangTheory                                                              OK
Starting work on wordLangTheory
exportTheory                                                                 OK
Starting work on flatLangTheory
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
data_simpTheory                                                              OK
Starting work on data_spaceTheory
bvi_letTheory                                                                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
bvi_to_dataTheory                                                            OK
Starting work on clos_fvsTheory
clos_callTheory                                                              OK
Starting work on clos_letopTheory
clos_fvsTheory                                                               OK
Starting work on clos_ticksTheory
clos_letopTheory                                                             OK
Starting work on clos_labelsTheory
clos_ticksTheory                                                             OK
Starting work on clos_knownTheory
clos_labelsTheory                                                            OK
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
bvl_constTheory                                                              OK
Starting work on bvl_handleTheory
word_bignumTheory                                                            OK
Starting work on word_instTheory
bvl_handleTheory                                                             OK
Starting work on bvl_inlineTheory
bvl_inlineTheory                                                             OK
Starting work on bvl_to_bviTheory
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
word_simpTheory                                                              OK
Starting work on pat_to_closTheory
word_allocTheory                                                             OK
Starting work on word_to_wordTheory
pat_to_closTheory                                                            OK
Starting work on displayLangTheory
word_to_wordTheory                                                           OK
Starting work on flat_elimTheory
displayLangTheory                                                            OK
Starting work on flat_exh_matchTheory
bvl_to_bviTheory                                                             OK
Starting work on data_to_wordTheory
flat_exh_matchTheory                                                         OK
Starting work on flat_reorder_matchTheory
flat_elimTheory                                                              OK
Starting work on flat_uncheck_ctorsTheory
flat_reorder_matchTheory                                                     OK
Starting work on stack_namesTheory
flat_uncheck_ctorsTheory                                                     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 word_elimTheory
word_to_stackTheory                                                          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