Job 2298

CakeML:806f5da2e637d64185fcd2d143e3acef62800f6e
  Merge remote-tracking branch 'origin/master' into alist_subst [Feb 08 07:52:47]
#981 (alist_subst)
Merging into:85f6656cc53ec1a72c2808e01f7dec102e8972df
  Merge pull request #980 from CakeML/xlrup [Feb 13 11:56:12]
HOL:c5f2bc287fa6507cfb3372b4b827105b9633636b
  Other cheatsheet additions: `iff_tac`/`eq_tac` and `ExclSF` [Feb 08 23:51:55]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Feb 13 11:57:58 Claimed job
Feb 13 11:58:05 Reusing HOL
Feb 13 11:58:46 Starting developers
Feb 13 11:58:51 Finished developers                                               5s 136MB
Feb 13 11:58:52 Starting developers/bin
Feb 13 11:58:58 Finished developers/bin                                           6s   1GB
Feb 13 11:58:58 Starting compiler/proofs
Feb 13 13:49:13 Finished compiler/proofs                                    1h50m15s  18GB
Feb 13 13:49:14 Starting compiler/bootstrap/translation
Feb 13 22:03:15 Finished compiler/bootstrap/translation                     8h14m00s  49GB
Feb 13 22:03:15 Starting semantics/ffi
Feb 13 22:03:20 Finished semantics/ffi                                            4s 383MB
Feb 13 22:03:20 Starting semantics
Feb 13 22:03:21 Finished semantics                                                1s  19MB
Feb 13 22:03:22 Starting semantics/proofs
Feb 13 22:03:55 Finished semantics/proofs                                        33s 730MB
Feb 13 22:03:55 Starting semantics/alt_semantics
Feb 13 22:04:27 Finished semantics/alt_semantics                                 32s 749MB
Feb 13 22:04:27 Starting semantics/alt_semantics/proofs
Feb 13 22:16:27 Finished semantics/alt_semantics/proofs                       12m00s   1GB
Feb 13 22:16:28 Starting basis/pure
Feb 13 22:16:29 Finished basis/pure                                               1s  18MB
Feb 13 22:16:29 Starting translator
Feb 13 22:18:20 Finished translator                                            1m50s   1GB
Feb 13 22:18:20 Starting compiler/parsing
Feb 13 22:18:22 Finished compiler/parsing                                         1s  18MB
Feb 13 22:18:22 Starting characteristic
Feb 13 22:18:24 Finished characteristic                                           1s  29MB
Feb 13 22:18:24 Starting translator/monadic
Feb 13 22:18:26 Finished translator/monadic                                       1s  21MB
Feb 13 22:18:26 Starting basis
Feb 13 22:22:07 Finished basis                                                 3m41s   3GB
Feb 13 22:22:07 Starting compiler/inference
Feb 13 22:22:09 Finished compiler/inference                                       1s  21MB
Feb 13 22:22:09 Starting compiler/backend/reg_alloc
Feb 13 22:22:11 Finished compiler/backend/reg_alloc                               1s  18MB
Feb 13 22:22:11 Starting compiler/backend/gc
Feb 13 22:22:13 Finished compiler/backend/gc                                      2s  25MB
Feb 13 22:22:13 Starting compiler/backend
Feb 13 22:22:26 Finished compiler/backend                                        12s 856MB
Feb 13 22:22:26 Starting compiler/encoders/asm
Feb 13 22:22:28 Finished compiler/encoders/asm                                    1s  23MB
Feb 13 22:22:28 Starting compiler/encoders/x64
Feb 13 22:22:30 Finished compiler/encoders/x64                                    1s  21MB
Feb 13 22:22:30 Starting compiler/encoders/arm7
Feb 13 22:22:32 Finished compiler/encoders/arm7                                   1s  24MB
Feb 13 22:22:32 Starting compiler/encoders/arm8
Feb 13 22:22:34 Finished compiler/encoders/arm8                                   1s  23MB
Feb 13 22:22:34 Starting compiler/encoders/arm8_asl
Feb 13 22:25:48 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Feb 13 22:25:49 Starting compiler/encoders/mips
Feb 13 22:25:50 Finished compiler/encoders/mips                                   1s  22MB
Feb 13 22:25:50 Starting compiler/encoders/riscv
Feb 13 22:25:52 Finished compiler/encoders/riscv                                  1s  24MB
Feb 13 22:25:52 Starting compiler/encoders/ag32
Feb 13 22:25:54 Finished compiler/encoders/ag32                                   1s  20MB
Feb 13 22:25:54 Starting compiler/backend/x64
Feb 13 22:25:56 Finished compiler/backend/x64                                     2s  29MB
Feb 13 22:25:57 Starting compiler/backend/arm7
Feb 13 22:25:59 Finished compiler/backend/arm7                                    2s  27MB
Feb 13 22:25:59 Starting compiler/backend/arm8
Feb 13 22:26:01 Finished compiler/backend/arm8                                    2s  24MB
Feb 13 22:26:01 Starting compiler/backend/mips
Feb 13 22:26:04 Finished compiler/backend/mips                                    2s  21MB
Feb 13 22:26:04 Starting compiler/backend/riscv
Feb 13 22:26:06 Finished compiler/backend/riscv                                   2s  26MB
Feb 13 22:26:06 Starting compiler/backend/ag32
Feb 13 22:27:30 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 13 22:27:30 Starting compiler/parsing/proofs
Feb 13 22:27:32 Finished compiler/parsing/proofs                                  1s  20MB
Feb 13 22:27:32 Starting compiler/inference/proofs
Feb 13 22:27:34 Finished compiler/inference/proofs                                1s  20MB
Feb 13 22:27:34 Starting compiler/backend/semantics
Feb 13 22:28:47 Finished compiler/backend/semantics                            1m13s   1GB
Feb 13 22:28:48 Starting compiler/backend/reg_alloc/proofs
Feb 13 22:28:50 Finished compiler/backend/reg_alloc/proofs                        1s  27MB
Feb 13 22:28:50 Starting compiler/backend/proofs
Feb 13 22:29:50 Finished compiler/backend/proofs                               1m00s   3GB
Feb 13 22:29:50 Starting compiler/backend/serialiser
Feb 13 22:29:53 Finished compiler/backend/serialiser                              2s  31MB
Feb 13 22:29:53 Starting compiler/encoders/x64/proofs
Feb 13 22:39:46 Finished compiler/encoders/x64/proofs                          9m52s   5GB
Feb 13 22:39:46 Starting compiler/encoders/arm7/proofs
Feb 13 22:53:30 Finished compiler/encoders/arm7/proofs                        13m44s   4GB
Feb 13 22:53:30 Starting compiler/encoders/arm8/proofs
Feb 13 23:00:26 Finished compiler/encoders/arm8/proofs                         6m55s   1GB
Feb 13 23:00:26 Starting compiler/encoders/arm8_asl/proofs
Feb 13 23:15:45 Finished compiler/encoders/arm8_asl/proofs                    15m19s   2GB
Feb 13 23:15:46 Starting compiler/encoders/mips/proofs
Feb 13 23:26:33 Finished compiler/encoders/mips/proofs                        10m47s   2GB
Feb 13 23:26:33 Starting compiler/encoders/riscv/proofs
Feb 13 23:35:39 Finished compiler/encoders/riscv/proofs                        9m06s   1GB
Feb 13 23:35:39 Starting compiler/encoders/ag32/proofs
Feb 13 23:38:11 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Feb 13 23:38:11 Starting compiler/backend/x64/proofs
Feb 13 23:38:42 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 13 23:38:42 Starting compiler/backend/arm7/proofs
Feb 13 23:39:14 Finished compiler/backend/arm7/proofs                            31s   2GB
Feb 13 23:39:14 Starting compiler/backend/arm8/proofs
Feb 13 23:39:45 Finished compiler/backend/arm8/proofs                            30s   1GB
Feb 13 23:39:45 Starting compiler/backend/arm8_asl
Feb 13 23:40:09 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 13 23:40:09 Starting compiler/backend/mips/proofs
Feb 13 23:40:44 Finished compiler/backend/mips/proofs                            34s   2GB
Feb 13 23:40:44 Starting compiler/backend/riscv/proofs
Feb 13 23:41:17 Finished compiler/backend/riscv/proofs                           32s   1GB
Feb 13 23:41:17 Starting compiler/backend/ag32/proofs
Feb 13 23:55:17 Finished compiler/backend/ag32/proofs                         13m59s   2GB
Feb 13 23:55:17 Starting candle/set-theory
Feb 13 23:55:56 Finished candle/set-theory                                       39s   1GB
Feb 13 23:55:56 Starting candle/syntax-lib
Feb 13 23:55:58 Finished candle/syntax-lib                                        1s  22MB
Feb 13 23:55:58 Starting candle/standard/syntax
Feb 13 23:56:09 Finished candle/standard/syntax                                  10s 757MB
Feb 13 23:56:09 Starting candle/standard/semantics
Feb 13 23:58:07 Finished candle/standard/semantics                             1m58s   1GB
Feb 13 23:58:07 Starting candle/standard/monadic
Feb 13 23:58:09 Finished candle/standard/monadic                                  1s  27MB
Feb 13 23:58:09 Starting candle/standard/ml_kernel
Feb 13 23:59:54 Finished candle/standard/ml_kernel                             1m44s   3GB
Feb 13 23:59:54 Starting candle/overloading/syntax
Feb 14 00:03:17 Finished candle/overloading/syntax                             3m22s   1GB
Feb 14 00:03:17 Starting candle/overloading/semantics
Feb 14 00:15:30 Finished candle/overloading/semantics                         12m12s   4GB
Feb 14 00:15:30 Starting candle/overloading/monadic
Feb 14 00:18:15 Finished candle/overloading/monadic                            2m44s   1GB
Feb 14 00:18:15 Starting candle/overloading/ml_kernel
Feb 14 00:26:16 Finished candle/overloading/ml_kernel                          8m00s   3GB
Feb 14 00:26:16 Starting candle/overloading/ml_checker
Feb 14 00:28:52 Finished candle/overloading/ml_checker                         2m35s   2GB
Feb 14 00:28:52 Starting candle/prover
Feb 14 00:39:00 Finished candle/prover                                        10m08s   4GB
Feb 14 00:39:00 Starting pancake
Feb 14 00:39:46 Finished pancake                                                 45s 874MB
Feb 14 00:39:46 Starting pancake/ffi
Feb 14 00:39:47 Finished pancake/ffi                                              0s  13MB
Feb 14 00:39:47 Starting pancake/semantics
Feb 14 00:42:15 Finished pancake/semantics                                     2m27s   1GB
Feb 14 00:42:15 Starting pancake/parser
Feb 14 00:42:37 Finished pancake/parser                                          22s 988MB
Feb 14 00:42:38 Starting pancake/proofs
Feb 14 01:15:45 Finished pancake/proofs                                       33m07s   5GB
Feb 14 01:15:45 Starting characteristic/examples
Feb 14 01:17:22 Finished characteristic/examples                               1m36s   2GB
Feb 14 01:17:22 Starting tutorial/solutions
Feb 14 01:32:27 Finished tutorial/solutions                                   15m05s  10GB
Feb 14 01:32:27 Starting translator/monadic/examples
Feb 14 01:36:35 Finished translator/monadic/examples                           4m07s   3GB
Feb 14 01:36:35 Starting examples
Feb 14 01:52:19 Finished examples                                             15m43s   4GB
Feb 14 01:52:19 Starting examples/compilation/x64
Feb 14 03:51:55 Finished examples/compilation/x64                           1h59m36s  19GB
Feb 14 03:51:55 Starting examples/compilation/x64/proofs
Feb 14 03:54:32 Finished examples/compilation/x64/proofs                       2m36s   4GB
Feb 14 03:54:32 Starting examples/compilation/ag32
Feb 14 04:24:52 Finished examples/compilation/ag32                            30m19s   9GB
Feb 14 04:24:52 Starting examples/compilation/ag32/proofs
Feb 14 04:25:56 Finished examples/compilation/ag32/proofs                      1m04s   5GB
Feb 14 04:25:56 Starting examples/compilation/to_word
Feb 14 04:29:16 Finished examples/compilation/to_word                          3m19s   6GB
Feb 14 04:29:16 Starting examples/lpr_checker
Feb 14 04:30:21 Finished examples/lpr_checker                                  1m04s   1GB
Feb 14 04:30:21 Starting examples/lpr_checker/array
Feb 14 05:01:44 Finished examples/lpr_checker/array                           31m22s   7GB
Feb 14 05:01:44 Starting examples/lpr_checker/array/compilation
Feb 14 05:54:58 Finished examples/lpr_checker/array/compilation               53m14s  33GB
Feb 14 05:54:58 Starting examples/lpr_checker/array/compilation/proofs
Feb 14 05:57:02 Finished examples/lpr_checker/array/compilation/proofs         2m03s   3GB
Feb 14 05:57:02 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 14 06:02:55 Finished examples/lpr_checker/array/compilation/proofsARM8     5m52s  25GB
Feb 14 06:02:55 Starting examples/xlrup_checker
Feb 14 06:03:54 Finished examples/xlrup_checker                                  58s   1GB
Feb 14 06:03:54 Starting examples/xlrup_checker/array
Feb 14 06:21:41 Finished examples/xlrup_checker/array                         17m46s   3GB
Feb 14 06:21:41 Starting examples/xlrup_checker/array/compilation
Feb 14 06:43:45 Finished examples/xlrup_checker/array/compilation             22m04s  21GB
Feb 14 06:43:45 Starting examples/xlrup_checker/array/compilation/proofs
Feb 14 06:44:53 Finished examples/xlrup_checker/array/compilation/proofs       1m07s   5GB
Feb 14 06:44:53 Starting examples/pseudo_bool
Feb 14 06:46:47 Finished examples/pseudo_bool                                  1m54s   1GB
Feb 14 06:46:47 Starting examples/pseudo_bool/cnf_encoding
Feb 14 06:47:13 Finished examples/pseudo_bool/cnf_encoding                       25s 604MB
Feb 14 06:47:13 Starting examples/pseudo_bool/graph_encoding
Feb 14 06:47:56 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Feb 14 06:47:56 Starting examples/pseudo_bool/array
Feb 14 07:55:25 Finished examples/pseudo_bool/array                         1h07m29s   6GB
Feb 14 07:55:25 Starting examples/pseudo_bool/array/compilation
Feb 14 10:10:44 FAILED: examples/pseudo_bool/array/compilation
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$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[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
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/array[0m
Scanned 83 directories
Starting work on README.md
Starting work on cliqueCompileTheory
Starting work on cnfCompileTheory
Starting work on mccisCompileTheory
README.md                                                                                                                                                                                                                         (0s)     OK
Starting work on mcisCompileTheory
cliqueCompileTheory                                                                                                                                                                                                             (213m)     OK
Starting work on npbc_fullCompileTheory
cnfCompileTheory                                                                                                                                                                                                                (206m)     OK
Starting work on subgraph_isoCompileTheory
mcisCompileTheory                                                                                                                                                                                                               (221m)     OK
Starting work on wcnfCompileTheory
mccisCompileTheory                                                                                                                                                                                                              (225m)     OK
subgraph_isoCompileTheory                                                                                                                                                                                                        (49m)FAIL<Signal 9>
                 to_data size: 911071
 Saved theorem _______ "to_data_thm"
            data_to_word eval: runtime: 2m31s,    gctime: 2.6s,     systime: 0.27183s.
            data_to_word real: 2m32s
            data_to_word size: 2444757
 Saved definition ____ "word_to_word_fn_def"
  inst,ssa,two-reg (par) eval: runtime: 16m03s,    gctime: 25.4s,     systime: 3.8s.
  inst,ssa,two-reg (par) real: 3m07s
  inst,ssa,two-reg (par) size: 6082860
 Saved definition ____ "clash_fn_def"
         get_clash (par) eval: 
npbc_fullCompileTheory                                                                                                                                                                                                           (42m)MKILLED
wcnfCompileTheory                                                                                                                                                                                                                (35m)MKILLED