Job 2612

CakeML:5f5ca9329795f6f38d4c456c3a3a1b979c5c311b
  Use new Quote syntax [Sep 21 10:45:00]
#1056 (new-quotes)
Merging into:49f0d44be26ff907ef52240f3818a4c3caa10598
  Merge pull request #1055 from CakeML/pan_news [Sep 18 13:05:16]
HOL:7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361
  Fix bug in reduceLib.NOT_CONV [Sep 09 04:53:02]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Sep 21 10:53:43 Claimed job
Sep 21 10:53:45 Reusing HOL
Sep 21 10:54:30 Starting developers
Sep 21 10:54:36 Finished developers                                               5s 145MB
Sep 21 10:54:36 Starting developers/bin
Sep 21 10:54:42 Finished developers/bin                                           6s   1GB
Sep 21 10:54:42 Starting compiler/proofs
Sep 21 12:52:38 Finished compiler/proofs                                    1h57m55s  15GB
Sep 21 12:52:38 Starting compiler/bootstrap/translation
Sep 21 21:50:30 Finished compiler/bootstrap/translation                     8h57m51s  43GB
Sep 21 21:50:30 Starting semantics/ffi
Sep 21 21:50:36 Finished semantics/ffi                                            5s 410MB
Sep 21 21:50:36 Starting semantics
Sep 21 21:50:37 Finished semantics                                                1s  16MB
Sep 21 21:50:37 Starting semantics/proofs
Sep 21 21:51:03 Finished semantics/proofs                                        26s 416MB
Sep 21 21:51:03 Starting semantics/alt_semantics
Sep 21 21:51:29 Finished semantics/alt_semantics                                 25s 578MB
Sep 21 21:51:30 Starting semantics/alt_semantics/proofs
Sep 21 22:03:12 Finished semantics/alt_semantics/proofs                       11m42s   1GB
Sep 21 22:03:12 Starting basis/pure
Sep 21 22:03:14 Finished basis/pure                                               1s  19MB
Sep 21 22:03:14 Starting translator
Sep 21 22:04:56 Finished translator                                            1m42s   2GB
Sep 21 22:04:56 Starting compiler/parsing
Sep 21 22:04:58 Finished compiler/parsing                                         1s  18MB
Sep 21 22:04:58 Starting characteristic
Sep 21 22:05:00 Finished characteristic                                           1s  21MB
Sep 21 22:05:00 Starting translator/monadic
Sep 21 22:05:02 Finished translator/monadic                                       1s  22MB
Sep 21 22:05:02 Starting basis
Sep 21 22:07:38 Finished basis                                                 2m35s   3GB
Sep 21 22:07:38 Starting compiler/inference
Sep 21 22:07:40 Finished compiler/inference                                       1s  21MB
Sep 21 22:07:40 Starting compiler/backend/reg_alloc
Sep 21 22:07:41 Finished compiler/backend/reg_alloc                               1s  18MB
Sep 21 22:07:41 Starting compiler/backend/gc
Sep 21 22:07:44 Finished compiler/backend/gc                                      2s  28MB
Sep 21 22:07:44 Starting compiler/backend
Sep 21 22:07:50 Finished compiler/backend                                         5s 295MB
Sep 21 22:07:50 Starting compiler/encoders/asm
Sep 21 22:07:52 Finished compiler/encoders/asm                                    1s  22MB
Sep 21 22:07:52 Starting compiler/encoders/x64
Sep 21 22:07:54 Finished compiler/encoders/x64                                    1s  23MB
Sep 21 22:07:54 Starting compiler/encoders/arm7
Sep 21 22:07:56 Finished compiler/encoders/arm7                                   1s  23MB
Sep 21 22:07:56 Starting compiler/encoders/arm8
Sep 21 22:07:58 Finished compiler/encoders/arm8                                   1s  19MB
Sep 21 22:07:58 Starting compiler/encoders/arm8_asl
Sep 21 22:11:03 Finished compiler/encoders/arm8_asl                            3m05s   1GB
Sep 21 22:11:03 Starting compiler/encoders/mips
Sep 21 22:11:05 Finished compiler/encoders/mips                                   1s  19MB
Sep 21 22:11:05 Starting compiler/encoders/riscv
Sep 21 22:11:07 Finished compiler/encoders/riscv                                  1s  27MB
Sep 21 22:11:07 Starting compiler/encoders/ag32
Sep 21 22:11:09 Finished compiler/encoders/ag32                                   1s  25MB
Sep 21 22:11:09 Starting compiler/backend/x64
Sep 21 22:11:11 Finished compiler/backend/x64                                     2s  33MB
Sep 21 22:11:12 Starting compiler/backend/arm7
Sep 21 22:11:14 Finished compiler/backend/arm7                                    2s  28MB
Sep 21 22:11:14 Starting compiler/backend/arm8
Sep 21 22:11:16 Finished compiler/backend/arm8                                    2s  25MB
Sep 21 22:11:16 Starting compiler/backend/mips
Sep 21 22:11:19 Finished compiler/backend/mips                                    2s  23MB
Sep 21 22:11:19 Starting compiler/backend/riscv
Sep 21 22:11:21 Finished compiler/backend/riscv                                   2s  27MB
Sep 21 22:11:21 Starting compiler/backend/ag32
Sep 21 22:12:50 Finished compiler/backend/ag32                                 1m28s   1GB
Sep 21 22:12:50 Starting compiler/parsing/proofs
Sep 21 22:12:52 Finished compiler/parsing/proofs                                  1s  20MB
Sep 21 22:12:52 Starting compiler/inference/proofs
Sep 21 22:12:54 Finished compiler/inference/proofs                                1s  20MB
Sep 21 22:12:54 Starting compiler/backend/semantics
Sep 21 22:16:17 Finished compiler/backend/semantics                            3m22s   2GB
Sep 21 22:16:17 Starting compiler/backend/reg_alloc/proofs
Sep 21 22:16:19 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Sep 21 22:16:19 Starting compiler/backend/proofs
Sep 21 22:17:12 Finished compiler/backend/proofs                                 53s   2GB
Sep 21 22:17:13 Starting compiler/backend/serialiser
Sep 21 22:17:15 Finished compiler/backend/serialiser                              2s  27MB
Sep 21 22:17:15 Starting compiler/encoders/x64/proofs
Sep 21 22:27:56 Finished compiler/encoders/x64/proofs                         10m40s   7GB
Sep 21 22:27:56 Starting compiler/encoders/arm7/proofs
Sep 21 22:42:05 Finished compiler/encoders/arm7/proofs                        14m09s   3GB
Sep 21 22:42:06 Starting compiler/encoders/arm8/proofs
Sep 21 22:49:26 Finished compiler/encoders/arm8/proofs                         7m20s   1GB
Sep 21 22:49:26 Starting compiler/encoders/arm8_asl/proofs
Sep 21 23:06:37 Finished compiler/encoders/arm8_asl/proofs                    17m10s   2GB
Sep 21 23:06:37 Starting compiler/encoders/mips/proofs
Sep 21 23:17:14 Finished compiler/encoders/mips/proofs                        10m37s   3GB
Sep 21 23:17:14 Starting compiler/encoders/riscv/proofs
Sep 21 23:26:22 Finished compiler/encoders/riscv/proofs                        9m08s   2GB
Sep 21 23:26:22 Starting compiler/encoders/ag32/proofs
Sep 21 23:29:39 Finished compiler/encoders/ag32/proofs                         3m16s   1GB
Sep 21 23:29:39 Starting compiler/backend/x64/proofs
Sep 21 23:30:13 Finished compiler/backend/x64/proofs                             33s   2GB
Sep 21 23:30:13 Starting compiler/backend/arm7/proofs
Sep 21 23:30:47 Finished compiler/backend/arm7/proofs                            33s   1GB
Sep 21 23:30:47 Starting compiler/backend/arm8/proofs
Sep 21 23:31:20 Finished compiler/backend/arm8/proofs                            32s   1GB
Sep 21 23:31:20 Starting compiler/backend/arm8_asl
Sep 21 23:31:45 Finished compiler/backend/arm8_asl                               24s   2GB
Sep 21 23:31:45 Starting compiler/backend/mips/proofs
Sep 21 23:32:19 Finished compiler/backend/mips/proofs                            33s   2GB
Sep 21 23:32:19 Starting compiler/backend/riscv/proofs
Sep 21 23:32:56 Finished compiler/backend/riscv/proofs                           37s   2GB
Sep 21 23:32:56 Starting compiler/backend/ag32/proofs
Sep 21 23:47:49 Finished compiler/backend/ag32/proofs                         14m52s   3GB
Sep 21 23:47:49 Starting compiler/backend/cv_compute
Sep 21 23:49:07 Finished compiler/backend/cv_compute                           1m18s   2GB
Sep 21 23:49:08 Starting cv_translator
Sep 22 00:10:10 Finished cv_translator                                        21m02s   6GB
Sep 22 00:10:10 Starting candle/set-theory
Sep 22 00:10:53 Finished candle/set-theory                                       42s   1GB
Sep 22 00:10:53 Starting candle/syntax-lib
Sep 22 00:10:55 Finished candle/syntax-lib                                        1s  22MB
Sep 22 00:10:55 Starting candle/standard/syntax
Sep 22 00:11:08 Finished candle/standard/syntax                                  13s 868MB
Sep 22 00:11:08 Starting candle/standard/semantics
Sep 22 00:13:21 Finished candle/standard/semantics                             2m12s   1GB
Sep 22 00:13:22 Starting candle/standard/monadic
Sep 22 00:13:23 Finished candle/standard/monadic                                  1s  23MB
Sep 22 00:13:24 Starting candle/standard/ml_kernel
Sep 22 00:15:06 Finished candle/standard/ml_kernel                             1m42s   2GB
Sep 22 00:15:06 Starting candle/overloading/syntax
Sep 22 00:18:39 Finished candle/overloading/syntax                             3m33s   1GB
Sep 22 00:18:39 Starting candle/overloading/semantics
Sep 22 00:31:22 Finished candle/overloading/semantics                         12m42s   2GB
Sep 22 00:31:22 Starting candle/overloading/monadic
Sep 22 00:34:07 Finished candle/overloading/monadic                            2m44s   2GB
Sep 22 00:34:07 Starting candle/overloading/ml_kernel
Sep 22 00:42:29 Finished candle/overloading/ml_kernel                          8m22s   4GB
Sep 22 00:42:29 Starting candle/overloading/ml_checker
Sep 22 00:45:15 Finished candle/overloading/ml_checker                         2m45s   2GB
Sep 22 00:45:15 Starting candle/prover
Sep 22 00:55:54 Finished candle/prover                                        10m38s   4GB
Sep 22 00:55:54 Starting pancake
Sep 22 00:56:19 Finished pancake                                                 25s 860MB
Sep 22 00:56:19 Starting pancake/ffi
Sep 22 00:56:20 Finished pancake/ffi                                              0s  13MB
Sep 22 00:56:20 Starting pancake/semantics
Sep 22 00:58:45 Finished pancake/semantics                                     2m24s   1GB
Sep 22 00:58:45 Starting pancake/parser
Sep 22 00:59:09 Finished pancake/parser                                          24s 501MB
Sep 22 00:59:09 Starting pancake/proofs
Sep 22 01:17:46 Finished pancake/proofs                                       18m35s   3GB
Sep 22 01:17:46 Starting compiler/dafny
Sep 22 01:20:12 Finished compiler/dafny                                        2m26s   8GB
Sep 22 01:20:12 Starting compiler/dafny/translation
Sep 22 01:50:18 Finished compiler/dafny/translation                           30m06s  12GB
Sep 22 01:50:18 Starting compiler/dafny/compilation
Sep 22 01:53:46 Finished compiler/dafny/compilation                            3m27s  10GB
Sep 22 01:53:46 Starting compiler/dafny/semantics
Sep 22 01:54:24 Finished compiler/dafny/semantics                                37s 975MB
Sep 22 01:54:24 Starting characteristic/examples
Sep 22 01:55:46 FAILED: characteristic/examples
Scanning [1m$(HOLDIR)/src/bag[0m
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/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
Scanned 29 directories
Starting work on README.md
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
README.md                                                                                                   (0s)     OK
cf_tutorialTheory                                                                                          (51s)     OK
cf_examplesTheory                                                                                          (78s)FAIL<1>
 
 rv sv s.
   STRING_TYPE s sv 
   app p strcat_foo_v [rv] (rv ~~> sv)
     (POSTv uv. SEP_EXISTS sv'.
        &(UNIT_TYPE () uv  STRING_TYPE (s ^ implode "foo") sv') * rv ~~> sv')
 
 failed.
 Failed to prove theorem strcat_foo_spec.
 Uncaught exception: HOL_ERR {message = "create_subst (THEN1 on line 390)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}