Job 3205

CakeML:86cbc789bcf72613597128d42d2c20897ce36c03
  Improve copy propagation: preserve store eqs across branches, skip re [Feb 07 08:27:15]
#1327 (word_store)
Merging into:375cc6c9d7c045b206ab7dd172763c80a92246eb
  Merge pull request #1301 from CakeML/new-prims [Feb 07 04:57:53]
HOL:b725f6e8834462a5b4bb2fb67b35e36f368cb8b6
  Tweak regular Holmakefile to clean selftest's log [Jan 30 05:30:27]
Machine:pavlova

Feb 07 09:42:35 Claimed job
Feb 07 09:42:39 Reusing HOL
Feb 07 09:42:47 Starting developers
Feb 07 09:42:53 Finished developers                                               4s 164MB
Feb 07 09:42:53 Starting developers/bin
Feb 07 09:42:58 Finished developers/bin                                           3s  91MB
Feb 07 09:42:59 Starting misc
Feb 07 09:43:43 Finished misc                                                    43s   1GB
Feb 07 09:43:44 Starting compiler/proofs
Feb 07 10:43:58 Finished compiler/proofs                                    1h00m13s  11GB
Feb 07 10:43:59 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 07 16:42:41 Finished compiler/bootstrap/compilation/x64/64/proofs       5h58m40s  91GB
Feb 07 16:42:41 Starting semantics/ffi
Feb 07 16:42:53 Finished semantics/ffi                                           10s 536MB
Feb 07 16:42:54 Starting semantics
Feb 07 16:42:55 Finished semantics                                                1s  95MB
Feb 07 16:42:56 Starting semantics/proofs
Feb 07 16:43:19 Finished semantics/proofs                                        21s 951MB
Feb 07 16:43:20 Starting semantics/alt_semantics
Feb 07 16:43:40 Finished semantics/alt_semantics                                 19s 589MB
Feb 07 16:43:41 Starting semantics/alt_semantics/proofs
Feb 07 16:47:09 Finished semantics/alt_semantics/proofs                        3m27s   1GB
Feb 07 16:47:09 Starting basis/pure
Feb 07 16:47:11 Finished basis/pure                                               0s  89MB
Feb 07 16:47:12 Starting translator
Feb 07 16:48:16 Finished translator                                            1m03s   2GB
Feb 07 16:48:17 Starting compiler/parsing
Feb 07 16:48:19 Finished compiler/parsing                                         1s 102MB
Feb 07 16:48:20 Starting characteristic
Feb 07 16:48:22 Finished characteristic                                           1s 120MB
Feb 07 16:48:23 Starting translator/monadic
Feb 07 16:48:25 Finished translator/monadic                                       1s 121MB
Feb 07 16:48:26 Starting translator/monadic/monad_base
Feb 07 16:48:28 Finished translator/monadic/monad_base                            0s  97MB
Feb 07 16:48:29 Starting profiler
Feb 07 16:48:59 Finished profiler                                                29s   1GB
Feb 07 16:49:00 Starting basis
Feb 07 16:50:35 Finished basis                                                 1m34s   4GB
Feb 07 16:50:36 Starting compiler
Feb 07 16:50:40 Finished compiler                                                 2s 216MB
Feb 07 16:50:40 Starting compiler/inference
Feb 07 16:50:43 Finished compiler/inference                                       1s 117MB
Feb 07 16:50:43 Starting compiler/backend/reg_alloc
Feb 07 16:50:45 Finished compiler/backend/reg_alloc                               1s  97MB
Feb 07 16:50:46 Starting compiler/backend/gc
Feb 07 16:50:49 Finished compiler/backend/gc                                      1s 136MB
Feb 07 16:50:49 Starting compiler/backend
Feb 07 16:50:55 Finished compiler/backend                                         4s 252MB
Feb 07 16:50:56 Starting compiler/encoders/asm
Feb 07 16:50:58 Finished compiler/encoders/asm                                    1s 100MB
Feb 07 16:50:59 Starting compiler/encoders/x64
Feb 07 16:51:01 Finished compiler/encoders/x64                                    1s 112MB
Feb 07 16:51:02 Starting compiler/encoders/arm7
Feb 07 16:51:04 Finished compiler/encoders/arm7                                   1s 110MB
Feb 07 16:51:05 Starting compiler/encoders/arm8
Feb 07 16:51:07 Finished compiler/encoders/arm8                                   1s 111MB
Feb 07 16:51:07 Starting compiler/encoders/arm8_asl
Feb 07 16:51:22 Finished compiler/encoders/arm8_asl                              13s   1GB
Feb 07 16:51:23 Starting compiler/encoders/mips
Feb 07 16:51:25 Finished compiler/encoders/mips                                   1s 106MB
Feb 07 16:51:26 Starting compiler/encoders/riscv
Feb 07 16:51:28 Finished compiler/encoders/riscv                                  1s 106MB
Feb 07 16:51:28 Starting compiler/encoders/ag32
Feb 07 16:51:30 Finished compiler/encoders/ag32                                   1s 105MB
Feb 07 16:51:31 Starting compiler/encoders/tests
Feb 07 16:51:33 Finished compiler/encoders/tests                                  1s 124MB
Feb 07 16:51:34 Starting compiler/encoders/monadic_enc
Feb 07 16:51:58 Finished compiler/encoders/monadic_enc                           22s   1GB
Feb 07 16:51:59 Starting compiler/backend/x64
Feb 07 16:52:01 Finished compiler/backend/x64                                     1s 147MB
Feb 07 16:52:02 Starting compiler/backend/arm7
Feb 07 16:52:04 Finished compiler/backend/arm7                                    1s 141MB
Feb 07 16:52:05 Starting compiler/backend/arm8
Feb 07 16:52:08 Finished compiler/backend/arm8                                    1s 141MB
Feb 07 16:52:08 Starting compiler/backend/mips
Feb 07 16:52:11 Finished compiler/backend/mips                                    1s 147MB
Feb 07 16:52:12 Starting compiler/backend/riscv
Feb 07 16:52:14 Finished compiler/backend/riscv                                   1s 141MB
Feb 07 16:52:15 Starting compiler/backend/ag32
Feb 07 16:53:16 Finished compiler/backend/ag32                                   59s   3GB
Feb 07 16:53:17 Starting compiler/backend/pattern_matching
Feb 07 16:53:18 Finished compiler/backend/pattern_matching                        0s  91MB
Feb 07 16:53:19 Starting compiler/parsing/ocaml
Feb 07 16:55:06 Finished compiler/parsing/ocaml                                1m45s   1GB
Feb 07 16:55:06 Starting compiler/printing
Feb 07 16:56:02 Finished compiler/printing                                       54s   1GB
Feb 07 16:56:03 Starting compiler/parsing/proofs
Feb 07 16:56:05 Finished compiler/parsing/proofs                                  1s 103MB
Feb 07 16:56:06 Starting compiler/inference/proofs
Feb 07 16:56:08 Finished compiler/inference/proofs                                1s 110MB
Feb 07 16:56:09 Starting compiler/backend/semantics
Feb 07 16:58:12 Finished compiler/backend/semantics                            2m02s   2GB
Feb 07 16:58:13 Starting compiler/backend/reg_alloc/proofs
Feb 07 16:58:15 Finished compiler/backend/reg_alloc/proofs                        1s 124MB
Feb 07 16:58:16 Starting compiler/backend/proofs
Feb 07 16:58:52 Finished compiler/backend/proofs                                 34s   1GB
Feb 07 16:58:52 Starting compiler/backend/serialiser
Feb 07 16:58:55 Finished compiler/backend/serialiser                              1s 152MB
Feb 07 16:58:56 Starting compiler/encoders/x64/proofs
Feb 07 16:58:58 Finished compiler/encoders/x64/proofs                             1s 107MB
Feb 07 16:58:59 Starting compiler/encoders/arm7/proofs
Feb 07 17:09:36 Finished compiler/encoders/arm7/proofs                        10m36s   6GB
Feb 07 17:09:37 Starting compiler/encoders/arm8/proofs
Feb 07 17:16:09 Finished compiler/encoders/arm8/proofs                         6m31s   6GB
Feb 07 17:16:10 Starting compiler/encoders/arm8_asl/proofs
Feb 07 17:31:02 Finished compiler/encoders/arm8_asl/proofs                    14m51s   5GB
Feb 07 17:31:03 Starting compiler/encoders/mips/proofs
Feb 07 17:39:54 Finished compiler/encoders/mips/proofs                         8m49s  11GB
Feb 07 17:39:54 Starting compiler/encoders/riscv/proofs
Feb 07 17:47:38 Finished compiler/encoders/riscv/proofs                        7m42s   6GB
Feb 07 17:47:39 Starting compiler/encoders/ag32/proofs
Feb 07 17:50:18 Finished compiler/encoders/ag32/proofs                         2m38s   2GB
Feb 07 17:50:19 Starting compiler/backend/x64/proofs
Feb 07 17:50:22 Finished compiler/backend/x64/proofs                              2s 221MB
Feb 07 17:50:23 Starting compiler/backend/arm7/proofs
Feb 07 17:51:02 Finished compiler/backend/arm7/proofs                            38s   2GB
Feb 07 17:51:03 Starting compiler/backend/arm8/proofs
Feb 07 17:51:37 Finished compiler/backend/arm8/proofs                            32s   1GB
Feb 07 17:51:37 Starting compiler/backend/arm8_asl
Feb 07 17:52:05 Finished compiler/backend/arm8_asl                               26s   2GB
Feb 07 17:52:05 Starting compiler/backend/mips/proofs
Feb 07 17:52:41 Finished compiler/backend/mips/proofs                            35s   2GB
Feb 07 17:52:42 Starting compiler/backend/riscv/proofs
Feb 07 17:53:20 Finished compiler/backend/riscv/proofs                           36s   2GB
Feb 07 17:53:21 Starting compiler/backend/ag32/proofs
Feb 07 18:05:32 Finished compiler/backend/ag32/proofs                         12m10s   5GB
Feb 07 18:05:33 Starting compiler/backend/cv_compute
Feb 07 18:06:01 Finished compiler/backend/cv_compute                             26s   1GB
Feb 07 18:06:02 Starting cv_translator
Feb 07 18:11:27 Finished cv_translator                                         5m24s   4GB
Feb 07 18:11:27 Starting candle
Feb 07 18:11:28 Finished candle                                                   0s  17MB
Feb 07 18:11:29 Starting candle/set-theory
Feb 07 18:11:59 Finished candle/set-theory                                       28s 957MB
Feb 07 18:12:00 Starting candle/syntax-lib
Feb 07 18:12:01 Finished candle/syntax-lib                                        0s  92MB
Feb 07 18:12:02 Starting candle/standard
Feb 07 18:12:03 Finished candle/standard                                          0s  17MB
Feb 07 18:12:04 Starting candle/standard/syntax
Feb 07 18:12:18 Finished candle/standard/syntax                                  13s 764MB
Feb 07 18:12:19 Starting candle/standard/semantics
Feb 07 18:14:30 Finished candle/standard/semantics                             2m10s   3GB
Feb 07 18:14:31 Starting candle/standard/monadic
Feb 07 18:14:33 Finished candle/standard/monadic                                  1s 122MB
Feb 07 18:14:34 Starting candle/standard/ml_kernel
Feb 07 18:16:30 Finished candle/standard/ml_kernel                             1m55s   5GB
Feb 07 18:16:31 Starting candle/overloading
Feb 07 18:16:32 Finished candle/overloading                                       0s  17MB
Feb 07 18:16:33 Starting candle/overloading/syntax
Feb 07 18:19:40 Finished candle/overloading/syntax                             3m06s   2GB
Feb 07 18:19:41 Starting candle/overloading/semantics
Feb 07 18:30:01 Finished candle/overloading/semantics                         10m19s   7GB
Feb 07 18:30:01 Starting candle/overloading/monadic
Feb 07 18:32:03 Finished candle/overloading/monadic                            2m00s   2GB
Feb 07 18:32:03 Starting candle/overloading/ml_kernel
Feb 07 18:38:15 Finished candle/overloading/ml_kernel                          6m10s   7GB
Feb 07 18:38:16 Starting candle/overloading/ml_checker
Feb 07 18:40:34 Finished candle/overloading/ml_checker                         2m17s   6GB
Feb 07 18:40:35 Starting candle/prover
Feb 07 18:40:38 Finished candle/prover                                            2s 169MB
Feb 07 18:40:39 Starting candle/prover/compute
Feb 07 18:40:42 Finished candle/prover/compute                                    1s 170MB
Feb 07 18:40:43 Starting pancake
Feb 07 18:40:45 Finished pancake                                                  1s 145MB
Feb 07 18:40:46 Starting pancake/semantics
Feb 07 18:43:27 Finished pancake/semantics                                     2m40s   2GB
Feb 07 18:43:28 Starting pancake/parser
Feb 07 18:43:57 Finished pancake/parser                                          28s 499MB
Feb 07 18:43:58 Starting pancake/static_checker
Feb 07 18:45:04 Finished pancake/static_checker                                1m04s   1GB
Feb 07 18:45:04 Starting pancake/proofs
Feb 07 18:46:28 FAILED: pancake/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/semantics
Scanned 55 directories
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on crep_inlineProofTheory
Starting work on loop_callProofTheory
README.md                                                           (0s)     OK
Starting work on loop_removeProofTheory
crep_arithProofTheory                                               (6s)     OK
Starting work on pan_globalsProofTheory
loop_callProofTheory                                               (14s)     OK
Starting work on loop_liveProofTheory
loop_liveProofTheory                                               (16s)     OK
Starting work on crep_to_loopProofTheory
pan_globalsProofTheory                                             (53s)     OK
Starting work on pan_itreeEquivProofTheory
loop_removeProofTheory                                             (68s)     OK
Starting work on loop_to_wordProofTheory
loop_to_wordProofTheory                                             (5s)FAIL<1>
      | SOME (Result v) =>
        res1 = SOME (Result retv [v])  t1.stack = t.stack 
        t1.handler = t.handler
      | SOME (Exception v') =>
        (res1  SOME Error  u1 u2. res1 = SOME (Exception u1 u2)) 
        r l1 l2.
          jump_exc (t1 with <|stack := t.stack; handler := t.handler|>) =
          SOME (r,l1,l2) 
          res1 = SOME (Exception (Loc l1 l2) v')  r = t1
      | SOME Break => F
      | SOME Continue => F
      | SOME TimeOut => res1 = SOME TimeOut
      | SOME (FinalFFI f) => res1 = SOME (FinalFFI f)
      | SOME Error => F) 
 s res s1 t ctxt retv l.
   evaluate (Tick,s) = (res,s1)  res  SOME Error  state_rel s t 
   locals_rel ctxt s.locals t.locals  lookup 0 t.locals = SOME retv 
   no_Loops Tick  good_dimindex (:)  isWord retv 
   domain (acc_vars Tick LN)  domain ctxt 
   t1 res1.
     evaluate (FST (comp ctxt Tick l),t) = (res1,t1)  state_rel s1 t1 
     case res of
       NONE =>
         res1 = NONE  lookup 0 t1.locals = SOME retv 
         locals_rel ctxt s1.locals t1.locals  t1.stack = t.stack 
         t1.handler = t.handler
     | SOME (Result v) =>
       res1 = SOME (Result retv [v])  t1.stack = t.stack 
       t1.handler = t.handler
     | SOME (Exception v') =>
       (res1  SOME Error  u1 u2. res1 = SOME (Exception u1 u2)) 
       r l1 l2.
         jump_exc (t1 with <|stack := t.stack; handler := t.handler|>) =
         SOME (r,l1,l2) 
         res1 = SOME (Exception (Loc l1 l2) v')  r = t1
     | SOME Break => F
     | SOME Continue => F
     | SOME TimeOut => res1 = SOME TimeOut
     | SOME (FinalFFI f) => res1 = SOME (FinalFFI f)
     | SOME Error => F
 
 failed.
 First unsolved sub-goal is
 
 F
 
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.TAC_PROOF: Failed to prove theorem "compile_Skip":
 unsolved goals
 Full log: /scratch/cakeml/regression/cakeml-3205/pancake/proofs/.hol/logs/loop_to_wordProofTheory
crep_inlineProofTheory                                             (75s)MKILLED
crep_to_loopProofTheory                                            (43s)MKILLED
pan_itreeEquivProofTheory                                          (14s)MKILLED