Job 2234

CakeML:d4b8eeab77c33aa3382b82a0e1cc30e6449703c1
  fix DUP in subgraph_iso [Nov 10 06:19:36]
#974 (dominance)
Merging into:7101a3f2e0c3885412c05e63735ec6da155253ee
  Fix for adjusted Inductive syntax [Nov 08 21:36:03]
HOL:be29184419aaa27f96bbbf8fb1b90d0e40385c33
  [emacs-mode] Handle new Inductive label syntaxes [Nov 08 03:19:35]
Machine:pavlova

Nov 10 22:31:53 Claimed job
Nov 10 22:32:02 Building HOL
Nov 10 22:46:41 Starting developers
Nov 10 22:46:45 Finished developers                                               2s 207MB
Nov 10 22:46:46 Starting developers/bin
Nov 10 22:46:57 Finished developers/bin                                          10s   1GB
Nov 10 22:46:58 Starting compiler/proofs
Nov 11 00:31:09 Finished compiler/proofs                                    1h44m10s  49GB
Nov 11 00:31:10 Starting compiler/bootstrap/translation
Nov 11 08:31:05 Finished compiler/bootstrap/translation                     7h59m53s  77GB
Nov 11 08:31:06 Starting semantics/ffi
Nov 11 08:31:14 Finished semantics/ffi                                            7s 562MB
Nov 11 08:31:15 Starting semantics
Nov 11 08:31:16 Finished semantics                                                0s  68MB
Nov 11 08:31:17 Starting semantics/proofs
Nov 11 08:31:53 Finished semantics/proofs                                        35s   2GB
Nov 11 08:31:54 Starting semantics/alt_semantics
Nov 11 08:32:34 Finished semantics/alt_semantics                                 39s   1GB
Nov 11 08:32:35 Starting semantics/alt_semantics/proofs
Nov 11 08:43:28 Finished semantics/alt_semantics/proofs                       10m51s   4GB
Nov 11 08:43:29 Starting basis/pure
Nov 11 08:43:30 Finished basis/pure                                               0s  67MB
Nov 11 08:43:31 Starting translator
Nov 11 08:45:13 Finished translator                                            1m40s   3GB
Nov 11 08:45:13 Starting compiler/parsing
Nov 11 08:45:15 Finished compiler/parsing                                         0s  69MB
Nov 11 08:45:16 Starting characteristic
Nov 11 08:45:17 Finished characteristic                                           0s  90MB
Nov 11 08:45:18 Starting translator/monadic
Nov 11 08:45:20 Finished translator/monadic                                       0s  91MB
Nov 11 08:45:20 Starting basis
Nov 11 08:49:01 Finished basis                                                 3m39s   5GB
Nov 11 08:49:02 Starting compiler/inference
Nov 11 08:49:03 Finished compiler/inference                                       0s  79MB
Nov 11 08:49:04 Starting compiler/backend/reg_alloc
Nov 11 08:49:05 Finished compiler/backend/reg_alloc                               0s  66MB
Nov 11 08:49:06 Starting compiler/backend/gc
Nov 11 08:49:08 Finished compiler/backend/gc                                      0s 131MB
Nov 11 08:49:09 Starting compiler/backend
Nov 11 08:49:26 Finished compiler/backend                                        16s   1GB
Nov 11 08:49:27 Starting compiler/encoders/asm
Nov 11 08:49:28 Finished compiler/encoders/asm                                    0s  83MB
Nov 11 08:49:29 Starting compiler/encoders/x64
Nov 11 08:49:30 Finished compiler/encoders/x64                                    0s  88MB
Nov 11 08:49:31 Starting compiler/encoders/arm7
Nov 11 08:49:33 Finished compiler/encoders/arm7                                   0s  93MB
Nov 11 08:49:34 Starting compiler/encoders/arm8
Nov 11 08:49:35 Finished compiler/encoders/arm8                                   0s  87MB
Nov 11 08:49:36 Starting compiler/encoders/arm8_asl
Nov 11 10:57:23 Finished compiler/encoders/arm8_asl                         2h07m45s  43GB
Nov 11 10:57:24 Starting compiler/encoders/mips
Nov 11 10:57:25 Finished compiler/encoders/mips                                   0s  87MB
Nov 11 10:57:26 Starting compiler/encoders/riscv
Nov 11 10:57:28 Finished compiler/encoders/riscv                                  0s  90MB
Nov 11 10:57:28 Starting compiler/encoders/ag32
Nov 11 10:57:30 Finished compiler/encoders/ag32                                   0s  90MB
Nov 11 10:57:31 Starting compiler/backend/x64
Nov 11 10:57:32 Finished compiler/backend/x64                                     0s 129MB
Nov 11 10:57:33 Starting compiler/backend/arm7
Nov 11 10:57:35 Finished compiler/backend/arm7                                    0s 129MB
Nov 11 10:57:36 Starting compiler/backend/arm8
Nov 11 10:57:38 Finished compiler/backend/arm8                                    0s 129MB
Nov 11 10:57:38 Starting compiler/backend/mips
Nov 11 10:57:40 Finished compiler/backend/mips                                    0s 129MB
Nov 11 10:57:41 Starting compiler/backend/riscv
Nov 11 10:57:43 Finished compiler/backend/riscv                                   0s 129MB
Nov 11 10:57:44 Starting compiler/backend/ag32
Nov 11 10:59:04 Finished compiler/backend/ag32                                 1m19s   4GB
Nov 11 10:59:04 Starting compiler/parsing/proofs
Nov 11 10:59:06 Finished compiler/parsing/proofs                                  0s  72MB
Nov 11 10:59:07 Starting compiler/inference/proofs
Nov 11 10:59:08 Finished compiler/inference/proofs                                0s  86MB
Nov 11 10:59:09 Starting compiler/backend/semantics
Nov 11 11:00:34 Finished compiler/backend/semantics                            1m23s   2GB
Nov 11 11:00:34 Starting compiler/backend/reg_alloc/proofs
Nov 11 11:00:36 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Nov 11 11:00:37 Starting compiler/backend/proofs
Nov 11 11:01:38 Finished compiler/backend/proofs                               1m00s   3GB
Nov 11 11:01:39 Starting compiler/backend/serialiser
Nov 11 11:01:41 Finished compiler/backend/serialiser                              1s 187MB
Nov 11 11:01:42 Starting compiler/encoders/x64/proofs
Nov 11 11:11:06 Finished compiler/encoders/x64/proofs                          9m23s   5GB
Nov 11 11:11:07 Starting compiler/encoders/arm7/proofs
Nov 11 11:23:52 Finished compiler/encoders/arm7/proofs                        12m44s   9GB
Nov 11 11:23:53 Starting compiler/encoders/arm8/proofs
Nov 11 11:30:52 Finished compiler/encoders/arm8/proofs                         6m58s   5GB
Nov 11 11:30:53 Starting compiler/encoders/arm8_asl/proofs
Nov 11 12:18:20 Finished compiler/encoders/arm8_asl/proofs                    47m25s  11GB
Nov 11 12:18:21 Starting compiler/encoders/mips/proofs
Nov 11 12:28:25 Finished compiler/encoders/mips/proofs                        10m02s   6GB
Nov 11 12:28:25 Starting compiler/encoders/riscv/proofs
Nov 11 12:36:46 Finished compiler/encoders/riscv/proofs                        8m19s   3GB
Nov 11 12:36:47 Starting compiler/encoders/ag32/proofs
Nov 11 12:39:10 Finished compiler/encoders/ag32/proofs                         2m22s   3GB
Nov 11 12:39:11 Starting compiler/backend/x64/proofs
Nov 11 12:39:50 Finished compiler/backend/x64/proofs                             37s   3GB
Nov 11 12:39:51 Starting compiler/backend/arm7/proofs
Nov 11 12:40:38 Finished compiler/backend/arm7/proofs                            46s   3GB
Nov 11 12:40:39 Starting compiler/backend/arm8/proofs
Nov 11 12:41:19 Finished compiler/backend/arm8/proofs                            39s   3GB
Nov 11 12:41:20 Starting compiler/backend/arm8_asl
Nov 11 12:41:49 Finished compiler/backend/arm8_asl                               27s   2GB
Nov 11 12:41:50 Starting compiler/backend/mips/proofs
Nov 11 12:42:32 Finished compiler/backend/mips/proofs                            41s   3GB
Nov 11 12:42:33 Starting compiler/backend/riscv/proofs
Nov 11 12:43:24 Finished compiler/backend/riscv/proofs                           50s   3GB
Nov 11 12:43:25 Starting compiler/backend/ag32/proofs
Nov 11 12:56:26 Finished compiler/backend/ag32/proofs                         13m00s   5GB
Nov 11 12:56:27 Starting candle/set-theory
Nov 11 12:57:13 Finished candle/set-theory                                       44s   1GB
Nov 11 12:57:14 Starting candle/syntax-lib
Nov 11 12:57:15 Finished candle/syntax-lib                                        0s  70MB
Nov 11 12:57:16 Starting candle/standard/syntax
Nov 11 12:57:33 Finished candle/standard/syntax                                  15s   1GB
Nov 11 12:57:34 Starting candle/standard/semantics
Nov 11 12:59:58 Finished candle/standard/semantics                             2m23s   2GB
Nov 11 12:59:59 Starting candle/standard/monadic
Nov 11 13:00:00 Finished candle/standard/monadic                                  0s 102MB
Nov 11 13:00:01 Starting candle/standard/ml_kernel
Nov 11 13:01:54 Finished candle/standard/ml_kernel                             1m51s   6GB
Nov 11 13:01:55 Starting candle/overloading/syntax
Nov 11 13:05:15 Finished candle/overloading/syntax                             3m19s   2GB
Nov 11 13:05:16 Starting candle/overloading/semantics
Nov 11 13:16:28 Finished candle/overloading/semantics                         11m10s   5GB
Nov 11 13:16:28 Starting candle/overloading/monadic
Nov 11 13:19:05 Finished candle/overloading/monadic                            2m35s   3GB
Nov 11 13:19:06 Starting candle/overloading/ml_kernel
Nov 11 13:26:35 Finished candle/overloading/ml_kernel                          7m28s   6GB
Nov 11 13:26:36 Starting candle/overloading/ml_checker
Nov 11 13:29:06 Finished candle/overloading/ml_checker                         2m28s   7GB
Nov 11 13:29:07 Starting candle/prover
Nov 11 13:38:54 Finished candle/prover                                         9m46s   5GB
Nov 11 13:38:55 Starting pancake
Nov 11 13:39:55 Finished pancake                                                 59s   1GB
Nov 11 13:39:56 Starting pancake/ffi
Nov 11 13:39:57 Finished pancake/ffi                                              0s  19MB
Nov 11 13:39:58 Starting pancake/semantics
Nov 11 13:42:20 Finished pancake/semantics                                     2m21s   2GB
Nov 11 13:42:21 Starting pancake/parser
Nov 11 13:42:48 Finished pancake/parser                                          26s   2GB
Nov 11 13:42:49 Starting pancake/proofs
Nov 11 14:12:16 Finished pancake/proofs                                       29m25s   8GB
Nov 11 14:12:17 Starting characteristic/examples
Nov 11 14:13:53 Finished characteristic/examples                               1m35s   5GB
Nov 11 14:13:54 Starting tutorial/solutions
Nov 11 14:29:14 Finished tutorial/solutions                                   15m18s  11GB
Nov 11 14:29:15 Starting translator/monadic/examples
Nov 11 14:32:57 Finished translator/monadic/examples                           3m41s   5GB
Nov 11 14:32:58 Starting examples
Nov 11 14:47:28 Finished examples                                             14m28s   7GB
Nov 11 14:47:28 Starting examples/compilation/x64
Nov 11 16:44:46 Finished examples/compilation/x64                           1h57m16s  37GB
Nov 11 16:44:47 Starting examples/compilation/x64/proofs
Nov 11 16:48:32 Finished examples/compilation/x64/proofs                       3m44s   6GB
Nov 11 16:48:33 Starting examples/compilation/ag32
Nov 11 17:18:35 Finished examples/compilation/ag32                            30m01s  12GB
Nov 11 17:18:36 Starting examples/compilation/ag32/proofs
Nov 11 17:20:05 Finished examples/compilation/ag32/proofs                      1m27s   7GB
Nov 11 17:20:06 Starting examples/compilation/to_word
Nov 11 17:24:04 Finished examples/compilation/to_word                          3m57s  13GB
Nov 11 17:24:05 Starting examples/lpr_checker
Nov 11 17:25:20 Finished examples/lpr_checker                                  1m14s   2GB
Nov 11 17:25:21 Starting examples/lpr_checker/array
Nov 11 17:26:36 FAILED: examples/lpr_checker/array
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker[0m
Scanned 32 directories
Starting work on README.md
Starting work on lpr_composeProgTheory
Starting work on lpr_listTheory
README.md                                                           (0s)     OK
lpr_listTheory                                                     (66s)FAIL<1>
 Saved theorem _______ "list_delete_list_FOLDL"
 Saved theorem _______ "ind_rel_list_delete_list"
 Saved theorem _______ "LENGTH_list_delete_list"
 Saved theorem _______ "fml_rel_list_delete_list"
 Saved theorem _______ "ind_rel_update_resize"
 Saved theorem _______ "fml_rel_update_resize"
 Saved theorem _______ "earliest_rel_list_delete_list"
 error in quse /scratch/cakeml/regression/cakeml-2234/examples/lpr_checker/array/lpr_listScript.sml : DUP "index_11"
 error in load /scratch/cakeml/regression/cakeml-2234/examples/lpr_checker/array/lpr_listScript : DUP "index_11"
 Uncaught exception: DUP "index_11"
lpr_composeProgTheory                                              (67s)MKILLED