Job 2598

CakeML:3b5f1f0ee87e88975f8eaabdfe24505a9fbc6adf
  Merge pull request #1051 from CakeML/pancake_itree2 [Sep 09 18:44:45]
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 10 12:45:58 Claimed job
Sep 10 12:46:05 Building HOL
Sep 10 13:00:30 Starting developers
Sep 10 13:00:36 Finished developers                                               5s 152MB
Sep 10 13:00:36 Starting developers/bin
Sep 10 13:00:48 Finished developers/bin                                          12s   1GB
Sep 10 13:00:48 Starting compiler/proofs
Sep 10 15:11:38 Finished compiler/proofs                                    2h10m48s  17GB
Sep 10 15:11:38 Starting compiler/bootstrap/translation
Sep 11 00:51:30 Finished compiler/bootstrap/translation                     9h39m52s  45GB
Sep 11 00:51:30 Starting semantics/ffi
Sep 11 00:51:36 Finished semantics/ffi                                            5s 410MB
Sep 11 00:51:36 Starting semantics
Sep 11 00:51:37 Finished semantics                                                1s  19MB
Sep 11 00:51:37 Starting semantics/proofs
Sep 11 00:52:03 Finished semantics/proofs                                        25s 433MB
Sep 11 00:52:03 Starting semantics/alt_semantics
Sep 11 00:52:29 Finished semantics/alt_semantics                                 25s 578MB
Sep 11 00:52:29 Starting semantics/alt_semantics/proofs
Sep 11 01:04:02 Finished semantics/alt_semantics/proofs                       11m32s   1GB
Sep 11 01:04:02 Starting basis/pure
Sep 11 01:04:03 Finished basis/pure                                               1s  20MB
Sep 11 01:04:03 Starting translator
Sep 11 01:05:48 Finished translator                                            1m44s   2GB
Sep 11 01:05:48 Starting compiler/parsing
Sep 11 01:05:50 Finished compiler/parsing                                         1s  21MB
Sep 11 01:05:50 Starting characteristic
Sep 11 01:05:52 Finished characteristic                                           1s  22MB
Sep 11 01:05:52 Starting translator/monadic
Sep 11 01:05:54 Finished translator/monadic                                       1s  21MB
Sep 11 01:05:54 Starting basis
Sep 11 01:08:30 Finished basis                                                 2m36s   2GB
Sep 11 01:08:30 Starting compiler/inference
Sep 11 01:08:32 Finished compiler/inference                                       1s  19MB
Sep 11 01:08:32 Starting compiler/backend/reg_alloc
Sep 11 01:08:34 Finished compiler/backend/reg_alloc                               1s  22MB
Sep 11 01:08:34 Starting compiler/backend/gc
Sep 11 01:08:37 Finished compiler/backend/gc                                      2s  27MB
Sep 11 01:08:37 Starting compiler/backend
Sep 11 01:08:42 Finished compiler/backend                                         5s 295MB
Sep 11 01:08:42 Starting compiler/encoders/asm
Sep 11 01:08:44 Finished compiler/encoders/asm                                    1s  24MB
Sep 11 01:08:44 Starting compiler/encoders/x64
Sep 11 01:08:46 Finished compiler/encoders/x64                                    1s  21MB
Sep 11 01:08:46 Starting compiler/encoders/arm7
Sep 11 01:08:48 Finished compiler/encoders/arm7                                   1s  30MB
Sep 11 01:08:48 Starting compiler/encoders/arm8
Sep 11 01:08:50 Finished compiler/encoders/arm8                                   1s  20MB
Sep 11 01:08:50 Starting compiler/encoders/arm8_asl
Sep 11 03:38:12 Finished compiler/encoders/arm8_asl                         2h29m21s  34GB
Sep 11 03:38:12 Starting compiler/encoders/mips
Sep 11 03:38:14 Finished compiler/encoders/mips                                   1s  24MB
Sep 11 03:38:14 Starting compiler/encoders/riscv
Sep 11 03:38:16 Finished compiler/encoders/riscv                                  1s  21MB
Sep 11 03:38:16 Starting compiler/encoders/ag32
Sep 11 03:38:18 Finished compiler/encoders/ag32                                   1s  23MB
Sep 11 03:38:18 Starting compiler/backend/x64
Sep 11 03:38:21 Finished compiler/backend/x64                                     2s  26MB
Sep 11 03:38:21 Starting compiler/backend/arm7
Sep 11 03:38:23 Finished compiler/backend/arm7                                    2s  26MB
Sep 11 03:38:23 Starting compiler/backend/arm8
Sep 11 03:38:25 Finished compiler/backend/arm8                                    2s  22MB
Sep 11 03:38:25 Starting compiler/backend/mips
Sep 11 03:38:28 Finished compiler/backend/mips                                    2s  24MB
Sep 11 03:38:28 Starting compiler/backend/riscv
Sep 11 03:38:30 Finished compiler/backend/riscv                                   2s  32MB
Sep 11 03:38:30 Starting compiler/backend/ag32
Sep 11 03:39:59 Finished compiler/backend/ag32                                 1m28s   1GB
Sep 11 03:39:59 Starting compiler/parsing/proofs
Sep 11 03:40:01 Finished compiler/parsing/proofs                                  1s  21MB
Sep 11 03:40:01 Starting compiler/inference/proofs
Sep 11 03:40:03 Finished compiler/inference/proofs                                1s  22MB
Sep 11 03:40:03 Starting compiler/backend/semantics
Sep 11 03:43:33 Finished compiler/backend/semantics                            3m29s   1GB
Sep 11 03:43:33 Starting compiler/backend/reg_alloc/proofs
Sep 11 03:43:35 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Sep 11 03:43:35 Starting compiler/backend/proofs
Sep 11 03:44:30 Finished compiler/backend/proofs                                 55s   2GB
Sep 11 03:44:30 Starting compiler/backend/serialiser
Sep 11 03:44:33 Finished compiler/backend/serialiser                              2s  30MB
Sep 11 03:44:33 Starting compiler/encoders/x64/proofs
Sep 11 03:55:12 Finished compiler/encoders/x64/proofs                         10m39s   5GB
Sep 11 03:55:12 Starting compiler/encoders/arm7/proofs
Sep 11 04:09:24 Finished compiler/encoders/arm7/proofs                        14m11s   3GB
Sep 11 04:09:24 Starting compiler/encoders/arm8/proofs
Sep 11 04:16:51 Finished compiler/encoders/arm8/proofs                         7m26s   1GB
Sep 11 04:16:51 Starting compiler/encoders/arm8_asl/proofs
Sep 11 05:13:27 Finished compiler/encoders/arm8_asl/proofs                    56m36s   6GB
Sep 11 05:13:27 Starting compiler/encoders/mips/proofs
Sep 11 05:24:14 Finished compiler/encoders/mips/proofs                        10m46s   3GB
Sep 11 05:24:14 Starting compiler/encoders/riscv/proofs
Sep 11 05:33:09 Finished compiler/encoders/riscv/proofs                        8m54s   2GB
Sep 11 05:33:09 Starting compiler/encoders/ag32/proofs
Sep 11 05:36:27 Finished compiler/encoders/ag32/proofs                         3m18s   1GB
Sep 11 05:36:27 Starting compiler/backend/x64/proofs
Sep 11 05:36:58 Finished compiler/backend/x64/proofs                             30s   1GB
Sep 11 05:36:59 Starting compiler/backend/arm7/proofs
Sep 11 05:37:32 Finished compiler/backend/arm7/proofs                            33s   1GB
Sep 11 05:37:32 Starting compiler/backend/arm8/proofs
Sep 11 05:38:07 Finished compiler/backend/arm8/proofs                            34s   2GB
Sep 11 05:38:07 Starting compiler/backend/arm8_asl
Sep 11 05:38:31 Finished compiler/backend/arm8_asl                               24s   1GB
Sep 11 05:38:32 Starting compiler/backend/mips/proofs
Sep 11 05:39:10 Finished compiler/backend/mips/proofs                            38s   1GB
Sep 11 05:39:10 Starting compiler/backend/riscv/proofs
Sep 11 05:39:48 Finished compiler/backend/riscv/proofs                           37s   2GB
Sep 11 05:39:48 Starting compiler/backend/ag32/proofs
Sep 11 05:54:35 Finished compiler/backend/ag32/proofs                         14m47s   3GB
Sep 11 05:54:35 Starting compiler/backend/cv_compute
Sep 11 05:55:56 Finished compiler/backend/cv_compute                           1m20s   2GB
Sep 11 05:55:56 Starting cv_translator
Sep 11 06:17:02 Finished cv_translator                                        21m06s   7GB
Sep 11 06:17:02 Starting candle/set-theory
Sep 11 06:17:46 Finished candle/set-theory                                       43s   1GB
Sep 11 06:17:46 Starting candle/syntax-lib
Sep 11 06:17:47 Finished candle/syntax-lib                                        1s  22MB
Sep 11 06:17:47 Starting candle/standard/syntax
Sep 11 06:18:01 Finished candle/standard/syntax                                  13s 868MB
Sep 11 06:18:01 Starting candle/standard/semantics
Sep 11 06:20:14 Finished candle/standard/semantics                             2m13s   1GB
Sep 11 06:20:14 Starting candle/standard/monadic
Sep 11 06:20:16 Finished candle/standard/monadic                                  1s  26MB
Sep 11 06:20:16 Starting candle/standard/ml_kernel
Sep 11 06:22:04 Finished candle/standard/ml_kernel                             1m47s   3GB
Sep 11 06:22:04 Starting candle/overloading/syntax
Sep 11 06:25:40 Finished candle/overloading/syntax                             3m36s   1GB
Sep 11 06:25:40 Starting candle/overloading/semantics
Sep 11 06:38:24 Finished candle/overloading/semantics                         12m43s   2GB
Sep 11 06:38:24 Starting candle/overloading/monadic
Sep 11 06:41:11 Finished candle/overloading/monadic                            2m47s   2GB
Sep 11 06:41:11 Starting candle/overloading/ml_kernel
Sep 11 06:49:30 Finished candle/overloading/ml_kernel                          8m18s   4GB
Sep 11 06:49:30 Starting candle/overloading/ml_checker
Sep 11 06:52:14 Finished candle/overloading/ml_checker                         2m44s   3GB
Sep 11 06:52:14 Starting candle/prover
Sep 11 07:02:35 Finished candle/prover                                        10m20s   4GB
Sep 11 07:02:35 Starting pancake
Sep 11 07:02:59 Finished pancake                                                 24s 768MB
Sep 11 07:02:59 Starting pancake/ffi
Sep 11 07:03:00 Finished pancake/ffi                                              0s  13MB
Sep 11 07:03:00 Starting pancake/semantics
Sep 11 07:05:24 Finished pancake/semantics                                     2m24s   1GB
Sep 11 07:05:24 Starting pancake/parser
Sep 11 07:05:50 Finished pancake/parser                                          25s 416MB
Sep 11 07:05:50 Starting pancake/proofs
Sep 11 07:24:25 Finished pancake/proofs                                       18m35s   3GB
Sep 11 07:24:25 Starting characteristic/examples
Sep 11 07:25:57 Finished characteristic/examples                               1m31s   2GB
Sep 11 07:25:57 Starting tutorial/solutions
Sep 11 07:28:45 Finished tutorial/solutions                                    2m47s   3GB
Sep 11 07:28:45 Starting translator/monadic/examples
Sep 11 07:32:37 Finished translator/monadic/examples                           3m52s   2GB
Sep 11 07:32:37 Starting examples
Sep 11 07:33:49 FAILED: 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)/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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/num/theories/cv_compute/automation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[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)/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 34 directories
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
README.md                                                                                         examples  (0s)     OK
Starting work on catProgTheory
source_valuesTheory                                                                     examples/bootstrap  (2s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                                                                     examples/bootstrap  (1s)     OK
Starting work on parsingTheory
regexp_parserTheory                                                      examples/formal-languages/regular (13s)     OK
Starting work on printingTheory
printingTheory                                                                          examples/bootstrap  (5s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]                                           (13.527s) 
Starting work on lcsTheory
parsingTheory                                                                           examples/bootstrap (22s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                                                          (31.513s) 
Starting work on divTheory
lcsTheory                                                                                         examples (16s)     OK
Starting work on diffTheory
catProgTheory                                                                                     examples (64s)     OK
Starting work on doubleArgProgTheory
diffTheory                                                                                        examples (29s)FAIL<1>
 P l.
   P []  (h l. (sl. IS_SUFFIX l sl  P sl)  P (h::l)) 
   sl. IS_SUFFIX l sl  P sl
 
 failed.
 First unsolved sub-goal is
 
 P (h'::t)
 
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
quicksortProgTheory                                                                               examples (67s)MKILLED
divTheory                                                                                         examples (39s)MKILLED
doubleArgProgTheory                                                                               examples  (0s)MKILLED