Job 1665

CakeML:adfe15ad7735ba36dea23e8a1721154e525f7e63
  Merge remote-tracking branch 'origin/pattern-aliases' into clos-smart-op [Nov 25 10:35:15]
#847 (clos-smart-op)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
  emacs-mode: adjust holmake command to get to use ANSI magic [Nov 23 06:58:28]
Machine:oven3 4.19.67.1.amd64-smp

Nov 25 18:41:13 Claimed job
Nov 25 18:41:26 Reusing HOL
Nov 25 18:42:19 Starting developers
Nov 25 18:42:27 Finished developers                                               7s 168MB
Nov 25 18:42:27 Starting developers/bin
Nov 25 18:42:39 Finished developers/bin                                          12s   1GB
Nov 25 18:42:39 Starting semantics/ffi
Nov 25 18:42:58 Finished semantics/ffi                                           18s 238MB
Nov 25 18:42:59 Starting semantics
Nov 25 18:45:50 Finished semantics                                             2m51s   1GB
Nov 25 18:45:50 Starting semantics/proofs
Nov 25 18:53:34 Finished semantics/proofs                                      7m43s   1GB
Nov 25 18:53:34 Starting semantics/alt_semantics
Nov 25 18:53:59 Finished semantics/alt_semantics                                 24s 403MB
Nov 25 18:54:00 Starting semantics/alt_semantics/proofs
Nov 25 18:59:12 Finished semantics/alt_semantics/proofs                        5m12s   1GB
Nov 25 18:59:12 Starting basis/pure
Nov 25 19:00:59 Finished basis/pure                                            1m46s 802MB
Nov 25 19:00:59 Starting translator
Nov 25 19:06:53 Finished translator                                            5m51s   2GB
Nov 25 19:06:53 Starting compiler/parsing
Nov 25 19:09:37 Finished compiler/parsing                                      2m43s   2GB
Nov 25 19:09:37 Starting characteristic
Nov 25 19:21:36 Finished characteristic                                       11m58s   2GB
Nov 25 19:21:36 Starting translator/monadic
Nov 25 19:25:07 Finished translator/monadic                                    3m30s   1GB
Nov 25 19:25:07 Starting basis
Nov 25 21:02:55 Finished basis                                              1h37m46s  17GB
Nov 25 21:02:55 Starting compiler/inference
Nov 25 21:05:19 Finished compiler/inference                                    2m24s   1GB
Nov 25 21:05:20 Starting compiler/backend/reg_alloc
Nov 25 21:07:27 Finished compiler/backend/reg_alloc                            2m06s   1GB
Nov 25 21:07:27 Starting compiler/backend/gc
Nov 25 21:13:59 Finished compiler/backend/gc                                   6m31s   2GB
Nov 25 21:13:59 Starting compiler/backend
Nov 25 21:22:46 Finished compiler/backend                                      8m46s   2GB
Nov 25 21:22:46 Starting compiler/encoders/asm
Nov 25 21:23:37 Finished compiler/encoders/asm                                   50s 724MB
Nov 25 21:23:37 Starting compiler/encoders/x64
Nov 25 21:24:34 Finished compiler/encoders/x64                                   56s   1GB
Nov 25 21:24:34 Starting compiler/encoders/arm7
Nov 25 21:26:29 Finished compiler/encoders/arm7                                1m54s 747MB
Nov 25 21:26:29 Starting compiler/encoders/arm8
Nov 25 21:26:58 Finished compiler/encoders/arm8                                  28s 694MB
Nov 25 21:26:58 Starting compiler/encoders/mips
Nov 25 21:27:34 Finished compiler/encoders/mips                                  36s   1GB
Nov 25 21:27:34 Starting compiler/encoders/riscv
Nov 25 21:28:13 Finished compiler/encoders/riscv                                 38s 967MB
Nov 25 21:28:13 Starting compiler/encoders/ag32
Nov 25 21:28:52 Finished compiler/encoders/ag32                                  38s 670MB
Nov 25 21:28:52 Starting compiler/backend/x64
Nov 25 21:29:34 Finished compiler/backend/x64                                    41s   1GB
Nov 25 21:29:34 Starting compiler/backend/arm7
Nov 25 21:30:20 Finished compiler/backend/arm7                                   45s   1GB
Nov 25 21:30:20 Starting compiler/backend/arm8
Nov 25 21:31:04 Finished compiler/backend/arm8                                   43s   1GB
Nov 25 21:31:04 Starting compiler/backend/mips
Nov 25 21:31:47 Finished compiler/backend/mips                                   43s   1GB
Nov 25 21:31:48 Starting compiler/backend/riscv
Nov 25 21:32:30 Finished compiler/backend/riscv                                  42s   1GB
Nov 25 21:32:30 Starting compiler/backend/ag32
Nov 25 21:35:00 Finished compiler/backend/ag32                                 2m29s   1GB
Nov 25 21:35:01 Starting compiler/parsing/proofs
Nov 25 21:43:08 Finished compiler/parsing/proofs                               8m07s   1GB
Nov 25 21:43:08 Starting compiler/inference/proofs
Nov 25 21:48:26 Finished compiler/inference/proofs                             5m17s   1GB
Nov 25 21:48:26 Starting compiler/backend/semantics
Nov 25 22:51:07 Finished compiler/backend/semantics                         1h02m41s   1GB
Nov 25 22:51:08 Starting compiler/backend/reg_alloc/proofs
Nov 25 22:58:42 Finished compiler/backend/reg_alloc/proofs                     7m34s 896MB
Nov 25 22:58:42 Starting compiler/backend/proofs
Nov 25 23:06:01 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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/quotient/src[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/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[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/topology[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  (2s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                                                                                                                                                                                    compiler/backend/proofs (26s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                                                                                                                                                   compiler/backend/proofs (51s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                                                                                                                                      compiler/backend/proofs (32s)     OK
Starting work on clos_annotateProofTheory
clos_annotateProofTheory                                                                                                                                                                                compiler/backend/proofs (48s)     OK
Starting work on clos_callProofTheory
data_liveProofTheory                                                                                                                                                                                    compiler/backend/proofs(139s)     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                                                                                                                                                                                    compiler/backend/proofs(191s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                                                                                                                                                   compiler/backend/proofs (36s)     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                                                                                                                                                                   compiler/backend/proofs (54s)     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                                                                                                                                                                     compiler/backend/proofs (28s)     OK
Starting work on clos_knownPropsTheory
bvi_tailrecProofTheory                                                                                                                                                                                  compiler/backend/proofs(345s)     OK
Starting work on bvl_to_bviProofTheory
clos_knownPropsTheory                                                                                                                                                                                   compiler/backend/proofs (19s)     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                                                                                                                                                                                   compiler/backend/proofs (31s)     OK
Starting work on clos_opProofTheory
bvi_to_dataProofTheory                                                                                                                                                                                  compiler/backend/proofs(252s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                                                                                                                                                                      compiler/backend/proofs (26s)FAIL<1>
 error in load /root/regression/cakeml-1665/compiler/backend/proofs/clos_opProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 539) (THEN1 on line 441)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 evaluate ([x1; y1],env1,r) = (Rval [h1; h2],r)  simple_exp x1 
 simple_exp y1  do_eq h1 h2 = Eq_val b 
 evaluate ([eq_pure x1 y1],env1,r) = (Rval [Boolv b],r)
 
 failed.
 Failed to prove theorem eq_pure_thm.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 539) (THEN1 on line 441)", origin_function = "THEN1", origin_structure = "Tactical"}
clos_callProofTheory                                                                                                                                                                                    compiler/backend/proofs(278s)MKILLED
bvl_to_bviProofTheory                                                                                                                                                                                   compiler/backend/proofs (77s)MKILLED
clos_ticksProofTheory                                                                                                                                                                                   compiler/backend/proofs (25s)MKILLED