Job 2376

CakeML:b28ac1dedcc965edf5e1813a72d1437aae9c8be0
  Fix cf proofs in compiler [Apr 22 19:26:31]
#992 (cf-fixes)
Merging into:9c063a7d92cadb36c49a6e45856ae0db734dc9e5
  Merge pull request #989 from CakeML/pan_errors [Apr 11 22:24:05]
HOL:12c611b12123da645e2d6dc86f640fe6cf52a981
  Fix Holmakefile INCLUDES error causing unnecessary HOL rebuilds [Apr 19 12:17:55]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Apr 24 05:26:51 Claimed job
Apr 24 05:26:56 Reusing HOL
Apr 24 05:27:39 Starting developers
Apr 24 05:27:44 Finished developers                                               5s 152MB
Apr 24 05:27:44 Starting developers/bin
Apr 24 05:27:50 Finished developers/bin                                           6s   1GB
Apr 24 05:27:50 Starting compiler/proofs
Apr 24 07:25:43 Finished compiler/proofs                                    1h57m52s  16GB
Apr 24 07:25:43 Starting compiler/bootstrap/translation
Apr 24 15:48:26 Finished compiler/bootstrap/translation                     8h22m43s  45GB
Apr 24 15:48:27 Starting semantics/ffi
Apr 24 15:48:33 Finished semantics/ffi                                            5s 210MB
Apr 24 15:48:33 Starting semantics
Apr 24 15:48:34 Finished semantics                                                1s  21MB
Apr 24 15:48:34 Starting semantics/proofs
Apr 24 15:49:07 Finished semantics/proofs                                        32s 785MB
Apr 24 15:49:07 Starting semantics/alt_semantics
Apr 24 15:49:39 Finished semantics/alt_semantics                                 31s 749MB
Apr 24 15:49:39 Starting semantics/alt_semantics/proofs
Apr 24 16:01:38 Finished semantics/alt_semantics/proofs                       11m58s   1GB
Apr 24 16:01:38 Starting basis/pure
Apr 24 16:01:40 Finished basis/pure                                               1s  18MB
Apr 24 16:01:40 Starting translator
Apr 24 16:03:29 Finished translator                                            1m48s   2GB
Apr 24 16:03:29 Starting compiler/parsing
Apr 24 16:03:30 Finished compiler/parsing                                         1s  19MB
Apr 24 16:03:30 Starting characteristic
Apr 24 16:03:32 Finished characteristic                                           1s  22MB
Apr 24 16:03:32 Starting translator/monadic
Apr 24 16:03:34 Finished translator/monadic                                       1s  25MB
Apr 24 16:03:34 Starting basis
Apr 24 16:07:11 Finished basis                                                 3m36s   3GB
Apr 24 16:07:11 Starting compiler/inference
Apr 24 16:07:12 Finished compiler/inference                                       1s  20MB
Apr 24 16:07:12 Starting compiler/backend/reg_alloc
Apr 24 16:07:14 Finished compiler/backend/reg_alloc                               1s  19MB
Apr 24 16:07:14 Starting compiler/backend/gc
Apr 24 16:07:17 Finished compiler/backend/gc                                      2s  25MB
Apr 24 16:07:17 Starting compiler/backend
Apr 24 16:07:30 Finished compiler/backend                                        13s 845MB
Apr 24 16:07:30 Starting compiler/encoders/asm
Apr 24 16:07:32 Finished compiler/encoders/asm                                    1s  21MB
Apr 24 16:07:32 Starting compiler/encoders/x64
Apr 24 16:07:34 Finished compiler/encoders/x64                                    1s  23MB
Apr 24 16:07:34 Starting compiler/encoders/arm7
Apr 24 16:07:36 Finished compiler/encoders/arm7                                   1s  22MB
Apr 24 16:07:36 Starting compiler/encoders/arm8
Apr 24 16:07:38 Finished compiler/encoders/arm8                                   1s  23MB
Apr 24 16:07:38 Starting compiler/encoders/arm8_asl
Apr 24 16:10:50 Finished compiler/encoders/arm8_asl                            3m11s   1GB
Apr 24 16:10:50 Starting compiler/encoders/mips
Apr 24 16:10:52 Finished compiler/encoders/mips                                   1s  24MB
Apr 24 16:10:52 Starting compiler/encoders/riscv
Apr 24 16:10:54 Finished compiler/encoders/riscv                                  1s  28MB
Apr 24 16:10:54 Starting compiler/encoders/ag32
Apr 24 16:10:55 Finished compiler/encoders/ag32                                   1s  22MB
Apr 24 16:10:56 Starting compiler/backend/x64
Apr 24 16:10:58 Finished compiler/backend/x64                                     2s  30MB
Apr 24 16:10:58 Starting compiler/backend/arm7
Apr 24 16:11:00 Finished compiler/backend/arm7                                    2s  25MB
Apr 24 16:11:00 Starting compiler/backend/arm8
Apr 24 16:11:03 Finished compiler/backend/arm8                                    2s  26MB
Apr 24 16:11:03 Starting compiler/backend/mips
Apr 24 16:11:05 Finished compiler/backend/mips                                    2s  22MB
Apr 24 16:11:05 Starting compiler/backend/riscv
Apr 24 16:11:07 Finished compiler/backend/riscv                                   2s  31MB
Apr 24 16:11:07 Starting compiler/backend/ag32
Apr 24 16:12:33 Finished compiler/backend/ag32                                 1m25s   1GB
Apr 24 16:12:33 Starting compiler/parsing/proofs
Apr 24 16:12:34 Finished compiler/parsing/proofs                                  1s  18MB
Apr 24 16:12:35 Starting compiler/inference/proofs
Apr 24 16:12:36 Finished compiler/inference/proofs                                1s  20MB
Apr 24 16:12:36 Starting compiler/backend/semantics
Apr 24 16:16:25 Finished compiler/backend/semantics                            3m48s   1GB
Apr 24 16:16:26 Starting compiler/backend/reg_alloc/proofs
Apr 24 16:16:28 Finished compiler/backend/reg_alloc/proofs                        1s  19MB
Apr 24 16:16:28 Starting compiler/backend/proofs
Apr 24 16:17:29 Finished compiler/backend/proofs                               1m01s   2GB
Apr 24 16:17:29 Starting compiler/backend/serialiser
Apr 24 16:17:32 Finished compiler/backend/serialiser                              2s  32MB
Apr 24 16:17:32 Starting compiler/encoders/x64/proofs
Apr 24 16:27:22 Finished compiler/encoders/x64/proofs                          9m49s   4GB
Apr 24 16:27:22 Starting compiler/encoders/arm7/proofs
Apr 24 16:41:08 Finished compiler/encoders/arm7/proofs                        13m46s   3GB
Apr 24 16:41:08 Starting compiler/encoders/arm8/proofs
Apr 24 16:48:07 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Apr 24 16:48:07 Starting compiler/encoders/arm8_asl/proofs
Apr 24 17:03:50 Finished compiler/encoders/arm8_asl/proofs                    15m42s   2GB
Apr 24 17:03:50 Starting compiler/encoders/mips/proofs
Apr 24 17:14:28 Finished compiler/encoders/mips/proofs                        10m37s   2GB
Apr 24 17:14:28 Starting compiler/encoders/riscv/proofs
Apr 24 17:23:28 Finished compiler/encoders/riscv/proofs                        9m00s   1GB
Apr 24 17:23:29 Starting compiler/encoders/ag32/proofs
Apr 24 17:25:58 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Apr 24 17:25:58 Starting compiler/backend/x64/proofs
Apr 24 17:26:30 Finished compiler/backend/x64/proofs                             31s   2GB
Apr 24 17:26:30 Starting compiler/backend/arm7/proofs
Apr 24 17:27:03 Finished compiler/backend/arm7/proofs                            33s   2GB
Apr 24 17:27:03 Starting compiler/backend/arm8/proofs
Apr 24 17:27:34 Finished compiler/backend/arm8/proofs                            30s   2GB
Apr 24 17:27:35 Starting compiler/backend/arm8_asl
Apr 24 17:27:59 Finished compiler/backend/arm8_asl                               24s   1GB
Apr 24 17:27:59 Starting compiler/backend/mips/proofs
Apr 24 17:28:32 Finished compiler/backend/mips/proofs                            32s   1GB
Apr 24 17:28:32 Starting compiler/backend/riscv/proofs
Apr 24 17:29:06 Finished compiler/backend/riscv/proofs                           34s   1GB
Apr 24 17:29:06 Starting compiler/backend/ag32/proofs
Apr 24 17:43:39 Finished compiler/backend/ag32/proofs                         14m32s   3GB
Apr 24 17:43:39 Starting candle/set-theory
Apr 24 17:44:19 Finished candle/set-theory                                       39s   1GB
Apr 24 17:44:19 Starting candle/syntax-lib
Apr 24 17:44:20 Finished candle/syntax-lib                                        1s  17MB
Apr 24 17:44:21 Starting candle/standard/syntax
Apr 24 17:44:31 Finished candle/standard/syntax                                  10s 782MB
Apr 24 17:44:31 Starting candle/standard/semantics
Apr 24 17:46:29 Finished candle/standard/semantics                             1m58s   1GB
Apr 24 17:46:29 Starting candle/standard/monadic
Apr 24 17:46:31 Finished candle/standard/monadic                                  1s  20MB
Apr 24 17:46:31 Starting candle/standard/ml_kernel
Apr 24 17:48:11 Finished candle/standard/ml_kernel                             1m39s   2GB
Apr 24 17:48:11 Starting candle/overloading/syntax
Apr 24 17:51:36 Finished candle/overloading/syntax                             3m24s   1GB
Apr 24 17:51:36 Starting candle/overloading/semantics
Apr 24 18:04:08 Finished candle/overloading/semantics                         12m31s   2GB
Apr 24 18:04:08 Starting candle/overloading/monadic
Apr 24 18:06:52 Finished candle/overloading/monadic                            2m43s   1GB
Apr 24 18:06:52 Starting candle/overloading/ml_kernel
Apr 24 18:14:54 Finished candle/overloading/ml_kernel                          8m02s   4GB
Apr 24 18:14:54 Starting candle/overloading/ml_checker
Apr 24 18:17:28 Finished candle/overloading/ml_checker                         2m33s   3GB
Apr 24 18:17:28 Starting candle/prover
Apr 24 18:27:31 Finished candle/prover                                        10m03s   3GB
Apr 24 18:27:31 Starting pancake
Apr 24 18:28:16 Finished pancake                                                 45s 866MB
Apr 24 18:28:16 Starting pancake/ffi
Apr 24 18:28:17 Finished pancake/ffi                                              0s  13MB
Apr 24 18:28:17 Starting pancake/semantics
Apr 24 18:31:00 Finished pancake/semantics                                     2m42s   1GB
Apr 24 18:31:00 Starting pancake/parser
Apr 24 18:31:25 Finished pancake/parser                                          25s 630MB
Apr 24 18:31:25 Starting pancake/proofs
Apr 24 19:05:58 Finished pancake/proofs                                       34m32s   5GB
Apr 24 19:05:58 Starting characteristic/examples
Apr 24 19:07:31 Finished characteristic/examples                               1m33s   3GB
Apr 24 19:07:31 Starting tutorial/solutions
Apr 24 19:22:55 Finished tutorial/solutions                                   15m23s   9GB
Apr 24 19:22:55 Starting translator/monadic/examples
Apr 24 19:27:08 Finished translator/monadic/examples                           4m12s   3GB
Apr 24 19:27:08 Starting examples
Apr 24 19:42:47 Finished examples                                             15m38s   4GB
Apr 24 19:42:47 Starting examples/compilation/x64
Apr 24 21:45:15 Finished examples/compilation/x64                           2h02m27s  21GB
Apr 24 21:45:15 Starting examples/compilation/x64/proofs
Apr 24 21:47:53 Finished examples/compilation/x64/proofs                       2m38s   4GB
Apr 24 21:47:53 Starting examples/compilation/ag32
Apr 24 22:19:02 Finished examples/compilation/ag32                            31m08s   8GB
Apr 24 22:19:02 Starting examples/compilation/ag32/proofs
Apr 24 22:20:06 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Apr 24 22:20:06 Starting examples/compilation/to_word
Apr 24 22:23:33 Finished examples/compilation/to_word                          3m26s   6GB
Apr 24 22:23:33 Starting examples/lpr_checker
Apr 24 22:24:38 Finished examples/lpr_checker                                  1m04s   1GB
Apr 24 22:24:38 Starting examples/lpr_checker/array
Apr 24 22:55:07 Finished examples/lpr_checker/array                           30m29s   6GB
Apr 24 22:55:07 Starting examples/lpr_checker/array/compilation
Apr 24 23:54:17 Finished examples/lpr_checker/array/compilation               59m09s  35GB
Apr 24 23:54:17 Starting examples/lpr_checker/array/compilation/proofs
Apr 24 23:56:04 Finished examples/lpr_checker/array/compilation/proofs         1m46s   3GB
Apr 24 23:56:04 Starting examples/lpr_checker/array/compilation/proofsARM8
Apr 25 00:01:39 Finished examples/lpr_checker/array/compilation/proofsARM8     5m35s  20GB
Apr 25 00:01:39 Starting examples/xlrup_checker
Apr 25 00:02:38 Finished examples/xlrup_checker                                  58s   1GB
Apr 25 00:02:38 Starting examples/xlrup_checker/array
Apr 25 00:18:45 Finished examples/xlrup_checker/array                         16m06s   4GB
Apr 25 00:18:46 Starting examples/xlrup_checker/array/compilation
Apr 25 00:40:56 Finished examples/xlrup_checker/array/compilation             22m10s  16GB
Apr 25 00:40:57 Starting examples/xlrup_checker/array/compilation/proofs
Apr 25 00:42:03 Finished examples/xlrup_checker/array/compilation/proofs       1m06s   5GB
Apr 25 00:42:03 Starting examples/pseudo_bool
Apr 25 00:44:00 Finished examples/pseudo_bool                                  1m56s   1GB
Apr 25 00:44:00 Starting examples/pseudo_bool/cnf_encoding
Apr 25 00:44:27 Finished examples/pseudo_bool/cnf_encoding                       27s 865MB
Apr 25 00:44:27 Starting examples/pseudo_bool/graph_encoding
Apr 25 00:45:10 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Apr 25 00:45:10 Starting examples/pseudo_bool/array
Apr 25 01:15:07 FAILED: examples/pseudo_bool/array
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/algorithms[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$(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$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/cnf_encoding[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/graph_encoding[0m
Scanned 40 directories
Starting work on README.md
Starting work on npbc_listTheory
README.md                                                                                                   (0s)     OK
npbc_listTheory                                                                                           (104s)     OK
Starting work on npbc_arrayProgTheory
npbc_arrayProgTheory                                                                                       (27m)FAIL<1>
 
 ls lsv accv accls.
   LIST_TYPE (PAIR_TYPE INT NUM) ls lsv 
   app p fold_update_resize_bitset_v [lsv; accv] (W8ARRAY accv accls)
     (POSTv v.
        W8ARRAY v (FOLDL (acc (c,i). update_resize acc w8z w8o i) accls ls))
 
 failed.
 Failed to prove theorem fold_update_resize_bitset_spec.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 3856)", origin_function = "THEN1", origin_structure = "Tactical"}