Job 2391

CakeML:4c5dc9f146a7a89de7e68e263a5f8952fb0965c5
  Refer to Discord instead of our (defunct) Slack channel [May 21 06:39:37]
HOL:fe0e72dc46aa5ca62a9ec826c69bd7dfe8dc301d
  Define simultaneous substitution for lambda/basics/cterm [May 16 07:08:33]
Machine:pavlova

May 22 19:33:11 Claimed job
May 22 19:33:20 Building HOL
May 22 19:48:01 Starting developers
May 22 19:48:05 Finished developers                                               2s 211MB
May 22 19:48:06 Starting developers/bin
May 22 19:48:24 Finished developers/bin                                          17s   1GB
May 22 19:48:25 Starting compiler/proofs
May 22 21:38:00 Finished compiler/proofs                                    1h49m34s  27GB
May 22 21:38:01 Starting compiler/bootstrap/translation
May 23 05:44:01 Finished compiler/bootstrap/translation                     8h05m59s  74GB
May 23 05:44:02 Starting semantics/ffi
May 23 05:44:11 Finished semantics/ffi                                            7s 679MB
May 23 05:44:12 Starting semantics
May 23 05:44:13 Finished semantics                                                0s  68MB
May 23 05:44:14 Starting semantics/proofs
May 23 05:44:49 Finished semantics/proofs                                        33s   2GB
May 23 05:44:50 Starting semantics/alt_semantics
May 23 05:45:29 Finished semantics/alt_semantics                                 38s   1GB
May 23 05:45:30 Starting semantics/alt_semantics/proofs
May 23 05:56:26 Finished semantics/alt_semantics/proofs                       10m55s   3GB
May 23 05:56:27 Starting basis/pure
May 23 05:56:28 Finished basis/pure                                               0s  71MB
May 23 05:56:29 Starting translator
May 23 05:58:11 Finished translator                                            1m40s   3GB
May 23 05:58:12 Starting compiler/parsing
May 23 05:58:13 Finished compiler/parsing                                         0s  72MB
May 23 05:58:14 Starting characteristic
May 23 05:58:16 Finished characteristic                                           0s  95MB
May 23 05:58:17 Starting translator/monadic
May 23 05:58:18 Finished translator/monadic                                       0s  92MB
May 23 05:58:19 Starting basis
May 23 06:01:48 Finished basis                                                 3m28s   5GB
May 23 06:01:49 Starting compiler/inference
May 23 06:01:51 Finished compiler/inference                                       0s  87MB
May 23 06:01:52 Starting compiler/backend/reg_alloc
May 23 06:01:53 Finished compiler/backend/reg_alloc                               0s  67MB
May 23 06:01:54 Starting compiler/backend/gc
May 23 06:01:56 Finished compiler/backend/gc                                      0s 140MB
May 23 06:01:57 Starting compiler/backend
May 23 06:02:14 Finished compiler/backend                                        16s   1GB
May 23 06:02:15 Starting compiler/encoders/asm
May 23 06:02:17 Finished compiler/encoders/asm                                    0s  98MB
May 23 06:02:18 Starting compiler/encoders/x64
May 23 06:02:19 Finished compiler/encoders/x64                                    0s  98MB
May 23 06:02:20 Starting compiler/encoders/arm7
May 23 06:02:22 Finished compiler/encoders/arm7                                   0s 105MB
May 23 06:02:23 Starting compiler/encoders/arm8
May 23 06:02:24 Finished compiler/encoders/arm8                                   0s  98MB
May 23 06:02:25 Starting compiler/encoders/arm8_asl
May 23 08:13:35 Finished compiler/encoders/arm8_asl                         2h11m09s  43GB
May 23 08:13:36 Starting compiler/encoders/mips
May 23 08:13:38 Finished compiler/encoders/mips                                   0s  99MB
May 23 08:13:39 Starting compiler/encoders/riscv
May 23 08:13:40 Finished compiler/encoders/riscv                                  0s  99MB
May 23 08:13:41 Starting compiler/encoders/ag32
May 23 08:13:43 Finished compiler/encoders/ag32                                   0s  97MB
May 23 08:13:44 Starting compiler/backend/x64
May 23 08:13:45 Finished compiler/backend/x64                                     0s 137MB
May 23 08:13:46 Starting compiler/backend/arm7
May 23 08:13:48 Finished compiler/backend/arm7                                    0s 137MB
May 23 08:13:49 Starting compiler/backend/arm8
May 23 08:13:51 Finished compiler/backend/arm8                                    0s 138MB
May 23 08:13:52 Starting compiler/backend/mips
May 23 08:13:54 Finished compiler/backend/mips                                    0s 137MB
May 23 08:13:55 Starting compiler/backend/riscv
May 23 08:13:56 Finished compiler/backend/riscv                                   0s 137MB
May 23 08:13:57 Starting compiler/backend/ag32
May 23 08:15:17 Finished compiler/backend/ag32                                 1m18s   3GB
May 23 08:15:18 Starting compiler/parsing/proofs
May 23 08:15:19 Finished compiler/parsing/proofs                                  0s  75MB
May 23 08:15:20 Starting compiler/inference/proofs
May 23 08:15:22 Finished compiler/inference/proofs                                0s  92MB
May 23 08:15:23 Starting compiler/backend/semantics
May 23 08:19:01 Finished compiler/backend/semantics                            3m37s   4GB
May 23 08:19:02 Starting compiler/backend/reg_alloc/proofs
May 23 08:19:03 Finished compiler/backend/reg_alloc/proofs                        0s  98MB
May 23 08:19:04 Starting compiler/backend/proofs
May 23 08:20:08 Finished compiler/backend/proofs                               1m02s   3GB
May 23 08:20:09 Starting compiler/backend/serialiser
May 23 08:20:11 Finished compiler/backend/serialiser                              1s 194MB
May 23 08:20:12 Starting compiler/encoders/x64/proofs
May 23 08:29:36 Finished compiler/encoders/x64/proofs                          9m22s   5GB
May 23 08:29:37 Starting compiler/encoders/arm7/proofs
May 23 08:42:25 Finished compiler/encoders/arm7/proofs                        12m47s  10GB
May 23 08:42:26 Starting compiler/encoders/arm8/proofs
May 23 08:49:06 Finished compiler/encoders/arm8/proofs                         6m38s   6GB
May 23 08:49:07 Starting compiler/encoders/arm8_asl/proofs
May 23 09:36:47 Finished compiler/encoders/arm8_asl/proofs                    47m39s  12GB
May 23 09:36:48 Starting compiler/encoders/mips/proofs
May 23 09:46:51 Finished compiler/encoders/mips/proofs                        10m02s  10GB
May 23 09:46:52 Starting compiler/encoders/riscv/proofs
May 23 09:55:06 Finished compiler/encoders/riscv/proofs                        8m13s   3GB
May 23 09:55:07 Starting compiler/encoders/ag32/proofs
May 23 09:57:29 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
May 23 09:57:30 Starting compiler/backend/x64/proofs
May 23 09:58:13 Finished compiler/backend/x64/proofs                             41s   3GB
May 23 09:58:14 Starting compiler/backend/arm7/proofs
May 23 09:59:00 Finished compiler/backend/arm7/proofs                            45s   2GB
May 23 09:59:01 Starting compiler/backend/arm8/proofs
May 23 09:59:40 Finished compiler/backend/arm8/proofs                            38s   2GB
May 23 09:59:41 Starting compiler/backend/arm8_asl
May 23 10:00:08 Finished compiler/backend/arm8_asl                               26s   1GB
May 23 10:00:09 Starting compiler/backend/mips/proofs
May 23 10:00:55 Finished compiler/backend/mips/proofs                            44s   2GB
May 23 10:00:55 Starting compiler/backend/riscv/proofs
May 23 10:01:44 Finished compiler/backend/riscv/proofs                           47s   4GB
May 23 10:01:45 Starting compiler/backend/ag32/proofs
May 23 10:15:37 Finished compiler/backend/ag32/proofs                         13m51s   6GB
May 23 10:15:38 Starting candle/set-theory
May 23 10:16:22 Finished candle/set-theory                                       42s   1GB
May 23 10:16:23 Starting candle/syntax-lib
May 23 10:16:24 Finished candle/syntax-lib                                        0s  69MB
May 23 10:16:25 Starting candle/standard/syntax
May 23 10:16:42 Finished candle/standard/syntax                                  15s   1GB
May 23 10:16:43 Starting candle/standard/semantics
May 23 10:19:08 Finished candle/standard/semantics                             2m24s   3GB
May 23 10:19:09 Starting candle/standard/monadic
May 23 10:19:10 Finished candle/standard/monadic                                  0s 104MB
May 23 10:19:11 Starting candle/standard/ml_kernel
May 23 10:21:01 Finished candle/standard/ml_kernel                             1m48s   5GB
May 23 10:21:02 Starting candle/overloading/syntax
May 23 10:24:28 Finished candle/overloading/syntax                             3m25s   3GB
May 23 10:24:29 Starting candle/overloading/semantics
May 23 10:35:52 Finished candle/overloading/semantics                         11m21s   6GB
May 23 10:35:53 Starting candle/overloading/monadic
May 23 10:38:24 Finished candle/overloading/monadic                            2m30s   2GB
May 23 10:38:25 Starting candle/overloading/ml_kernel
May 23 10:46:00 Finished candle/overloading/ml_kernel                          7m34s   6GB
May 23 10:46:01 Starting candle/overloading/ml_checker
May 23 10:48:35 Finished candle/overloading/ml_checker                         2m32s   6GB
May 23 10:48:36 Starting candle/prover
May 23 10:58:28 Finished candle/prover                                         9m50s   5GB
May 23 10:58:29 Starting pancake
May 23 10:59:30 Finished pancake                                               1m00s   1GB
May 23 10:59:31 Starting pancake/ffi
May 23 10:59:32 Finished pancake/ffi                                              0s  20MB
May 23 10:59:33 Starting pancake/semantics
May 23 11:02:09 Finished pancake/semantics                                     2m35s   2GB
May 23 11:02:10 Starting pancake/parser
May 23 11:02:40 Finished pancake/parser                                          28s   2GB
May 23 11:02:41 Starting pancake/proofs
May 23 11:33:33 Finished pancake/proofs                                       30m50s  10GB
May 23 11:33:34 Starting characteristic/examples
May 23 11:35:08 Finished characteristic/examples                               1m32s   6GB
May 23 11:35:08 Starting tutorial/solutions
May 23 11:50:45 Finished tutorial/solutions                                   15m35s  11GB
May 23 11:50:46 Starting translator/monadic/examples
May 23 11:54:37 Finished translator/monadic/examples                           3m50s   5GB
May 23 11:54:37 Starting examples
May 23 11:57:21 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 (15s)     OK
Starting work on printingTheory
parsingTheory                                   examples/bootstrap (15s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]   (15.030s) 
Starting work on lcsTheory
printingTheory                                  examples/bootstrap  (5s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (24.660s) 
Starting work on divTheory
lcsTheory                                                 examples (20s)     OK
Starting work on diffTheory
diffTheory                                                examples (43s)     OK
Starting work on diffProgTheory
catProgTheory                                             examples (84s)     OK
Starting work on doubleArgProgTheory
quicksortProgTheory                                       examples (96s)     OK
Starting work on array_searchProgTheory
divTheory                                                 examples(113s)     OK
Starting work on echoProgTheory
array_searchProgTheory                                    examples (52s)FAIL<1>
 
 failed.
 Failed to prove theorem linear_search_spec.
 
 Exception raised at BasicProvers.Induct_on:
 at BasicProvers.induct_on_type:
 Type: : list ->  list -> bool is not registered in the types database (THEN1 on line 101)
 error in quse /scratch/cakeml/regression/cakeml-2391/examples/array_searchProgScript.sml : HOL_ERR {message = "at BasicProvers.induct_on_type:\nType: :\206\177 list -> \206\177 list -> bool is not registered in the types database (THEN1 on line 101)", origin_function = "Induct_on", origin_structure = "BasicProvers"}
 error in load /scratch/cakeml/regression/cakeml-2391/examples/array_searchProgScript : HOL_ERR {message = "at BasicProvers.induct_on_type:\nType: :\206\177 list -> \206\177 list -> bool is not registered in the types database (THEN1 on line 101)", origin_function = "Induct_on", origin_structure = "BasicProvers"}
 Uncaught exception: HOL_ERR {message = "at BasicProvers.induct_on_type:\nType: :\206\177 list -> \206\177 list -> bool is not registered in the types database (THEN1 on line 101)", origin_function = "Induct_on", origin_structure = "BasicProvers"}
diffProgTheory                                            examples (67s)MKILLED
doubleArgProgTheory                                       examples (64s)MKILLED
echoProgTheory                                            examples (16s)MKILLED