Job 2566

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:5fc7a6047d48839800489adfb2c2eac7f3ffd5fc
  Add missing export [Aug 21 10:25:23]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 22 07:22:59 Claimed job
Aug 22 07:23:08 Building HOL
Aug 22 07:37:02 Starting developers
Aug 22 07:37:07 Finished developers                                               5s 185MB
Aug 22 07:37:07 Starting developers/bin
Aug 22 07:37:14 Finished developers/bin                                           5s   1GB
Aug 22 07:37:14 Starting compiler/proofs
Aug 22 09:42:55 Finished compiler/proofs                                    2h05m41s  18GB
Aug 22 09:42:55 Starting compiler/bootstrap/translation
Aug 22 18:49:37 Finished compiler/bootstrap/translation                     9h06m41s  64GB
Aug 22 18:49:37 Starting semantics/ffi
Aug 22 18:49:44 Finished semantics/ffi                                            6s 221MB
Aug 22 18:49:44 Starting semantics
Aug 22 18:49:46 Finished semantics                                                1s  21MB
Aug 22 18:49:46 Starting semantics/proofs
Aug 22 18:50:19 Finished semantics/proofs                                        32s   1GB
Aug 22 18:50:19 Starting semantics/alt_semantics
Aug 22 18:50:59 Finished semantics/alt_semantics                                 40s   1GB
Aug 22 18:50:59 Starting semantics/alt_semantics/proofs
Aug 22 19:03:14 Finished semantics/alt_semantics/proofs                       12m14s   1GB
Aug 22 19:03:14 Starting basis/pure
Aug 22 19:03:16 Finished basis/pure                                               1s  22MB
Aug 22 19:03:16 Starting translator
Aug 22 19:05:06 Finished translator                                            1m50s   2GB
Aug 22 19:05:06 Starting compiler/parsing
Aug 22 19:05:08 Finished compiler/parsing                                         1s  18MB
Aug 22 19:05:08 Starting characteristic
Aug 22 19:05:10 Finished characteristic                                           2s  22MB
Aug 22 19:05:10 Starting translator/monadic
Aug 22 19:05:12 Finished translator/monadic                                       1s  20MB
Aug 22 19:05:12 Starting basis
Aug 22 19:07:54 Finished basis                                                 2m41s   3GB
Aug 22 19:07:54 Starting compiler/inference
Aug 22 19:07:56 Finished compiler/inference                                       1s  26MB
Aug 22 19:07:56 Starting compiler/backend/reg_alloc
Aug 22 19:07:58 Finished compiler/backend/reg_alloc                               1s  22MB
Aug 22 19:07:58 Starting compiler/backend/gc
Aug 22 19:08:01 Finished compiler/backend/gc                                      2s  24MB
Aug 22 19:08:01 Starting compiler/backend
Aug 22 19:08:16 Finished compiler/backend                                        14s 970MB
Aug 22 19:08:16 Starting compiler/encoders/asm
Aug 22 19:08:18 Finished compiler/encoders/asm                                    1s  25MB
Aug 22 19:08:18 Starting compiler/encoders/x64
Aug 22 19:08:20 Finished compiler/encoders/x64                                    1s  21MB
Aug 22 19:08:20 Starting compiler/encoders/arm7
Aug 22 19:08:22 Finished compiler/encoders/arm7                                   1s  25MB
Aug 22 19:08:22 Starting compiler/encoders/arm8
Aug 22 19:08:24 Finished compiler/encoders/arm8                                   1s  22MB
Aug 22 19:08:24 Starting compiler/encoders/arm8_asl
Aug 22 21:39:40 Finished compiler/encoders/arm8_asl                         2h31m15s  45GB
Aug 22 21:39:40 Starting compiler/encoders/mips
Aug 22 21:39:42 Finished compiler/encoders/mips                                   1s  21MB
Aug 22 21:39:42 Starting compiler/encoders/riscv
Aug 22 21:39:44 Finished compiler/encoders/riscv                                  1s  24MB
Aug 22 21:39:44 Starting compiler/encoders/ag32
Aug 22 21:39:46 Finished compiler/encoders/ag32                                   1s  27MB
Aug 22 21:39:46 Starting compiler/backend/x64
Aug 22 21:39:48 Finished compiler/backend/x64                                     2s  31MB
Aug 22 21:39:48 Starting compiler/backend/arm7
Aug 22 21:39:51 Finished compiler/backend/arm7                                    2s  27MB
Aug 22 21:39:51 Starting compiler/backend/arm8
Aug 22 21:39:53 Finished compiler/backend/arm8                                    2s  28MB
Aug 22 21:39:53 Starting compiler/backend/mips
Aug 22 21:39:55 Finished compiler/backend/mips                                    2s  28MB
Aug 22 21:39:56 Starting compiler/backend/riscv
Aug 22 21:39:58 Finished compiler/backend/riscv                                   2s  25MB
Aug 22 21:39:58 Starting compiler/backend/ag32
Aug 22 21:41:27 Finished compiler/backend/ag32                                 1m28s   1GB
Aug 22 21:41:27 Starting compiler/parsing/proofs
Aug 22 21:41:29 Finished compiler/parsing/proofs                                  1s  21MB
Aug 22 21:41:29 Starting compiler/inference/proofs
Aug 22 21:41:31 Finished compiler/inference/proofs                                1s  19MB
Aug 22 21:41:31 Starting compiler/backend/semantics
Aug 22 21:45:27 Finished compiler/backend/semantics                            3m55s   1GB
Aug 22 21:45:27 Starting compiler/backend/reg_alloc/proofs
Aug 22 21:45:29 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Aug 22 21:45:29 Starting compiler/backend/proofs
Aug 22 21:46:29 Finished compiler/backend/proofs                                 59s   2GB
Aug 22 21:46:29 Starting compiler/backend/serialiser
Aug 22 21:46:31 Finished compiler/backend/serialiser                              2s  30MB
Aug 22 21:46:31 Starting compiler/encoders/x64/proofs
Aug 22 21:56:20 Finished compiler/encoders/x64/proofs                          9m48s   6GB
Aug 22 21:56:20 Starting compiler/encoders/arm7/proofs
Aug 22 22:10:11 Finished compiler/encoders/arm7/proofs                        13m50s   4GB
Aug 22 22:10:11 Starting compiler/encoders/arm8/proofs
Aug 22 22:17:20 Finished compiler/encoders/arm8/proofs                         7m09s   1GB
Aug 22 22:17:20 Starting compiler/encoders/arm8_asl/proofs
Aug 22 23:12:37 Finished compiler/encoders/arm8_asl/proofs                    55m16s   9GB
Aug 22 23:12:37 Starting compiler/encoders/mips/proofs
Aug 22 23:23:10 Finished compiler/encoders/mips/proofs                        10m32s   3GB
Aug 22 23:23:10 Starting compiler/encoders/riscv/proofs
Aug 22 23:32:15 Finished compiler/encoders/riscv/proofs                        9m04s   1GB
Aug 22 23:32:15 Starting compiler/encoders/ag32/proofs
Aug 22 23:34:46 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Aug 22 23:34:46 Starting compiler/backend/x64/proofs
Aug 22 23:35:17 Finished compiler/backend/x64/proofs                             30s   1GB
Aug 22 23:35:17 Starting compiler/backend/arm7/proofs
Aug 22 23:35:51 Finished compiler/backend/arm7/proofs                            33s   1GB
Aug 22 23:35:51 Starting compiler/backend/arm8/proofs
Aug 22 23:36:23 Finished compiler/backend/arm8/proofs                            31s   1GB
Aug 22 23:36:23 Starting compiler/backend/arm8_asl
Aug 22 23:36:48 Finished compiler/backend/arm8_asl                               24s   1GB
Aug 22 23:36:48 Starting compiler/backend/mips/proofs
Aug 22 23:37:23 Finished compiler/backend/mips/proofs                            35s   2GB
Aug 22 23:37:23 Starting compiler/backend/riscv/proofs
Aug 22 23:38:00 Finished compiler/backend/riscv/proofs                           36s   2GB
Aug 22 23:38:00 Starting compiler/backend/ag32/proofs
Aug 22 23:52:36 Finished compiler/backend/ag32/proofs                         14m35s   2GB
Aug 22 23:52:36 Starting compiler/backend/cv_compute
Aug 22 23:53:55 Finished compiler/backend/cv_compute                           1m18s   2GB
Aug 22 23:53:55 Starting cv_translator
Aug 23 00:14:18 Finished cv_translator                                        20m23s   8GB
Aug 23 00:14:18 Starting candle/set-theory
Aug 23 00:15:02 Finished candle/set-theory                                       43s   1GB
Aug 23 00:15:02 Starting candle/syntax-lib
Aug 23 00:15:03 Finished candle/syntax-lib                                        1s  21MB
Aug 23 00:15:04 Starting candle/standard/syntax
Aug 23 00:15:16 Finished candle/standard/syntax                                  12s 668MB
Aug 23 00:15:16 Starting candle/standard/semantics
Aug 23 00:17:29 Finished candle/standard/semantics                             2m12s   1GB
Aug 23 00:17:29 Starting candle/standard/monadic
Aug 23 00:17:31 Finished candle/standard/monadic                                  1s  28MB
Aug 23 00:17:31 Starting candle/standard/ml_kernel
Aug 23 00:19:18 Finished candle/standard/ml_kernel                             1m47s   5GB
Aug 23 00:19:18 Starting candle/overloading/syntax
Aug 23 00:22:48 Finished candle/overloading/syntax                             3m29s   1GB
Aug 23 00:22:48 Starting candle/overloading/semantics
Aug 23 00:35:23 Finished candle/overloading/semantics                         12m34s   2GB
Aug 23 00:35:23 Starting candle/overloading/monadic
Aug 23 00:38:06 Finished candle/overloading/monadic                            2m43s   2GB
Aug 23 00:38:06 Starting candle/overloading/ml_kernel
Aug 23 00:46:20 Finished candle/overloading/ml_kernel                          8m13s   3GB
Aug 23 00:46:20 Starting candle/overloading/ml_checker
Aug 23 00:49:21 Finished candle/overloading/ml_checker                         3m00s   4GB
Aug 23 00:49:21 Starting candle/prover
Aug 23 00:59:35 Finished candle/prover                                        10m13s   3GB
Aug 23 00:59:35 Starting pancake
Aug 23 01:00:25 Finished pancake                                                 49s 940MB
Aug 23 01:00:25 Starting pancake/ffi
Aug 23 01:00:26 Finished pancake/ffi                                              0s  13MB
Aug 23 01:00:26 Starting pancake/semantics
Aug 23 01:03:13 Finished pancake/semantics                                     2m46s   1GB
Aug 23 01:03:13 Starting pancake/parser
Aug 23 01:03:44 Finished pancake/parser                                          30s   1GB
Aug 23 01:03:44 Starting pancake/proofs
Aug 23 01:21:37 Finished pancake/proofs                                       17m53s   4GB
Aug 23 01:21:37 Starting characteristic/examples
Aug 23 01:23:15 Finished characteristic/examples                               1m37s   4GB
Aug 23 01:23:15 Starting tutorial/solutions
Aug 23 01:26:07 Finished tutorial/solutions                                    2m51s   3GB
Aug 23 01:26:07 Starting translator/monadic/examples
Aug 23 01:31:06 Finished translator/monadic/examples                           4m58s   3GB
Aug 23 01:31:06 Starting examples
Aug 23 01:51:37 Finished examples                                             20m31s   4GB
Aug 23 01:51:37 Starting examples/compilation/x64
Aug 23 02:00:50 Finished examples/compilation/x64                              9m12s   5GB
Aug 23 02:00:50 Starting examples/compilation/x64/proofs
Aug 23 02:04:08 Finished examples/compilation/x64/proofs                       3m17s   5GB
Aug 23 02:04:08 Starting examples/compilation/ag32
Aug 23 02:06:27 Finished examples/compilation/ag32                             2m18s   2GB
Aug 23 02:06:27 Starting examples/compilation/ag32/proofs
Aug 23 02:07:44 Finished examples/compilation/ag32/proofs                      1m17s   5GB
Aug 23 02:07:44 Starting examples/compilation/to_word
Aug 23 02:11:19 Finished examples/compilation/to_word                          3m34s   7GB
Aug 23 02:11:19 Starting examples/lpr_checker
Aug 23 02:12:32 Finished examples/lpr_checker                                  1m13s   1GB
Aug 23 02:12:32 Starting examples/lpr_checker/array
Aug 23 02:45:51 Finished examples/lpr_checker/array                           33m17s   9GB
Aug 23 02:45:51 Starting examples/lpr_checker/array/compilation
Aug 23 02:49:49 Finished examples/lpr_checker/array/compilation                3m58s   8GB
Aug 23 02:49:49 Starting examples/lpr_checker/array/compilation/proofs
Aug 23 02:51:12 Finished examples/lpr_checker/array/compilation/proofs         1m22s   6GB
Aug 23 02:51:12 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 23 02:52:32 Finished examples/lpr_checker/array/compilation/proofsARM8     1m19s   7GB
Aug 23 02:52:32 Starting examples/xlrup_checker
Aug 23 02:53:38 Finished examples/xlrup_checker                                1m05s   1GB
Aug 23 02:53:38 Starting examples/xlrup_checker/array
Aug 23 03:11:19 Finished examples/xlrup_checker/array                         17m41s   6GB
Aug 23 03:11:19 Starting examples/xlrup_checker/array/compilation
Aug 23 03:12:56 Finished examples/xlrup_checker/array/compilation              1m36s   4GB
Aug 23 03:12:56 Starting examples/xlrup_checker/array/compilation/proofs
Aug 23 03:14:16 Finished examples/xlrup_checker/array/compilation/proofs       1m20s   4GB
Aug 23 03:14:16 Starting examples/pseudo_bool
Aug 23 03:16:49 Finished examples/pseudo_bool                                  2m32s   1GB
Aug 23 03:16:49 Starting examples/pseudo_bool/cnf_encoding
Aug 23 03:17:24 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Aug 23 03:17:24 Starting examples/pseudo_bool/graph_encoding
Aug 23 03:18:23 Finished examples/pseudo_bool/graph_encoding                     59s   1GB
Aug 23 03:18:24 Starting examples/pseudo_bool/array
Aug 23 04:39:59 Finished examples/pseudo_bool/array                         1h21m35s   9GB
Aug 23 04:39:59 Starting examples/pseudo_bool/array/compilation
Aug 23 04:56:21 Finished examples/pseudo_bool/array/compilation               16m21s  25GB
Aug 23 04:56:21 Starting examples/pseudo_bool/array/compilation/proofs
Aug 23 05:00:10 Finished examples/pseudo_bool/array/compilation/proofs         3m49s   7GB
Aug 23 05:00:11 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 23 05:01:44 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m33s   7GB
Aug 23 05:01:45 Starting examples/opentheory
Aug 23 05:10:58 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                                                                                                                                                                                                                     (28s)     OK
Starting work on readerTheory
readerTheory                                                                                                                                                                                                                     (65s)     OK
Starting work on reader_initTheory
reader_initTheory                                                                                                                                                                                                                (34s)     OK
Starting work on readerProofTheory
readerProofTheory                                                                                                                                                                                                                (84s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                                                                                                                                                                            (28s)     OK
reader_commonProgTheory                                                                                                                                                                                                         (323s)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"}