Job 2557

CakeML:8620f3df78d7960734a2f98b4264564047077b81
  Update cc calls in makefiles [Aug 10 13:40:56]
#1032 (new-double-ffi)
Merging into:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:a18a10ab99c90f2d4e47536b411eeee5bec72004
  some FUNPOW Tau and spin lemmas for itreeTau [Aug 16 00:45:50]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 20 10:40:16 Claimed job
Aug 20 10:40:24 Building HOL
Aug 20 10:53:59 Starting developers
Aug 20 10:54:04 Finished developers                                               5s 123MB
Aug 20 10:54:04 Starting developers/bin
Aug 20 10:54:11 Finished developers/bin                                           6s   1GB
Aug 20 10:54:11 Starting compiler/proofs
Aug 20 13:00:01 Finished compiler/proofs                                    2h05m50s  18GB
Aug 20 13:00:02 Starting compiler/bootstrap/translation
Aug 20 21:57:41 Finished compiler/bootstrap/translation                     8h57m38s  44GB
Aug 20 21:57:41 Starting semantics/ffi
Aug 20 21:57:47 Finished semantics/ffi                                            5s 362MB
Aug 20 21:57:47 Starting semantics
Aug 20 21:57:49 Finished semantics                                                1s  24MB
Aug 20 21:57:49 Starting semantics/proofs
Aug 20 21:58:21 Finished semantics/proofs                                        32s   1GB
Aug 20 21:58:22 Starting semantics/alt_semantics
Aug 20 21:59:03 Finished semantics/alt_semantics                                 41s   1GB
Aug 20 21:59:03 Starting semantics/alt_semantics/proofs
Aug 20 22:11:17 Finished semantics/alt_semantics/proofs                       12m14s   1GB
Aug 20 22:11:18 Starting basis/pure
Aug 20 22:11:19 Finished basis/pure                                               1s  19MB
Aug 20 22:11:19 Starting translator
Aug 20 22:13:07 Finished translator                                            1m47s   2GB
Aug 20 22:13:07 Starting compiler/parsing
Aug 20 22:13:09 Finished compiler/parsing                                         1s  18MB
Aug 20 22:13:09 Starting characteristic
Aug 20 22:13:11 Finished characteristic                                           2s  19MB
Aug 20 22:13:11 Starting translator/monadic
Aug 20 22:13:13 Finished translator/monadic                                       1s  25MB
Aug 20 22:13:13 Starting basis
Aug 20 22:15:54 Finished basis                                                 2m40s   2GB
Aug 20 22:15:54 Starting compiler/inference
Aug 20 22:15:56 Finished compiler/inference                                       1s  24MB
Aug 20 22:15:56 Starting compiler/backend/reg_alloc
Aug 20 22:15:57 Finished compiler/backend/reg_alloc                               1s  21MB
Aug 20 22:15:57 Starting compiler/backend/gc
Aug 20 22:16:00 Finished compiler/backend/gc                                      2s  27MB
Aug 20 22:16:00 Starting compiler/backend
Aug 20 22:16:15 Finished compiler/backend                                        15s 971MB
Aug 20 22:16:15 Starting compiler/encoders/asm
Aug 20 22:16:17 Finished compiler/encoders/asm                                    1s  20MB
Aug 20 22:16:17 Starting compiler/encoders/x64
Aug 20 22:16:19 Finished compiler/encoders/x64                                    1s  25MB
Aug 20 22:16:19 Starting compiler/encoders/arm7
Aug 20 22:16:21 Finished compiler/encoders/arm7                                   1s  27MB
Aug 20 22:16:21 Starting compiler/encoders/arm8
Aug 20 22:16:23 Finished compiler/encoders/arm8                                   1s  22MB
Aug 20 22:16:23 Starting compiler/encoders/arm8_asl
Aug 21 00:48:43 Finished compiler/encoders/arm8_asl                         2h32m18s  35GB
Aug 21 00:48:43 Starting compiler/encoders/mips
Aug 21 00:48:45 Finished compiler/encoders/mips                                   1s  20MB
Aug 21 00:48:45 Starting compiler/encoders/riscv
Aug 21 00:48:47 Finished compiler/encoders/riscv                                  1s  21MB
Aug 21 00:48:47 Starting compiler/encoders/ag32
Aug 21 00:48:49 Finished compiler/encoders/ag32                                   1s  27MB
Aug 21 00:48:49 Starting compiler/backend/x64
Aug 21 00:48:51 Finished compiler/backend/x64                                     2s  25MB
Aug 21 00:48:51 Starting compiler/backend/arm7
Aug 21 00:48:54 Finished compiler/backend/arm7                                    2s  25MB
Aug 21 00:48:54 Starting compiler/backend/arm8
Aug 21 00:48:56 Finished compiler/backend/arm8                                    2s  25MB
Aug 21 00:48:56 Starting compiler/backend/mips
Aug 21 00:48:59 Finished compiler/backend/mips                                    2s  32MB
Aug 21 00:48:59 Starting compiler/backend/riscv
Aug 21 00:49:01 Finished compiler/backend/riscv                                   2s  21MB
Aug 21 00:49:01 Starting compiler/backend/ag32
Aug 21 00:50:29 Finished compiler/backend/ag32                                 1m27s   1GB
Aug 21 00:50:29 Starting compiler/parsing/proofs
Aug 21 00:50:31 Finished compiler/parsing/proofs                                  1s  21MB
Aug 21 00:50:31 Starting compiler/inference/proofs
Aug 21 00:50:33 Finished compiler/inference/proofs                                1s  20MB
Aug 21 00:50:33 Starting compiler/backend/semantics
Aug 21 00:54:25 Finished compiler/backend/semantics                            3m51s   1GB
Aug 21 00:54:25 Starting compiler/backend/reg_alloc/proofs
Aug 21 00:54:27 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Aug 21 00:54:27 Starting compiler/backend/proofs
Aug 21 00:55:27 Finished compiler/backend/proofs                                 59s   2GB
Aug 21 00:55:27 Starting compiler/backend/serialiser
Aug 21 00:55:29 Finished compiler/backend/serialiser                              2s  29MB
Aug 21 00:55:29 Starting compiler/encoders/x64/proofs
Aug 21 01:05:20 Finished compiler/encoders/x64/proofs                          9m50s   6GB
Aug 21 01:05:20 Starting compiler/encoders/arm7/proofs
Aug 21 01:19:09 Finished compiler/encoders/arm7/proofs                        13m48s   4GB
Aug 21 01:19:09 Starting compiler/encoders/arm8/proofs
Aug 21 01:26:21 Finished compiler/encoders/arm8/proofs                         7m11s   1GB
Aug 21 01:26:21 Starting compiler/encoders/arm8_asl/proofs
Aug 21 02:18:57 Finished compiler/encoders/arm8_asl/proofs                    52m35s   5GB
Aug 21 02:18:57 Starting compiler/encoders/mips/proofs
Aug 21 02:29:43 Finished compiler/encoders/mips/proofs                        10m45s   3GB
Aug 21 02:29:43 Starting compiler/encoders/riscv/proofs
Aug 21 02:38:45 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Aug 21 02:38:45 Starting compiler/encoders/ag32/proofs
Aug 21 02:41:20 Finished compiler/encoders/ag32/proofs                         2m35s   1GB
Aug 21 02:41:20 Starting compiler/backend/x64/proofs
Aug 21 02:41:51 Finished compiler/backend/x64/proofs                             30s   1GB
Aug 21 02:41:51 Starting compiler/backend/arm7/proofs
Aug 21 02:42:24 Finished compiler/backend/arm7/proofs                            32s   1GB
Aug 21 02:42:24 Starting compiler/backend/arm8/proofs
Aug 21 02:42:57 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 21 02:42:57 Starting compiler/backend/arm8_asl
Aug 21 02:43:22 Finished compiler/backend/arm8_asl                               24s   2GB
Aug 21 02:43:22 Starting compiler/backend/mips/proofs
Aug 21 02:43:58 Finished compiler/backend/mips/proofs                            35s   2GB
Aug 21 02:43:58 Starting compiler/backend/riscv/proofs
Aug 21 02:44:35 Finished compiler/backend/riscv/proofs                           36s   2GB
Aug 21 02:44:35 Starting compiler/backend/ag32/proofs
Aug 21 02:59:23 Finished compiler/backend/ag32/proofs                         14m47s   2GB
Aug 21 02:59:23 Starting compiler/backend/cv_compute
Aug 21 03:00:43 Finished compiler/backend/cv_compute                           1m19s   2GB
Aug 21 03:00:43 Starting cv_translator
Aug 21 03:21:18 Finished cv_translator                                        20m35s   7GB
Aug 21 03:21:18 Starting candle/set-theory
Aug 21 03:22:03 Finished candle/set-theory                                       44s   1GB
Aug 21 03:22:03 Starting candle/syntax-lib
Aug 21 03:22:05 Finished candle/syntax-lib                                        1s  21MB
Aug 21 03:22:05 Starting candle/standard/syntax
Aug 21 03:22:17 Finished candle/standard/syntax                                  12s 668MB
Aug 21 03:22:17 Starting candle/standard/semantics
Aug 21 03:24:30 Finished candle/standard/semantics                             2m12s   1GB
Aug 21 03:24:30 Starting candle/standard/monadic
Aug 21 03:24:32 Finished candle/standard/monadic                                  1s  22MB
Aug 21 03:24:32 Starting candle/standard/ml_kernel
Aug 21 03:26:19 Finished candle/standard/ml_kernel                             1m46s   4GB
Aug 21 03:26:19 Starting candle/overloading/syntax
Aug 21 03:29:51 Finished candle/overloading/syntax                             3m32s   1GB
Aug 21 03:29:51 Starting candle/overloading/semantics
Aug 21 03:42:20 Finished candle/overloading/semantics                         12m28s   2GB
Aug 21 03:42:20 Starting candle/overloading/monadic
Aug 21 03:45:04 Finished candle/overloading/monadic                            2m43s   2GB
Aug 21 03:45:04 Starting candle/overloading/ml_kernel
Aug 21 03:53:15 Finished candle/overloading/ml_kernel                          8m11s   3GB
Aug 21 03:53:15 Starting candle/overloading/ml_checker
Aug 21 03:55:55 Finished candle/overloading/ml_checker                         2m39s   3GB
Aug 21 03:55:55 Starting candle/prover
Aug 21 04:06:07 Finished candle/prover                                        10m10s   3GB
Aug 21 04:06:07 Starting pancake
Aug 21 04:06:59 Finished pancake                                                 52s   1GB
Aug 21 04:06:59 Starting pancake/ffi
Aug 21 04:07:00 Finished pancake/ffi                                              0s  13MB
Aug 21 04:07:00 Starting pancake/semantics
Aug 21 04:09:43 Finished pancake/semantics                                     2m43s   1GB
Aug 21 04:09:43 Starting pancake/parser
Aug 21 04:10:14 Finished pancake/parser                                          31s   1GB
Aug 21 04:10:15 Starting pancake/proofs
Aug 21 04:27:56 Finished pancake/proofs                                       17m40s   6GB
Aug 21 04:27:56 Starting characteristic/examples
Aug 21 04:29:33 Finished characteristic/examples                               1m37s   3GB
Aug 21 04:29:34 Starting tutorial/solutions
Aug 21 04:32:21 Finished tutorial/solutions                                    2m46s   3GB
Aug 21 04:32:21 Starting translator/monadic/examples
Aug 21 04:36:41 Finished translator/monadic/examples                           4m20s   2GB
Aug 21 04:36:41 Starting examples
Aug 21 04:53:25 Finished examples                                             16m43s   5GB
Aug 21 04:53:25 Starting examples/compilation/x64
Aug 21 05:02:24 Finished examples/compilation/x64                              8m58s   5GB
Aug 21 05:02:24 Starting examples/compilation/x64/proofs
Aug 21 05:05:18 Finished examples/compilation/x64/proofs                       2m53s   4GB
Aug 21 05:05:18 Starting examples/compilation/ag32
Aug 21 05:07:34 Finished examples/compilation/ag32                             2m15s   3GB
Aug 21 05:07:34 Starting examples/compilation/ag32/proofs
Aug 21 05:08:44 Finished examples/compilation/ag32/proofs                      1m10s   5GB
Aug 21 05:08:44 Starting examples/compilation/to_word
Aug 21 05:12:14 Finished examples/compilation/to_word                          3m30s   7GB
Aug 21 05:12:14 Starting examples/lpr_checker
Aug 21 05:13:25 Finished examples/lpr_checker                                  1m10s   1GB
Aug 21 05:13:25 Starting examples/lpr_checker/array
Aug 21 05:43:53 Finished examples/lpr_checker/array                           30m27s   7GB
Aug 21 05:43:53 Starting examples/lpr_checker/array/compilation
Aug 21 05:46:33 Finished examples/lpr_checker/array/compilation                2m39s   7GB
Aug 21 05:46:33 Starting examples/lpr_checker/array/compilation/proofs
Aug 21 05:47:58 Finished examples/lpr_checker/array/compilation/proofs         1m24s   5GB
Aug 21 05:47:58 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 21 05:49:16 Finished examples/lpr_checker/array/compilation/proofsARM8     1m18s   7GB
Aug 21 05:49:16 Starting examples/xlrup_checker
Aug 21 05:50:19 Finished examples/xlrup_checker                                1m02s   1GB
Aug 21 05:50:19 Starting examples/xlrup_checker/array
Aug 21 06:07:00 Finished examples/xlrup_checker/array                         16m39s   5GB
Aug 21 06:07:00 Starting examples/xlrup_checker/array/compilation
Aug 21 06:08:22 Finished examples/xlrup_checker/array/compilation              1m22s   5GB
Aug 21 06:08:22 Starting examples/xlrup_checker/array/compilation/proofs
Aug 21 06:09:26 Finished examples/xlrup_checker/array/compilation/proofs       1m03s   5GB
Aug 21 06:09:26 Starting examples/pseudo_bool
Aug 21 06:11:31 Finished examples/pseudo_bool                                  2m04s   1GB
Aug 21 06:11:31 Starting examples/pseudo_bool/cnf_encoding
Aug 21 06:12:00 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Aug 21 06:12:00 Starting examples/pseudo_bool/graph_encoding
Aug 21 06:12:47 Finished examples/pseudo_bool/graph_encoding                     46s   1GB
Aug 21 06:12:47 Starting examples/pseudo_bool/array
Aug 21 07:23:21 Finished examples/pseudo_bool/array                         1h10m33s   9GB
Aug 21 07:23:21 Starting examples/pseudo_bool/array/compilation
Aug 21 07:38:04 Finished examples/pseudo_bool/array/compilation               14m42s  28GB
Aug 21 07:38:04 Starting examples/pseudo_bool/array/compilation/proofs
Aug 21 07:41:02 Finished examples/pseudo_bool/array/compilation/proofs         2m57s   7GB
Aug 21 07:41:02 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 21 07:42:24 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m22s   5GB
Aug 21 07:42:25 Starting examples/opentheory
Aug 21 07:50:40 FAILED: examples/opentheory
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
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanned 36 directories
Starting work on README.md
Starting work on prettyTheory
README.md                                                                                                                                                                                                                         (0s)     OK
prettyTheory                                                                                                                                                                                                                     (22s)     OK
Starting work on readerTheory
readerTheory                                                                                                                                                                                                                     (59s)     OK
Starting work on reader_initTheory
reader_initTheory                                                                                                                                                                                                                (28s)     OK
Starting work on readerProofTheory
readerProofTheory                                                                                                                                                                                                                (76s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                                                                                                                                                                            (24s)     OK
reader_commonProgTheory                                                                                                                                                                                                         (293s)FAIL<1>
    Mem
      (5 +
       LENGTH
         (... ++ ... ++ stderr_refs ++ init_type_constants_refs ++
          init_term_constants_refs ++ init_axioms_refs ++ init_context_refs))
      (Refv init_context_v)}
 
 failed.
 Failed to prove theorem HOL_STORE_init_precond.
 Uncaught exception: HOL_ERR {message = "No matching sub-term found (THEN1 on line 268)", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}