Job 1756

CakeML:d5753a736ad17c7c86c8e25d769324b233f782d4
  Merge branch 'CakeML:master' into cyclicity-check-rebase [Feb 05 14:52:07]
#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 06 19:02:15 Claimed job
Feb 06 19:02:16 Reusing HOL
Feb 06 19:02:30 Starting developers
Feb 06 19:02:34 Finished developers                                               4s 122MB
Feb 06 19:02:34 Starting developers/bin
Feb 06 19:02:38 Finished developers/bin                                           4s 674MB
Feb 06 19:02:39 Starting semantics/ffi
Feb 06 19:02:48 Finished semantics/ffi                                            9s 217MB
Feb 06 19:02:48 Starting semantics
Feb 06 19:04:12 Finished semantics                                             1m23s   1GB
Feb 06 19:04:12 Starting semantics/proofs
Feb 06 19:07:51 Finished semantics/proofs                                      3m38s   1GB
Feb 06 19:07:51 Starting semantics/alt_semantics
Feb 06 19:08:03 Finished semantics/alt_semantics                                 11s 347MB
Feb 06 19:08:03 Starting semantics/alt_semantics/proofs
Feb 06 19:10:32 Finished semantics/alt_semantics/proofs                        2m28s 838MB
Feb 06 19:10:32 Starting basis/pure
Feb 06 19:11:23 Finished basis/pure                                              51s 862MB
Feb 06 19:11:24 Starting translator
Feb 06 19:14:16 Finished translator                                            2m52s   1GB
Feb 06 19:14:16 Starting compiler/parsing
Feb 06 19:15:29 Finished compiler/parsing                                      1m12s   2GB
Feb 06 19:15:29 Starting characteristic
Feb 06 19:21:17 Finished characteristic                                        5m47s   1GB
Feb 06 19:21:17 Starting translator/monadic
Feb 06 19:23:03 Finished translator/monadic                                    1m45s   1GB
Feb 06 19:23:03 Starting basis
Feb 06 20:08:44 Finished basis                                                45m38s  13GB
Feb 06 20:08:44 Starting compiler/inference
Feb 06 20:09:52 Finished compiler/inference                                    1m08s   1GB
Feb 06 20:09:52 Starting compiler/backend/reg_alloc
Feb 06 20:10:59 Finished compiler/backend/reg_alloc                            1m06s   1GB
Feb 06 20:10:59 Starting compiler/backend/gc
Feb 06 20:14:28 Finished compiler/backend/gc                                   3m28s   1GB
Feb 06 20:14:28 Starting compiler/backend
Feb 06 20:16:36 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
data_simpTheory                                                                                                                                               compiler/backend  (9s)     OK
Starting work on data_spaceTheory
bviTheory                                                                                                                                                     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 (12s)     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
bvlTheory                                                                                                                                                     compiler/backend (11s)     OK
Starting work on bvl_constTheory
pattern_compTheory                                                                                                                           compiler/backend/pattern_matching (14s)     OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3]                                                                                                            (34.440s) 
Starting work on db_varsTheory
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 (13s)     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
jsonLangTheory                                                                                                                                                compiler/backend (11s)     OK
Starting work on labLangTheory
flatLangTheory                                                                                                                                                compiler/backend (16s)     OK
Starting work on flat_to_closTheory
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 (11s)     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-1756/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-1756/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  (4s)MKILLED
lab_filterTheory                                                                                                                                              compiler/backend  (3s)MKILLED