Job 2293

CakeML:15a818af942b7e66d408173c0294c09f37103f91
  fix README [Feb 05 01:34:53]
#980 (xlrup)
Merging into:b76383b2a589101f171319130980075afdc90158
  Fix data_to_word_assignProof given integer$Num rewrites changes [Jan 30 06:21:36]
HOL:e1d4cc75edea2fa5a722e5775ffe85178b976b38
  Add a paragraph on Keccak to next-release [Feb 01 22:32:30]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Feb 07 19:59:12 Claimed job
Feb 07 19:59:25 Reusing HOL
Feb 07 20:00:07 Starting developers
Feb 07 20:00:13 Finished developers                                               5s 144MB
Feb 07 20:00:13 Starting developers/bin
Feb 07 20:00:20 Finished developers/bin                                           7s   1GB
Feb 07 20:00:20 Starting compiler/proofs
Feb 07 21:50:40 Finished compiler/proofs                                    1h50m19s  18GB
Feb 07 21:50:40 Starting compiler/bootstrap/translation
Feb 08 06:05:49 Finished compiler/bootstrap/translation                     8h15m08s  43GB
Feb 08 06:05:49 Starting semantics/ffi
Feb 08 06:05:54 Finished semantics/ffi                                            4s 376MB
Feb 08 06:05:54 Starting semantics
Feb 08 06:05:55 Finished semantics                                                1s  19MB
Feb 08 06:05:55 Starting semantics/proofs
Feb 08 06:06:28 Finished semantics/proofs                                        32s 729MB
Feb 08 06:06:28 Starting semantics/alt_semantics
Feb 08 06:07:01 Finished semantics/alt_semantics                                 32s 840MB
Feb 08 06:07:01 Starting semantics/alt_semantics/proofs
Feb 08 06:19:02 Finished semantics/alt_semantics/proofs                       12m01s   1GB
Feb 08 06:19:02 Starting basis/pure
Feb 08 06:19:04 Finished basis/pure                                               1s  23MB
Feb 08 06:19:04 Starting translator
Feb 08 06:20:54 Finished translator                                            1m49s   1GB
Feb 08 06:20:54 Starting compiler/parsing
Feb 08 06:20:56 Finished compiler/parsing                                         1s  18MB
Feb 08 06:20:56 Starting characteristic
Feb 08 06:20:58 Finished characteristic                                           1s  25MB
Feb 08 06:20:58 Starting translator/monadic
Feb 08 06:21:00 Finished translator/monadic                                       1s  22MB
Feb 08 06:21:00 Starting basis
Feb 08 06:24:50 Finished basis                                                 3m49s   2GB
Feb 08 06:24:50 Starting compiler/inference
Feb 08 06:24:52 Finished compiler/inference                                       1s  23MB
Feb 08 06:24:52 Starting compiler/backend/reg_alloc
Feb 08 06:24:53 Finished compiler/backend/reg_alloc                               1s  21MB
Feb 08 06:24:53 Starting compiler/backend/gc
Feb 08 06:24:56 Finished compiler/backend/gc                                      2s  23MB
Feb 08 06:24:56 Starting compiler/backend
Feb 08 06:25:09 Finished compiler/backend                                        12s 791MB
Feb 08 06:25:09 Starting compiler/encoders/asm
Feb 08 06:25:11 Finished compiler/encoders/asm                                    1s  24MB
Feb 08 06:25:11 Starting compiler/encoders/x64
Feb 08 06:25:13 Finished compiler/encoders/x64                                    1s  20MB
Feb 08 06:25:13 Starting compiler/encoders/arm7
Feb 08 06:25:15 Finished compiler/encoders/arm7                                   1s  24MB
Feb 08 06:25:15 Starting compiler/encoders/arm8
Feb 08 06:25:17 Finished compiler/encoders/arm8                                   1s  22MB
Feb 08 06:25:17 Starting compiler/encoders/arm8_asl
Feb 08 06:28:29 Finished compiler/encoders/arm8_asl                            3m12s   1GB
Feb 08 06:28:29 Starting compiler/encoders/mips
Feb 08 06:28:31 Finished compiler/encoders/mips                                   1s  23MB
Feb 08 06:28:31 Starting compiler/encoders/riscv
Feb 08 06:28:33 Finished compiler/encoders/riscv                                  1s  25MB
Feb 08 06:28:33 Starting compiler/encoders/ag32
Feb 08 06:28:35 Finished compiler/encoders/ag32                                   1s  21MB
Feb 08 06:28:35 Starting compiler/backend/x64
Feb 08 06:28:37 Finished compiler/backend/x64                                     2s  26MB
Feb 08 06:28:37 Starting compiler/backend/arm7
Feb 08 06:28:40 Finished compiler/backend/arm7                                    2s  32MB
Feb 08 06:28:40 Starting compiler/backend/arm8
Feb 08 06:28:42 Finished compiler/backend/arm8                                    2s  29MB
Feb 08 06:28:42 Starting compiler/backend/mips
Feb 08 06:28:44 Finished compiler/backend/mips                                    2s  26MB
Feb 08 06:28:45 Starting compiler/backend/riscv
Feb 08 06:28:47 Finished compiler/backend/riscv                                   2s  24MB
Feb 08 06:28:47 Starting compiler/backend/ag32
Feb 08 06:30:12 Finished compiler/backend/ag32                                 1m25s   1GB
Feb 08 06:30:12 Starting compiler/parsing/proofs
Feb 08 06:30:14 Finished compiler/parsing/proofs                                  1s  22MB
Feb 08 06:30:14 Starting compiler/inference/proofs
Feb 08 06:30:16 Finished compiler/inference/proofs                                1s  19MB
Feb 08 06:30:16 Starting compiler/backend/semantics
Feb 08 06:31:30 Finished compiler/backend/semantics                            1m13s   1GB
Feb 08 06:31:30 Starting compiler/backend/reg_alloc/proofs
Feb 08 06:31:32 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Feb 08 06:31:32 Starting compiler/backend/proofs
Feb 08 06:32:30 Finished compiler/backend/proofs                                 57s   2GB
Feb 08 06:32:30 Starting compiler/backend/serialiser
Feb 08 06:32:33 Finished compiler/backend/serialiser                              2s  33MB
Feb 08 06:32:33 Starting compiler/encoders/x64/proofs
Feb 08 06:42:26 Finished compiler/encoders/x64/proofs                          9m52s   6GB
Feb 08 06:42:26 Starting compiler/encoders/arm7/proofs
Feb 08 06:56:12 Finished compiler/encoders/arm7/proofs                        13m46s   3GB
Feb 08 06:56:12 Starting compiler/encoders/arm8/proofs
Feb 08 07:03:18 Finished compiler/encoders/arm8/proofs                         7m04s   1GB
Feb 08 07:03:18 Starting compiler/encoders/arm8_asl/proofs
Feb 08 07:18:51 Finished compiler/encoders/arm8_asl/proofs                    15m33s   2GB
Feb 08 07:18:52 Starting compiler/encoders/mips/proofs
Feb 08 07:29:33 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Feb 08 07:29:33 Starting compiler/encoders/riscv/proofs
Feb 08 07:38:35 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Feb 08 07:38:35 Starting compiler/encoders/ag32/proofs
Feb 08 07:41:10 Finished compiler/encoders/ag32/proofs                         2m35s 948MB
Feb 08 07:41:10 Starting compiler/backend/x64/proofs
Feb 08 07:41:41 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 08 07:41:41 Starting compiler/backend/arm7/proofs
Feb 08 07:42:15 Finished compiler/backend/arm7/proofs                            33s   2GB
Feb 08 07:42:15 Starting compiler/backend/arm8/proofs
Feb 08 07:42:44 Finished compiler/backend/arm8/proofs                            29s   1GB
Feb 08 07:42:44 Starting compiler/backend/arm8_asl
Feb 08 07:43:09 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 08 07:43:09 Starting compiler/backend/mips/proofs
Feb 08 07:43:41 Finished compiler/backend/mips/proofs                            31s   1GB
Feb 08 07:43:41 Starting compiler/backend/riscv/proofs
Feb 08 07:44:17 Finished compiler/backend/riscv/proofs                           35s   2GB
Feb 08 07:44:17 Starting compiler/backend/ag32/proofs
Feb 08 07:57:56 Finished compiler/backend/ag32/proofs                         13m39s   4GB
Feb 08 07:57:56 Starting candle/set-theory
Feb 08 07:58:36 Finished candle/set-theory                                       40s   1GB
Feb 08 07:58:36 Starting candle/syntax-lib
Feb 08 07:58:38 Finished candle/syntax-lib                                        1s  22MB
Feb 08 07:58:38 Starting candle/standard/syntax
Feb 08 07:58:49 Finished candle/standard/syntax                                  10s 792MB
Feb 08 07:58:49 Starting candle/standard/semantics
Feb 08 08:00:48 Finished candle/standard/semantics                             1m58s   1GB
Feb 08 08:00:48 Starting candle/standard/monadic
Feb 08 08:00:50 Finished candle/standard/monadic                                  1s  23MB
Feb 08 08:00:50 Starting candle/standard/ml_kernel
Feb 08 08:02:33 Finished candle/standard/ml_kernel                             1m42s   3GB
Feb 08 08:02:33 Starting candle/overloading/syntax
Feb 08 08:05:58 Finished candle/overloading/syntax                             3m24s   1GB
Feb 08 08:05:58 Starting candle/overloading/semantics
Feb 08 08:18:29 Finished candle/overloading/semantics                         12m31s   2GB
Feb 08 08:18:29 Starting candle/overloading/monadic
Feb 08 08:21:15 Finished candle/overloading/monadic                            2m45s   1GB
Feb 08 08:21:15 Starting candle/overloading/ml_kernel
Feb 08 08:29:12 Finished candle/overloading/ml_kernel                          7m57s   3GB
Feb 08 08:29:12 Starting candle/overloading/ml_checker
Feb 08 08:31:50 Finished candle/overloading/ml_checker                         2m37s   2GB
Feb 08 08:31:50 Starting candle/prover
Feb 08 08:41:52 Finished candle/prover                                        10m02s   4GB
Feb 08 08:41:52 Starting pancake
Feb 08 08:42:38 Finished pancake                                                 45s 871MB
Feb 08 08:42:38 Starting pancake/ffi
Feb 08 08:42:39 Finished pancake/ffi                                              0s  13MB
Feb 08 08:42:39 Starting pancake/semantics
Feb 08 08:45:11 Finished pancake/semantics                                     2m32s   1GB
Feb 08 08:45:11 Starting pancake/parser
Feb 08 08:45:34 Finished pancake/parser                                          23s   1GB
Feb 08 08:45:35 Starting pancake/proofs
Feb 08 09:19:25 Finished pancake/proofs                                       33m50s   7GB
Feb 08 09:19:25 Starting characteristic/examples
Feb 08 09:21:01 Finished characteristic/examples                               1m35s   2GB
Feb 08 09:21:01 Starting tutorial/solutions
Feb 08 09:36:17 Finished tutorial/solutions                                   15m16s   9GB
Feb 08 09:36:18 Starting translator/monadic/examples
Feb 08 09:40:21 Finished translator/monadic/examples                           4m03s   4GB
Feb 08 09:40:21 Starting examples
Feb 08 09:56:15 Finished examples                                             15m53s   4GB
Feb 08 09:56:15 Starting examples/compilation/x64
Feb 08 11:55:57 Finished examples/compilation/x64                           1h59m42s  21GB
Feb 08 11:55:57 Starting examples/compilation/x64/proofs
Feb 08 11:58:34 Finished examples/compilation/x64/proofs                       2m36s   4GB
Feb 08 11:58:34 Starting examples/compilation/ag32
Feb 08 12:29:09 Finished examples/compilation/ag32                            30m34s  10GB
Feb 08 12:29:09 Starting examples/compilation/ag32/proofs
Feb 08 12:30:10 Finished examples/compilation/ag32/proofs                      1m01s   4GB
Feb 08 12:30:10 Starting examples/compilation/to_word
Feb 08 12:33:31 Finished examples/compilation/to_word                          3m20s   4GB
Feb 08 12:33:31 Starting examples/lpr_checker
Feb 08 12:34:37 Finished examples/lpr_checker                                  1m05s   1GB
Feb 08 12:34:37 Starting examples/lpr_checker/array
Feb 08 13:05:58 Finished examples/lpr_checker/array                           31m20s   6GB
Feb 08 13:05:58 Starting examples/lpr_checker/array/compilation
Feb 08 13:58:09 Finished examples/lpr_checker/array/compilation               52m11s  22GB
Feb 08 13:58:09 Starting examples/lpr_checker/array/compilation/proofs
Feb 08 14:00:12 Finished examples/lpr_checker/array/compilation/proofs         2m02s   3GB
Feb 08 14:00:12 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 08 14:05:43 Finished examples/lpr_checker/array/compilation/proofsARM8     5m30s  17GB
Feb 08 14:05:43 Starting examples/xlrup_checker
Feb 08 14:05:59 FAILED: examples/xlrup_checker
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
Scanned 28 directories
Starting work on README.md
Starting work on cnf_xorTheory
README.md                                                                                                   (0s)     OK
cnf_xorTheory                                                                                              (13s)FAIL<1>
 Proof of 
 
 ys maxvar acc.
   EVERY (l. var_lit l  0  var_lit l  maxvar) ys 
   parse_lits_aux maxvar (toks (print_clause ys)) acc =
   SOME (REVERSE acc ++ ys)
 
 failed.
 Failed to prove theorem parse_lits_aux_print_clause.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 333)", origin_function = "THEN1", origin_structure = "Tactical"}