Job 3196

CakeML:cf6b916cd951893e5151c0c6c1c87eef1f2d0df5
  fix all cheats [Feb 04 14:14:47]
#1322 (word-If-fix)
Merging into:ca9ed45f6d34fe6f89826b16c39ea5b45220a4b2
  Adjust pretty-printing for type abbreviations (#1316) [Feb 05 05:10:14]
HOL:b725f6e8834462a5b4bb2fb67b35e36f368cb8b6
  Tweak regular Holmakefile to clean selftest's log [Jan 30 05:30:27]
Machine:pavlova

Feb 05 11:52:30 Claimed job
Feb 05 11:52:33 Reusing HOL
Feb 05 11:52:41 Starting developers
Feb 05 11:52:46 Finished developers                                               4s 182MB
Feb 05 11:52:47 Starting developers/bin
Feb 05 11:52:51 Finished developers/bin                                           3s  91MB
Feb 05 11:52:52 Starting misc
Feb 05 11:53:34 Finished misc                                                    41s   1GB
Feb 05 11:53:35 Starting compiler/proofs
Feb 05 12:55:56 Finished compiler/proofs                                    1h02m20s  12GB
Feb 05 12:55:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 05 18:58:38 Finished compiler/bootstrap/compilation/x64/64/proofs       6h02m40s  67GB
Feb 05 18:58:39 Starting semantics/ffi
Feb 05 18:58:51 Finished semantics/ffi                                           10s 535MB
Feb 05 18:58:51 Starting semantics
Feb 05 18:58:53 Finished semantics                                                1s  97MB
Feb 05 18:58:54 Starting semantics/proofs
Feb 05 18:59:17 Finished semantics/proofs                                        21s 722MB
Feb 05 18:59:17 Starting semantics/alt_semantics
Feb 05 18:59:38 Finished semantics/alt_semantics                                 19s 630MB
Feb 05 18:59:39 Starting semantics/alt_semantics/proofs
Feb 05 19:03:41 Finished semantics/alt_semantics/proofs                        4m01s   2GB
Feb 05 19:03:42 Starting basis/pure
Feb 05 19:03:44 Finished basis/pure                                               0s  85MB
Feb 05 19:03:45 Starting translator
Feb 05 19:04:48 Finished translator                                            1m02s   3GB
Feb 05 19:04:49 Starting compiler/parsing
Feb 05 19:04:51 Finished compiler/parsing                                         1s 102MB
Feb 05 19:04:52 Starting characteristic
Feb 05 19:04:54 Finished characteristic                                           1s 119MB
Feb 05 19:04:55 Starting translator/monadic
Feb 05 19:04:57 Finished translator/monadic                                       1s 120MB
Feb 05 19:04:58 Starting translator/monadic/monad_base
Feb 05 19:05:00 Finished translator/monadic/monad_base                            0s  95MB
Feb 05 19:05:01 Starting profiler
Feb 05 19:05:28 Finished profiler                                                26s   1GB
Feb 05 19:05:29 Starting basis
Feb 05 19:07:06 Finished basis                                                 1m36s   4GB
Feb 05 19:07:07 Starting compiler
Feb 05 19:07:10 Finished compiler                                                 2s 205MB
Feb 05 19:07:11 Starting compiler/inference
Feb 05 19:07:13 Finished compiler/inference                                       1s 116MB
Feb 05 19:07:14 Starting compiler/backend/reg_alloc
Feb 05 19:07:16 Finished compiler/backend/reg_alloc                               1s 100MB
Feb 05 19:07:17 Starting compiler/backend/gc
Feb 05 19:07:19 Finished compiler/backend/gc                                      1s 137MB
Feb 05 19:07:20 Starting compiler/backend
Feb 05 19:07:26 Finished compiler/backend                                         5s 299MB
Feb 05 19:07:27 Starting compiler/encoders/asm
Feb 05 19:07:29 Finished compiler/encoders/asm                                    1s 100MB
Feb 05 19:07:30 Starting compiler/encoders/x64
Feb 05 19:07:32 Finished compiler/encoders/x64                                    1s 106MB
Feb 05 19:07:33 Starting compiler/encoders/arm7
Feb 05 19:07:35 Finished compiler/encoders/arm7                                   1s 112MB
Feb 05 19:07:36 Starting compiler/encoders/arm8
Feb 05 19:07:38 Finished compiler/encoders/arm8                                   1s 105MB
Feb 05 19:07:39 Starting compiler/encoders/arm8_asl
Feb 05 21:08:39 Finished compiler/encoders/arm8_asl                         2h00m59s  37GB
Feb 05 21:08:40 Starting compiler/encoders/mips
Feb 05 21:08:42 Finished compiler/encoders/mips                                   1s 109MB
Feb 05 21:08:43 Starting compiler/encoders/riscv
Feb 05 21:08:45 Finished compiler/encoders/riscv                                  1s 111MB
Feb 05 21:08:46 Starting compiler/encoders/ag32
Feb 05 21:08:48 Finished compiler/encoders/ag32                                   1s 103MB
Feb 05 21:08:49 Starting compiler/encoders/tests
Feb 05 21:08:51 Finished compiler/encoders/tests                                  1s 139MB
Feb 05 21:08:52 Starting compiler/encoders/monadic_enc
Feb 05 21:09:17 Finished compiler/encoders/monadic_enc                           23s   1GB
Feb 05 21:09:18 Starting compiler/backend/x64
Feb 05 21:09:20 Finished compiler/backend/x64                                     1s 140MB
Feb 05 21:09:21 Starting compiler/backend/arm7
Feb 05 21:09:23 Finished compiler/backend/arm7                                    1s 143MB
Feb 05 21:09:24 Starting compiler/backend/arm8
Feb 05 21:09:27 Finished compiler/backend/arm8                                    1s 143MB
Feb 05 21:09:28 Starting compiler/backend/mips
Feb 05 21:09:30 Finished compiler/backend/mips                                    1s 144MB
Feb 05 21:09:31 Starting compiler/backend/riscv
Feb 05 21:09:33 Finished compiler/backend/riscv                                   1s 143MB
Feb 05 21:09:34 Starting compiler/backend/ag32
Feb 05 21:10:34 Finished compiler/backend/ag32                                   58s   3GB
Feb 05 21:10:35 Starting compiler/backend/pattern_matching
Feb 05 21:10:37 Finished compiler/backend/pattern_matching                        0s  92MB
Feb 05 21:10:38 Starting compiler/parsing/ocaml
Feb 05 21:12:23 Finished compiler/parsing/ocaml                                1m44s   1GB
Feb 05 21:12:24 Starting compiler/printing
Feb 05 21:13:19 Finished compiler/printing                                       54s   1GB
Feb 05 21:13:20 Starting compiler/parsing/proofs
Feb 05 21:13:22 Finished compiler/parsing/proofs                                  1s 104MB
Feb 05 21:13:23 Starting compiler/inference/proofs
Feb 05 21:13:25 Finished compiler/inference/proofs                                1s 112MB
Feb 05 21:13:26 Starting compiler/backend/semantics
Feb 05 21:15:38 Finished compiler/backend/semantics                            2m10s   2GB
Feb 05 21:15:39 Starting compiler/backend/reg_alloc/proofs
Feb 05 21:15:41 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Feb 05 21:15:42 Starting compiler/backend/proofs
Feb 05 21:16:22 Finished compiler/backend/proofs                                 38s   2GB
Feb 05 21:16:23 Starting compiler/backend/serialiser
Feb 05 21:16:25 Finished compiler/backend/serialiser                              1s 147MB
Feb 05 21:16:26 Starting compiler/encoders/x64/proofs
Feb 05 21:16:28 Finished compiler/encoders/x64/proofs                             1s 113MB
Feb 05 21:16:29 Starting compiler/encoders/arm7/proofs
Feb 05 21:27:13 Finished compiler/encoders/arm7/proofs                        10m43s  10GB
Feb 05 21:27:14 Starting compiler/encoders/arm8/proofs
Feb 05 21:33:54 Finished compiler/encoders/arm8/proofs                         6m38s   6GB
Feb 05 21:33:55 Starting compiler/encoders/arm8_asl/proofs
Feb 05 22:22:54 Finished compiler/encoders/arm8_asl/proofs                    48m58s  20GB
Feb 05 22:22:55 Starting compiler/encoders/mips/proofs
Feb 05 22:31:59 Finished compiler/encoders/mips/proofs                         9m03s  10GB
Feb 05 22:32:00 Starting compiler/encoders/riscv/proofs
Feb 05 22:39:45 Finished compiler/encoders/riscv/proofs                        7m43s   3GB
Feb 05 22:39:45 Starting compiler/encoders/ag32/proofs
Feb 05 22:42:24 Finished compiler/encoders/ag32/proofs                         2m37s   2GB
Feb 05 22:42:25 Starting compiler/backend/x64/proofs
Feb 05 22:42:28 Finished compiler/backend/x64/proofs                              2s 212MB
Feb 05 22:42:29 Starting compiler/backend/arm7/proofs
Feb 05 22:43:06 Finished compiler/backend/arm7/proofs                            36s   2GB
Feb 05 22:43:07 Starting compiler/backend/arm8/proofs
Feb 05 22:43:42 Finished compiler/backend/arm8/proofs                            33s   2GB
Feb 05 22:43:43 Starting compiler/backend/arm8_asl
Feb 05 22:44:09 Finished compiler/backend/arm8_asl                               24s   2GB
Feb 05 22:44:10 Starting compiler/backend/mips/proofs
Feb 05 22:44:46 Finished compiler/backend/mips/proofs                            35s   2GB
Feb 05 22:44:47 Starting compiler/backend/riscv/proofs
Feb 05 22:45:26 Finished compiler/backend/riscv/proofs                           37s   2GB
Feb 05 22:45:26 Starting compiler/backend/ag32/proofs
Feb 05 22:59:05 Finished compiler/backend/ag32/proofs                         13m37s   5GB
Feb 05 22:59:05 Starting compiler/backend/cv_compute
Feb 05 22:59:34 Finished compiler/backend/cv_compute                             27s   1GB
Feb 05 22:59:35 Starting cv_translator
Feb 05 23:04:48 Finished cv_translator                                         5m12s   4GB
Feb 05 23:04:49 Starting candle
Feb 05 23:04:50 Finished candle                                                   0s  17MB
Feb 05 23:04:51 Starting candle/set-theory
Feb 05 23:05:20 Finished candle/set-theory                                       28s 957MB
Feb 05 23:05:21 Starting candle/syntax-lib
Feb 05 23:05:23 Finished candle/syntax-lib                                        0s  92MB
Feb 05 23:05:24 Starting candle/standard
Feb 05 23:05:24 Finished candle/standard                                          0s  17MB
Feb 05 23:05:25 Starting candle/standard/syntax
Feb 05 23:05:37 Finished candle/standard/syntax                                  11s 790MB
Feb 05 23:05:38 Starting candle/standard/semantics
Feb 05 23:07:50 Finished candle/standard/semantics                             2m10s   3GB
Feb 05 23:07:51 Starting candle/standard/monadic
Feb 05 23:07:53 Finished candle/standard/monadic                                  1s 128MB
Feb 05 23:07:54 Starting candle/standard/ml_kernel
Feb 05 23:09:49 Finished candle/standard/ml_kernel                             1m53s   4GB
Feb 05 23:09:50 Starting candle/overloading
Feb 05 23:09:51 Finished candle/overloading                                       0s  17MB
Feb 05 23:09:52 Starting candle/overloading/syntax
Feb 05 23:12:59 Finished candle/overloading/syntax                             3m06s   2GB
Feb 05 23:13:00 Starting candle/overloading/semantics
Feb 05 23:23:23 Finished candle/overloading/semantics                         10m22s   7GB
Feb 05 23:23:24 Starting candle/overloading/monadic
Feb 05 23:25:27 Finished candle/overloading/monadic                            2m02s   2GB
Feb 05 23:25:28 Starting candle/overloading/ml_kernel
Feb 05 23:31:43 Finished candle/overloading/ml_kernel                          6m13s   7GB
Feb 05 23:31:44 Starting candle/overloading/ml_checker
Feb 05 23:34:10 Finished candle/overloading/ml_checker                         2m24s   6GB
Feb 05 23:34:11 Starting candle/prover
Feb 05 23:34:14 Finished candle/prover                                            2s 168MB
Feb 05 23:34:15 Starting candle/prover/compute
Feb 05 23:34:18 Finished candle/prover/compute                                    1s 164MB
Feb 05 23:34:18 Starting pancake
Feb 05 23:34:21 Finished pancake                                                  1s 140MB
Feb 05 23:34:22 Starting pancake/semantics
Feb 05 23:37:10 Finished pancake/semantics                                     2m46s   2GB
Feb 05 23:37:10 Starting pancake/parser
Feb 05 23:37:39 Finished pancake/parser                                          28s 526MB
Feb 05 23:37:40 Starting pancake/static_checker
Feb 05 23:38:46 Finished pancake/static_checker                                1m04s   1GB
Feb 05 23:38:47 Starting pancake/proofs
Feb 05 23:39:00 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                                               (6s)     OK
Starting work on pan_itreeEquivProofTheory
pan_globalsProofTheory                                              (7s)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/regression/cakeml-3196/pancake/proofs/.hol/logs/pan_globalsProofTheory
loop_callProofTheory                                                (8s)MKILLED
loop_removeProofTheory                                              (8s)MKILLED
pan_itreeEquivProofTheory                                           (1s)MKILLED