Job 3118

CakeML:b98a99fc61917d6e4715b4f27875956b26d157d5
  Fix a proof [Jan 09 22:55:35]
#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:pavlova

Jan 09 23:23:59 Claimed job
Jan 09 23:24:03 Reusing HOL
Jan 09 23:24:10 Starting developers
Jan 09 23:24:16 Finished developers                                               4s 209MB
Jan 09 23:24:17 Starting developers/bin
Jan 09 23:24:21 Finished developers/bin                                           3s  91MB
Jan 09 23:24:22 Starting misc
Jan 09 23:25:01 Finished misc                                                    38s   1GB
Jan 09 23:25:02 Starting compiler/proofs
Jan 10 00:26:25 Finished compiler/proofs                                    1h01m21s  12GB
Jan 10 00:26:26 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 10 06:14:45 Finished compiler/bootstrap/compilation/x64/64/proofs       5h48m18s  81GB
Jan 10 06:14:46 Starting semantics/ffi
Jan 10 06:14:56 Finished semantics/ffi                                            9s 569MB
Jan 10 06:14:56 Starting semantics
Jan 10 06:14:58 Finished semantics                                                0s  62MB
Jan 10 06:14:59 Starting semantics/proofs
Jan 10 06:15:21 Finished semantics/proofs                                        21s 869MB
Jan 10 06:15:22 Starting semantics/alt_semantics
Jan 10 06:15:41 Finished semantics/alt_semantics                                 18s 721MB
Jan 10 06:15:42 Starting semantics/alt_semantics/proofs
Jan 10 06:19:46 Finished semantics/alt_semantics/proofs                        4m03s   2GB
Jan 10 06:19:47 Starting basis/pure
Jan 10 06:19:48 Finished basis/pure                                               1s  90MB
Jan 10 06:19:49 Starting translator
Jan 10 06:20:51 Finished translator                                            1m00s   3GB
Jan 10 06:20:52 Starting compiler/parsing
Jan 10 06:20:54 Finished compiler/parsing                                         0s  64MB
Jan 10 06:20:54 Starting characteristic
Jan 10 06:20:57 Finished characteristic                                           1s 118MB
Jan 10 06:20:57 Starting translator/monadic
Jan 10 06:21:00 Finished translator/monadic                                       1s 120MB
Jan 10 06:21:01 Starting translator/monadic/monad_base
Jan 10 06:21:02 Finished translator/monadic/monad_base                            0s  63MB
Jan 10 06:21:03 Starting profiler
Jan 10 06:21:32 Finished profiler                                                28s   1GB
Jan 10 06:21:33 Starting basis
Jan 10 06:23:03 Finished basis                                                 1m28s   4GB
Jan 10 06:23:04 Starting compiler
Jan 10 06:23:07 Finished compiler                                                 2s 221MB
Jan 10 06:23:08 Starting compiler/inference
Jan 10 06:23:10 Finished compiler/inference                                       1s 116MB
Jan 10 06:23:11 Starting compiler/backend/reg_alloc
Jan 10 06:23:13 Finished compiler/backend/reg_alloc                               1s  93MB
Jan 10 06:23:14 Starting compiler/backend/gc
Jan 10 06:23:16 Finished compiler/backend/gc                                      1s 144MB
Jan 10 06:23:17 Starting compiler/backend
Jan 10 06:23:23 Finished compiler/backend                                         5s 273MB
Jan 10 06:23:24 Starting compiler/encoders/asm
Jan 10 06:23:26 Finished compiler/encoders/asm                                    0s  95MB
Jan 10 06:23:26 Starting compiler/encoders/x64
Jan 10 06:23:28 Finished compiler/encoders/x64                                    1s  94MB
Jan 10 06:23:29 Starting compiler/encoders/arm7
Jan 10 06:23:31 Finished compiler/encoders/arm7                                   1s  94MB
Jan 10 06:23:32 Starting compiler/encoders/arm8
Jan 10 06:23:34 Finished compiler/encoders/arm8                                   1s  96MB
Jan 10 06:23:35 Starting compiler/encoders/arm8_asl
Jan 10 06:23:50 Finished compiler/encoders/arm8_asl                              14s   1GB
Jan 10 06:23:50 Starting compiler/encoders/mips
Jan 10 06:23:52 Finished compiler/encoders/mips                                   1s  96MB
Jan 10 06:23:53 Starting compiler/encoders/riscv
Jan 10 06:23:55 Finished compiler/encoders/riscv                                  1s  95MB
Jan 10 06:23:56 Starting compiler/encoders/ag32
Jan 10 06:23:58 Finished compiler/encoders/ag32                                   0s  90MB
Jan 10 06:23:59 Starting compiler/encoders/tests
Jan 10 06:24:01 Finished compiler/encoders/tests                                  1s 106MB
Jan 10 06:24:02 Starting compiler/encoders/monadic_enc
Jan 10 06:24:25 Finished compiler/encoders/monadic_enc                           22s   1GB
Jan 10 06:24:26 Starting compiler/backend/x64
Jan 10 06:24:28 Finished compiler/backend/x64                                     1s 141MB
Jan 10 06:24:29 Starting compiler/backend/arm7
Jan 10 06:24:31 Finished compiler/backend/arm7                                    1s 140MB
Jan 10 06:24:32 Starting compiler/backend/arm8
Jan 10 06:24:35 Finished compiler/backend/arm8                                    1s 139MB
Jan 10 06:24:36 Starting compiler/backend/mips
Jan 10 06:24:38 Finished compiler/backend/mips                                    1s 140MB
Jan 10 06:24:39 Starting compiler/backend/riscv
Jan 10 06:24:41 Finished compiler/backend/riscv                                   1s 140MB
Jan 10 06:24:42 Starting compiler/backend/ag32
Jan 10 06:25:43 Finished compiler/backend/ag32                                   59s   3GB
Jan 10 06:25:44 Starting compiler/backend/pattern_matching
Jan 10 06:25:45 Finished compiler/backend/pattern_matching                        0s  61MB
Jan 10 06:25:46 Starting compiler/parsing/ocaml
Jan 10 06:27:32 Finished compiler/parsing/ocaml                                1m45s   1GB
Jan 10 06:27:33 Starting compiler/printing
Jan 10 06:27:35 Finished compiler/printing                                        1s 121MB
Jan 10 06:27:36 Starting compiler/parsing/proofs
Jan 10 06:27:38 Finished compiler/parsing/proofs                                  0s  71MB
Jan 10 06:27:39 Starting compiler/inference/proofs
Jan 10 06:27:41 Finished compiler/inference/proofs                                1s 111MB
Jan 10 06:27:42 Starting compiler/backend/semantics
Jan 10 06:29:50 Finished compiler/backend/semantics                            2m06s   2GB
Jan 10 06:29:50 Starting compiler/backend/reg_alloc/proofs
Jan 10 06:29:53 Finished compiler/backend/reg_alloc/proofs                        1s 113MB
Jan 10 06:29:54 Starting compiler/backend/proofs
Jan 10 06:30:39 Finished compiler/backend/proofs                                 44s   3GB
Jan 10 06:30:39 Starting compiler/backend/serialiser
Jan 10 06:30:42 Finished compiler/backend/serialiser                              1s 144MB
Jan 10 06:30:43 Starting compiler/encoders/x64/proofs
Jan 10 06:30:45 Finished compiler/encoders/x64/proofs                             1s  93MB
Jan 10 06:30:46 Starting compiler/encoders/arm7/proofs
Jan 10 06:41:34 Finished compiler/encoders/arm7/proofs                        10m47s  11GB
Jan 10 06:41:35 Starting compiler/encoders/arm8/proofs
Jan 10 06:48:06 Finished compiler/encoders/arm8/proofs                         6m29s   7GB
Jan 10 06:48:07 Starting compiler/encoders/arm8_asl/proofs
Jan 10 07:02:24 Finished compiler/encoders/arm8_asl/proofs                    14m16s   4GB
Jan 10 07:02:25 Starting compiler/encoders/mips/proofs
Jan 10 07:11:16 Finished compiler/encoders/mips/proofs                         8m50s   8GB
Jan 10 07:11:17 Starting compiler/encoders/riscv/proofs
Jan 10 07:19:04 Finished compiler/encoders/riscv/proofs                        7m45s   6GB
Jan 10 07:19:05 Starting compiler/encoders/ag32/proofs
Jan 10 07:21:41 Finished compiler/encoders/ag32/proofs                         2m35s   2GB
Jan 10 07:21:42 Starting compiler/backend/x64/proofs
Jan 10 07:21:45 Finished compiler/backend/x64/proofs                              2s 208MB
Jan 10 07:21:46 Starting compiler/backend/arm7/proofs
Jan 10 07:22:26 Finished compiler/backend/arm7/proofs                            39s   2GB
Jan 10 07:22:27 Starting compiler/backend/arm8/proofs
Jan 10 07:23:00 Finished compiler/backend/arm8/proofs                            32s   1GB
Jan 10 07:23:01 Starting compiler/backend/arm8_asl
Jan 10 07:23:26 Finished compiler/backend/arm8_asl                               24s   1GB
Jan 10 07:23:27 Starting compiler/backend/mips/proofs
Jan 10 07:24:03 Finished compiler/backend/mips/proofs                            34s   2GB
Jan 10 07:24:04 Starting compiler/backend/riscv/proofs
Jan 10 07:24:42 Finished compiler/backend/riscv/proofs                           37s   2GB
Jan 10 07:24:43 Starting compiler/backend/ag32/proofs
Jan 10 07:35:37 Finished compiler/backend/ag32/proofs                         10m53s   5GB
Jan 10 07:35:38 Starting compiler/backend/cv_compute
Jan 10 07:36:05 Finished compiler/backend/cv_compute                             25s   1GB
Jan 10 07:36:05 Starting cv_translator
Jan 10 07:41:07 Finished cv_translator                                         5m00s   5GB
Jan 10 07:41:08 Starting candle
Jan 10 07:41:09 Finished candle                                                   0s  18MB
Jan 10 07:41:09 Starting candle/set-theory
Jan 10 07:41:39 Finished candle/set-theory                                       28s 915MB
Jan 10 07:41:39 Starting candle/syntax-lib
Jan 10 07:41:41 Finished candle/syntax-lib                                        1s  97MB
Jan 10 07:41:42 Starting candle/standard
Jan 10 07:41:43 Finished candle/standard                                          0s  18MB
Jan 10 07:41:44 Starting candle/standard/syntax
Jan 10 07:41:58 Finished candle/standard/syntax                                  13s 792MB
Jan 10 07:41:59 Starting candle/standard/semantics
Jan 10 07:44:06 Finished candle/standard/semantics                             2m06s   3GB
Jan 10 07:44:07 Starting candle/standard/monadic
Jan 10 07:44:09 Finished candle/standard/monadic                                  1s 123MB
Jan 10 07:44:10 Starting candle/standard/ml_kernel
Jan 10 07:46:01 Finished candle/standard/ml_kernel                             1m50s   4GB
Jan 10 07:46:02 Starting candle/overloading
Jan 10 07:46:03 Finished candle/overloading                                       0s  17MB
Jan 10 07:46:04 Starting candle/overloading/syntax
Jan 10 07:49:06 Finished candle/overloading/syntax                             3m00s   2GB
Jan 10 07:49:06 Starting candle/overloading/semantics
Jan 10 07:59:25 Finished candle/overloading/semantics                         10m17s   9GB
Jan 10 07:59:26 Starting candle/overloading/monadic
Jan 10 08:01:32 Finished candle/overloading/monadic                            2m04s   1GB
Jan 10 08:01:32 Starting candle/overloading/ml_kernel
Jan 10 08:07:39 Finished candle/overloading/ml_kernel                          6m05s   6GB
Jan 10 08:07:40 Starting candle/overloading/ml_checker
Jan 10 08:09:52 Finished candle/overloading/ml_checker                         2m10s   6GB
Jan 10 08:09:53 Starting candle/prover
Jan 10 08:09:56 Finished candle/prover                                            2s 160MB
Jan 10 08:09:57 Starting candle/prover/compute
Jan 10 08:09:59 Finished candle/prover/compute                                    1s 150MB
Jan 10 08:10:00 Starting pancake
Jan 10 08:10:03 Finished pancake                                                  1s 140MB
Jan 10 08:10:03 Starting pancake/semantics
Jan 10 08:10:16 FAILED: pancake/semantics
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
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 $(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)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/pancake
Scanned 47 directories
Starting work on README.md
Starting work on panSemTheory
Starting work on pan_commonPropsTheory
Starting work on loopSemTheory
README.md                                                           (0s)     OK
pan_commonPropsTheory                                               (8s)FAIL<1>
 Saved theorem _______ "opt_mmap_el"
 Saved theorem _______ "opt_mmap_length_eq"
 Saved theorem _______ "opt_mmap_opt_map"
 Saved theorem _______ "distinct_lists_append"
 Saved theorem _______ "distinct_lists_commutes"
 Saved theorem _______ "distinct_lists_cons"
 Saved theorem _______ "distinct_lists_simp_cons"
 Saved theorem _______ "distinct_lists_append_intro"
 Saved theorem _______ "opt_mmap_flookup_update"
 Saved theorem _______ "opt_mmap_some_eq_zip_flookup"
 Saved theorem _______ "opt_mmap_disj_zip_flookup"
 Saved theorem _______ "genlist_distinct_max"
 Saved theorem _______ "genlist_distinct_max'"
 Saved theorem _______ "update_eq_zip_flookup"
 Saved theorem _______ "update_eq_zip_map_flookup"
 Saved theorem _______ "flookup_fupdate_zip_not_mem"
 Saved theorem _______ "map_flookup_fupdate_zip_not_mem"
 Saved theorem _______ "domsub_commutes_fupdate"
 Saved theorem _______ "map_the_some_cancel"
 Proved triviality ___ "FUPDATE_LIST_APPLY_NOT_MEM_ZIP"
 Saved theorem _______ "fm_multi_update"
 Saved theorem _______ "el_reduc_tl"
 Saved theorem _______ "zero_not_mem_genlist_offset"
 Saved theorem _______ "all_distinct_take"
 Saved theorem _______ "all_distinct_drop"
 Saved theorem _______ "disjoint_take_drop_sum"
 Saved theorem _______ "disjoint_drop_take_sum"
 Saved theorem _______ "fm_empty_zip_alist"
 Saved theorem _______ "fm_empty_zip_flookup"
 Saved theorem _______ "fm_empty_zip_flookup_el"
 Saved theorem _______ "all_distinct_flookup_all_distinct"
 Saved theorem _______ "no_overlap_flookup_distinct"
 Saved theorem _______ "all_distinct_take_frop_disjoint"
 Saved theorem _______ "fupdate_flookup_zip_elim"
 Saved theorem _______ "not_mem_fst_zip_flookup_empty"
 Saved theorem _______ "fm_zip_append_take_drop"
 Saved theorem _______ "disjoint_not_mem_el"
 Saved theorem _______ "map_some_the_map"
 Saved theorem _______ "set_eq_membership"
 Saved theorem _______ "max_set_MAX_LIST"
 Proof of 
 
 xs. MEM (MAX_LIST xs + 1) xs
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.POP_ASSUM:
   Failed to prove theorem "MAX_LIST_add_not_mem":
 no assum
 Full log: /scratch/cakeml/regression/cakeml-3118/pancake/semantics/.hol/logs/pan_commonPropsTheory
panSemTheory                                                        (8s)MKILLED
loopSemTheory                                                       (8s)MKILLED