Job 3120

CakeML:ce46491842f6a05bd429de3a3488e83b12ae1da5
  Fix a proof [Jan 10 08:39:24]
#1299 (listmax)
Merging into:1516f558501b58a9bff7891a1d62f24e3fbaf45a
  Convert process_topdecs patterns to Quote syntax (#1294) [Jan 06 23:47:11]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:lammmington

Jan 10 08:54:38 Claimed job
Jan 10 08:54:42 Reusing HOL
Jan 10 08:54:50 Starting developers
Jan 10 08:54:55 Finished developers                                               4s 172MB
Jan 10 08:54:56 Starting developers/bin
Jan 10 08:55:00 Finished developers/bin                                           3s  91MB
Jan 10 08:55:01 Starting misc
Jan 10 08:55:42 Finished misc                                                    40s   1GB
Jan 10 08:55:43 Starting compiler/proofs
Jan 10 09:57:58 Finished compiler/proofs                                    1h02m14s  13GB
Jan 10 09:57:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 10 15:46:22 Finished compiler/bootstrap/compilation/x64/64/proofs       5h48m22s  99GB
Jan 10 15:46:23 Starting semantics/ffi
Jan 10 15:46:34 Finished semantics/ffi                                            9s 569MB
Jan 10 15:46:34 Starting semantics
Jan 10 15:46:36 Finished semantics                                                0s  59MB
Jan 10 15:46:37 Starting semantics/proofs
Jan 10 15:46:59 Finished semantics/proofs                                        21s 525MB
Jan 10 15:47:00 Starting semantics/alt_semantics
Jan 10 15:47:19 Finished semantics/alt_semantics                                 18s 721MB
Jan 10 15:47:20 Starting semantics/alt_semantics/proofs
Jan 10 15:51:24 Finished semantics/alt_semantics/proofs                        4m03s   2GB
Jan 10 15:51:25 Starting basis/pure
Jan 10 15:51:27 Finished basis/pure                                               1s  89MB
Jan 10 15:51:28 Starting translator
Jan 10 15:52:29 Finished translator                                            1m00s   3GB
Jan 10 15:52:30 Starting compiler/parsing
Jan 10 15:52:31 Finished compiler/parsing                                         0s  69MB
Jan 10 15:52:32 Starting characteristic
Jan 10 15:52:35 Finished characteristic                                           1s 109MB
Jan 10 15:52:35 Starting translator/monadic
Jan 10 15:52:38 Finished translator/monadic                                       1s 114MB
Jan 10 15:52:39 Starting translator/monadic/monad_base
Jan 10 15:52:40 Finished translator/monadic/monad_base                            0s  64MB
Jan 10 15:52:41 Starting profiler
Jan 10 15:53:11 Finished profiler                                                29s   1GB
Jan 10 15:53:12 Starting basis
Jan 10 15:54:40 Finished basis                                                 1m27s   4GB
Jan 10 15:54:41 Starting compiler
Jan 10 15:54:45 Finished compiler                                                 2s 219MB
Jan 10 15:54:45 Starting compiler/inference
Jan 10 15:54:48 Finished compiler/inference                                       1s 109MB
Jan 10 15:54:48 Starting compiler/backend/reg_alloc
Jan 10 15:54:50 Finished compiler/backend/reg_alloc                               1s  92MB
Jan 10 15:54:51 Starting compiler/backend/gc
Jan 10 15:54:54 Finished compiler/backend/gc                                      1s 145MB
Jan 10 15:54:55 Starting compiler/backend
Jan 10 15:55:01 Finished compiler/backend                                         5s 274MB
Jan 10 15:55:01 Starting compiler/encoders/asm
Jan 10 15:55:03 Finished compiler/encoders/asm                                    0s  89MB
Jan 10 15:55:04 Starting compiler/encoders/x64
Jan 10 15:55:06 Finished compiler/encoders/x64                                    1s  94MB
Jan 10 15:55:07 Starting compiler/encoders/arm7
Jan 10 15:55:09 Finished compiler/encoders/arm7                                   1s  95MB
Jan 10 15:55:10 Starting compiler/encoders/arm8
Jan 10 15:55:11 Finished compiler/encoders/arm8                                   1s  94MB
Jan 10 15:55:12 Starting compiler/encoders/arm8_asl
Jan 10 15:55:27 Finished compiler/encoders/arm8_asl                              13s   1GB
Jan 10 15:55:28 Starting compiler/encoders/mips
Jan 10 15:55:30 Finished compiler/encoders/mips                                   1s  96MB
Jan 10 15:55:31 Starting compiler/encoders/riscv
Jan 10 15:55:32 Finished compiler/encoders/riscv                                  1s  94MB
Jan 10 15:55:33 Starting compiler/encoders/ag32
Jan 10 15:55:35 Finished compiler/encoders/ag32                                   1s  90MB
Jan 10 15:55:36 Starting compiler/encoders/tests
Jan 10 15:55:38 Finished compiler/encoders/tests                                  1s 112MB
Jan 10 15:55:39 Starting compiler/encoders/monadic_enc
Jan 10 15:56:03 Finished compiler/encoders/monadic_enc                           22s   1GB
Jan 10 15:56:03 Starting compiler/backend/x64
Jan 10 15:56:06 Finished compiler/backend/x64                                     1s 136MB
Jan 10 15:56:07 Starting compiler/backend/arm7
Jan 10 15:56:09 Finished compiler/backend/arm7                                    1s 140MB
Jan 10 15:56:10 Starting compiler/backend/arm8
Jan 10 15:56:12 Finished compiler/backend/arm8                                    1s 136MB
Jan 10 15:56:13 Starting compiler/backend/mips
Jan 10 15:56:16 Finished compiler/backend/mips                                    1s 136MB
Jan 10 15:56:17 Starting compiler/backend/riscv
Jan 10 15:56:19 Finished compiler/backend/riscv                                   1s 140MB
Jan 10 15:56:20 Starting compiler/backend/ag32
Jan 10 15:57:20 Finished compiler/backend/ag32                                   59s   2GB
Jan 10 15:57:21 Starting compiler/backend/pattern_matching
Jan 10 15:57:23 Finished compiler/backend/pattern_matching                        0s  64MB
Jan 10 15:57:24 Starting compiler/parsing/ocaml
Jan 10 15:59:11 Finished compiler/parsing/ocaml                                1m46s   1GB
Jan 10 15:59:12 Starting compiler/printing
Jan 10 15:59:14 Finished compiler/printing                                        1s 113MB
Jan 10 15:59:15 Starting compiler/parsing/proofs
Jan 10 15:59:16 Finished compiler/parsing/proofs                                  0s  70MB
Jan 10 15:59:17 Starting compiler/inference/proofs
Jan 10 15:59:19 Finished compiler/inference/proofs                                1s 111MB
Jan 10 15:59:20 Starting compiler/backend/semantics
Jan 10 16:01:26 Finished compiler/backend/semantics                            2m05s   2GB
Jan 10 16:01:27 Starting compiler/backend/reg_alloc/proofs
Jan 10 16:01:29 Finished compiler/backend/reg_alloc/proofs                        1s 123MB
Jan 10 16:01:30 Starting compiler/backend/proofs
Jan 10 16:02:09 Finished compiler/backend/proofs                                 37s   1GB
Jan 10 16:02:10 Starting compiler/backend/serialiser
Jan 10 16:02:12 Finished compiler/backend/serialiser                              1s 143MB
Jan 10 16:02:13 Starting compiler/encoders/x64/proofs
Jan 10 16:02:15 Finished compiler/encoders/x64/proofs                             1s 100MB
Jan 10 16:02:16 Starting compiler/encoders/arm7/proofs
Jan 10 16:13:01 Finished compiler/encoders/arm7/proofs                        10m43s  10GB
Jan 10 16:13:02 Starting compiler/encoders/arm8/proofs
Jan 10 16:19:34 Finished compiler/encoders/arm8/proofs                         6m31s   6GB
Jan 10 16:19:35 Starting compiler/encoders/arm8_asl/proofs
Jan 10 16:34:17 Finished compiler/encoders/arm8_asl/proofs                    14m41s   3GB
Jan 10 16:34:18 Starting compiler/encoders/mips/proofs
Jan 10 16:43:03 Finished compiler/encoders/mips/proofs                         8m44s   8GB
Jan 10 16:43:04 Starting compiler/encoders/riscv/proofs
Jan 10 16:50:37 Finished compiler/encoders/riscv/proofs                        7m32s   5GB
Jan 10 16:50:38 Starting compiler/encoders/ag32/proofs
Jan 10 16:53:13 Finished compiler/encoders/ag32/proofs                         2m34s   2GB
Jan 10 16:53:14 Starting compiler/backend/x64/proofs
Jan 10 16:53:18 Finished compiler/backend/x64/proofs                              2s 207MB
Jan 10 16:53:18 Starting compiler/backend/arm7/proofs
Jan 10 16:53:55 Finished compiler/backend/arm7/proofs                            35s   2GB
Jan 10 16:53:55 Starting compiler/backend/arm8/proofs
Jan 10 16:54:32 Finished compiler/backend/arm8/proofs                            35s   2GB
Jan 10 16:54:33 Starting compiler/backend/arm8_asl
Jan 10 16:55:01 Finished compiler/backend/arm8_asl                               26s   2GB
Jan 10 16:55:01 Starting compiler/backend/mips/proofs
Jan 10 16:55:38 Finished compiler/backend/mips/proofs                            35s   2GB
Jan 10 16:55:39 Starting compiler/backend/riscv/proofs
Jan 10 16:56:17 Finished compiler/backend/riscv/proofs                           37s   2GB
Jan 10 16:56:18 Starting compiler/backend/ag32/proofs
Jan 10 17:07:04 Finished compiler/backend/ag32/proofs                         10m45s   5GB
Jan 10 17:07:05 Starting compiler/backend/cv_compute
Jan 10 17:07:33 Finished compiler/backend/cv_compute                             27s   1GB
Jan 10 17:07:34 Starting cv_translator
Jan 10 17:12:41 Finished cv_translator                                         5m05s   4GB
Jan 10 17:12:42 Starting candle
Jan 10 17:12:43 Finished candle                                                   0s  18MB
Jan 10 17:12:44 Starting candle/set-theory
Jan 10 17:13:13 Finished candle/set-theory                                       27s 930MB
Jan 10 17:13:13 Starting candle/syntax-lib
Jan 10 17:13:15 Finished candle/syntax-lib                                        1s  89MB
Jan 10 17:13:16 Starting candle/standard
Jan 10 17:13:17 Finished candle/standard                                          0s  18MB
Jan 10 17:13:18 Starting candle/standard/syntax
Jan 10 17:13:32 Finished candle/standard/syntax                                  13s 794MB
Jan 10 17:13:33 Starting candle/standard/semantics
Jan 10 17:15:41 Finished candle/standard/semantics                             2m07s   3GB
Jan 10 17:15:42 Starting candle/standard/monadic
Jan 10 17:15:45 Finished candle/standard/monadic                                  1s 126MB
Jan 10 17:15:45 Starting candle/standard/ml_kernel
Jan 10 17:17:35 Finished candle/standard/ml_kernel                             1m49s   4GB
Jan 10 17:17:36 Starting candle/overloading
Jan 10 17:17:37 Finished candle/overloading                                       0s  18MB
Jan 10 17:17:38 Starting candle/overloading/syntax
Jan 10 17:20:44 Finished candle/overloading/syntax                             3m04s   2GB
Jan 10 17:20:45 Starting candle/overloading/semantics
Jan 10 17:30:56 Finished candle/overloading/semantics                         10m10s   6GB
Jan 10 17:30:56 Starting candle/overloading/monadic
Jan 10 17:33:02 Finished candle/overloading/monadic                            2m04s   2GB
Jan 10 17:33:03 Starting candle/overloading/ml_kernel
Jan 10 17:39:32 Finished candle/overloading/ml_kernel                          6m28s   6GB
Jan 10 17:39:33 Starting candle/overloading/ml_checker
Jan 10 17:41:49 Finished candle/overloading/ml_checker                         2m15s   6GB
Jan 10 17:41:50 Starting candle/prover
Jan 10 17:41:53 Finished candle/prover                                            2s 160MB
Jan 10 17:41:54 Starting candle/prover/compute
Jan 10 17:41:57 Finished candle/prover/compute                                    1s 146MB
Jan 10 17:41:57 Starting pancake
Jan 10 17:42:00 Finished pancake                                                  1s 145MB
Jan 10 17:42:01 Starting pancake/semantics
Jan 10 17:44:41 Finished pancake/semantics                                     2m39s   2GB
Jan 10 17:44:42 Starting pancake/parser
Jan 10 17:45:12 Finished pancake/parser                                          29s 639MB
Jan 10 17:45:13 Starting pancake/static_checker
Jan 10 17:46:18 Finished pancake/static_checker                                1m04s   1GB
Jan 10 17:46:19 Starting pancake/proofs
Jan 10 17:49:32 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                                               (7s)     OK
Starting work on pan_itreeEquivProofTheory
loop_callProofTheory                                               (14s)     OK
Starting work on loop_liveProofTheory
loop_liveProofTheory                                               (16s)     OK
Starting work on crep_to_loopProofTheory
pan_globalsProofTheory                                             (52s)     OK
Starting work on pan_simpProofTheory
loop_removeProofTheory                                             (69s)     OK
Starting work on loop_to_wordProofTheory
crep_to_loopProofTheory                                            (43s)     OK
Starting work on pan_to_crepProofTheory
pan_simpProofTheory                                                (40s)     OK
loop_to_wordProofTheory                                            (44s)     OK
pan_to_crepProofTheory                                            (105s)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-3120/pancake/proofs/.hol/logs/pan_to_crepProofTheory
pan_itreeEquivProofTheory                                         (173s)MKILLED