Job 3115

CakeML:ebaa9cd44bd8880f5b420098fc2a8e2b3583e734
  Replace list_max with MAX_LIST [Jan 09 13:04:27]
#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 13:28:50 Claimed job
Jan 09 13:28:54 Reusing HOL
Jan 09 13:29:02 Starting developers
Jan 09 13:29:07 Finished developers                                               4s 149MB
Jan 09 13:29:08 Starting developers/bin
Jan 09 13:29:12 Finished developers/bin                                           3s  91MB
Jan 09 13:29:13 Starting misc
Jan 09 13:29:56 Finished misc                                                    42s   1GB
Jan 09 13:29:57 Starting compiler/proofs
Jan 09 14:31:23 Finished compiler/proofs                                    1h01m25s  11GB
Jan 09 14:31:24 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 09 20:17:11 Finished compiler/bootstrap/compilation/x64/64/proofs       5h45m45s  84GB
Jan 09 20:17:11 Starting semantics/ffi
Jan 09 20:17:22 Finished semantics/ffi                                            9s 565MB
Jan 09 20:17:23 Starting semantics
Jan 09 20:17:24 Finished semantics                                                0s  62MB
Jan 09 20:17:25 Starting semantics/proofs
Jan 09 20:17:47 Finished semantics/proofs                                        21s 899MB
Jan 09 20:17:48 Starting semantics/alt_semantics
Jan 09 20:18:07 Finished semantics/alt_semantics                                 18s 721MB
Jan 09 20:18:08 Starting semantics/alt_semantics/proofs
Jan 09 20:22:13 Finished semantics/alt_semantics/proofs                        4m04s   2GB
Jan 09 20:22:14 Starting basis/pure
Jan 09 20:22:16 Finished basis/pure                                               1s  95MB
Jan 09 20:22:17 Starting translator
Jan 09 20:23:19 Finished translator                                            1m00s   2GB
Jan 09 20:23:20 Starting compiler/parsing
Jan 09 20:23:21 Finished compiler/parsing                                         0s  64MB
Jan 09 20:23:22 Starting characteristic
Jan 09 20:23:24 Finished characteristic                                           1s 118MB
Jan 09 20:23:25 Starting translator/monadic
Jan 09 20:23:27 Finished translator/monadic                                       1s 120MB
Jan 09 20:23:28 Starting translator/monadic/monad_base
Jan 09 20:23:30 Finished translator/monadic/monad_base                            0s  63MB
Jan 09 20:23:31 Starting profiler
Jan 09 20:24:00 Finished profiler                                                28s   1GB
Jan 09 20:24:01 Starting basis
Jan 09 20:25:34 Finished basis                                                 1m32s   4GB
Jan 09 20:25:35 Starting compiler
Jan 09 20:25:38 Finished compiler                                                 2s 220MB
Jan 09 20:25:39 Starting compiler/inference
Jan 09 20:25:41 Finished compiler/inference                                       1s 109MB
Jan 09 20:25:42 Starting compiler/backend/reg_alloc
Jan 09 20:25:44 Finished compiler/backend/reg_alloc                               1s  93MB
Jan 09 20:25:45 Starting compiler/backend/gc
Jan 09 20:25:47 Finished compiler/backend/gc                                      1s 137MB
Jan 09 20:25:48 Starting compiler/backend
Jan 09 20:25:54 Finished compiler/backend                                         5s 273MB
Jan 09 20:25:55 Starting compiler/encoders/asm
Jan 09 20:25:57 Finished compiler/encoders/asm                                    0s  95MB
Jan 09 20:25:58 Starting compiler/encoders/x64
Jan 09 20:26:00 Finished compiler/encoders/x64                                    1s  93MB
Jan 09 20:26:01 Starting compiler/encoders/arm7
Jan 09 20:26:03 Finished compiler/encoders/arm7                                   1s  94MB
Jan 09 20:26:03 Starting compiler/encoders/arm8
Jan 09 20:26:05 Finished compiler/encoders/arm8                                   1s  96MB
Jan 09 20:26:06 Starting compiler/encoders/arm8_asl
Jan 09 20:26:20 Finished compiler/encoders/arm8_asl                              13s   1GB
Jan 09 20:26:21 Starting compiler/encoders/mips
Jan 09 20:26:23 Finished compiler/encoders/mips                                   1s  96MB
Jan 09 20:26:24 Starting compiler/encoders/riscv
Jan 09 20:26:26 Finished compiler/encoders/riscv                                  1s  95MB
Jan 09 20:26:27 Starting compiler/encoders/ag32
Jan 09 20:26:28 Finished compiler/encoders/ag32                                   0s  89MB
Jan 09 20:26:29 Starting compiler/encoders/tests
Jan 09 20:26:31 Finished compiler/encoders/tests                                  1s 107MB
Jan 09 20:26:32 Starting compiler/encoders/monadic_enc
Jan 09 20:26:54 Finished compiler/encoders/monadic_enc                           21s   1GB
Jan 09 20:26:55 Starting compiler/backend/x64
Jan 09 20:26:58 Finished compiler/backend/x64                                     1s 141MB
Jan 09 20:26:59 Starting compiler/backend/arm7
Jan 09 20:27:01 Finished compiler/backend/arm7                                    1s 141MB
Jan 09 20:27:02 Starting compiler/backend/arm8
Jan 09 20:27:04 Finished compiler/backend/arm8                                    1s 141MB
Jan 09 20:27:05 Starting compiler/backend/mips
Jan 09 20:27:08 Finished compiler/backend/mips                                    1s 141MB
Jan 09 20:27:09 Starting compiler/backend/riscv
Jan 09 20:27:11 Finished compiler/backend/riscv                                   1s 140MB
Jan 09 20:27:12 Starting compiler/backend/ag32
Jan 09 20:28:11 Finished compiler/backend/ag32                                   58s   3GB
Jan 09 20:28:12 Starting compiler/backend/pattern_matching
Jan 09 20:28:13 Finished compiler/backend/pattern_matching                        0s  61MB
Jan 09 20:28:14 Starting compiler/parsing/ocaml
Jan 09 20:29:58 Finished compiler/parsing/ocaml                                1m42s   1GB
Jan 09 20:29:58 Starting compiler/printing
Jan 09 20:30:01 Finished compiler/printing                                        1s 121MB
Jan 09 20:30:01 Starting compiler/parsing/proofs
Jan 09 20:30:03 Finished compiler/parsing/proofs                                  0s  70MB
Jan 09 20:30:04 Starting compiler/inference/proofs
Jan 09 20:30:06 Finished compiler/inference/proofs                                1s 111MB
Jan 09 20:30:07 Starting compiler/backend/semantics
Jan 09 20:32:16 Finished compiler/backend/semantics                            2m08s   2GB
Jan 09 20:32:17 Starting compiler/backend/reg_alloc/proofs
Jan 09 20:32:20 Finished compiler/backend/reg_alloc/proofs                        1s 114MB
Jan 09 20:32:20 Starting compiler/backend/proofs
Jan 09 20:33:02 Finished compiler/backend/proofs                                 40s   2GB
Jan 09 20:33:02 Starting compiler/backend/serialiser
Jan 09 20:33:05 Finished compiler/backend/serialiser                              1s 144MB
Jan 09 20:33:06 Starting compiler/encoders/x64/proofs
Jan 09 20:33:08 Finished compiler/encoders/x64/proofs                             1s  94MB
Jan 09 20:33:09 Starting compiler/encoders/arm7/proofs
Jan 09 20:44:04 Finished compiler/encoders/arm7/proofs                        10m54s  13GB
Jan 09 20:44:05 Starting compiler/encoders/arm8/proofs
Jan 09 20:50:42 Finished compiler/encoders/arm8/proofs                         6m36s   5GB
Jan 09 20:50:43 Starting compiler/encoders/arm8_asl/proofs
Jan 09 21:05:25 Finished compiler/encoders/arm8_asl/proofs                    14m40s   5GB
Jan 09 21:05:26 Starting compiler/encoders/mips/proofs
Jan 09 21:14:16 Finished compiler/encoders/mips/proofs                         8m49s   8GB
Jan 09 21:14:17 Starting compiler/encoders/riscv/proofs
Jan 09 21:21:56 Finished compiler/encoders/riscv/proofs                        7m38s   3GB
Jan 09 21:21:57 Starting compiler/encoders/ag32/proofs
Jan 09 21:24:33 Finished compiler/encoders/ag32/proofs                         2m35s   2GB
Jan 09 21:24:34 Starting compiler/backend/x64/proofs
Jan 09 21:24:37 Finished compiler/backend/x64/proofs                              2s 209MB
Jan 09 21:24:38 Starting compiler/backend/arm7/proofs
Jan 09 21:25:17 Finished compiler/backend/arm7/proofs                            38s   2GB
Jan 09 21:25:18 Starting compiler/backend/arm8/proofs
Jan 09 21:25:52 Finished compiler/backend/arm8/proofs                            32s   1GB
Jan 09 21:25:53 Starting compiler/backend/arm8_asl
Jan 09 21:26:18 Finished compiler/backend/arm8_asl                               24s   1GB
Jan 09 21:26:19 Starting compiler/backend/mips/proofs
Jan 09 21:26:55 Finished compiler/backend/mips/proofs                            34s   2GB
Jan 09 21:26:55 Starting compiler/backend/riscv/proofs
Jan 09 21:27:33 Finished compiler/backend/riscv/proofs                           36s   2GB
Jan 09 21:27:34 Starting compiler/backend/ag32/proofs
Jan 09 21:38:25 Finished compiler/backend/ag32/proofs                         10m50s   5GB
Jan 09 21:38:26 Starting compiler/backend/cv_compute
Jan 09 21:38:53 Finished compiler/backend/cv_compute                             25s   1GB
Jan 09 21:38:53 Starting cv_translator
Jan 09 21:44:06 Finished cv_translator                                         5m11s   5GB
Jan 09 21:44:07 Starting candle
Jan 09 21:44:08 Finished candle                                                   0s  17MB
Jan 09 21:44:08 Starting candle/set-theory
Jan 09 21:44:37 Finished candle/set-theory                                       28s 917MB
Jan 09 21:44:38 Starting candle/syntax-lib
Jan 09 21:44:40 Finished candle/syntax-lib                                        1s  97MB
Jan 09 21:44:41 Starting candle/standard
Jan 09 21:44:42 Finished candle/standard                                          0s  18MB
Jan 09 21:44:43 Starting candle/standard/syntax
Jan 09 21:44:56 Finished candle/standard/syntax                                  12s 793MB
Jan 09 21:44:57 Starting candle/standard/semantics
Jan 09 21:47:04 Finished candle/standard/semantics                             2m05s   3GB
Jan 09 21:47:05 Starting candle/standard/monadic
Jan 09 21:47:07 Finished candle/standard/monadic                                  1s 121MB
Jan 09 21:47:08 Starting candle/standard/ml_kernel
Jan 09 21:48:59 Finished candle/standard/ml_kernel                             1m50s   4GB
Jan 09 21:49:00 Starting candle/overloading
Jan 09 21:49:01 Finished candle/overloading                                       0s  18MB
Jan 09 21:49:02 Starting candle/overloading/syntax
Jan 09 21:50:13 FAILED: candle/overloading/syntax
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)/src/integer
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)/examples/machine-code/hoare-triple
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)/candle/syntax-lib
Scanned 31 directories
Starting work on README.md
Starting work on holSyntaxTheory
Starting work on holSyntaxRenamingTheory
README.md                                                           (0s)     OK
holSyntaxRenamingTheory                                            (11s)     OK
holSyntaxTheory                                                    (25s)     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                               (36s)FAIL<1>
 Saved theorem _______ "term_ok_extend"
 Saved theorem _______ "term_ok_updates"
 Saved theorem _______ "is_std_sig_extend"
 Saved theorem _______ "updates_theory_ok"
 Saved theorem _______ "extends_theory_ok"
 Saved theorem _______ "init_theory_ok"
 Saved theorem _______ "is_std_sig_extends"
 Saved theorem _______ "dependency_init_ctxt_size_directed"
 Saved theorem _______ "subst_clos_init_ctxt_size_directed"
 Saved theorem _______ "init_ctxt_wf"
 Saved theorem _______ "dependency_simps"
 Saved theorem _______ "orth_ctxt_simps"
 Saved theorem _______ "orth_ctxt_CONS"
 Saved theorem _______ "orth_ctxt_APPEND"
 Saved theorem _______ "list_subset_NIL"
 Saved theorem _______ "list_subset_SING"
 Saved theorem _______ "list_subset_IDENT"
 Saved theorem _______ "list_subset_SIMP"
 Saved theorem _______ "list_subset_MEM"
 Saved theorem _______ "list_subset_NIL2"
 Saved theorem _______ "list_subset_NOT_NIL"
 Saved theorem _______ "list_subset_set"
 Proved triviality ___ "list_inter_mono"
 Proved triviality ___ "list_inter_map"
 Proved triviality ___ "NULL_list_inter_tyvars_Tyapp"
 Proved triviality ___ "list_inter_map_inj"
 Saved theorem _______ "list_inter_distinct_prop"
 Proved triviality ___ "list_inter_heads"
 Proved triviality ___ "list_inter_tails"
 Proved triviality ___ "list_inter_elem"
 Proved triviality ___ "list_inter_subset"
 Proved triviality ___ "list_inter_set_symm"
 Proved triviality ___ "list_inter_set"
 Proved triviality ___ "list_inter_NULL_symm"
 Proved triviality ___ "list_inter_subset_outer"
 Proved triviality ___ "list_inter_subset_inner"
 Proved triviality ___ "NULL_list_inter_APPEND1"
 Proved triviality ___ "NULL_list_inter_APPEND"
 Proved triviality ___ "NULL_list_inter_SING"
 Proved triviality ___ "MAX_LIST_MEM_local"
 Proof of 
 
 l x y. MAX_LIST l  MAX_LIST (x ++ l ++ y)
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.THEN1:
   Failed to prove theorem "MAX_LIST_APPEND":
 goal completely solved by first tactic
 Full log: /scratch/cakeml/regression/cakeml-3115/candle/overloading/syntax/.hol/logs/holSyntaxExtraTheory