Job 2304

CakeML:078b5dabc339348758411ad4d46b392ba6ff8890
  remove _ from sexp op names [Feb 19 14:46:17]
#983 (fromsexpfix)
Merging into:647a11e7fd30db7a862d9655aa3abbb231c1e199
  Fix Candle breakage caused by HOL-Theorem-Prover/HOL@d64dda1e4e [Feb 20 01:19:56]
HOL:525694a1f1c7016dea954894bea6e6e396f7d6b3
  HolSmt: add unit tests for circular definitions [Feb 21 23:04:33]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Feb 25 18:18:33 Claimed job
Feb 25 18:18:37 Building HOL
Feb 25 18:31:33 Starting developers
Feb 25 18:31:38 Finished developers                                               5s 168MB
Feb 25 18:31:38 Starting developers/bin
Feb 25 18:31:45 Finished developers/bin                                           6s   1GB
Feb 25 18:31:45 Starting compiler/proofs
Feb 25 20:25:38 Finished compiler/proofs                                    1h53m53s  18GB
Feb 25 20:25:38 Starting compiler/bootstrap/translation
Feb 26 04:36:07 Finished compiler/bootstrap/translation                     8h10m28s  37GB
Feb 26 04:36:07 Starting semantics/ffi
Feb 26 04:36:13 Finished semantics/ffi                                            5s 210MB
Feb 26 04:36:13 Starting semantics
Feb 26 04:36:15 Finished semantics                                                1s  22MB
Feb 26 04:36:15 Starting semantics/proofs
Feb 26 04:36:50 Finished semantics/proofs                                        34s   1GB
Feb 26 04:36:50 Starting semantics/alt_semantics
Feb 26 04:37:22 Finished semantics/alt_semantics                                 31s 666MB
Feb 26 04:37:22 Starting semantics/alt_semantics/proofs
Feb 26 04:49:15 Finished semantics/alt_semantics/proofs                       11m52s   1GB
Feb 26 04:49:15 Starting basis/pure
Feb 26 04:49:16 Finished basis/pure                                               1s  21MB
Feb 26 04:49:17 Starting translator
Feb 26 04:51:06 Finished translator                                            1m49s   2GB
Feb 26 04:51:06 Starting compiler/parsing
Feb 26 04:51:08 Finished compiler/parsing                                         1s  18MB
Feb 26 04:51:08 Starting characteristic
Feb 26 04:51:10 Finished characteristic                                           1s  24MB
Feb 26 04:51:10 Starting translator/monadic
Feb 26 04:51:12 Finished translator/monadic                                       1s  24MB
Feb 26 04:51:12 Starting basis
Feb 26 04:54:56 Finished basis                                                 3m43s   2GB
Feb 26 04:54:56 Starting compiler/inference
Feb 26 04:54:58 Finished compiler/inference                                       1s  18MB
Feb 26 04:54:58 Starting compiler/backend/reg_alloc
Feb 26 04:54:59 Finished compiler/backend/reg_alloc                               1s  18MB
Feb 26 04:54:59 Starting compiler/backend/gc
Feb 26 04:55:02 Finished compiler/backend/gc                                      2s  33MB
Feb 26 04:55:02 Starting compiler/backend
Feb 26 04:55:14 Finished compiler/backend                                        12s 822MB
Feb 26 04:55:14 Starting compiler/encoders/asm
Feb 26 04:55:16 Finished compiler/encoders/asm                                    1s  20MB
Feb 26 04:55:16 Starting compiler/encoders/x64
Feb 26 04:55:18 Finished compiler/encoders/x64                                    1s  26MB
Feb 26 04:55:18 Starting compiler/encoders/arm7
Feb 26 04:55:20 Finished compiler/encoders/arm7                                   1s  24MB
Feb 26 04:55:20 Starting compiler/encoders/arm8
Feb 26 04:55:22 Finished compiler/encoders/arm8                                   1s  23MB
Feb 26 04:55:22 Starting compiler/encoders/arm8_asl
Feb 26 07:21:01 Finished compiler/encoders/arm8_asl                         2h25m39s  34GB
Feb 26 07:21:01 Starting compiler/encoders/mips
Feb 26 07:21:03 Finished compiler/encoders/mips                                   1s  24MB
Feb 26 07:21:03 Starting compiler/encoders/riscv
Feb 26 07:21:05 Finished compiler/encoders/riscv                                  1s  28MB
Feb 26 07:21:05 Starting compiler/encoders/ag32
Feb 26 07:21:07 Finished compiler/encoders/ag32                                   1s  24MB
Feb 26 07:21:07 Starting compiler/backend/x64
Feb 26 07:21:09 Finished compiler/backend/x64                                     2s  29MB
Feb 26 07:21:09 Starting compiler/backend/arm7
Feb 26 07:21:12 Finished compiler/backend/arm7                                    2s  25MB
Feb 26 07:21:12 Starting compiler/backend/arm8
Feb 26 07:21:14 Finished compiler/backend/arm8                                    2s  24MB
Feb 26 07:21:14 Starting compiler/backend/mips
Feb 26 07:21:17 Finished compiler/backend/mips                                    2s  26MB
Feb 26 07:21:17 Starting compiler/backend/riscv
Feb 26 07:21:19 Finished compiler/backend/riscv                                   2s  24MB
Feb 26 07:21:19 Starting compiler/backend/ag32
Feb 26 07:22:45 Finished compiler/backend/ag32                                 1m25s   1GB
Feb 26 07:22:45 Starting compiler/parsing/proofs
Feb 26 07:22:46 Finished compiler/parsing/proofs                                  1s  22MB
Feb 26 07:22:47 Starting compiler/inference/proofs
Feb 26 07:22:48 Finished compiler/inference/proofs                                1s  22MB
Feb 26 07:22:49 Starting compiler/backend/semantics
Feb 26 07:24:04 Finished compiler/backend/semantics                            1m15s   1GB
Feb 26 07:24:04 Starting compiler/backend/reg_alloc/proofs
Feb 26 07:24:06 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Feb 26 07:24:06 Starting compiler/backend/proofs
Feb 26 07:25:05 Finished compiler/backend/proofs                                 58s   2GB
Feb 26 07:25:05 Starting compiler/backend/serialiser
Feb 26 07:25:08 Finished compiler/backend/serialiser                              2s  30MB
Feb 26 07:25:08 Starting compiler/encoders/x64/proofs
Feb 26 07:34:56 Finished compiler/encoders/x64/proofs                          9m47s   6GB
Feb 26 07:34:56 Starting compiler/encoders/arm7/proofs
Feb 26 07:48:59 Finished compiler/encoders/arm7/proofs                        14m02s   4GB
Feb 26 07:48:59 Starting compiler/encoders/arm8/proofs
Feb 26 07:56:02 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Feb 26 07:56:02 Starting compiler/encoders/arm8_asl/proofs
Feb 26 08:48:33 Finished compiler/encoders/arm8_asl/proofs                    52m30s   5GB
Feb 26 08:48:33 Starting compiler/encoders/mips/proofs
Feb 26 08:59:20 Finished compiler/encoders/mips/proofs                        10m46s   2GB
Feb 26 08:59:20 Starting compiler/encoders/riscv/proofs
Feb 26 09:08:15 Finished compiler/encoders/riscv/proofs                        8m55s   1GB
Feb 26 09:08:16 Starting compiler/encoders/ag32/proofs
Feb 26 09:10:47 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Feb 26 09:10:47 Starting compiler/backend/x64/proofs
Feb 26 09:11:17 Finished compiler/backend/x64/proofs                             29s   1GB
Feb 26 09:11:17 Starting compiler/backend/arm7/proofs
Feb 26 09:11:52 Finished compiler/backend/arm7/proofs                            34s   2GB
Feb 26 09:11:52 Starting compiler/backend/arm8/proofs
Feb 26 09:12:24 Finished compiler/backend/arm8/proofs                            31s   2GB
Feb 26 09:12:24 Starting compiler/backend/arm8_asl
Feb 26 09:12:49 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 26 09:12:49 Starting compiler/backend/mips/proofs
Feb 26 09:13:21 Finished compiler/backend/mips/proofs                            32s   2GB
Feb 26 09:13:21 Starting compiler/backend/riscv/proofs
Feb 26 09:13:55 Finished compiler/backend/riscv/proofs                           34s   2GB
Feb 26 09:13:55 Starting compiler/backend/ag32/proofs
Feb 26 09:27:57 Finished compiler/backend/ag32/proofs                         14m01s   2GB
Feb 26 09:27:57 Starting candle/set-theory
Feb 26 09:28:35 Finished candle/set-theory                                       38s   1GB
Feb 26 09:28:36 Starting candle/syntax-lib
Feb 26 09:28:37 Finished candle/syntax-lib                                        1s  19MB
Feb 26 09:28:37 Starting candle/standard/syntax
Feb 26 09:28:48 Finished candle/standard/syntax                                  10s 767MB
Feb 26 09:28:48 Starting candle/standard/semantics
Feb 26 09:30:49 Finished candle/standard/semantics                             2m00s   1GB
Feb 26 09:30:49 Starting candle/standard/monadic
Feb 26 09:30:51 Finished candle/standard/monadic                                  1s  21MB
Feb 26 09:30:51 Starting candle/standard/ml_kernel
Feb 26 09:32:28 Finished candle/standard/ml_kernel                             1m36s   3GB
Feb 26 09:32:28 Starting candle/overloading/syntax
Feb 26 09:35:53 Finished candle/overloading/syntax                             3m24s   1GB
Feb 26 09:35:53 Starting candle/overloading/semantics
Feb 26 09:48:08 Finished candle/overloading/semantics                         12m15s   2GB
Feb 26 09:48:08 Starting candle/overloading/monadic
Feb 26 09:50:54 Finished candle/overloading/monadic                            2m45s   1GB
Feb 26 09:50:54 Starting candle/overloading/ml_kernel
Feb 26 09:58:49 Finished candle/overloading/ml_kernel                          7m54s   5GB
Feb 26 09:58:49 Starting candle/overloading/ml_checker
Feb 26 10:01:29 Finished candle/overloading/ml_checker                         2m39s   2GB
Feb 26 10:01:29 Starting candle/prover
Feb 26 10:11:36 Finished candle/prover                                        10m07s   3GB
Feb 26 10:11:36 Starting pancake
Feb 26 10:12:22 Finished pancake                                                 45s 868MB
Feb 26 10:12:22 Starting pancake/ffi
Feb 26 10:12:22 Finished pancake/ffi                                              0s  13MB
Feb 26 10:12:23 Starting pancake/semantics
Feb 26 10:14:50 Finished pancake/semantics                                     2m27s   1GB
Feb 26 10:14:50 Starting pancake/parser
Feb 26 10:15:13 Finished pancake/parser                                          22s 649MB
Feb 26 10:15:13 Starting pancake/proofs
Feb 26 10:48:50 Finished pancake/proofs                                       33m36s   5GB
Feb 26 10:48:50 Starting characteristic/examples
Feb 26 10:50:25 Finished characteristic/examples                               1m35s   2GB
Feb 26 10:50:25 Starting tutorial/solutions
Feb 26 11:05:47 Finished tutorial/solutions                                   15m21s   8GB
Feb 26 11:05:48 Starting translator/monadic/examples
Feb 26 11:09:57 Finished translator/monadic/examples                           4m09s   2GB
Feb 26 11:09:58 Starting examples
Feb 26 11:26:16 Finished examples                                             16m18s   4GB
Feb 26 11:26:16 Starting examples/compilation/x64
Feb 26 13:26:02 Finished examples/compilation/x64                           1h59m45s  18GB
Feb 26 13:26:02 Starting examples/compilation/x64/proofs
Feb 26 13:28:37 Finished examples/compilation/x64/proofs                       2m34s   4GB
Feb 26 13:28:37 Starting examples/compilation/ag32
Feb 26 13:59:19 Finished examples/compilation/ag32                            30m41s   7GB
Feb 26 13:59:19 Starting examples/compilation/ag32/proofs
Feb 26 14:00:24 Finished examples/compilation/ag32/proofs                      1m05s   4GB
Feb 26 14:00:24 Starting examples/compilation/to_word
Feb 26 14:03:48 Finished examples/compilation/to_word                          3m24s   6GB
Feb 26 14:03:48 Starting examples/lpr_checker
Feb 26 14:04:53 Finished examples/lpr_checker                                  1m04s   1GB
Feb 26 14:04:53 Starting examples/lpr_checker/array
Feb 26 14:36:08 Finished examples/lpr_checker/array                           31m15s   5GB
Feb 26 14:36:08 Starting examples/lpr_checker/array/compilation
Feb 26 15:27:55 Finished examples/lpr_checker/array/compilation               51m46s  26GB
Feb 26 15:27:55 Starting examples/lpr_checker/array/compilation/proofs
Feb 26 15:29:59 Finished examples/lpr_checker/array/compilation/proofs         2m03s   3GB
Feb 26 15:29:59 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 26 15:35:47 Finished examples/lpr_checker/array/compilation/proofsARM8     5m48s  21GB
Feb 26 15:35:47 Starting examples/xlrup_checker
Feb 26 16:48:58 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                                                                                              (37m)FAIL<Signal 9>
 Saved definition ____ "print_clause_def"
 Saved definition ____ "print_xor_def"
 Saved definition ____ "print_header_line_def"
 Saved definition ____ "var_lit_def"
 Saved definition ____ "max_list_def"
 Saved definition ____ "print_cnf_xor_def"
 Saved theorem _______ "tokens_unchanged"
 Proved triviality _ "isDigit_not_blanks"
 Saved theorem _______ "tokens_blanks_print_lit"
 Saved theorem _______ "tokens_print_clause_nonempty"