Job 2197

CakeML:6ff7f36f3d121f06266c2280d68bf9e2dd52a6de
  Update perms_ok proofs [Aug 17 19:40:01]
#969 (issue-916)
Merging into:5c1bae6b33cf93343962f658faefefee12f74a9c
  Merge pull request #965 from CakeML/explorer [Aug 10 04:53:38]
HOL:c505f5761a545a06f2a80c536262e608021c3955
  Fix the proof of zagier_fix in experimental kernel. [Aug 17 06:53:11]
Machine:oven1 5.19.0-46-generic x86_64 GNU/Linux

Aug 20 14:59:32 Claimed job
Aug 20 14:59:36 Building HOL
Aug 20 15:13:38 Starting developers
Aug 20 15:13:44 Finished developers                                               5s 105MB
Aug 20 15:13:44 Starting developers/bin
Aug 20 15:13:52 Finished developers/bin                                           7s   1GB
Aug 20 15:13:52 Starting compiler/proofs
Aug 20 17:16:06 Finished compiler/proofs                                    2h02m13s  18GB
Aug 20 17:16:06 Starting compiler/bootstrap/translation
Aug 21 01:33:03 Finished compiler/bootstrap/translation                     8h16m55s  35GB
Aug 21 01:33:03 Starting semantics/ffi
Aug 21 01:33:09 Finished semantics/ffi                                            5s 219MB
Aug 21 01:33:09 Starting semantics
Aug 21 01:33:10 Finished semantics                                                1s  20MB
Aug 21 01:33:11 Starting semantics/proofs
Aug 21 01:33:45 Finished semantics/proofs                                        34s   1GB
Aug 21 01:33:45 Starting semantics/alt_semantics
Aug 21 01:34:18 Finished semantics/alt_semantics                                 32s 810MB
Aug 21 01:34:18 Starting semantics/alt_semantics/proofs
Aug 21 01:46:12 Finished semantics/alt_semantics/proofs                       11m53s   1GB
Aug 21 01:46:12 Starting basis/pure
Aug 21 01:46:13 Finished basis/pure                                               1s  20MB
Aug 21 01:46:14 Starting translator
Aug 21 01:48:06 Finished translator                                            1m52s   1GB
Aug 21 01:48:06 Starting compiler/parsing
Aug 21 01:48:08 Finished compiler/parsing                                         1s  19MB
Aug 21 01:48:08 Starting characteristic
Aug 21 01:48:10 Finished characteristic                                           1s  23MB
Aug 21 01:48:10 Starting translator/monadic
Aug 21 01:48:12 Finished translator/monadic                                       1s  25MB
Aug 21 01:48:12 Starting basis
Aug 21 01:52:32 Finished basis                                                 4m19s   3GB
Aug 21 01:52:32 Starting compiler/inference
Aug 21 01:52:34 Finished compiler/inference                                       1s  18MB
Aug 21 01:52:34 Starting compiler/backend/reg_alloc
Aug 21 01:52:35 Finished compiler/backend/reg_alloc                               1s  17MB
Aug 21 01:52:35 Starting compiler/backend/gc
Aug 21 01:52:38 Finished compiler/backend/gc                                      2s  25MB
Aug 21 01:52:38 Starting compiler/backend
Aug 21 01:52:50 Finished compiler/backend                                        12s 858MB
Aug 21 01:52:50 Starting compiler/encoders/asm
Aug 21 01:52:52 Finished compiler/encoders/asm                                    1s  23MB
Aug 21 01:52:52 Starting compiler/encoders/x64
Aug 21 01:52:54 Finished compiler/encoders/x64                                    1s  26MB
Aug 21 01:52:54 Starting compiler/encoders/arm7
Aug 21 01:52:56 Finished compiler/encoders/arm7                                   1s  25MB
Aug 21 01:52:56 Starting compiler/encoders/arm8
Aug 21 01:52:58 Finished compiler/encoders/arm8                                   1s  25MB
Aug 21 01:52:58 Starting compiler/encoders/arm8_asl
Aug 21 04:18:19 Finished compiler/encoders/arm8_asl                         2h25m20s  40GB
Aug 21 04:18:19 Starting compiler/encoders/mips
Aug 21 04:18:21 Finished compiler/encoders/mips                                   1s  26MB
Aug 21 04:18:21 Starting compiler/encoders/riscv
Aug 21 04:18:23 Finished compiler/encoders/riscv                                  1s  24MB
Aug 21 04:18:23 Starting compiler/encoders/ag32
Aug 21 04:18:25 Finished compiler/encoders/ag32                                   1s  21MB
Aug 21 04:18:25 Starting compiler/backend/x64
Aug 21 04:18:28 Finished compiler/backend/x64                                     2s  23MB
Aug 21 04:18:28 Starting compiler/backend/arm7
Aug 21 04:18:30 Finished compiler/backend/arm7                                    2s  23MB
Aug 21 04:18:30 Starting compiler/backend/arm8
Aug 21 04:18:32 Finished compiler/backend/arm8                                    2s  21MB
Aug 21 04:18:33 Starting compiler/backend/mips
Aug 21 04:18:35 Finished compiler/backend/mips                                    2s  27MB
Aug 21 04:18:35 Starting compiler/backend/riscv
Aug 21 04:18:37 Finished compiler/backend/riscv                                   2s  21MB
Aug 21 04:18:37 Starting compiler/backend/ag32
Aug 21 04:20:05 Finished compiler/backend/ag32                                 1m27s   1GB
Aug 21 04:20:05 Starting compiler/parsing/proofs
Aug 21 04:20:07 Finished compiler/parsing/proofs                                  1s  19MB
Aug 21 04:20:07 Starting compiler/inference/proofs
Aug 21 04:20:09 Finished compiler/inference/proofs                                1s  24MB
Aug 21 04:20:09 Starting compiler/backend/semantics
Aug 21 04:21:22 Finished compiler/backend/semantics                            1m13s   1GB
Aug 21 04:21:22 Starting compiler/backend/reg_alloc/proofs
Aug 21 04:21:24 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Aug 21 04:21:24 Starting compiler/backend/proofs
Aug 21 04:22:25 Finished compiler/backend/proofs                               1m00s   2GB
Aug 21 04:22:25 Starting compiler/backend/serialiser
Aug 21 04:22:28 Finished compiler/backend/serialiser                              2s  30MB
Aug 21 04:22:28 Starting compiler/encoders/x64/proofs
Aug 21 04:32:17 Finished compiler/encoders/x64/proofs                          9m48s   6GB
Aug 21 04:32:17 Starting compiler/encoders/arm7/proofs
Aug 21 04:46:09 Finished compiler/encoders/arm7/proofs                        13m51s   4GB
Aug 21 04:46:10 Starting compiler/encoders/arm8/proofs
Aug 21 04:53:13 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Aug 21 04:53:13 Starting compiler/encoders/arm8_asl/proofs
Aug 21 05:46:00 Finished compiler/encoders/arm8_asl/proofs                    52m45s   9GB
Aug 21 05:46:00 Starting compiler/encoders/mips/proofs
Aug 21 05:56:43 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Aug 21 05:56:43 Starting compiler/encoders/riscv/proofs
Aug 21 06:05:46 Finished compiler/encoders/riscv/proofs                        9m03s   1GB
Aug 21 06:05:47 Starting compiler/encoders/ag32/proofs
Aug 21 06:08:25 Finished compiler/encoders/ag32/proofs                         2m38s 991MB
Aug 21 06:08:26 Starting compiler/backend/x64/proofs
Aug 21 06:08:56 Finished compiler/backend/x64/proofs                             30s   2GB
Aug 21 06:08:56 Starting compiler/backend/arm7/proofs
Aug 21 06:09:31 Finished compiler/backend/arm7/proofs                            34s   2GB
Aug 21 06:09:31 Starting compiler/backend/arm8/proofs
Aug 21 06:10:01 Finished compiler/backend/arm8/proofs                            30s   1GB
Aug 21 06:10:01 Starting compiler/backend/arm8_asl
Aug 21 06:10:24 Finished compiler/backend/arm8_asl                               22s   1GB
Aug 21 06:10:25 Starting compiler/backend/mips/proofs
Aug 21 06:10:57 Finished compiler/backend/mips/proofs                            31s   2GB
Aug 21 06:10:57 Starting compiler/backend/riscv/proofs
Aug 21 06:11:31 Finished compiler/backend/riscv/proofs                           34s   2GB
Aug 21 06:11:31 Starting compiler/backend/ag32/proofs
Aug 21 06:25:13 Finished compiler/backend/ag32/proofs                         13m41s   2GB
Aug 21 06:25:13 Starting candle/set-theory
Aug 21 06:25:52 Finished candle/set-theory                                       38s   1GB
Aug 21 06:25:52 Starting candle/syntax-lib
Aug 21 06:25:54 Finished candle/syntax-lib                                        1s  18MB
Aug 21 06:25:54 Starting candle/standard/syntax
Aug 21 06:26:05 Finished candle/standard/syntax                                  10s 853MB
Aug 21 06:26:05 Starting candle/standard/semantics
Aug 21 06:28:08 Finished candle/standard/semantics                             2m02s   1GB
Aug 21 06:28:08 Starting candle/standard/monadic
Aug 21 06:28:10 Finished candle/standard/monadic                                  1s  21MB
Aug 21 06:28:10 Starting candle/standard/ml_kernel
Aug 21 06:29:46 Finished candle/standard/ml_kernel                             1m35s   2GB
Aug 21 06:29:46 Starting candle/overloading/syntax
Aug 21 06:33:14 Finished candle/overloading/syntax                             3m28s   1GB
Aug 21 06:33:14 Starting candle/overloading/semantics
Aug 21 06:45:36 Finished candle/overloading/semantics                         12m21s   2GB
Aug 21 06:45:36 Starting candle/overloading/monadic
Aug 21 06:48:21 Finished candle/overloading/monadic                            2m44s   1GB
Aug 21 06:48:21 Starting candle/overloading/ml_kernel
Aug 21 06:56:18 Finished candle/overloading/ml_kernel                          7m57s   3GB
Aug 21 06:56:18 Starting candle/overloading/ml_checker
Aug 21 06:58:52 Finished candle/overloading/ml_checker                         2m33s   2GB
Aug 21 06:58:52 Starting candle/prover
Aug 21 07:09:05 Finished candle/prover                                        10m13s   3GB
Aug 21 07:09:05 Starting pancake
Aug 21 07:09:51 Finished pancake                                                 46s   1GB
Aug 21 07:09:52 Starting pancake/ffi
Aug 21 07:09:52 Finished pancake/ffi                                              0s  13MB
Aug 21 07:09:52 Starting pancake/semantics
Aug 21 07:12:21 Finished pancake/semantics                                     2m28s   1GB
Aug 21 07:12:21 Starting pancake/parser
Aug 21 07:12:40 Finished pancake/parser                                          18s 716MB
Aug 21 07:12:40 Starting pancake/proofs
Aug 21 07:46:11 Finished pancake/proofs                                       33m30s   5GB
Aug 21 07:46:11 Starting characteristic/examples
Aug 21 07:47:50 Finished characteristic/examples                               1m38s   1GB
Aug 21 07:47:50 Starting tutorial/solutions
Aug 21 08:03:08 Finished tutorial/solutions                                   15m17s   9GB
Aug 21 08:03:08 Starting translator/monadic/examples
Aug 21 08:07:30 Finished translator/monadic/examples                           4m21s   3GB
Aug 21 08:07:30 Starting examples
Aug 21 08:25:19 Finished examples                                             17m48s   3GB
Aug 21 08:25:19 Starting examples/compilation/x64
Aug 21 10:26:59 Finished examples/compilation/x64                           2h01m39s  14GB
Aug 21 10:26:59 Starting examples/compilation/x64/proofs
Aug 21 10:29:47 Finished examples/compilation/x64/proofs                       2m47s   4GB
Aug 21 10:29:47 Starting examples/compilation/ag32
Aug 21 11:00:45 Finished examples/compilation/ag32                            30m58s   7GB
Aug 21 11:00:46 Starting examples/compilation/ag32/proofs
Aug 21 11:01:58 Finished examples/compilation/ag32/proofs                      1m12s   4GB
Aug 21 11:01:58 Starting examples/compilation/to_word
Aug 21 11:05:23 Finished examples/compilation/to_word                          3m24s   7GB
Aug 21 11:05:24 Starting examples/lpr_checker
Aug 21 11:06:33 Finished examples/lpr_checker                                  1m08s   1GB
Aug 21 11:06:33 Starting examples/lpr_checker/array
Aug 21 11:43:47 Finished examples/lpr_checker/array                           37m14s   7GB
Aug 21 11:43:48 Starting examples/lpr_checker/array/compilation
Aug 21 11:57:45 FAILED: examples/lpr_checker/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/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)/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/lpr_checker[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker/array[0m
Scanned 78 directories
Starting work on README.md
Starting work on lpr_array.S
Starting work on lpr_arrayPackingCompileTheory
Starting work on lpr_arrayRamseyCompileTheory
README.md                                                                                         (0s)     OK
lpr_arrayRamseyCompileTheory                                                                     (27m)FAIL<Signal 9>
 
 runtime: 11.6s,    gctime: 0.09155s,     systime: 0.00744s.
         external oracle real: 11.6s
         external oracle size: 305771
      apply colour (par) eval: runtime: 4m34s,    gctime: 3.9s,     systime: 1.1s.
      apply colour (par) real: 1m28s
      apply colour (par) size: 1244028
            check colour eval: runtime: 22.6s,    gctime: 0.00000s,     systime: 0.00000s.
            check colour real: 23.3s
            check colour size: 1244832
           word_to_stack eval: 
lpr_array.S                                                                                      (24m)MKILLED
lpr_arrayPackingCompileTheory                                                                    (22m)MKILLED