Job 2199

CakeML:5696cf2a85f55b22b92cbb2810d120e9259e144e
  Merge pull request #967 from CakeML/lpr_arm8 [Aug 21 07:03:02]
HOL:1b35c0108cfd82d6f6a4960cfe747ff4e5cf3ee5
  Initial work on making triangular unification tail-recursive [Aug 18 07:44:40]
Machine:oven1 5.19.0-46-generic x86_64 GNU/Linux

Aug 21 18:56:50 Claimed job
Aug 21 18:56:52 Reusing HOL
Aug 21 18:57:32 Starting developers
Aug 21 18:57:38 Finished developers                                               5s 101MB
Aug 21 18:57:38 Starting developers/bin
Aug 21 18:57:45 Finished developers/bin                                           6s   1GB
Aug 21 18:57:45 Starting compiler/proofs
Aug 21 20:56:33 Finished compiler/proofs                                    1h58m47s  22GB
Aug 21 20:56:33 Starting compiler/bootstrap/translation
Aug 22 05:07:27 Finished compiler/bootstrap/translation                     8h10m53s  53GB
Aug 22 05:07:28 Starting semantics/ffi
Aug 22 05:07:32 Finished semantics/ffi                                            4s 395MB
Aug 22 05:07:33 Starting semantics
Aug 22 05:07:34 Finished semantics                                                1s  18MB
Aug 22 05:07:34 Starting semantics/proofs
Aug 22 05:08:07 Finished semantics/proofs                                        32s 715MB
Aug 22 05:08:07 Starting semantics/alt_semantics
Aug 22 05:08:39 Finished semantics/alt_semantics                                 31s 672MB
Aug 22 05:08:39 Starting semantics/alt_semantics/proofs
Aug 22 05:20:26 Finished semantics/alt_semantics/proofs                       11m46s   1GB
Aug 22 05:20:26 Starting basis/pure
Aug 22 05:20:28 Finished basis/pure                                               1s  17MB
Aug 22 05:20:28 Starting translator
Aug 22 05:22:20 Finished translator                                            1m51s   1GB
Aug 22 05:22:20 Starting compiler/parsing
Aug 22 05:22:22 Finished compiler/parsing                                         1s  22MB
Aug 22 05:22:22 Starting characteristic
Aug 22 05:22:24 Finished characteristic                                           1s  25MB
Aug 22 05:22:24 Starting translator/monadic
Aug 22 05:22:26 Finished translator/monadic                                       1s  21MB
Aug 22 05:22:26 Starting basis
Aug 22 05:26:29 Finished basis                                                 4m02s   3GB
Aug 22 05:26:29 Starting compiler/inference
Aug 22 05:26:31 Finished compiler/inference                                       1s  23MB
Aug 22 05:26:31 Starting compiler/backend/reg_alloc
Aug 22 05:26:33 Finished compiler/backend/reg_alloc                               1s  19MB
Aug 22 05:26:33 Starting compiler/backend/gc
Aug 22 05:26:35 Finished compiler/backend/gc                                      2s  25MB
Aug 22 05:26:35 Starting compiler/backend
Aug 22 05:26:48 Finished compiler/backend                                        12s 811MB
Aug 22 05:26:48 Starting compiler/encoders/asm
Aug 22 05:26:50 Finished compiler/encoders/asm                                    1s  20MB
Aug 22 05:26:50 Starting compiler/encoders/x64
Aug 22 05:26:52 Finished compiler/encoders/x64                                    1s  20MB
Aug 22 05:26:52 Starting compiler/encoders/arm7
Aug 22 05:26:54 Finished compiler/encoders/arm7                                   1s  25MB
Aug 22 05:26:54 Starting compiler/encoders/arm8
Aug 22 05:26:56 Finished compiler/encoders/arm8                                   1s  20MB
Aug 22 05:26:56 Starting compiler/encoders/arm8_asl
Aug 22 07:52:34 Finished compiler/encoders/arm8_asl                         2h25m38s  42GB
Aug 22 07:52:34 Starting compiler/encoders/mips
Aug 22 07:52:36 Finished compiler/encoders/mips                                   1s  24MB
Aug 22 07:52:36 Starting compiler/encoders/riscv
Aug 22 07:52:38 Finished compiler/encoders/riscv                                  1s  25MB
Aug 22 07:52:38 Starting compiler/encoders/ag32
Aug 22 07:52:40 Finished compiler/encoders/ag32                                   1s  18MB
Aug 22 07:52:40 Starting compiler/backend/x64
Aug 22 07:52:42 Finished compiler/backend/x64                                     2s  22MB
Aug 22 07:52:43 Starting compiler/backend/arm7
Aug 22 07:52:45 Finished compiler/backend/arm7                                    2s  21MB
Aug 22 07:52:45 Starting compiler/backend/arm8
Aug 22 07:52:47 Finished compiler/backend/arm8                                    2s  23MB
Aug 22 07:52:47 Starting compiler/backend/mips
Aug 22 07:52:50 Finished compiler/backend/mips                                    2s  28MB
Aug 22 07:52:50 Starting compiler/backend/riscv
Aug 22 07:52:52 Finished compiler/backend/riscv                                   2s  28MB
Aug 22 07:52:52 Starting compiler/backend/ag32
Aug 22 07:54:20 Finished compiler/backend/ag32                                 1m27s   2GB
Aug 22 07:54:20 Starting compiler/parsing/proofs
Aug 22 07:54:22 Finished compiler/parsing/proofs                                  1s  19MB
Aug 22 07:54:22 Starting compiler/inference/proofs
Aug 22 07:54:24 Finished compiler/inference/proofs                                1s  20MB
Aug 22 07:54:24 Starting compiler/backend/semantics
Aug 22 07:55:39 Finished compiler/backend/semantics                            1m14s   1GB
Aug 22 07:55:39 Starting compiler/backend/reg_alloc/proofs
Aug 22 07:55:41 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Aug 22 07:55:41 Starting compiler/backend/proofs
Aug 22 07:56:41 Finished compiler/backend/proofs                                 59s   2GB
Aug 22 07:56:41 Starting compiler/backend/serialiser
Aug 22 07:56:44 Finished compiler/backend/serialiser                              2s  34MB
Aug 22 07:56:44 Starting compiler/encoders/x64/proofs
Aug 22 08:06:38 Finished compiler/encoders/x64/proofs                          9m53s   5GB
Aug 22 08:06:39 Starting compiler/encoders/arm7/proofs
Aug 22 08:20:26 Finished compiler/encoders/arm7/proofs                        13m47s   4GB
Aug 22 08:20:26 Starting compiler/encoders/arm8/proofs
Aug 22 08:27:20 Finished compiler/encoders/arm8/proofs                         6m52s   1GB
Aug 22 08:27:20 Starting compiler/encoders/arm8_asl/proofs
Aug 22 09:19:57 Finished compiler/encoders/arm8_asl/proofs                    52m36s   6GB
Aug 22 09:19:57 Starting compiler/encoders/mips/proofs
Aug 22 09:30:40 Finished compiler/encoders/mips/proofs                        10m42s   3GB
Aug 22 09:30:40 Starting compiler/encoders/riscv/proofs
Aug 22 09:39:50 Finished compiler/encoders/riscv/proofs                        9m09s   1GB
Aug 22 09:39:50 Starting compiler/encoders/ag32/proofs
Aug 22 09:42:26 Finished compiler/encoders/ag32/proofs                         2m35s   1GB
Aug 22 09:42:26 Starting compiler/backend/x64/proofs
Aug 22 09:42:56 Finished compiler/backend/x64/proofs                             29s   1GB
Aug 22 09:42:56 Starting compiler/backend/arm7/proofs
Aug 22 09:43:29 Finished compiler/backend/arm7/proofs                            32s   2GB
Aug 22 09:43:29 Starting compiler/backend/arm8/proofs
Aug 22 09:44:00 Finished compiler/backend/arm8/proofs                            30s   2GB
Aug 22 09:44:00 Starting compiler/backend/arm8_asl
Aug 22 09:44:23 Finished compiler/backend/arm8_asl                               23s   2GB
Aug 22 09:44:24 Starting compiler/backend/mips/proofs
Aug 22 09:44:54 Finished compiler/backend/mips/proofs                            30s   2GB
Aug 22 09:44:55 Starting compiler/backend/riscv/proofs
Aug 22 09:45:29 Finished compiler/backend/riscv/proofs                           34s   3GB
Aug 22 09:45:29 Starting compiler/backend/ag32/proofs
Aug 22 09:59:24 Finished compiler/backend/ag32/proofs                         13m54s   2GB
Aug 22 09:59:24 Starting candle/set-theory
Aug 22 10:00:04 Finished candle/set-theory                                       39s   1GB
Aug 22 10:00:04 Starting candle/syntax-lib
Aug 22 10:00:05 Finished candle/syntax-lib                                        1s  20MB
Aug 22 10:00:06 Starting candle/standard/syntax
Aug 22 10:00:16 Finished candle/standard/syntax                                  10s 821MB
Aug 22 10:00:16 Starting candle/standard/semantics
Aug 22 10:02:15 Finished candle/standard/semantics                             1m58s   1GB
Aug 22 10:02:15 Starting candle/standard/monadic
Aug 22 10:02:17 Finished candle/standard/monadic                                  1s  23MB
Aug 22 10:02:17 Starting candle/standard/ml_kernel
Aug 22 10:04:04 Finished candle/standard/ml_kernel                             1m47s   3GB
Aug 22 10:04:05 Starting candle/overloading/syntax
Aug 22 10:07:29 Finished candle/overloading/syntax                             3m24s   1GB
Aug 22 10:07:29 Starting candle/overloading/semantics
Aug 22 10:20:02 Finished candle/overloading/semantics                         12m30s   2GB
Aug 22 10:20:02 Starting candle/overloading/monadic
Aug 22 10:22:49 Finished candle/overloading/monadic                            2m47s   2GB
Aug 22 10:22:50 Starting candle/overloading/ml_kernel
Aug 22 10:30:48 Finished candle/overloading/ml_kernel                          7m58s   3GB
Aug 22 10:30:48 Starting candle/overloading/ml_checker
Aug 22 10:33:29 Finished candle/overloading/ml_checker                         2m41s   2GB
Aug 22 10:33:29 Starting candle/prover
Aug 22 10:43:43 Finished candle/prover                                        10m13s   3GB
Aug 22 10:43:43 Starting pancake
Aug 22 10:44:28 Finished pancake                                                 44s 858MB
Aug 22 10:44:29 Starting pancake/ffi
Aug 22 10:44:29 Finished pancake/ffi                                              0s  12MB
Aug 22 10:44:29 Starting pancake/semantics
Aug 22 10:47:03 Finished pancake/semantics                                     2m33s   1GB
Aug 22 10:47:03 Starting pancake/parser
Aug 22 10:47:22 Finished pancake/parser                                          19s 646MB
Aug 22 10:47:22 Starting pancake/proofs
Aug 22 11:20:55 Finished pancake/proofs                                       33m31s   4GB
Aug 22 11:20:55 Starting characteristic/examples
Aug 22 11:22:26 Finished characteristic/examples                               1m31s   2GB
Aug 22 11:22:26 Starting tutorial/solutions
Aug 22 11:37:47 Finished tutorial/solutions                                   15m20s  10GB
Aug 22 11:37:47 Starting translator/monadic/examples
Aug 22 11:42:04 Finished translator/monadic/examples                           4m16s   3GB
Aug 22 11:42:04 Starting examples
Aug 22 11:59:38 Finished examples                                             17m33s   5GB
Aug 22 11:59:38 Starting examples/compilation/x64
Aug 22 14:00:44 Finished examples/compilation/x64                           2h01m06s  13GB
Aug 22 14:00:44 Starting examples/compilation/x64/proofs
Aug 22 14:03:25 Finished examples/compilation/x64/proofs                       2m40s   4GB
Aug 22 14:03:25 Starting examples/compilation/ag32
Aug 22 14:33:56 Finished examples/compilation/ag32                            30m31s   7GB
Aug 22 14:33:57 Starting examples/compilation/ag32/proofs
Aug 22 14:35:01 Finished examples/compilation/ag32/proofs                      1m04s   4GB
Aug 22 14:35:01 Starting examples/compilation/to_word
Aug 22 14:38:25 Finished examples/compilation/to_word                          3m24s   7GB
Aug 22 14:38:26 Starting examples/lpr_checker
Aug 22 14:39:31 Finished examples/lpr_checker                                  1m05s   1GB
Aug 22 14:39:31 Starting examples/lpr_checker/array
Aug 22 15:16:23 Finished examples/lpr_checker/array                           36m49s   9GB
Aug 22 15:16:23 Starting examples/lpr_checker/array/compilation
Aug 22 15:31:37 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)/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/lpr_checker[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker/array[0m
Scanned 79 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: 12.0s,    gctime: 0.00000s,     systime: 0.00000s.
         external oracle real: 12.0s
         external oracle size: 305771
      apply colour (par) eval: runtime: 4m43s,    gctime: 4.8s,     systime: 1.2s.
      apply colour (par) real: 1m54s
      apply colour (par) size: 1244028
            check colour eval: runtime: 29.2s,    gctime: 0.50602s,     systime: 0.10476s.
            check colour real: 33.3s
            check colour size: 1244832
lpr_arrayCompileARM8Theory                                                                       (22m)MKILLED
lpr_arrayCompileTheory                                                                           (21m)MKILLED
lpr_arrayPackingCompileTheory                                                                    (21m)MKILLED