Job 1758

CakeML:62355d1569fbecf5ed8d03eb7c503322622c95aa
  adds README for `candle/overloading` [Feb 07 06:51:45]
#860 (cyclicity-check-rebase)
Merging into:5525b2dc1da264a4ad4d5b5dd23599b8fe8bafe3
  Use Definition.new_definition [Feb 06 17:14:33]
HOL:4cf5152547dba4db8875c3221511ca11e364ed9c
  Fix more Holmakefiles for unlikely parallel build scenarios [Feb 01 01:04:20]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 07 13:37:04 Claimed job
Feb 07 13:37:11 Reusing HOL
Feb 07 13:37:24 Starting developers
Feb 07 13:37:28 Finished developers                                               4s 149MB
Feb 07 13:37:28 Starting developers/bin
Feb 07 13:37:33 Finished developers/bin                                           4s 674MB
Feb 07 13:37:33 Starting semantics/ffi
Feb 07 13:37:42 Finished semantics/ffi                                            9s 206MB
Feb 07 13:37:42 Starting semantics
Feb 07 13:39:05 Finished semantics                                             1m23s   1GB
Feb 07 13:39:06 Starting semantics/proofs
Feb 07 13:42:36 Finished semantics/proofs                                      3m29s   1GB
Feb 07 13:42:36 Starting semantics/alt_semantics
Feb 07 13:42:48 Finished semantics/alt_semantics                                 11s 347MB
Feb 07 13:42:48 Starting semantics/alt_semantics/proofs
Feb 07 13:45:16 Finished semantics/alt_semantics/proofs                        2m27s 981MB
Feb 07 13:45:16 Starting basis/pure
Feb 07 13:46:07 Finished basis/pure                                              51s 688MB
Feb 07 13:46:07 Starting translator
Feb 07 13:49:01 Finished translator                                            2m53s   2GB
Feb 07 13:49:01 Starting compiler/parsing
Feb 07 13:50:13 Finished compiler/parsing                                      1m12s   2GB
Feb 07 13:50:13 Starting characteristic
Feb 07 13:56:04 Finished characteristic                                        5m50s   1GB
Feb 07 13:56:04 Starting translator/monadic
Feb 07 13:57:48 Finished translator/monadic                                    1m43s   1GB
Feb 07 13:57:48 Starting basis
Feb 07 14:43:36 Finished basis                                                45m47s  26GB
Feb 07 14:43:36 Starting compiler/inference
Feb 07 14:44:45 Finished compiler/inference                                    1m08s 991MB
Feb 07 14:44:45 Starting compiler/backend/reg_alloc
Feb 07 14:45:52 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 07 14:45:53 Starting compiler/backend/gc
Feb 07 14:49:19 Finished compiler/backend/gc                                   3m26s   2GB
Feb 07 14:49:19 Starting compiler/backend
Feb 07 14:51:26 FAILED: compiler/backend
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[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)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 38 directories
Starting work on pattern_commonTheory
Starting work on README.md
Starting work on bviTheory
Starting work on data_liveTheory
README.md                                                                                                                                                     compiler/backend  (0s)     OK
Starting work on data_simpTheory
pattern_commonTheory                                                                                                                         compiler/backend/pattern_matching  (7s)     OK
Starting work on pattern_semanticsTheory
bviTheory                                                                                                                                                     compiler/backend (10s)     OK
Starting work on data_spaceTheory
data_simpTheory                                                                                                                                               compiler/backend (10s)     OK
Starting work on bvi_letTheory
data_liveTheory                                                                                                                                               compiler/backend (14s)     OK
Starting work on bvi_tailrecTheory
pattern_semanticsTheory                                                                                                                      compiler/backend/pattern_matching (11s)     OK
Starting work on pattern_compTheory
bvi_letTheory                                                                                                                                                 compiler/backend (11s)     OK
Starting work on bvlTheory
data_spaceTheory                                                                                                                                              compiler/backend (14s)     OK
Starting work on bvi_to_dataTheory
pattern_compTheory                                                                                                                           compiler/backend/pattern_matching (14s)     OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3]                                                                                                            (33.880s) 
Starting work on db_varsTheory
bvlTheory                                                                                                                                                     compiler/backend (10s)     OK
Starting work on bvl_constTheory
bvi_to_dataTheory                                                                                                                                             compiler/backend (17s)     OK
Starting work on bvl_jumpTheory
db_varsTheory                                                                                                                                                 compiler/backend (10s)     OK
Starting work on clos_annotateTheory
bvl_jumpTheory                                                                                                                                                compiler/backend (10s)     OK
Starting work on clos_callTheory
bvi_tailrecTheory                                                                                                                                             compiler/backend (41s)     OK
Starting work on clos_fvsTheory
clos_annotateTheory                                                                                                                                           compiler/backend (13s)     OK
Starting work on clos_letopTheory
clos_fvsTheory                                                                                                                                                compiler/backend (10s)     OK
Starting work on clos_opTheory
clos_callTheory                                                                                                                                               compiler/backend (14s)     OK
Starting work on clos_ticksTheory
clos_letopTheory                                                                                                                                              compiler/backend (11s)     OK
Starting work on clos_mtiTheory
clos_ticksTheory                                                                                                                                              compiler/backend (10s)     OK
Starting work on clos_numberTheory
clos_mtiTheory                                                                                                                                                compiler/backend (13s)     OK
Starting work on flatLangTheory
clos_numberTheory                                                                                                                                             compiler/backend (10s)     OK
Starting work on jsonLangTheory
bvl_constTheory                                                                                                                                               compiler/backend (66s)     OK
Starting work on bvl_handleTheory
flatLangTheory                                                                                                                                                compiler/backend (16s)     OK
Starting work on flat_to_closTheory
jsonLangTheory                                                                                                                                                compiler/backend (11s)     OK
Starting work on labLangTheory
clos_opTheory                                                                                                                                                 compiler/backend (37s)     OK
Starting work on clos_knownTheory
bvl_handleTheory                                                                                                                                              compiler/backend (13s)     OK
Starting work on bvl_inlineTheory
labLangTheory                                                                                                                                                 compiler/backend (12s)     OK
Starting work on lab_filterTheory
clos_knownTheory                                                                                                                                              compiler/backend (13s)FAIL<1>
 Exception raised at Tactical.FIRST_ASSUM:
 
 
 Exception raised at TotalDefn.tDefine:
 at Defn.tprove:
 at Tactical.FIRST_ASSUM:
 
 error in quse /home/cug/hk324/cml-regression/cakeml-1758/compiler/backend/clos_knownScript.sml : HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1758/compiler/backend/clos_knownScript : HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
flat_to_closTheory                                                                                                                                            compiler/backend (15s)MKILLED
bvl_inlineTheory                                                                                                                                              compiler/backend  (3s)MKILLED
lab_filterTheory                                                                                                                                              compiler/backend  (1s)MKILLED