Overview

Job 1665

CakeML:adfe15ad7735ba36dea23e8a1721154e525f7e63
  Merge remote-tracking branch 'origin/pattern-aliases' into clos-smart-op
#847 (clos-smart-op)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
  emacs-mode: adjust holmake command to get to use ANSI magic
Machine:oven3 4.19.67.1.amd64-smp

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               7s 168MB
 Starting developers/bin
 Finished developers/bin                                          12s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           18s 238MB
 Starting semantics
 Finished semantics                                             2m51s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      7m43s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 24s 403MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        5m12s   1GB
 Starting basis/pure
 Finished basis/pure                                            1m46s 802MB
 Starting translator
 Finished translator                                            5m51s   2GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m43s   2GB
 Starting characteristic
 Finished characteristic                                       11m58s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m30s   1GB
 Starting basis
 Finished basis                                              1h37m46s  17GB
 Starting compiler/inference
 Finished compiler/inference                                    2m24s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            2m06s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   6m31s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      8m46s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   50s 724MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   56s   1GB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                1m54s 747MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  28s 694MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  36s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 38s 967MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  38s 670MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    41s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   45s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   43s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   43s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  42s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 2m29s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               8m07s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             5m17s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                         1h02m41s   1GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     7m34s 896MB
 Starting compiler/backend/proofs
 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