Job 2393

CakeML:30058919dee54ba63c352c10b14731a85ddb14a3
  Add arm8 bootstrap [Apr 30 10:13:13]
#991 (master)
Merging into: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:lammmington

May 23 15:17:35 Claimed job
May 23 15:17:45 Building HOL
May 23 15:32:17 Starting developers
May 23 15:32:21 Finished developers                                               2s 225MB
May 23 15:32:22 Starting developers/bin
May 23 15:32:40 Finished developers/bin                                          17s   1GB
May 23 15:32:41 Starting compiler/proofs
May 23 17:28:42 Finished compiler/proofs                                    1h55m59s  33GB
May 23 17:28:43 Starting compiler/bootstrap/translation
May 24 01:46:16 Finished compiler/bootstrap/translation                     8h17m32s  88GB
May 24 01:46:17 Starting semantics/ffi
May 24 01:46:26 Finished semantics/ffi                                            7s 603MB
May 24 01:46:26 Starting semantics
May 24 01:46:28 Finished semantics                                                0s  68MB
May 24 01:46:29 Starting semantics/proofs
May 24 01:47:04 Finished semantics/proofs                                        34s   2GB
May 24 01:47:05 Starting semantics/alt_semantics
May 24 01:47:46 Finished semantics/alt_semantics                                 39s   1GB
May 24 01:47:47 Starting semantics/alt_semantics/proofs
May 24 01:58:42 Finished semantics/alt_semantics/proofs                       10m54s   4GB
May 24 01:58:43 Starting basis/pure
May 24 01:58:44 Finished basis/pure                                               0s  75MB
May 24 01:58:45 Starting translator
May 24 02:00:29 Finished translator                                            1m42s   4GB
May 24 02:00:30 Starting compiler/parsing
May 24 02:00:31 Finished compiler/parsing                                         0s  72MB
May 24 02:00:32 Starting characteristic
May 24 02:00:34 Finished characteristic                                           0s  89MB
May 24 02:00:35 Starting translator/monadic
May 24 02:00:36 Finished translator/monadic                                       0s 100MB
May 24 02:00:37 Starting basis
May 24 02:04:07 Finished basis                                                 3m29s   5GB
May 24 02:04:08 Starting compiler/inference
May 24 02:04:10 Finished compiler/inference                                       0s  81MB
May 24 02:04:11 Starting compiler/backend/reg_alloc
May 24 02:04:12 Finished compiler/backend/reg_alloc                               0s  69MB
May 24 02:04:13 Starting compiler/backend/gc
May 24 02:04:15 Finished compiler/backend/gc                                      0s 140MB
May 24 02:04:16 Starting compiler/backend
May 24 02:04:34 Finished compiler/backend                                        17s   1GB
May 24 02:04:35 Starting compiler/encoders/asm
May 24 02:04:36 Finished compiler/encoders/asm                                    0s  97MB
May 24 02:04:37 Starting compiler/encoders/x64
May 24 02:04:39 Finished compiler/encoders/x64                                    0s 103MB
May 24 02:04:40 Starting compiler/encoders/arm7
May 24 02:04:41 Finished compiler/encoders/arm7                                   0s 102MB
May 24 02:04:42 Starting compiler/encoders/arm8
May 24 02:04:44 Finished compiler/encoders/arm8                                   0s  98MB
May 24 02:04:44 Starting compiler/encoders/arm8_asl
May 24 04:17:16 Finished compiler/encoders/arm8_asl                         2h12m31s  40GB
May 24 04:17:17 Starting compiler/encoders/mips
May 24 04:17:19 Finished compiler/encoders/mips                                   0s 101MB
May 24 04:17:20 Starting compiler/encoders/riscv
May 24 04:17:21 Finished compiler/encoders/riscv                                  0s  99MB
May 24 04:17:22 Starting compiler/encoders/ag32
May 24 04:17:24 Finished compiler/encoders/ag32                                   0s  90MB
May 24 04:17:25 Starting compiler/backend/x64
May 24 04:17:27 Finished compiler/backend/x64                                     0s 136MB
May 24 04:17:27 Starting compiler/backend/arm7
May 24 04:17:29 Finished compiler/backend/arm7                                    0s 136MB
May 24 04:17:30 Starting compiler/backend/arm8
May 24 04:17:32 Finished compiler/backend/arm8                                    0s 136MB
May 24 04:17:33 Starting compiler/backend/mips
May 24 04:17:35 Finished compiler/backend/mips                                    0s 136MB
May 24 04:17:36 Starting compiler/backend/riscv
May 24 04:17:37 Finished compiler/backend/riscv                                   0s 136MB
May 24 04:17:38 Starting compiler/backend/ag32
May 24 04:18:57 Finished compiler/backend/ag32                                 1m17s   2GB
May 24 04:18:57 Starting compiler/parsing/proofs
May 24 04:18:59 Finished compiler/parsing/proofs                                  0s  74MB
May 24 04:19:00 Starting compiler/inference/proofs
May 24 04:19:01 Finished compiler/inference/proofs                                0s  89MB
May 24 04:19:02 Starting compiler/backend/semantics
May 24 04:22:42 Finished compiler/backend/semantics                            3m38s   3GB
May 24 04:22:43 Starting compiler/backend/reg_alloc/proofs
May 24 04:22:44 Finished compiler/backend/reg_alloc/proofs                        0s  98MB
May 24 04:22:45 Starting compiler/backend/proofs
May 24 04:23:48 Finished compiler/backend/proofs                               1m01s   2GB
May 24 04:23:48 Starting compiler/backend/serialiser
May 24 04:23:51 Finished compiler/backend/serialiser                              1s 191MB
May 24 04:23:52 Starting compiler/encoders/x64/proofs
May 24 04:33:27 Finished compiler/encoders/x64/proofs                          9m34s   5GB
May 24 04:33:28 Starting compiler/encoders/arm7/proofs
May 24 04:46:16 Finished compiler/encoders/arm7/proofs                        12m46s   8GB
May 24 04:46:17 Starting compiler/encoders/arm8/proofs
May 24 04:52:39 Finished compiler/encoders/arm8/proofs                         6m22s   6GB
May 24 04:52:40 Starting compiler/encoders/arm8_asl/proofs
May 24 05:40:21 Finished compiler/encoders/arm8_asl/proofs                    47m39s  12GB
May 24 05:40:22 Starting compiler/encoders/mips/proofs
May 24 05:50:23 Finished compiler/encoders/mips/proofs                        10m00s   7GB
May 24 05:50:24 Starting compiler/encoders/riscv/proofs
May 24 05:58:27 Finished compiler/encoders/riscv/proofs                        8m02s   4GB
May 24 05:58:28 Starting compiler/encoders/ag32/proofs
May 24 06:00:51 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
May 24 06:00:52 Starting compiler/backend/x64/proofs
May 24 06:01:33 Finished compiler/backend/x64/proofs                             40s   3GB
May 24 06:01:34 Starting compiler/backend/arm7/proofs
May 24 06:02:18 Finished compiler/backend/arm7/proofs                            42s   2GB
May 24 06:02:18 Starting compiler/backend/arm8/proofs
May 24 06:03:01 Finished compiler/backend/arm8/proofs                            41s   3GB
May 24 06:03:02 Starting compiler/backend/arm8_asl
May 24 06:03:32 Finished compiler/backend/arm8_asl                               29s   2GB
May 24 06:03:33 Starting compiler/backend/mips/proofs
May 24 06:04:18 Finished compiler/backend/mips/proofs                            43s   3GB
May 24 06:04:19 Starting compiler/backend/riscv/proofs
May 24 06:05:09 Finished compiler/backend/riscv/proofs                           48s   3GB
May 24 06:05:10 Starting compiler/backend/ag32/proofs
May 24 06:19:20 Finished compiler/backend/ag32/proofs                         14m09s   6GB
May 24 06:19:21 Starting candle/set-theory
May 24 06:20:06 Finished candle/set-theory                                       43s   1GB
May 24 06:20:07 Starting candle/syntax-lib
May 24 06:20:08 Finished candle/syntax-lib                                        0s  69MB
May 24 06:20:09 Starting candle/standard/syntax
May 24 06:20:25 Finished candle/standard/syntax                                  14s   1GB
May 24 06:20:26 Starting candle/standard/semantics
May 24 06:22:54 Finished candle/standard/semantics                             2m26s   3GB
May 24 06:22:55 Starting candle/standard/monadic
May 24 06:22:56 Finished candle/standard/monadic                                  0s 104MB
May 24 06:22:57 Starting candle/standard/ml_kernel
May 24 06:24:47 Finished candle/standard/ml_kernel                             1m48s   5GB
May 24 06:24:48 Starting candle/overloading/syntax
May 24 06:28:18 Finished candle/overloading/syntax                             3m28s   3GB
May 24 06:28:19 Starting candle/overloading/semantics
May 24 06:39:25 Finished candle/overloading/semantics                         11m05s   5GB
May 24 06:39:26 Starting candle/overloading/monadic
May 24 06:41:58 Finished candle/overloading/monadic                            2m30s   3GB
May 24 06:41:59 Starting candle/overloading/ml_kernel
May 24 06:49:35 Finished candle/overloading/ml_kernel                          7m35s   6GB
May 24 06:49:36 Starting candle/overloading/ml_checker
May 24 06:52:11 Finished candle/overloading/ml_checker                         2m34s   7GB
May 24 06:52:12 Starting candle/prover
May 24 07:02:07 Finished candle/prover                                         9m53s   5GB
May 24 07:02:08 Starting pancake
May 24 07:03:08 Finished pancake                                                 59s   1GB
May 24 07:03:09 Starting pancake/ffi
May 24 07:03:10 Finished pancake/ffi                                              0s  22MB
May 24 07:03:11 Starting pancake/semantics
May 24 07:05:47 Finished pancake/semantics                                     2m35s   2GB
May 24 07:05:48 Starting pancake/parser
May 24 07:06:18 Finished pancake/parser                                          28s   2GB
May 24 07:06:19 Starting pancake/proofs
May 24 07:37:25 Finished pancake/proofs                                       31m05s   9GB
May 24 07:37:26 Starting characteristic/examples
May 24 07:39:03 Finished characteristic/examples                               1m35s   6GB
May 24 07:39:04 Starting tutorial/solutions
May 24 07:55:29 Finished tutorial/solutions                                   16m24s  28GB
May 24 07:55:30 Starting translator/monadic/examples
May 24 07:59:19 Finished translator/monadic/examples                           3m47s   5GB
May 24 07:59:20 Starting examples
May 24 08:02:01 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  (1s)     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.600s) 
Starting work on lcsTheory
parsingTheory                                   examples/bootstrap (15s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (24.780s) 
Starting work on divTheory
lcsTheory                                                 examples (19s)     OK
Starting work on diffTheory
diffTheory                                                examples (43s)     OK
Starting work on diffProgTheory
catProgTheory                                             examples (84s)     OK
Starting work on doubleArgProgTheory
quicksortProgTheory                                       examples (92s)     OK
Starting work on array_searchProgTheory
divTheory                                                 examples(113s)     OK
Starting work on echoProgTheory
array_searchProgTheory                                    examples (53s)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/regression2/cakeml-2393/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/regression2/cakeml-2393/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 (63s)MKILLED
doubleArgProgTheory                                       examples (61s)MKILLED
echoProgTheory                                            examples (16s)MKILLED