Job 1722

CakeML:e478de77a5255174e482f2b80da2b0edd1ad95d1
  Add a heap to embody misc; use it in semantics [Jan 05 06:03:03]
#855 (minor-reheapification)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:0e74a42a431c508b13c303f1ef44290a2ba31e2c
  Fix typo in documentation of SRULE [Jan 17 23:32:45]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 18 11:24:53 Claimed job
Jan 18 11:24:58 Building HOL
Jan 18 11:34:11 Starting developers
Jan 18 11:34:15 Finished developers                                               4s 165MB
Jan 18 11:34:15 Starting developers/bin
Jan 18 11:34:19 Finished developers/bin                                           4s 674MB
Jan 18 11:34:19 Starting semantics/ffi
Jan 18 11:34:27 Finished semantics/ffi                                            8s 212MB
Jan 18 11:34:28 Starting semantics
Jan 18 11:36:13 Finished semantics                                             1m45s 963MB
Jan 18 11:36:13 Starting semantics/proofs
Jan 18 11:39:41 Finished semantics/proofs                                      3m27s   1GB
Jan 18 11:39:41 Starting semantics/alt_semantics
Jan 18 11:39:53 Finished semantics/alt_semantics                                 12s 400MB
Jan 18 11:39:54 Starting semantics/alt_semantics/proofs
Jan 18 11:42:17 Finished semantics/alt_semantics/proofs                        2m23s   1GB
Jan 18 11:42:18 Starting basis/pure
Jan 18 11:45:06 Finished basis/pure                                            2m48s 703MB
Jan 18 11:45:06 Starting translator
Jan 18 11:47:55 Finished translator                                            2m48s   2GB
Jan 18 11:47:55 Starting compiler/parsing
Jan 18 11:49:07 Finished compiler/parsing                                      1m12s   1GB
Jan 18 11:49:07 Starting characteristic
Jan 18 11:54:50 Finished characteristic                                        5m42s   2GB
Jan 18 11:54:50 Starting translator/monadic
Jan 18 11:56:30 Finished translator/monadic                                    1m39s   1GB
Jan 18 11:56:30 Starting basis
Jan 18 12:41:39 Finished basis                                                45m06s  21GB
Jan 18 12:41:39 Starting compiler/inference
Jan 18 12:42:54 Finished compiler/inference                                    1m15s   1GB
Jan 18 12:42:54 Starting compiler/backend/reg_alloc
Jan 18 12:43:59 Finished compiler/backend/reg_alloc                            1m04s   1GB
Jan 18 12:43:59 Starting compiler/backend/gc
Jan 18 12:47:22 Finished compiler/backend/gc                                   3m22s   2GB
Jan 18 12:47:22 Starting compiler/backend
Jan 18 12:51:52 Finished compiler/backend                                      4m30s   2GB
Jan 18 12:51:53 Starting compiler/encoders/asm
Jan 18 12:52:16 Finished compiler/encoders/asm                                   22s 669MB
Jan 18 12:52:16 Starting compiler/encoders/x64
Jan 18 12:53:15 Finished compiler/encoders/x64                                   59s 989MB
Jan 18 12:53:15 Starting compiler/encoders/arm7
Jan 18 12:55:13 Finished compiler/encoders/arm7                                1m57s   1GB
Jan 18 12:55:13 Starting compiler/encoders/arm8
Jan 18 12:55:50 Finished compiler/encoders/arm8                                  36s 942MB
Jan 18 12:55:50 Starting compiler/encoders/mips
Jan 18 12:57:15 Finished compiler/encoders/mips                                1m24s   1GB
Jan 18 12:57:15 Starting compiler/encoders/riscv
Jan 18 12:58:56 Finished compiler/encoders/riscv                               1m41s   1GB
Jan 18 12:58:56 Starting compiler/encoders/ag32
Jan 18 12:59:14 Finished compiler/encoders/ag32                                  17s 557MB
Jan 18 12:59:14 Starting compiler/backend/x64
Jan 18 12:59:33 Finished compiler/backend/x64                                    18s   1GB
Jan 18 12:59:33 Starting compiler/backend/arm7
Jan 18 12:59:55 Finished compiler/backend/arm7                                   21s   1GB
Jan 18 12:59:55 Starting compiler/backend/arm8
Jan 18 13:00:14 Finished compiler/backend/arm8                                   19s   1GB
Jan 18 13:00:14 Starting compiler/backend/mips
Jan 18 13:00:34 Finished compiler/backend/mips                                   19s   1GB
Jan 18 13:00:34 Starting compiler/backend/riscv
Jan 18 13:00:53 Finished compiler/backend/riscv                                  19s   1GB
Jan 18 13:00:54 Starting compiler/backend/ag32
Jan 18 13:02:00 Finished compiler/backend/ag32                                 1m06s   1GB
Jan 18 13:02:00 Starting compiler/parsing/proofs
Jan 18 13:05:39 Finished compiler/parsing/proofs                               3m38s   1GB
Jan 18 13:05:39 Starting compiler/inference/proofs
Jan 18 13:08:01 Finished compiler/inference/proofs                             2m22s   1GB
Jan 18 13:08:01 Starting compiler/backend/semantics
Jan 18 13:35:44 Finished compiler/backend/semantics                           27m42s   3GB
Jan 18 13:35:45 Starting compiler/backend/reg_alloc/proofs
Jan 18 13:39:06 Finished compiler/backend/reg_alloc/proofs                     3m21s   1GB
Jan 18 13:39:06 Starting compiler/backend/proofs
Jan 18 13:50:54 FAILED: compiler/backend/proofs
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)/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/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Finished $(CAKEMLDIR)/misc                                                           (0.000s) 
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
README.md                                                compiler/backend/proofs  (1s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                                     compiler/backend/proofs (13s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                    compiler/backend/proofs (24s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                       compiler/backend/proofs (17s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                     compiler/backend/proofs (68s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                 compiler/backend/proofs (24s)     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                     compiler/backend/proofs (94s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                    compiler/backend/proofs (18s)     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                    compiler/backend/proofs (29s)     OK
Starting work on clos_fvsProofTheory
bvi_tailrecProofTheory                                   compiler/backend/proofs(166s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                      compiler/backend/proofs (15s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                    compiler/backend/proofs (10s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                   compiler/backend/proofs(123s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                    compiler/backend/proofs (16s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                       compiler/backend/proofs (20s)     OK
Starting work on clos_mtiProofTheory
clos_callProofTheory                                     compiler/backend/proofs(152s)     OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory                                    compiler/backend/proofs (22s)     OK
Starting work on clos_knownProofTheory
clos_numberProofTheory                                   compiler/backend/proofs (23s)     OK
Starting work on bvl_jumpProofTheory
clos_mtiProofTheory                                      compiler/backend/proofs (31s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                      compiler/backend/proofs  (9s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                     compiler/backend/proofs (48s)     OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                                   compiler/backend/proofs (29s)     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                                    compiler/backend/proofs(172s)     OK
Starting work on word_allocProofTheory
clos_knownProofTheory                                    compiler/backend/proofs(126s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                   compiler/backend/proofs(190s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                     compiler/backend/proofs (48s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                   compiler/backend/proofs (27s)     OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory                                   compiler/backend/proofs(189s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                  compiler/backend/proofs (39s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                                    compiler/backend/proofs (60s)     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                                    compiler/backend/proofs (55s)     OK
Starting work on stack_removeProofTheory
flat_to_closProofTheory                                  compiler/backend/proofs (74s)     OK
Starting work on source_evalProofTheory
source_evalProofTheory                                   compiler/backend/proofs (30s)FAIL<1>
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 1347, character 2 and line 1359, character 14:
 at Defn.prim_mk_defn:
 Simple definition failed with message: Definition.new_definition: at Thm.new_specification:
 Free variables in rhs of definition: "shift_seq"
 error in quse /home/cug/hk324/cml-regression/cakeml-1722/compiler/backend/proofs/source_evalProofScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1347, character 2 and line 1359, character 14:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"shift_seq\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1722/compiler/backend/proofs/source_evalProofScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1347, character 2 and line 1359, character 14:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"shift_seq\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1347, character 2 and line 1359, character 14:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"shift_seq\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
data_to_word_memoryProofTheory                           compiler/backend/proofs(365s)MKILLED
word_allocProofTheory                                    compiler/backend/proofs(353s)MKILLED
stack_removeProofTheory                                  compiler/backend/proofs (47s)MKILLED