Job 2392

CakeML:9435b5c9b8574935c4b39fec492d0e78ce82c8f5
  Partly fix and partly comment out tests [May 23 15:03:37]
#985 (cvunify)
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:stove 5.15.0-86-generic x86_64 GNU/Linux

May 23 15:15:17 Claimed job
May 23 15:15:27 Building HOL
May 23 15:29:05 Starting developers
May 23 15:29:11 Finished developers                                               5s  94MB
May 23 15:29:11 Starting developers/bin
May 23 15:29:33 Finished developers/bin                                          21s   1GB
May 23 15:29:33 Starting compiler/proofs
May 23 17:29:58 Finished compiler/proofs                                    2h00m25s  21GB
May 23 17:29:59 Starting compiler/bootstrap/translation
May 24 01:50:53 Finished compiler/bootstrap/translation                     8h20m54s  34GB
May 24 01:50:54 Starting semantics/ffi
May 24 01:51:00 Finished semantics/ffi                                            6s 222MB
May 24 01:51:00 Starting semantics
May 24 01:51:02 Finished semantics                                                1s  18MB
May 24 01:51:02 Starting semantics/proofs
May 24 01:51:39 Finished semantics/proofs                                        37s   1GB
May 24 01:51:40 Starting semantics/alt_semantics
May 24 01:52:14 Finished semantics/alt_semantics                                 34s 692MB
May 24 01:52:14 Starting semantics/alt_semantics/proofs
May 24 02:04:46 Finished semantics/alt_semantics/proofs                       12m31s   1GB
May 24 02:04:46 Starting basis/pure
May 24 02:04:48 Finished basis/pure                                               1s  19MB
May 24 02:04:48 Starting translator
May 24 02:06:37 Finished translator                                            1m49s   2GB
May 24 02:06:37 Starting compiler/parsing
May 24 02:06:39 Finished compiler/parsing                                         1s  21MB
May 24 02:06:39 Starting characteristic
May 24 02:06:41 Finished characteristic                                           1s  22MB
May 24 02:06:41 Starting translator/monadic
May 24 02:06:43 Finished translator/monadic                                       1s  24MB
May 24 02:06:43 Starting basis
May 24 02:10:42 Finished basis                                                 3m59s   3GB
May 24 02:10:42 Starting compiler/inference
May 24 02:10:45 Finished compiler/inference                                       2s  31MB
May 24 02:10:45 Starting compiler/backend/reg_alloc
May 24 02:10:47 Finished compiler/backend/reg_alloc                               1s  23MB
May 24 02:10:47 Starting compiler/backend/gc
May 24 02:10:49 Finished compiler/backend/gc                                      2s  27MB
May 24 02:10:49 Starting compiler/backend
May 24 02:11:03 Finished compiler/backend                                        13s 848MB
May 24 02:11:03 Starting compiler/encoders/asm
May 24 02:11:05 Finished compiler/encoders/asm                                    1s  22MB
May 24 02:11:05 Starting compiler/encoders/x64
May 24 02:11:07 Finished compiler/encoders/x64                                    1s  20MB
May 24 02:11:07 Starting compiler/encoders/arm7
May 24 02:11:09 Finished compiler/encoders/arm7                                   1s  27MB
May 24 02:11:09 Starting compiler/encoders/arm8
May 24 02:11:11 Finished compiler/encoders/arm8                                   1s  22MB
May 24 02:11:11 Starting compiler/encoders/arm8_asl
May 24 04:54:39 Finished compiler/encoders/arm8_asl                         2h43m28s  39GB
May 24 04:54:39 Starting compiler/encoders/mips
May 24 04:54:41 Finished compiler/encoders/mips                                   1s  22MB
May 24 04:54:41 Starting compiler/encoders/riscv
May 24 04:54:43 Finished compiler/encoders/riscv                                  1s  21MB
May 24 04:54:43 Starting compiler/encoders/ag32
May 24 04:54:45 Finished compiler/encoders/ag32                                   1s  24MB
May 24 04:54:45 Starting compiler/backend/x64
May 24 04:54:47 Finished compiler/backend/x64                                     2s  27MB
May 24 04:54:47 Starting compiler/backend/arm7
May 24 04:54:50 Finished compiler/backend/arm7                                    2s  25MB
May 24 04:54:50 Starting compiler/backend/arm8
May 24 04:54:52 Finished compiler/backend/arm8                                    2s  23MB
May 24 04:54:52 Starting compiler/backend/mips
May 24 04:54:54 Finished compiler/backend/mips                                    2s  28MB
May 24 04:54:55 Starting compiler/backend/riscv
May 24 04:54:57 Finished compiler/backend/riscv                                   2s  29MB
May 24 04:54:57 Starting compiler/backend/ag32
May 24 04:56:22 Finished compiler/backend/ag32                                 1m25s   1GB
May 24 04:56:23 Starting compiler/parsing/proofs
May 24 04:56:24 Finished compiler/parsing/proofs                                  1s  21MB
May 24 04:56:24 Starting compiler/inference/proofs
May 24 04:56:27 Finished compiler/inference/proofs                                2s  27MB
May 24 04:56:27 Starting compiler/backend/semantics
May 24 05:00:16 Finished compiler/backend/semantics                            3m48s   1GB
May 24 05:00:16 Starting compiler/backend/reg_alloc/proofs
May 24 05:00:18 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
May 24 05:00:18 Starting compiler/backend/proofs
May 24 05:01:20 Finished compiler/backend/proofs                               1m01s   3GB
May 24 05:01:20 Starting compiler/backend/serialiser
May 24 05:01:22 Finished compiler/backend/serialiser                              2s  28MB
May 24 05:01:22 Starting compiler/encoders/x64/proofs
May 24 05:11:14 Finished compiler/encoders/x64/proofs                          9m51s   7GB
May 24 05:11:14 Starting compiler/encoders/arm7/proofs
May 24 05:25:12 Finished compiler/encoders/arm7/proofs                        13m58s   3GB
May 24 05:25:12 Starting compiler/encoders/arm8/proofs
May 24 05:32:11 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
May 24 05:32:12 Starting compiler/encoders/arm8_asl/proofs
May 24 06:25:35 Finished compiler/encoders/arm8_asl/proofs                    53m23s   8GB
May 24 06:25:35 Starting compiler/encoders/mips/proofs
May 24 06:36:09 Finished compiler/encoders/mips/proofs                        10m33s   3GB
May 24 06:36:09 Starting compiler/encoders/riscv/proofs
May 24 06:45:07 Finished compiler/encoders/riscv/proofs                        8m58s   1GB
May 24 06:45:07 Starting compiler/encoders/ag32/proofs
May 24 06:47:39 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
May 24 06:47:39 Starting compiler/backend/x64/proofs
May 24 06:48:12 Finished compiler/backend/x64/proofs                             32s   1GB
May 24 06:48:12 Starting compiler/backend/arm7/proofs
May 24 06:48:45 Finished compiler/backend/arm7/proofs                            33s   1GB
May 24 06:48:45 Starting compiler/backend/arm8/proofs
May 24 06:49:16 Finished compiler/backend/arm8/proofs                            31s   1GB
May 24 06:49:16 Starting compiler/backend/arm8_asl
May 24 06:49:42 Finished compiler/backend/arm8_asl                               25s   2GB
May 24 06:49:42 Starting compiler/backend/mips/proofs
May 24 06:50:15 Finished compiler/backend/mips/proofs                            33s   2GB
May 24 06:50:15 Starting compiler/backend/riscv/proofs
May 24 06:50:51 Finished compiler/backend/riscv/proofs                           35s   2GB
May 24 06:50:51 Starting compiler/backend/ag32/proofs
May 24 07:05:21 Finished compiler/backend/ag32/proofs                         14m29s   3GB
May 24 07:05:21 Starting compiler/backend/cv_compute
May 24 07:06:37 Finished compiler/backend/cv_compute                           1m15s   2GB
May 24 07:06:37 Starting cv_translator
May 24 07:17:11 Finished cv_translator                                        10m34s   5GB
May 24 07:17:11 Starting candle/set-theory
May 24 07:17:51 Finished candle/set-theory                                       39s   1GB
May 24 07:17:51 Starting candle/syntax-lib
May 24 07:17:53 Finished candle/syntax-lib                                        1s  27MB
May 24 07:17:53 Starting candle/standard/syntax
May 24 07:18:04 Finished candle/standard/syntax                                  11s 806MB
May 24 07:18:04 Starting candle/standard/semantics
May 24 07:20:04 Finished candle/standard/semantics                             1m59s   1GB
May 24 07:20:04 Starting candle/standard/monadic
May 24 07:20:06 Finished candle/standard/monadic                                  1s  21MB
May 24 07:20:06 Starting candle/standard/ml_kernel
May 24 07:21:49 Finished candle/standard/ml_kernel                             1m43s   3GB
May 24 07:21:50 Starting candle/overloading/syntax
May 24 07:25:13 Finished candle/overloading/syntax                             3m22s   1GB
May 24 07:25:13 Starting candle/overloading/semantics
May 24 07:37:45 Finished candle/overloading/semantics                         12m32s   2GB
May 24 07:37:45 Starting candle/overloading/monadic
May 24 07:40:30 Finished candle/overloading/monadic                            2m44s   1GB
May 24 07:40:30 Starting candle/overloading/ml_kernel
May 24 07:48:32 Finished candle/overloading/ml_kernel                          8m02s   3GB
May 24 07:48:32 Starting candle/overloading/ml_checker
May 24 07:51:14 Finished candle/overloading/ml_checker                         2m42s   2GB
May 24 07:51:15 Starting candle/prover
May 24 08:01:30 Finished candle/prover                                        10m15s   3GB
May 24 08:01:30 Starting pancake
May 24 08:02:16 Finished pancake                                                 46s 910MB
May 24 08:02:17 Starting pancake/ffi
May 24 08:02:17 Finished pancake/ffi                                              0s  13MB
May 24 08:02:17 Starting pancake/semantics
May 24 08:05:04 Finished pancake/semantics                                     2m47s   1GB
May 24 08:05:05 Starting pancake/parser
May 24 08:05:30 Finished pancake/parser                                          25s   1GB
May 24 08:05:30 Starting pancake/proofs
May 24 08:40:15 Finished pancake/proofs                                       34m44s   5GB
May 24 08:40:15 Starting characteristic/examples
May 24 08:41:51 Finished characteristic/examples                               1m35s   2GB
May 24 08:41:51 Starting tutorial/solutions
May 24 08:57:07 Finished tutorial/solutions                                   15m16s   9GB
May 24 08:57:07 Starting translator/monadic/examples
May 24 09:01:22 Finished translator/monadic/examples                           4m14s   3GB
May 24 09:01:22 Starting examples
May 24 09:04:14 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.057s) 
Starting work on lcsTheory
parsingTheory                                                                                                                                                                         examples/bootstrap (23s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                                                                                                                                                        (32.195s) 
Starting work on divTheory
lcsTheory                                                                                                                                                                                       examples (18s)     OK
Starting work on diffTheory
diffTheory                                                                                                                                                                                      examples (50s)     OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                                                   examples (95s)     OK
Starting work on doubleArgProgTheory
quicksortProgTheory                                                                                                                                                                             examples(106s)     OK
Starting work on array_searchProgTheory
divTheory                                                                                                                                                                                       examples(132s)     OK
Starting work on echoProgTheory
array_searchProgTheory                                                                                                                                                                          examples (56s)FAIL<1>
     (POSTv ret_v.
        ARRAY arr_v elem_vs *
        SEP_EXISTS ret.
          &(OPTION_TYPE NUM ret ret_v 
           (MEM value elems  n. ret = SOME n  ... ... elems = value) 
           (MEM value elems  ret = NONE)))
 
 failed.
 Failed to prove theorem linear_search_spec.
 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 (74s)MKILLED
doubleArgProgTheory                                                                                                                                                                             examples (68s)MKILLED
echoProgTheory                                                                                                                                                                                  examples  (4s)MKILLED