Job 2193

CakeML:70c9116352cfd04905fbfb3bd8726ca1aaec0f1d
  fix Holmakefile [Aug 16 02:50:12]
#967 (lpr_arm8)
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 18 21:28:03 Claimed job
Aug 18 21:28:05 Building HOL
Aug 18 21:42:09 Starting developers
Aug 18 21:42:15 Finished developers                                               5s 107MB
Aug 18 21:42:15 Starting developers/bin
Aug 18 21:42:21 Finished developers/bin                                           6s   1GB
Aug 18 21:42:21 Starting compiler/proofs
Aug 18 23:45:16 Finished compiler/proofs                                    2h02m54s  16GB
Aug 18 23:45:16 Starting compiler/bootstrap/translation
Aug 19 08:05:51 Finished compiler/bootstrap/translation                     8h20m34s  44GB
Aug 19 08:05:51 Starting semantics/ffi
Aug 19 08:05:57 Finished semantics/ffi                                            5s 216MB
Aug 19 08:05:57 Starting semantics
Aug 19 08:05:59 Finished semantics                                                1s  19MB
Aug 19 08:05:59 Starting semantics/proofs
Aug 19 08:06:33 Finished semantics/proofs                                        34s   1GB
Aug 19 08:06:33 Starting semantics/alt_semantics
Aug 19 08:07:05 Finished semantics/alt_semantics                                 31s 939MB
Aug 19 08:07:06 Starting semantics/alt_semantics/proofs
Aug 19 08:19:03 Finished semantics/alt_semantics/proofs                       11m56s   1GB
Aug 19 08:19:03 Starting basis/pure
Aug 19 08:19:04 Finished basis/pure                                               1s  18MB
Aug 19 08:19:05 Starting translator
Aug 19 08:20:55 Finished translator                                            1m49s   1GB
Aug 19 08:20:55 Starting compiler/parsing
Aug 19 08:20:56 Finished compiler/parsing                                         1s  21MB
Aug 19 08:20:57 Starting characteristic
Aug 19 08:20:59 Finished characteristic                                           1s  26MB
Aug 19 08:20:59 Starting translator/monadic
Aug 19 08:21:01 Finished translator/monadic                                       1s  21MB
Aug 19 08:21:01 Starting basis
Aug 19 08:25:05 Finished basis                                                 4m03s   3GB
Aug 19 08:25:05 Starting compiler/inference
Aug 19 08:25:07 Finished compiler/inference                                       1s  18MB
Aug 19 08:25:07 Starting compiler/backend/reg_alloc
Aug 19 08:25:09 Finished compiler/backend/reg_alloc                               1s  19MB
Aug 19 08:25:09 Starting compiler/backend/gc
Aug 19 08:25:11 Finished compiler/backend/gc                                      2s  22MB
Aug 19 08:25:11 Starting compiler/backend
Aug 19 08:25:24 Finished compiler/backend                                        12s 810MB
Aug 19 08:25:24 Starting compiler/encoders/asm
Aug 19 08:25:26 Finished compiler/encoders/asm                                    1s  25MB
Aug 19 08:25:26 Starting compiler/encoders/x64
Aug 19 08:25:28 Finished compiler/encoders/x64                                    1s  19MB
Aug 19 08:25:28 Starting compiler/encoders/arm7
Aug 19 08:25:29 Finished compiler/encoders/arm7                                   1s  19MB
Aug 19 08:25:30 Starting compiler/encoders/arm8
Aug 19 08:25:32 Finished compiler/encoders/arm8                                   1s  19MB
Aug 19 08:25:32 Starting compiler/encoders/arm8_asl
Aug 19 10:51:30 Finished compiler/encoders/arm8_asl                         2h25m58s  42GB
Aug 19 10:51:31 Starting compiler/encoders/mips
Aug 19 10:51:32 Finished compiler/encoders/mips                                   1s  23MB
Aug 19 10:51:33 Starting compiler/encoders/riscv
Aug 19 10:51:34 Finished compiler/encoders/riscv                                  1s  18MB
Aug 19 10:51:35 Starting compiler/encoders/ag32
Aug 19 10:51:36 Finished compiler/encoders/ag32                                   1s  20MB
Aug 19 10:51:37 Starting compiler/backend/x64
Aug 19 10:51:39 Finished compiler/backend/x64                                     2s  23MB
Aug 19 10:51:39 Starting compiler/backend/arm7
Aug 19 10:51:41 Finished compiler/backend/arm7                                    2s  25MB
Aug 19 10:51:41 Starting compiler/backend/arm8
Aug 19 10:51:44 Finished compiler/backend/arm8                                    2s  23MB
Aug 19 10:51:44 Starting compiler/backend/mips
Aug 19 10:51:46 Finished compiler/backend/mips                                    2s  26MB
Aug 19 10:51:46 Starting compiler/backend/riscv
Aug 19 10:51:48 Finished compiler/backend/riscv                                   2s  22MB
Aug 19 10:51:49 Starting compiler/backend/ag32
Aug 19 10:53:16 Finished compiler/backend/ag32                                 1m27s   1GB
Aug 19 10:53:16 Starting compiler/parsing/proofs
Aug 19 10:53:18 Finished compiler/parsing/proofs                                  1s  18MB
Aug 19 10:53:18 Starting compiler/inference/proofs
Aug 19 10:53:20 Finished compiler/inference/proofs                                1s  19MB
Aug 19 10:53:20 Starting compiler/backend/semantics
Aug 19 10:54:34 Finished compiler/backend/semantics                            1m13s   1GB
Aug 19 10:54:34 Starting compiler/backend/reg_alloc/proofs
Aug 19 10:54:36 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Aug 19 10:54:36 Starting compiler/backend/proofs
Aug 19 10:55:36 Finished compiler/backend/proofs                               1m00s   3GB
Aug 19 10:55:37 Starting compiler/backend/serialiser
Aug 19 10:55:40 Finished compiler/backend/serialiser                              2s  38MB
Aug 19 10:55:40 Starting compiler/encoders/x64/proofs
Aug 19 11:05:31 Finished compiler/encoders/x64/proofs                          9m51s   6GB
Aug 19 11:05:31 Starting compiler/encoders/arm7/proofs
Aug 19 11:19:32 Finished compiler/encoders/arm7/proofs                        14m00s   4GB
Aug 19 11:19:32 Starting compiler/encoders/arm8/proofs
Aug 19 11:26:32 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
Aug 19 11:26:32 Starting compiler/encoders/arm8_asl/proofs
Aug 19 12:19:12 Finished compiler/encoders/arm8_asl/proofs                    52m40s   7GB
Aug 19 12:19:13 Starting compiler/encoders/mips/proofs
Aug 19 12:29:57 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Aug 19 12:29:57 Starting compiler/encoders/riscv/proofs
Aug 19 12:39:01 Finished compiler/encoders/riscv/proofs                        9m03s   1GB
Aug 19 12:39:01 Starting compiler/encoders/ag32/proofs
Aug 19 12:41:39 Finished compiler/encoders/ag32/proofs                         2m38s 985MB
Aug 19 12:41:40 Starting compiler/backend/x64/proofs
Aug 19 12:42:09 Finished compiler/backend/x64/proofs                             29s   1GB
Aug 19 12:42:09 Starting compiler/backend/arm7/proofs
Aug 19 12:42:44 Finished compiler/backend/arm7/proofs                            34s   2GB
Aug 19 12:42:44 Starting compiler/backend/arm8/proofs
Aug 19 12:43:15 Finished compiler/backend/arm8/proofs                            29s   1GB
Aug 19 12:43:15 Starting compiler/backend/arm8_asl
Aug 19 12:43:37 Finished compiler/backend/arm8_asl                               22s   1GB
Aug 19 12:43:38 Starting compiler/backend/mips/proofs
Aug 19 12:44:09 Finished compiler/backend/mips/proofs                            31s   2GB
Aug 19 12:44:09 Starting compiler/backend/riscv/proofs
Aug 19 12:44:44 Finished compiler/backend/riscv/proofs                           34s   2GB
Aug 19 12:44:44 Starting compiler/backend/ag32/proofs
Aug 19 12:58:29 Finished compiler/backend/ag32/proofs                         13m44s   3GB
Aug 19 12:58:29 Starting candle/set-theory
Aug 19 12:59:07 Finished candle/set-theory                                       38s   1GB
Aug 19 12:59:07 Starting candle/syntax-lib
Aug 19 12:59:09 Finished candle/syntax-lib                                        1s  18MB
Aug 19 12:59:09 Starting candle/standard/syntax
Aug 19 12:59:20 Finished candle/standard/syntax                                  10s 854MB
Aug 19 12:59:20 Starting candle/standard/semantics
Aug 19 13:01:22 Finished candle/standard/semantics                             2m02s   1GB
Aug 19 13:01:22 Starting candle/standard/monadic
Aug 19 13:01:24 Finished candle/standard/monadic                                  1s  20MB
Aug 19 13:01:25 Starting candle/standard/ml_kernel
Aug 19 13:03:03 Finished candle/standard/ml_kernel                             1m38s   3GB
Aug 19 13:03:03 Starting candle/overloading/syntax
Aug 19 13:06:28 Finished candle/overloading/syntax                             3m24s   1GB
Aug 19 13:06:28 Starting candle/overloading/semantics
Aug 19 13:18:45 Finished candle/overloading/semantics                         12m17s   2GB
Aug 19 13:18:45 Starting candle/overloading/monadic
Aug 19 13:21:31 Finished candle/overloading/monadic                            2m45s   1GB
Aug 19 13:21:31 Starting candle/overloading/ml_kernel
Aug 19 13:29:23 Finished candle/overloading/ml_kernel                          7m51s   4GB
Aug 19 13:29:23 Starting candle/overloading/ml_checker
Aug 19 13:31:55 Finished candle/overloading/ml_checker                         2m31s   2GB
Aug 19 13:31:55 Starting candle/prover
Aug 19 13:41:55 Finished candle/prover                                         9m59s   3GB
Aug 19 13:41:55 Starting pancake
Aug 19 13:42:40 Finished pancake                                                 44s   1GB
Aug 19 13:42:40 Starting pancake/ffi
Aug 19 13:42:41 Finished pancake/ffi                                              0s  13MB
Aug 19 13:42:41 Starting pancake/semantics
Aug 19 13:45:13 Finished pancake/semantics                                     2m31s   1GB
Aug 19 13:45:13 Starting pancake/parser
Aug 19 13:45:32 Finished pancake/parser                                          18s 716MB
Aug 19 13:45:32 Starting pancake/proofs
Aug 19 14:19:14 Finished pancake/proofs                                       33m42s   7GB
Aug 19 14:19:15 Starting characteristic/examples
Aug 19 14:20:54 Finished characteristic/examples                               1m39s   1GB
Aug 19 14:20:55 Starting tutorial/solutions
Aug 19 14:36:41 Finished tutorial/solutions                                   15m46s   8GB
Aug 19 14:36:41 Starting translator/monadic/examples
Aug 19 14:41:01 Finished translator/monadic/examples                           4m19s   3GB
Aug 19 14:41:01 Starting examples
Aug 19 14:45:33 Resuming examples
Aug 19 15:00:16 Finished examples                                             14m42s   4GB
Aug 19 15:00:16 Starting examples/compilation/x64
Aug 19 17:03:03 Finished examples/compilation/x64                           2h02m46s  14GB
Aug 19 17:03:03 Starting examples/compilation/x64/proofs
Aug 19 17:05:45 Finished examples/compilation/x64/proofs                       2m41s   4GB
Aug 19 17:05:45 Starting examples/compilation/ag32
Aug 19 17:36:24 Finished examples/compilation/ag32                            30m39s   6GB
Aug 19 17:36:24 Starting examples/compilation/ag32/proofs
Aug 19 17:37:29 Finished examples/compilation/ag32/proofs                      1m04s   4GB
Aug 19 17:37:29 Starting examples/compilation/to_word
Aug 19 17:40:51 Finished examples/compilation/to_word                          3m21s   6GB
Aug 19 17:40:51 Starting examples/lpr_checker
Aug 19 17:42:01 Finished examples/lpr_checker                                  1m09s   1GB
Aug 19 17:42:01 Starting examples/lpr_checker/array
Aug 19 18:18:47 Finished examples/lpr_checker/array                           36m46s   7GB
Aug 19 18:18:48 Starting examples/lpr_checker/array/compilation
Aug 19 18:34:32 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_arrayCompileARM8Theory
Starting work on lpr_arrayCompileTheory
Starting work on lpr_arrayPackingCompileTheory
README.md                                                                                         (0s)     OK
Starting work on lpr_arrayRamseyCompileTheory
lpr_arrayRamseyCompileTheory                                                                     (27m)FAIL<Signal 9>
 
 runtime: 9.1s,    gctime: 0.00000s,     systime: 0.00000s.
         external oracle real: 9.1s
         external oracle size: 305771
      apply colour (par) eval: runtime: 4m48s,    gctime: 6.3s,     systime: 1.4s.
      apply colour (par) real: 2m04s
      apply colour (par) size: 1244028
            check colour eval: runtime: 28.0s,    gctime: 0.36214s,     systime: 0.03144s.
            check colour real: 32.1s
            check colour size: 1244832
           word_to_stack eval: 
lpr_arrayCompileARM8Theory                                                                       (22m)MKILLED
lpr_arrayCompileTheory                                                                           (23m)MKILLED
lpr_arrayPackingCompileTheory                                                                    (22m)MKILLED