Job 3124

CakeML:ce46491842f6a05bd429de3a3488e83b12ae1da5
  Fix a proof [Jan 10 08:39:24]
#1299 (listmax)
Merging into:3164c9b611542b008be6d3a6da80968a2b7b3c6f
  Merge pull request #1296 from CakeML/new-prims [Jan 10 11:44:33]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:lammmington

Jan 10 19:01:03 Claimed job
Jan 10 19:01:06 Reusing HOL
Jan 10 19:01:14 Starting developers
Jan 10 19:01:19 Finished developers                                               4s 138MB
Jan 10 19:01:20 Starting developers/bin
Jan 10 19:01:24 Finished developers/bin                                           3s  91MB
Jan 10 19:01:25 Starting misc
Jan 10 19:02:05 Finished misc                                                    38s   1GB
Jan 10 19:02:06 Starting compiler/proofs
Jan 10 20:03:43 Finished compiler/proofs                                    1h01m36s  10GB
Jan 10 20:03:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 11 01:53:57 Finished compiler/bootstrap/compilation/x64/64/proofs       5h50m11s  97GB
Jan 11 01:53:58 Starting semantics/ffi
Jan 11 01:54:08 Finished semantics/ffi                                            9s 568MB
Jan 11 01:54:09 Starting semantics
Jan 11 01:54:10 Finished semantics                                                0s  59MB
Jan 11 01:54:11 Starting semantics/proofs
Jan 11 01:54:33 Finished semantics/proofs                                        21s 537MB
Jan 11 01:54:34 Starting semantics/alt_semantics
Jan 11 01:54:54 Finished semantics/alt_semantics                                 18s 712MB
Jan 11 01:54:54 Starting semantics/alt_semantics/proofs
Jan 11 01:59:01 Finished semantics/alt_semantics/proofs                        4m05s   1GB
Jan 11 01:59:02 Starting basis/pure
Jan 11 01:59:04 Finished basis/pure                                               1s  89MB
Jan 11 01:59:05 Starting translator
Jan 11 02:00:07 Finished translator                                            1m01s   3GB
Jan 11 02:00:07 Starting compiler/parsing
Jan 11 02:00:09 Finished compiler/parsing                                         0s  69MB
Jan 11 02:00:10 Starting characteristic
Jan 11 02:00:12 Finished characteristic                                           1s 109MB
Jan 11 02:00:13 Starting translator/monadic
Jan 11 02:00:15 Finished translator/monadic                                       1s 120MB
Jan 11 02:00:16 Starting translator/monadic/monad_base
Jan 11 02:00:18 Finished translator/monadic/monad_base                            0s  64MB
Jan 11 02:00:18 Starting profiler
Jan 11 02:00:49 Finished profiler                                                29s   1GB
Jan 11 02:00:50 Starting basis
Jan 11 02:02:21 Finished basis                                                 1m30s   4GB
Jan 11 02:02:22 Starting compiler
Jan 11 02:02:25 Finished compiler                                                 2s 218MB
Jan 11 02:02:26 Starting compiler/inference
Jan 11 02:02:28 Finished compiler/inference                                       1s 109MB
Jan 11 02:02:29 Starting compiler/backend/reg_alloc
Jan 11 02:02:31 Finished compiler/backend/reg_alloc                               1s  92MB
Jan 11 02:02:32 Starting compiler/backend/gc
Jan 11 02:02:34 Finished compiler/backend/gc                                      1s 145MB
Jan 11 02:02:35 Starting compiler/backend
Jan 11 02:02:41 Finished compiler/backend                                         5s 290MB
Jan 11 02:02:42 Starting compiler/encoders/asm
Jan 11 02:02:44 Finished compiler/encoders/asm                                    0s  89MB
Jan 11 02:02:44 Starting compiler/encoders/x64
Jan 11 02:02:46 Finished compiler/encoders/x64                                    1s  94MB
Jan 11 02:02:47 Starting compiler/encoders/arm7
Jan 11 02:02:49 Finished compiler/encoders/arm7                                   1s  95MB
Jan 11 02:02:50 Starting compiler/encoders/arm8
Jan 11 02:02:52 Finished compiler/encoders/arm8                                   1s  94MB
Jan 11 02:02:53 Starting compiler/encoders/arm8_asl
Jan 11 02:03:07 Finished compiler/encoders/arm8_asl                              13s   1GB
Jan 11 02:03:08 Starting compiler/encoders/mips
Jan 11 02:03:10 Finished compiler/encoders/mips                                   1s  97MB
Jan 11 02:03:11 Starting compiler/encoders/riscv
Jan 11 02:03:13 Finished compiler/encoders/riscv                                  1s  94MB
Jan 11 02:03:14 Starting compiler/encoders/ag32
Jan 11 02:03:15 Finished compiler/encoders/ag32                                   1s  90MB
Jan 11 02:03:16 Starting compiler/encoders/tests
Jan 11 02:03:18 Finished compiler/encoders/tests                                  1s 112MB
Jan 11 02:03:19 Starting compiler/encoders/monadic_enc
Jan 11 02:03:43 Finished compiler/encoders/monadic_enc                           22s   1GB
Jan 11 02:03:44 Starting compiler/backend/x64
Jan 11 02:03:46 Finished compiler/backend/x64                                     1s 136MB
Jan 11 02:03:47 Starting compiler/backend/arm7
Jan 11 02:03:50 Finished compiler/backend/arm7                                    1s 140MB
Jan 11 02:03:50 Starting compiler/backend/arm8
Jan 11 02:03:53 Finished compiler/backend/arm8                                    1s 140MB
Jan 11 02:03:54 Starting compiler/backend/mips
Jan 11 02:03:56 Finished compiler/backend/mips                                    1s 136MB
Jan 11 02:03:57 Starting compiler/backend/riscv
Jan 11 02:04:00 Finished compiler/backend/riscv                                   1s 140MB
Jan 11 02:04:00 Starting compiler/backend/ag32
Jan 11 02:05:01 Finished compiler/backend/ag32                                   59s   3GB
Jan 11 02:05:01 Starting compiler/backend/pattern_matching
Jan 11 02:05:03 Finished compiler/backend/pattern_matching                        0s  64MB
Jan 11 02:05:04 Starting compiler/parsing/ocaml
Jan 11 02:06:51 Finished compiler/parsing/ocaml                                1m46s   1GB
Jan 11 02:06:52 Starting compiler/printing
Jan 11 02:06:54 Finished compiler/printing                                        1s 113MB
Jan 11 02:06:55 Starting compiler/parsing/proofs
Jan 11 02:06:56 Finished compiler/parsing/proofs                                  0s  70MB
Jan 11 02:06:57 Starting compiler/inference/proofs
Jan 11 02:07:00 Finished compiler/inference/proofs                                1s 111MB
Jan 11 02:07:00 Starting compiler/backend/semantics
Jan 11 02:09:07 Finished compiler/backend/semantics                            2m06s   2GB
Jan 11 02:09:08 Starting compiler/backend/reg_alloc/proofs
Jan 11 02:09:10 Finished compiler/backend/reg_alloc/proofs                        1s 124MB
Jan 11 02:09:11 Starting compiler/backend/proofs
Jan 11 02:09:55 Finished compiler/backend/proofs                                 42s   2GB
Jan 11 02:09:56 Starting compiler/backend/serialiser
Jan 11 02:09:58 Finished compiler/backend/serialiser                              1s 145MB
Jan 11 02:09:59 Starting compiler/encoders/x64/proofs
Jan 11 02:10:01 Finished compiler/encoders/x64/proofs                             1s 100MB
Jan 11 02:10:02 Starting compiler/encoders/arm7/proofs
Jan 11 02:20:44 Finished compiler/encoders/arm7/proofs                        10m41s   9GB
Jan 11 02:20:45 Starting compiler/encoders/arm8/proofs
Jan 11 02:27:19 Finished compiler/encoders/arm8/proofs                         6m32s   7GB
Jan 11 02:27:20 Starting compiler/encoders/arm8_asl/proofs
Jan 11 02:42:27 Finished compiler/encoders/arm8_asl/proofs                    15m06s   5GB
Jan 11 02:42:28 Starting compiler/encoders/mips/proofs
Jan 11 02:51:08 Finished compiler/encoders/mips/proofs                         8m38s   9GB
Jan 11 02:51:09 Starting compiler/encoders/riscv/proofs
Jan 11 02:58:53 Finished compiler/encoders/riscv/proofs                        7m43s   5GB
Jan 11 02:58:54 Starting compiler/encoders/ag32/proofs
Jan 11 03:01:31 Finished compiler/encoders/ag32/proofs                         2m35s   2GB
Jan 11 03:01:31 Starting compiler/backend/x64/proofs
Jan 11 03:01:35 Finished compiler/backend/x64/proofs                              2s 207MB
Jan 11 03:01:36 Starting compiler/backend/arm7/proofs
Jan 11 03:02:13 Finished compiler/backend/arm7/proofs                            36s   2GB
Jan 11 03:02:14 Starting compiler/backend/arm8/proofs
Jan 11 03:02:51 Finished compiler/backend/arm8/proofs                            35s   2GB
Jan 11 03:02:52 Starting compiler/backend/arm8_asl
Jan 11 03:03:17 Finished compiler/backend/arm8_asl                               24s   1GB
Jan 11 03:03:18 Starting compiler/backend/mips/proofs
Jan 11 03:03:52 Finished compiler/backend/mips/proofs                            33s   2GB
Jan 11 03:03:53 Starting compiler/backend/riscv/proofs
Jan 11 03:04:31 Finished compiler/backend/riscv/proofs                           37s   2GB
Jan 11 03:04:32 Starting compiler/backend/ag32/proofs
Jan 11 03:15:17 Finished compiler/backend/ag32/proofs                         10m43s   5GB
Jan 11 03:15:18 Starting compiler/backend/cv_compute
Jan 11 03:15:45 Finished compiler/backend/cv_compute                             26s   1GB
Jan 11 03:15:46 Starting cv_translator
Jan 11 03:20:59 Finished cv_translator                                         5m12s   4GB
Jan 11 03:21:00 Starting candle
Jan 11 03:21:01 Finished candle                                                   0s  18MB
Jan 11 03:21:01 Starting candle/set-theory
Jan 11 03:21:30 Finished candle/set-theory                                       27s 932MB
Jan 11 03:21:31 Starting candle/syntax-lib
Jan 11 03:21:33 Finished candle/syntax-lib                                        1s  89MB
Jan 11 03:21:34 Starting candle/standard
Jan 11 03:21:35 Finished candle/standard                                          0s  18MB
Jan 11 03:21:36 Starting candle/standard/syntax
Jan 11 03:21:50 Finished candle/standard/syntax                                  13s 795MB
Jan 11 03:21:51 Starting candle/standard/semantics
Jan 11 03:23:59 Finished candle/standard/semantics                             2m07s   3GB
Jan 11 03:24:00 Starting candle/standard/monadic
Jan 11 03:24:02 Finished candle/standard/monadic                                  1s 126MB
Jan 11 03:24:03 Starting candle/standard/ml_kernel
Jan 11 03:25:54 Finished candle/standard/ml_kernel                             1m50s   4GB
Jan 11 03:25:55 Starting candle/overloading
Jan 11 03:25:56 Finished candle/overloading                                       0s  18MB
Jan 11 03:25:57 Starting candle/overloading/syntax
Jan 11 03:28:59 Finished candle/overloading/syntax                             3m01s   2GB
Jan 11 03:29:00 Starting candle/overloading/semantics
Jan 11 03:39:35 Finished candle/overloading/semantics                         10m33s  15GB
Jan 11 03:39:36 Starting candle/overloading/monadic
Jan 11 03:41:40 Finished candle/overloading/monadic                            2m03s   2GB
Jan 11 03:41:41 Starting candle/overloading/ml_kernel
Jan 11 03:47:57 Finished candle/overloading/ml_kernel                          6m14s   6GB
Jan 11 03:47:58 Starting candle/overloading/ml_checker
Jan 11 03:50:17 Finished candle/overloading/ml_checker                         2m18s   6GB
Jan 11 03:50:17 Starting candle/prover
Jan 11 03:50:20 Finished candle/prover                                            2s 161MB
Jan 11 03:50:21 Starting candle/prover/compute
Jan 11 03:50:24 Finished candle/prover/compute                                    1s 146MB
Jan 11 03:50:25 Starting pancake
Jan 11 03:50:27 Finished pancake                                                  1s 144MB
Jan 11 03:50:28 Starting pancake/semantics
Jan 11 03:53:17 Finished pancake/semantics                                     2m47s   2GB
Jan 11 03:53:18 Starting pancake/parser
Jan 11 03:53:47 Finished pancake/parser                                          28s 504MB
Jan 11 03:53:48 Starting pancake/static_checker
Jan 11 03:54:54 Finished pancake/static_checker                                1m04s   1GB
Jan 11 03:54:55 Starting pancake/proofs
Jan 11 03:58:10 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)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
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
loop_callProofTheory                                               (14s)     OK
Starting work on loop_liveProofTheory
loop_liveProofTheory                                               (17s)     OK
Starting work on crep_to_loopProofTheory
pan_globalsProofTheory                                             (53s)     OK
Starting work on pan_simpProofTheory
loop_removeProofTheory                                             (70s)     OK
Starting work on loop_to_wordProofTheory
crep_to_loopProofTheory                                            (44s)     OK
Starting work on pan_to_crepProofTheory
pan_simpProofTheory                                                (40s)     OK
loop_to_wordProofTheory                                            (44s)     OK
pan_to_crepProofTheory                                            (106s)FAIL<1>
 Saved theorem _______ "not_mem_context_assigned_mem_gt"
 Saved theorem _______ "rewritten_context_unassigned"
 Saved theorem _______ "ctxt_max_el_leq"
 Saved theorem _______ "compile_Dec"
 Saved theorem _______ "compile_Store"
 Saved theorem _______ "compile_Store32"
 Saved theorem _______ "compile_StoreByte"
 Saved theorem _______ "shape_of_alt"
 Saved theorem _______ "compile_ShMemLoad"
 Saved theorem _______ "compile_ShMemStore"
 Saved theorem _______ "compile_exp_not_mem_load_glob"
 Saved theorem _______ "compile_Return"
 Saved theorem _______ "compile_Raise"
 Saved theorem _______ "compile_Seq"
 Saved theorem _______ "compile_If"
 Saved theorem _______ "compile_While"
 Saved theorem _______ "eval_map_comp_exp_flat_eq"
 Saved theorem _______ "local_rel_gt_vmax_preserved"
 Saved theorem _______ "local_rel_le_zip_update_preserved"
 Saved theorem _______ "ctxt_fc_funcs_eq"
 Saved theorem _______ "ctxt_fc_eids_eq"
 Saved theorem _______ "ctxt_fc_vmax"
 Saved definition ____ "slc_def"
 Saved definition ____ "tlc_def"
 Saved theorem _______ "slc_tlc_rw"
 Saved theorem _______ "call_preserve_state_code_locals_rel"
 Proved triviality ___ "flatten_nil_no_size"
 Saved theorem _______ "compile_Call"
 Proved triviality ___ "locals_id_update"
 Saved theorem _______ "MAP_SOME_MEM_lemma"
 Saved theorem _______ "update_locals_not_vars_eval_mmap"
 Saved theorem _______ "res_var_commutes'"
 Saved theorem _______ "EL_load_globals"
 Saved theorem _______ "evaluate_nested_decs_load_globals"
 Saved theorem _______ "compile_DecCall"
 Saved theorem _______ "MAX_LIST_APPEND"
 Proof of 
 
 x > MAX_LIST l  MEM x l
 
 failed.
 First unsolved sub-goal is
 
 h. x > MAX h (MAX_LIST l)  x  h  MEM x l
 
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.TAC_PROOF:
   Failed to prove theorem "MAX_LIST_NOT_MEM":
 unsolved goals
 Full log: /scratch/cakeml/regression3/cakeml-3124/pancake/proofs/.hol/logs/pan_to_crepProofTheory
pan_itreeEquivProofTheory                                         (178s)MKILLED