Job 2227

CakeML:d31b99f24aed144a39d8c6ea6af2d11b9862800b
  Fix rebinds [Oct 20 10:27:08]
HOL:7a4ed25a1c86b11f888c1dcbe99f988258bb9210
  Various fixes for theorem-rebind errors [Oct 11 00:17:28]
Machine:pavlova

Oct 20 10:27:59 Claimed job
Oct 20 10:28:02 Reusing HOL
Oct 20 10:28:12 Starting developers
Oct 20 10:28:16 Finished developers                                               2s 186MB
Oct 20 10:28:17 Starting developers/bin
Oct 20 10:28:28 Finished developers/bin                                          10s   1GB
Oct 20 10:28:29 Starting compiler/proofs
Oct 20 12:09:46 Finished compiler/proofs                                    1h41m15s  24GB
Oct 20 12:09:47 Starting compiler/bootstrap/translation
Oct 20 20:15:49 Finished compiler/bootstrap/translation                     8h06m01s  64GB
Oct 20 20:15:50 Starting semantics/ffi
Oct 20 20:15:58 Finished semantics/ffi                                            7s 535MB
Oct 20 20:15:59 Starting semantics
Oct 20 20:16:01 Finished semantics                                                0s  67MB
Oct 20 20:16:02 Starting semantics/proofs
Oct 20 20:16:40 Finished semantics/proofs                                        37s   2GB
Oct 20 20:16:41 Starting semantics/alt_semantics
Oct 20 20:17:21 Finished semantics/alt_semantics                                 38s   1GB
Oct 20 20:17:22 Starting semantics/alt_semantics/proofs
Oct 20 20:28:20 Finished semantics/alt_semantics/proofs                       10m57s   5GB
Oct 20 20:28:21 Starting basis/pure
Oct 20 20:28:22 Finished basis/pure                                               0s  71MB
Oct 20 20:28:23 Starting translator
Oct 20 20:30:04 Finished translator                                            1m39s   3GB
Oct 20 20:30:05 Starting compiler/parsing
Oct 20 20:30:06 Finished compiler/parsing                                         0s  71MB
Oct 20 20:30:07 Starting characteristic
Oct 20 20:30:09 Finished characteristic                                           0s  92MB
Oct 20 20:30:10 Starting translator/monadic
Oct 20 20:30:11 Finished translator/monadic                                       0s  98MB
Oct 20 20:30:12 Starting basis
Oct 20 20:34:04 Finished basis                                                 3m50s   4GB
Oct 20 20:34:05 Starting compiler/inference
Oct 20 20:34:06 Finished compiler/inference                                       0s  83MB
Oct 20 20:34:07 Starting compiler/backend/reg_alloc
Oct 20 20:34:08 Finished compiler/backend/reg_alloc                               0s  65MB
Oct 20 20:34:09 Starting compiler/backend/gc
Oct 20 20:34:11 Finished compiler/backend/gc                                      0s 130MB
Oct 20 20:34:12 Starting compiler/backend
Oct 20 20:34:30 Finished compiler/backend                                        16s   1GB
Oct 20 20:34:31 Starting compiler/encoders/asm
Oct 20 20:34:33 Finished compiler/encoders/asm                                    0s  89MB
Oct 20 20:34:33 Starting compiler/encoders/x64
Oct 20 20:34:35 Finished compiler/encoders/x64                                    0s  94MB
Oct 20 20:34:36 Starting compiler/encoders/arm7
Oct 20 20:34:37 Finished compiler/encoders/arm7                                   0s  94MB
Oct 20 20:34:38 Starting compiler/encoders/arm8
Oct 20 20:34:40 Finished compiler/encoders/arm8                                   0s  89MB
Oct 20 20:34:41 Starting compiler/encoders/arm8_asl
Oct 20 20:36:54 Finished compiler/encoders/arm8_asl                            2m12s   1GB
Oct 20 20:36:55 Starting compiler/encoders/mips
Oct 20 20:36:57 Finished compiler/encoders/mips                                   0s  90MB
Oct 20 20:36:57 Starting compiler/encoders/riscv
Oct 20 20:36:59 Finished compiler/encoders/riscv                                  0s  90MB
Oct 20 20:37:00 Starting compiler/encoders/ag32
Oct 20 20:37:01 Finished compiler/encoders/ag32                                   0s  85MB
Oct 20 20:37:02 Starting compiler/backend/x64
Oct 20 20:37:04 Finished compiler/backend/x64                                     0s 127MB
Oct 20 20:37:05 Starting compiler/backend/arm7
Oct 20 20:37:07 Finished compiler/backend/arm7                                    0s 127MB
Oct 20 20:37:08 Starting compiler/backend/arm8
Oct 20 20:37:10 Finished compiler/backend/arm8                                    0s 127MB
Oct 20 20:37:10 Starting compiler/backend/mips
Oct 20 20:37:12 Finished compiler/backend/mips                                    0s 127MB
Oct 20 20:37:13 Starting compiler/backend/riscv
Oct 20 20:37:15 Finished compiler/backend/riscv                                   0s 127MB
Oct 20 20:37:16 Starting compiler/backend/ag32
Oct 20 20:38:36 Finished compiler/backend/ag32                                 1m19s   2GB
Oct 20 20:38:37 Starting compiler/parsing/proofs
Oct 20 20:38:39 Finished compiler/parsing/proofs                                  0s  75MB
Oct 20 20:38:40 Starting compiler/inference/proofs
Oct 20 20:38:41 Finished compiler/inference/proofs                                0s  83MB
Oct 20 20:38:42 Starting compiler/backend/semantics
Oct 20 20:40:08 Finished compiler/backend/semantics                            1m24s   2GB
Oct 20 20:40:09 Starting compiler/backend/reg_alloc/proofs
Oct 20 20:40:10 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Oct 20 20:40:11 Starting compiler/backend/proofs
Oct 20 20:41:13 Finished compiler/backend/proofs                               1m01s   3GB
Oct 20 20:41:14 Starting compiler/backend/serialiser
Oct 20 20:41:17 Finished compiler/backend/serialiser                              1s 201MB
Oct 20 20:41:18 Starting compiler/encoders/x64/proofs
Oct 20 20:51:02 Finished compiler/encoders/x64/proofs                          9m43s   5GB
Oct 20 20:51:03 Starting compiler/encoders/arm7/proofs
Oct 20 21:03:48 Finished compiler/encoders/arm7/proofs                        12m44s   9GB
Oct 20 21:03:49 Starting compiler/encoders/arm8/proofs
Oct 20 21:10:26 Finished compiler/encoders/arm8/proofs                         6m36s   4GB
Oct 20 21:10:27 Starting compiler/encoders/arm8_asl/proofs
Oct 20 21:24:37 Finished compiler/encoders/arm8_asl/proofs                    14m08s   4GB
Oct 20 21:24:38 Starting compiler/encoders/mips/proofs
Oct 20 21:34:43 Finished compiler/encoders/mips/proofs                        10m04s   6GB
Oct 20 21:34:44 Starting compiler/encoders/riscv/proofs
Oct 20 21:43:14 Finished compiler/encoders/riscv/proofs                        8m29s   4GB
Oct 20 21:43:15 Starting compiler/encoders/ag32/proofs
Oct 20 21:45:45 Finished compiler/encoders/ag32/proofs                         2m29s   2GB
Oct 20 21:45:46 Starting compiler/backend/x64/proofs
Oct 20 21:46:28 Finished compiler/backend/x64/proofs                             40s   2GB
Oct 20 21:46:29 Starting compiler/backend/arm7/proofs
Oct 20 21:47:15 Finished compiler/backend/arm7/proofs                            44s   3GB
Oct 20 21:47:16 Starting compiler/backend/arm8/proofs
Oct 20 21:47:58 Finished compiler/backend/arm8/proofs                            41s   3GB
Oct 20 21:47:59 Starting compiler/backend/arm8_asl
Oct 20 21:48:27 Finished compiler/backend/arm8_asl                               27s   2GB
Oct 20 21:48:28 Starting compiler/backend/mips/proofs
Oct 20 21:49:13 Finished compiler/backend/mips/proofs                            43s   3GB
Oct 20 21:49:14 Starting compiler/backend/riscv/proofs
Oct 20 21:50:05 Finished compiler/backend/riscv/proofs                           50s   3GB
Oct 20 21:50:06 Starting compiler/backend/ag32/proofs
Oct 20 22:05:04 Finished compiler/backend/ag32/proofs                         14m57s   4GB
Oct 20 22:05:05 Starting candle/set-theory
Oct 20 22:05:51 Finished candle/set-theory                                       44s   1GB
Oct 20 22:05:52 Starting candle/syntax-lib
Oct 20 22:05:53 Finished candle/syntax-lib                                        0s  72MB
Oct 20 22:05:54 Starting candle/standard/syntax
Oct 20 22:06:10 Finished candle/standard/syntax                                  14s   1GB
Oct 20 22:06:11 Starting candle/standard/semantics
Oct 20 22:08:36 Finished candle/standard/semantics                             2m24s   2GB
Oct 20 22:08:37 Starting candle/standard/monadic
Oct 20 22:08:39 Finished candle/standard/monadic                                  0s 100MB
Oct 20 22:08:40 Starting candle/standard/ml_kernel
Oct 20 22:10:27 Finished candle/standard/ml_kernel                             1m46s   5GB
Oct 20 22:10:28 Starting candle/overloading/syntax
Oct 20 22:13:57 Finished candle/overloading/syntax                             3m27s   3GB
Oct 20 22:13:58 Starting candle/overloading/semantics
Oct 20 22:25:22 Finished candle/overloading/semantics                         11m22s   4GB
Oct 20 22:25:23 Starting candle/overloading/monadic
Oct 20 22:28:00 Finished candle/overloading/monadic                            2m36s   3GB
Oct 20 22:28:01 Starting candle/overloading/ml_kernel
Oct 20 22:35:31 Finished candle/overloading/ml_kernel                          7m28s   6GB
Oct 20 22:35:32 Starting candle/overloading/ml_checker
Oct 20 22:38:03 Finished candle/overloading/ml_checker                         2m29s   7GB
Oct 20 22:38:04 Starting candle/prover
Oct 20 22:47:56 Finished candle/prover                                         9m50s   5GB
Oct 20 22:47:57 Starting pancake
Oct 20 22:48:57 Finished pancake                                                 59s   1GB
Oct 20 22:48:58 Starting pancake/ffi
Oct 20 22:48:59 Finished pancake/ffi                                              0s  20MB
Oct 20 22:49:00 Starting pancake/semantics
Oct 20 22:51:25 Finished pancake/semantics                                     2m24s   2GB
Oct 20 22:51:26 Starting pancake/parser
Oct 20 22:51:54 Finished pancake/parser                                          26s   2GB
Oct 20 22:51:55 Starting pancake/proofs
Oct 20 23:21:34 Finished pancake/proofs                                       29m38s   8GB
Oct 20 23:21:35 Starting characteristic/examples
Oct 20 23:23:10 Finished characteristic/examples                               1m33s   6GB
Oct 20 23:23:11 Starting tutorial/solutions
Oct 20 23:38:40 Finished tutorial/solutions                                   15m27s  13GB
Oct 20 23:38:40 Starting translator/monadic/examples
Oct 20 23:42:20 Finished translator/monadic/examples                           3m39s   5GB
Oct 20 23:42:21 Starting examples
Oct 20 23:56:48 Finished examples                                             14m25s   7GB
Oct 20 23:56:49 Starting examples/compilation/x64
Oct 21 01:53:32 Finished examples/compilation/x64                           1h56m42s  22GB
Oct 21 01:53:33 Starting examples/compilation/x64/proofs
Oct 21 01:57:18 Finished examples/compilation/x64/proofs                       3m44s   5GB
Oct 21 01:57:19 Starting examples/compilation/ag32
Oct 21 02:26:58 Finished examples/compilation/ag32                            29m37s  10GB
Oct 21 02:26:59 Starting examples/compilation/ag32/proofs
Oct 21 02:28:29 Finished examples/compilation/ag32/proofs                      1m28s   6GB
Oct 21 02:28:30 Starting examples/compilation/to_word
Oct 21 02:32:18 Finished examples/compilation/to_word                          3m47s  11GB
Oct 21 02:32:19 Starting examples/lpr_checker
Oct 21 02:33:33 Finished examples/lpr_checker                                  1m12s   2GB
Oct 21 02:33:34 Starting examples/lpr_checker/array
Oct 21 03:08:18 Finished examples/lpr_checker/array                           34m42s   8GB
Oct 21 03:08:19 Starting examples/lpr_checker/array/compilation
Oct 21 03:41:48 Finished examples/lpr_checker/array/compilation               33m28s  59GB
Oct 21 03:41:49 Starting examples/lpr_checker/array/compilation/proofs
Oct 21 03:43:45 Finished examples/lpr_checker/array/compilation/proofs         1m55s   9GB
Oct 21 03:43:46 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 21 03:55:33 Finished examples/lpr_checker/array/compilation/proofsARM8    11m46s  37GB
Oct 21 03:55:34 Starting examples/opentheory
Oct 21 04:06:30 Finished examples/opentheory                                  10m54s   7GB
Oct 21 04:06:31 Starting examples/opentheory
Oct 21 04:06:32 Finished examples/opentheory                                      0s 123MB
Oct 21 04:06:33 Starting examples/opentheory/compilation
Oct 21 04:08:25 FAILED: examples/opentheory/compilation
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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/examples/cost[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/examples/opentheory[0m
Scanned 93 directories
Starting work on costPropsTheory
Starting work on README.md
README.md                          examples/opentheory/compilation  (0s)     OK
costPropsTheory                                      examples/cost (98s)FAIL<1>
 Saved theorem _______ "closed_ptrs_cons"
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "live_ptr_list_def"
 Saved induction _____ "live_ptr_list_ind"
 Saved definition ____ "live_ptr_def"
 Saved theorem _______ "live_ptr_cons"
 error in quse /scratch/cakeml/regression/cakeml-2227/examples/cost/costPropsScript.sml : DUP "size_of_refs_subspt"
 error in load /scratch/cakeml/regression/cakeml-2227/examples/cost/costPropsScript : DUP "size_of_refs_subspt"
 Uncaught exception: DUP "size_of_refs_subspt"