Job 2561

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:257a82233211da227f76888bb05d6fce7c91769c
  Remove some unused code [Aug 20 04:07:40]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Aug 21 09:10:42 Claimed job
Aug 21 09:10:52 Building HOL
Aug 21 09:24:48 Starting developers
Aug 21 09:24:54 Finished developers                                               5s 108MB
Aug 21 09:24:54 Starting developers/bin
Aug 21 09:25:00 Finished developers/bin                                           6s   1GB
Aug 21 09:25:00 Starting compiler/proofs
Aug 21 11:30:20 Finished compiler/proofs                                    2h05m20s  24GB
Aug 21 11:30:20 Starting compiler/bootstrap/translation
Aug 21 20:32:12 Finished compiler/bootstrap/translation                     9h01m51s  43GB
Aug 21 20:32:12 Starting semantics/ffi
Aug 21 20:32:17 Finished semantics/ffi                                            5s 361MB
Aug 21 20:32:17 Starting semantics
Aug 21 20:32:19 Finished semantics                                                1s  21MB
Aug 21 20:32:19 Starting semantics/proofs
Aug 21 20:32:52 Finished semantics/proofs                                        32s 885MB
Aug 21 20:32:52 Starting semantics/alt_semantics
Aug 21 20:33:33 Finished semantics/alt_semantics                                 40s   1GB
Aug 21 20:33:33 Starting semantics/alt_semantics/proofs
Aug 21 20:45:48 Finished semantics/alt_semantics/proofs                       12m14s   1GB
Aug 21 20:45:48 Starting basis/pure
Aug 21 20:45:49 Finished basis/pure                                               1s  17MB
Aug 21 20:45:50 Starting translator
Aug 21 20:47:39 Finished translator                                            1m49s   2GB
Aug 21 20:47:39 Starting compiler/parsing
Aug 21 20:47:41 Finished compiler/parsing                                         1s  21MB
Aug 21 20:47:41 Starting characteristic
Aug 21 20:47:43 Finished characteristic                                           1s  27MB
Aug 21 20:47:43 Starting translator/monadic
Aug 21 20:47:45 Finished translator/monadic                                       1s  20MB
Aug 21 20:47:45 Starting basis
Aug 21 20:50:27 Finished basis                                                 2m41s   3GB
Aug 21 20:50:27 Starting compiler/inference
Aug 21 20:50:29 Finished compiler/inference                                       1s  22MB
Aug 21 20:50:29 Starting compiler/backend/reg_alloc
Aug 21 20:50:30 Finished compiler/backend/reg_alloc                               1s  20MB
Aug 21 20:50:31 Starting compiler/backend/gc
Aug 21 20:50:33 Finished compiler/backend/gc                                      2s  23MB
Aug 21 20:50:33 Starting compiler/backend
Aug 21 20:50:48 Finished compiler/backend                                        14s 920MB
Aug 21 20:50:48 Starting compiler/encoders/asm
Aug 21 20:50:50 Finished compiler/encoders/asm                                    1s  23MB
Aug 21 20:50:50 Starting compiler/encoders/x64
Aug 21 20:50:52 Finished compiler/encoders/x64                                    1s  21MB
Aug 21 20:50:52 Starting compiler/encoders/arm7
Aug 21 20:50:54 Finished compiler/encoders/arm7                                   1s  24MB
Aug 21 20:50:54 Starting compiler/encoders/arm8
Aug 21 20:50:56 Finished compiler/encoders/arm8                                   1s  20MB
Aug 21 20:50:56 Starting compiler/encoders/arm8_asl
Aug 21 23:21:05 Finished compiler/encoders/arm8_asl                         2h30m08s  26GB
Aug 21 23:21:05 Starting compiler/encoders/mips
Aug 21 23:21:07 Finished compiler/encoders/mips                                   1s  27MB
Aug 21 23:21:07 Starting compiler/encoders/riscv
Aug 21 23:21:09 Finished compiler/encoders/riscv                                  1s  23MB
Aug 21 23:21:10 Starting compiler/encoders/ag32
Aug 21 23:21:11 Finished compiler/encoders/ag32                                   1s  25MB
Aug 21 23:21:12 Starting compiler/backend/x64
Aug 21 23:21:14 Finished compiler/backend/x64                                     2s  28MB
Aug 21 23:21:14 Starting compiler/backend/arm7
Aug 21 23:21:16 Finished compiler/backend/arm7                                    2s  22MB
Aug 21 23:21:17 Starting compiler/backend/arm8
Aug 21 23:21:19 Finished compiler/backend/arm8                                    2s  24MB
Aug 21 23:21:19 Starting compiler/backend/mips
Aug 21 23:21:21 Finished compiler/backend/mips                                    2s  29MB
Aug 21 23:21:21 Starting compiler/backend/riscv
Aug 21 23:21:24 Finished compiler/backend/riscv                                   2s  31MB
Aug 21 23:21:24 Starting compiler/backend/ag32
Aug 21 23:22:52 Finished compiler/backend/ag32                                 1m28s   1GB
Aug 21 23:22:52 Starting compiler/parsing/proofs
Aug 21 23:22:54 Finished compiler/parsing/proofs                                  1s  20MB
Aug 21 23:22:54 Starting compiler/inference/proofs
Aug 21 23:22:56 Finished compiler/inference/proofs                                1s  22MB
Aug 21 23:22:56 Starting compiler/backend/semantics
Aug 21 23:26:50 Finished compiler/backend/semantics                            3m53s   1GB
Aug 21 23:26:50 Starting compiler/backend/reg_alloc/proofs
Aug 21 23:26:52 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Aug 21 23:26:52 Starting compiler/backend/proofs
Aug 21 23:27:55 Finished compiler/backend/proofs                               1m02s   3GB
Aug 21 23:27:55 Starting compiler/backend/serialiser
Aug 21 23:27:57 Finished compiler/backend/serialiser                              2s  25MB
Aug 21 23:27:57 Starting compiler/encoders/x64/proofs
Aug 21 23:37:48 Finished compiler/encoders/x64/proofs                          9m50s   6GB
Aug 21 23:37:48 Starting compiler/encoders/arm7/proofs
Aug 21 23:51:43 Finished compiler/encoders/arm7/proofs                        13m54s   4GB
Aug 21 23:51:43 Starting compiler/encoders/arm8/proofs
Aug 21 23:58:47 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Aug 21 23:58:47 Starting compiler/encoders/arm8_asl/proofs
Aug 22 00:50:51 Finished compiler/encoders/arm8_asl/proofs                    52m04s   5GB
Aug 22 00:50:51 Starting compiler/encoders/mips/proofs
Aug 22 01:01:31 Finished compiler/encoders/mips/proofs                        10m39s   3GB
Aug 22 01:01:32 Starting compiler/encoders/riscv/proofs
Aug 22 01:10:21 Finished compiler/encoders/riscv/proofs                        8m49s   2GB
Aug 22 01:10:22 Starting compiler/encoders/ag32/proofs
Aug 22 01:12:54 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Aug 22 01:12:54 Starting compiler/backend/x64/proofs
Aug 22 01:13:26 Finished compiler/backend/x64/proofs                             31s   1GB
Aug 22 01:13:26 Starting compiler/backend/arm7/proofs
Aug 22 01:13:59 Finished compiler/backend/arm7/proofs                            32s   1GB
Aug 22 01:13:59 Starting compiler/backend/arm8/proofs
Aug 22 01:14:31 Finished compiler/backend/arm8/proofs                            31s   1GB
Aug 22 01:14:31 Starting compiler/backend/arm8_asl
Aug 22 01:14:56 Finished compiler/backend/arm8_asl                               25s   1GB
Aug 22 01:14:56 Starting compiler/backend/mips/proofs
Aug 22 01:15:33 Finished compiler/backend/mips/proofs                            36s   2GB
Aug 22 01:15:33 Starting compiler/backend/riscv/proofs
Aug 22 01:16:11 Finished compiler/backend/riscv/proofs                           38s   2GB
Aug 22 01:16:11 Starting compiler/backend/ag32/proofs
Aug 22 01:30:49 Finished compiler/backend/ag32/proofs                         14m36s   3GB
Aug 22 01:30:49 Starting compiler/backend/cv_compute
Aug 22 01:32:09 Finished compiler/backend/cv_compute                           1m20s   2GB
Aug 22 01:32:09 Starting cv_translator
Aug 22 01:52:37 Finished cv_translator                                        20m27s   8GB
Aug 22 01:52:37 Starting candle/set-theory
Aug 22 01:53:21 Finished candle/set-theory                                       43s   1GB
Aug 22 01:53:21 Starting candle/syntax-lib
Aug 22 01:53:23 Finished candle/syntax-lib                                        1s  18MB
Aug 22 01:53:23 Starting candle/standard/syntax
Aug 22 01:53:35 Finished candle/standard/syntax                                  12s 668MB
Aug 22 01:53:35 Starting candle/standard/semantics
Aug 22 01:55:49 Finished candle/standard/semantics                             2m13s   1GB
Aug 22 01:55:49 Starting candle/standard/monadic
Aug 22 01:55:51 Finished candle/standard/monadic                                  1s  21MB
Aug 22 01:55:51 Starting candle/standard/ml_kernel
Aug 22 01:57:39 Finished candle/standard/ml_kernel                             1m47s   5GB
Aug 22 01:57:39 Starting candle/overloading/syntax
Aug 22 02:01:13 Finished candle/overloading/syntax                             3m34s   1GB
Aug 22 02:01:13 Starting candle/overloading/semantics
Aug 22 02:13:58 Finished candle/overloading/semantics                         12m45s   2GB
Aug 22 02:13:58 Starting candle/overloading/monadic
Aug 22 02:16:43 Finished candle/overloading/monadic                            2m44s   2GB
Aug 22 02:16:43 Starting candle/overloading/ml_kernel
Aug 22 02:24:59 Finished candle/overloading/ml_kernel                          8m15s   4GB
Aug 22 02:24:59 Starting candle/overloading/ml_checker
Aug 22 02:28:04 Finished candle/overloading/ml_checker                         3m04s   4GB
Aug 22 02:28:04 Starting candle/prover
Aug 22 02:38:27 Finished candle/prover                                        10m22s   3GB
Aug 22 02:38:27 Starting pancake
Aug 22 02:39:17 Finished pancake                                                 50s   1GB
Aug 22 02:39:18 Starting pancake/ffi
Aug 22 02:39:18 Finished pancake/ffi                                              0s  13MB
Aug 22 02:39:18 Starting pancake/semantics
Aug 22 02:42:11 Finished pancake/semantics                                     2m52s   1GB
Aug 22 02:42:11 Starting pancake/parser
Aug 22 02:42:42 Finished pancake/parser                                          31s   1GB
Aug 22 02:42:42 Starting pancake/proofs
Aug 22 03:00:47 Finished pancake/proofs                                       18m04s   3GB
Aug 22 03:00:47 Starting characteristic/examples
Aug 22 03:02:27 Finished characteristic/examples                               1m39s   3GB
Aug 22 03:02:27 Starting tutorial/solutions
Aug 22 03:05:13 Finished tutorial/solutions                                    2m46s   3GB
Aug 22 03:05:13 Starting translator/monadic/examples
Aug 22 03:09:35 Finished translator/monadic/examples                           4m21s   3GB
Aug 22 03:09:35 Starting examples
Aug 22 03:26:14 Finished examples                                             16m38s   5GB
Aug 22 03:26:14 Starting examples/compilation/x64
Aug 22 03:35:15 Finished examples/compilation/x64                              9m00s   5GB
Aug 22 03:35:15 Starting examples/compilation/x64/proofs
Aug 22 03:38:11 Finished examples/compilation/x64/proofs                       2m55s   5GB
Aug 22 03:38:11 Starting examples/compilation/ag32
Aug 22 03:40:26 Finished examples/compilation/ag32                             2m15s   3GB
Aug 22 03:40:26 Starting examples/compilation/ag32/proofs
Aug 22 03:41:37 Finished examples/compilation/ag32/proofs                      1m10s   5GB
Aug 22 03:41:37 Starting examples/compilation/to_word
Aug 22 03:45:02 Finished examples/compilation/to_word                          3m25s   5GB
Aug 22 03:45:02 Starting examples/lpr_checker
Aug 22 03:46:12 Finished examples/lpr_checker                                  1m09s   1GB
Aug 22 03:46:12 Starting examples/lpr_checker/array
Aug 22 04:16:41 Finished examples/lpr_checker/array                           30m28s   7GB
Aug 22 04:16:41 Starting examples/lpr_checker/array/compilation
Aug 22 04:19:24 Finished examples/lpr_checker/array/compilation                2m42s   7GB
Aug 22 04:19:24 Starting examples/lpr_checker/array/compilation/proofs
Aug 22 04:20:42 Finished examples/lpr_checker/array/compilation/proofs         1m18s   5GB
Aug 22 04:20:42 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 22 04:22:02 Finished examples/lpr_checker/array/compilation/proofsARM8     1m19s   7GB
Aug 22 04:22:02 Starting examples/xlrup_checker
Aug 22 04:23:06 Finished examples/xlrup_checker                                1m04s   1GB
Aug 22 04:23:06 Starting examples/xlrup_checker/array
Aug 22 04:39:28 Finished examples/xlrup_checker/array                         16m21s   5GB
Aug 22 04:39:28 Starting examples/xlrup_checker/array/compilation
Aug 22 04:40:52 Finished examples/xlrup_checker/array/compilation              1m24s   4GB
Aug 22 04:40:52 Starting examples/xlrup_checker/array/compilation/proofs
Aug 22 04:41:57 Finished examples/xlrup_checker/array/compilation/proofs       1m04s   5GB
Aug 22 04:41:57 Starting examples/pseudo_bool
Aug 22 04:44:07 Finished examples/pseudo_bool                                  2m09s   1GB
Aug 22 04:44:07 Starting examples/pseudo_bool/cnf_encoding
Aug 22 04:44:36 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Aug 22 04:44:36 Starting examples/pseudo_bool/graph_encoding
Aug 22 04:45:22 Finished examples/pseudo_bool/graph_encoding                     45s   1GB
Aug 22 04:45:22 Starting examples/pseudo_bool/array
Aug 22 05:55:41 Finished examples/pseudo_bool/array                         1h10m18s   8GB
Aug 22 05:55:41 Starting examples/pseudo_bool/array/compilation
Aug 22 06:10:13 Finished examples/pseudo_bool/array/compilation               14m31s  26GB
Aug 22 06:10:13 Starting examples/pseudo_bool/array/compilation/proofs
Aug 22 06:13:12 Finished examples/pseudo_bool/array/compilation/proofs         2m58s   7GB
Aug 22 06:13:12 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 22 06:14:29 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m16s   6GB
Aug 22 06:14:29 Starting examples/opentheory
Aug 22 06:22:56 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                                                                                                                                                                                                                     (60s)     OK
Starting work on reader_initTheory
reader_initTheory                                                                                                                                                                                                                (28s)     OK
Starting work on readerProofTheory
readerProofTheory                                                                                                                                                                                                                (75s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                                                                                                                                                                            (24s)     OK
reader_commonProgTheory                                                                                                                                                                                                         (303s)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"}