Job 3192

CakeML:cf6b916cd951893e5151c0c6c1c87eef1f2d0df5
  fix all cheats [Feb 04 14:14:47]
#1322 (word-If-fix)
Merging into:b33556e9b0cdd780bb380194889c2959ffe86191
  Mcandidate fix (#1321) [Jan 30 15:03:50]
HOL:b725f6e8834462a5b4bb2fb67b35e36f368cb8b6
  Tweak regular Holmakefile to clean selftest's log [Jan 30 05:30:27]
Machine:timtam

Feb 05 02:06:18 Claimed job
Feb 05 02:06:23 Reusing HOL
Feb 05 02:06:31 Starting developers
Feb 05 02:06:36 Finished developers                                               4s 135MB
Feb 05 02:06:37 Starting developers/bin
Feb 05 02:06:41 Finished developers/bin                                           3s  91MB
Feb 05 02:06:42 Starting misc
Feb 05 02:07:26 Finished misc                                                    43s   1GB
Feb 05 02:07:27 Starting compiler/proofs
Feb 05 03:08:44 Finished compiler/proofs                                    1h01m14s  15GB
Feb 05 03:08:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 05 09:12:17 Finished compiler/bootstrap/compilation/x64/64/proofs       6h03m29s  64GB
Feb 05 09:12:18 Starting semantics/ffi
Feb 05 09:12:29 Finished semantics/ffi                                           10s 538MB
Feb 05 09:12:30 Starting semantics
Feb 05 09:12:32 Finished semantics                                                1s  96MB
Feb 05 09:12:32 Starting semantics/proofs
Feb 05 09:12:55 Finished semantics/proofs                                        21s 747MB
Feb 05 09:12:55 Starting semantics/alt_semantics
Feb 05 09:13:16 Finished semantics/alt_semantics                                 19s 630MB
Feb 05 09:13:17 Starting semantics/alt_semantics/proofs
Feb 05 09:17:19 Finished semantics/alt_semantics/proofs                        4m01s   2GB
Feb 05 09:17:20 Starting basis/pure
Feb 05 09:17:22 Finished basis/pure                                               0s  91MB
Feb 05 09:17:23 Starting translator
Feb 05 09:18:25 Finished translator                                            1m01s   3GB
Feb 05 09:18:26 Starting compiler/parsing
Feb 05 09:18:28 Finished compiler/parsing                                         1s 100MB
Feb 05 09:18:29 Starting characteristic
Feb 05 09:18:31 Finished characteristic                                           1s 127MB
Feb 05 09:18:32 Starting translator/monadic
Feb 05 09:18:34 Finished translator/monadic                                       1s 114MB
Feb 05 09:18:35 Starting translator/monadic/monad_base
Feb 05 09:18:37 Finished translator/monadic/monad_base                            1s  99MB
Feb 05 09:18:38 Starting profiler
Feb 05 09:19:05 Finished profiler                                                26s   1GB
Feb 05 09:19:06 Starting basis
Feb 05 09:20:40 Finished basis                                                 1m33s   4GB
Feb 05 09:20:40 Starting compiler
Feb 05 09:20:44 Finished compiler                                                 2s 212MB
Feb 05 09:20:45 Starting compiler/inference
Feb 05 09:20:47 Finished compiler/inference                                       1s 119MB
Feb 05 09:20:48 Starting compiler/backend/reg_alloc
Feb 05 09:20:49 Finished compiler/backend/reg_alloc                               1s  95MB
Feb 05 09:20:50 Starting compiler/backend/gc
Feb 05 09:20:53 Finished compiler/backend/gc                                      1s 144MB
Feb 05 09:20:54 Starting compiler/backend
Feb 05 09:21:00 Finished compiler/backend                                         5s 288MB
Feb 05 09:21:01 Starting compiler/encoders/asm
Feb 05 09:21:03 Finished compiler/encoders/asm                                    1s 104MB
Feb 05 09:21:03 Starting compiler/encoders/x64
Feb 05 09:21:06 Finished compiler/encoders/x64                                    1s 104MB
Feb 05 09:21:06 Starting compiler/encoders/arm7
Feb 05 09:21:08 Finished compiler/encoders/arm7                                   1s 106MB
Feb 05 09:21:09 Starting compiler/encoders/arm8
Feb 05 09:21:11 Finished compiler/encoders/arm8                                   1s 106MB
Feb 05 09:21:12 Starting compiler/encoders/arm8_asl
Feb 05 09:21:27 Finished compiler/encoders/arm8_asl                              13s   1GB
Feb 05 09:21:27 Starting compiler/encoders/mips
Feb 05 09:21:29 Finished compiler/encoders/mips                                   1s 111MB
Feb 05 09:21:30 Starting compiler/encoders/riscv
Feb 05 09:21:32 Finished compiler/encoders/riscv                                  1s 105MB
Feb 05 09:21:33 Starting compiler/encoders/ag32
Feb 05 09:21:35 Finished compiler/encoders/ag32                                   1s 104MB
Feb 05 09:21:36 Starting compiler/encoders/tests
Feb 05 09:21:38 Finished compiler/encoders/tests                                  1s 121MB
Feb 05 09:21:39 Starting compiler/encoders/monadic_enc
Feb 05 09:22:01 Finished compiler/encoders/monadic_enc                           21s   1GB
Feb 05 09:22:02 Starting compiler/backend/x64
Feb 05 09:22:04 Finished compiler/backend/x64                                     1s 147MB
Feb 05 09:22:05 Starting compiler/backend/arm7
Feb 05 09:22:08 Finished compiler/backend/arm7                                    1s 147MB
Feb 05 09:22:09 Starting compiler/backend/arm8
Feb 05 09:22:11 Finished compiler/backend/arm8                                    1s 147MB
Feb 05 09:22:12 Starting compiler/backend/mips
Feb 05 09:22:14 Finished compiler/backend/mips                                    1s 147MB
Feb 05 09:22:15 Starting compiler/backend/riscv
Feb 05 09:22:17 Finished compiler/backend/riscv                                   1s 147MB
Feb 05 09:22:18 Starting compiler/backend/ag32
Feb 05 09:23:17 Finished compiler/backend/ag32                                   57s   1GB
Feb 05 09:23:18 Starting compiler/backend/pattern_matching
Feb 05 09:23:19 Finished compiler/backend/pattern_matching                        1s  90MB
Feb 05 09:23:20 Starting compiler/parsing/ocaml
Feb 05 09:25:08 Finished compiler/parsing/ocaml                                1m46s   1GB
Feb 05 09:25:09 Starting compiler/printing
Feb 05 09:25:11 Finished compiler/printing                                        1s 111MB
Feb 05 09:25:12 Starting compiler/parsing/proofs
Feb 05 09:25:14 Finished compiler/parsing/proofs                                  1s 102MB
Feb 05 09:25:15 Starting compiler/inference/proofs
Feb 05 09:25:17 Finished compiler/inference/proofs                                1s 116MB
Feb 05 09:25:18 Starting compiler/backend/semantics
Feb 05 09:27:24 Finished compiler/backend/semantics                            2m04s   1GB
Feb 05 09:27:25 Starting compiler/backend/reg_alloc/proofs
Feb 05 09:27:27 Finished compiler/backend/reg_alloc/proofs                        1s 124MB
Feb 05 09:27:28 Starting compiler/backend/proofs
Feb 05 09:28:12 Finished compiler/backend/proofs                                 43s   2GB
Feb 05 09:28:13 Starting compiler/backend/serialiser
Feb 05 09:28:15 Finished compiler/backend/serialiser                              1s 144MB
Feb 05 09:28:16 Starting compiler/encoders/x64/proofs
Feb 05 09:28:18 Finished compiler/encoders/x64/proofs                             1s 106MB
Feb 05 09:28:19 Starting compiler/encoders/arm7/proofs
Feb 05 09:39:01 Finished compiler/encoders/arm7/proofs                        10m41s  10GB
Feb 05 09:39:02 Starting compiler/encoders/arm8/proofs
Feb 05 09:45:46 Finished compiler/encoders/arm8/proofs                         6m42s   5GB
Feb 05 09:45:46 Starting compiler/encoders/arm8_asl/proofs
Feb 05 10:00:44 Finished compiler/encoders/arm8_asl/proofs                    14m56s   5GB
Feb 05 10:00:44 Starting compiler/encoders/mips/proofs
Feb 05 10:09:42 Finished compiler/encoders/mips/proofs                         8m56s  11GB
Feb 05 10:09:43 Starting compiler/encoders/riscv/proofs
Feb 05 10:17:32 Finished compiler/encoders/riscv/proofs                        7m48s   7GB
Feb 05 10:17:33 Starting compiler/encoders/ag32/proofs
Feb 05 10:20:12 Finished compiler/encoders/ag32/proofs                         2m37s   3GB
Feb 05 10:20:12 Starting compiler/backend/x64/proofs
Feb 05 10:20:16 Finished compiler/backend/x64/proofs                              2s 226MB
Feb 05 10:20:17 Starting compiler/backend/arm7/proofs
Feb 05 10:20:54 Finished compiler/backend/arm7/proofs                            37s   2GB
Feb 05 10:20:55 Starting compiler/backend/arm8/proofs
Feb 05 10:21:31 Finished compiler/backend/arm8/proofs                            35s   2GB
Feb 05 10:21:32 Starting compiler/backend/arm8_asl
Feb 05 10:21:59 Finished compiler/backend/arm8_asl                               25s   2GB
Feb 05 10:21:59 Starting compiler/backend/mips/proofs
Feb 05 10:22:36 Finished compiler/backend/mips/proofs                            35s   2GB
Feb 05 10:22:37 Starting compiler/backend/riscv/proofs
Feb 05 10:23:17 Finished compiler/backend/riscv/proofs                           38s   2GB
Feb 05 10:23:17 Starting compiler/backend/ag32/proofs
Feb 05 10:34:02 Finished compiler/backend/ag32/proofs                         10m44s   3GB
Feb 05 10:34:03 Starting compiler/backend/cv_compute
Feb 05 10:34:32 Finished compiler/backend/cv_compute                             27s   1GB
Feb 05 10:34:33 Starting cv_translator
Feb 05 10:39:49 Finished cv_translator                                         5m15s   4GB
Feb 05 10:39:50 Starting candle
Feb 05 10:39:51 Finished candle                                                   0s  17MB
Feb 05 10:39:51 Starting candle/set-theory
Feb 05 10:40:22 Finished candle/set-theory                                       29s 933MB
Feb 05 10:40:22 Starting candle/syntax-lib
Feb 05 10:40:24 Finished candle/syntax-lib                                        0s  86MB
Feb 05 10:40:25 Starting candle/standard
Feb 05 10:40:26 Finished candle/standard                                          0s  17MB
Feb 05 10:40:27 Starting candle/standard/syntax
Feb 05 10:40:41 Finished candle/standard/syntax                                  13s 771MB
Feb 05 10:40:42 Starting candle/standard/semantics
Feb 05 10:42:54 Finished candle/standard/semantics                             2m10s   3GB
Feb 05 10:42:55 Starting candle/standard/monadic
Feb 05 10:42:57 Finished candle/standard/monadic                                  1s 132MB
Feb 05 10:42:58 Starting candle/standard/ml_kernel
Feb 05 10:44:52 Finished candle/standard/ml_kernel                             1m53s   4GB
Feb 05 10:44:53 Starting candle/overloading
Feb 05 10:44:54 Finished candle/overloading                                       0s  17MB
Feb 05 10:44:55 Starting candle/overloading/syntax
Feb 05 10:47:59 Finished candle/overloading/syntax                             3m03s   2GB
Feb 05 10:48:00 Starting candle/overloading/semantics
Feb 05 10:58:37 Finished candle/overloading/semantics                         10m35s   9GB
Feb 05 10:58:37 Starting candle/overloading/monadic
Feb 05 11:00:41 Finished candle/overloading/monadic                            2m02s   2GB
Feb 05 11:00:42 Starting candle/overloading/ml_kernel
Feb 05 11:07:06 Finished candle/overloading/ml_kernel                          6m23s   7GB
Feb 05 11:07:07 Starting candle/overloading/ml_checker
Feb 05 11:09:31 Finished candle/overloading/ml_checker                         2m22s   6GB
Feb 05 11:09:32 Starting candle/prover
Feb 05 11:09:35 Finished candle/prover                                            2s 168MB
Feb 05 11:09:36 Starting candle/prover/compute
Feb 05 11:09:38 Finished candle/prover/compute                                    1s 151MB
Feb 05 11:09:39 Starting pancake
Feb 05 11:09:41 Finished pancake                                                  1s 145MB
Feb 05 11:09:42 Starting pancake/semantics
Feb 05 11:12:29 Finished pancake/semantics                                     2m46s   2GB
Feb 05 11:12:30 Starting pancake/parser
Feb 05 11:13:01 Finished pancake/parser                                          29s 495MB
Feb 05 11:13:02 Starting pancake/static_checker
Feb 05 11:14:09 Finished pancake/static_checker                                1m06s   1GB
Feb 05 11:14:10 Starting pancake/proofs
Feb 05 11:14:23 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 loop_callProofTheory
Starting work on loop_removeProofTheory
README.md                                                           (0s)     OK
Starting work on pan_globalsProofTheory
crep_arithProofTheory                                               (7s)     OK
Starting work on pan_itreeEquivProofTheory
pan_globalsProofTheory                                              (8s)FAIL<1>
 <<HOL message: Created theory "pan_globalsProof">>
 Saved definition ____ "disjoint_globals_def"
 Saved definition ____ "state_rel_def"
 Saved theorem _______ "state_rel_mem_load"
 Saved theorem _______ "compile_exp_correct"
 <<HOL message: mk_functional: 
   pattern completion has added 3 clauses to the original specification.>>
 Saved definition ____ "good_res_def"
 Saved induction _____ "good_res_ind"
 Saved theorem _______ "compile_Skip_Break_Continue_Annot_Tick"
 Saved theorem _______ "mem_stores_append"
 Saved theorem _______ "mem_stores_memory_swap"
 Saved theorem _______ "mem_load_mem_store"
 Saved theorem _______ "mem_stores_lookup"
 Saved theorem _______ "mem_stores_load_disjoint"
 Proof of 
 
 (val addr addrs memory m.
    mem_stores addr (flatten val) addrs memory = SOME m 
    LENGTH (flatten val) * w2n bytes_in_word < dimword (:) 
    good_dimindex (:) 
    mem_load (shape_of val) addr addrs m = SOME val) 
 vals addr addrs memory m.
   mem_stores addr (FLAT (MAP (a. flatten a) vals)) addrs memory = SOME m 
   LENGTH (FLAT (MAP (a. flatten a) vals)) * w2n bytes_in_word < dimword (:) 
   good_dimindex (:) 
   mem_loads (MAP shape_of vals) addr addrs m = SOME vals
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.THEN1:
   Failed to prove theorem "mem_stores_mem_load_back":
 first subgoal not solved by second tactic
 Full log: /scratch/cakeml/regression2/cakeml-3192/pancake/proofs/.hol/logs/pan_globalsProofTheory
loop_callProofTheory                                                (8s)MKILLED
loop_removeProofTheory                                              (9s)MKILLED
pan_itreeEquivProofTheory                                           (1s)MKILLED