Job 958

CakeML:771865c05a96606969aac5f75811602d8c061768
  Fix proof broken by HOL's removal of relationTheory.RTC_DEF [Jul 24 12:06:35]
HOL:e736cb4999577a492e6abd84f789113b9a4c80c3
  Use new Inductive syntax in PEG theory [Jul 23 03:51:48]
Machine:brain08 4.14.127.1.amd64-smp
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz

Jul 24 14:50:52 Claimed job
Jul 24 14:50:54 Reusing HOL
Jul 24 14:51:18 Starting developers
Jul 24 14:51:19 Finished developers                                               0s  33MB
Jul 24 14:51:19 Starting developers/bin
Jul 24 14:51:29 Finished developers/bin                                           9s 971MB
Jul 24 14:51:29 Starting semantics/ffi
Jul 24 14:51:48 Finished semantics/ffi                                           18s 278MB
Jul 24 14:51:48 Starting semantics
Jul 24 14:54:11 Finished semantics                                             2m22s   1GB
Jul 24 14:54:11 Starting semantics/proofs
Jul 24 14:59:57 Finished semantics/proofs                                      5m45s   1GB
Jul 24 14:59:58 Starting semantics/alt_semantics
Jul 24 15:00:13 Finished semantics/alt_semantics                                 15s 324MB
Jul 24 15:00:14 Starting semantics/alt_semantics/proofs
Jul 24 15:03:38 Finished semantics/alt_semantics/proofs                        3m23s   1GB
Jul 24 15:03:38 Starting basis/pure
Jul 24 15:05:07 Finished basis/pure                                            1m28s   1GB
Jul 24 15:05:07 Starting translator
Jul 24 15:08:16 Finished translator                                            3m08s   1GB
Jul 24 15:08:16 Starting compiler/parsing
Jul 24 15:09:58 Finished compiler/parsing                                      1m42s   2GB
Jul 24 15:09:59 Starting characteristic
Jul 24 15:20:06 Finished characteristic                                       10m06s   2GB
Jul 24 15:20:06 Starting translator/monadic
Jul 24 15:22:57 Finished translator/monadic                                    2m50s   1GB
Jul 24 15:22:57 Starting basis
Jul 24 15:56:39 Finished basis                                                33m41s   6GB
Jul 24 15:56:40 Starting compiler/inference
Jul 24 15:59:46 Finished compiler/inference                                    3m05s   3GB
Jul 24 15:59:46 Starting compiler/backend/reg_alloc
Jul 24 16:01:24 Finished compiler/backend/reg_alloc                            1m37s   1GB
Jul 24 16:01:24 Starting compiler/backend/gc
Jul 24 16:15:30 Finished compiler/backend/gc                                  14m05s   1GB
Jul 24 16:15:30 Starting compiler/backend
Jul 24 16:15:32 Finished compiler/backend                                         1s  31MB
Jul 24 16:15:33 Starting compiler/encoders/asm
Jul 24 16:15:33 Finished compiler/encoders/asm                                    0s  26MB
Jul 24 16:15:34 Starting compiler/encoders/x64
Jul 24 16:16:23 Finished compiler/encoders/x64                                   48s   1GB
Jul 24 16:16:23 Starting compiler/encoders/arm7
Jul 24 16:17:58 Finished compiler/encoders/arm7                                1m34s 753MB
Jul 24 16:17:58 Starting compiler/encoders/arm8
Jul 24 16:18:23 Finished compiler/encoders/arm8                                  24s 593MB
Jul 24 16:18:23 Starting compiler/encoders/mips
Jul 24 16:18:55 Finished compiler/encoders/mips                                  32s   1GB
Jul 24 16:18:56 Starting compiler/encoders/riscv
Jul 24 16:19:24 Finished compiler/encoders/riscv                                 27s   1GB
Jul 24 16:19:24 Starting compiler/encoders/ag32
Jul 24 16:19:56 Finished compiler/encoders/ag32                                  31s 699MB
Jul 24 16:19:56 Starting compiler/backend/x64
Jul 24 16:20:29 Finished compiler/backend/x64                                    32s   1GB
Jul 24 16:20:29 Starting compiler/backend/arm7
Jul 24 16:21:07 Finished compiler/backend/arm7                                   38s   1GB
Jul 24 16:21:07 Starting compiler/backend/arm8
Jul 24 16:21:41 Finished compiler/backend/arm8                                   33s   1GB
Jul 24 16:21:41 Starting compiler/backend/mips
Jul 24 16:22:18 Finished compiler/backend/mips                                   36s   1GB
Jul 24 16:22:18 Starting compiler/backend/riscv
Jul 24 16:22:53 Finished compiler/backend/riscv                                  33s   1GB
Jul 24 16:22:53 Starting compiler/backend/ag32
Jul 24 16:24:53 Finished compiler/backend/ag32                                 2m00s   2GB
Jul 24 16:24:53 Starting compiler/parsing/proofs
Jul 24 16:34:50 Finished compiler/parsing/proofs                               9m56s   1GB
Jul 24 16:34:50 Starting compiler/inference/proofs
Jul 24 16:40:09 Finished compiler/inference/proofs                             5m18s   1GB
Jul 24 16:40:09 Starting compiler/backend/semantics
Jul 24 16:52:34 Finished compiler/backend/semantics                           12m24s   2GB
Jul 24 16:52:34 Starting compiler/backend/reg_alloc/proofs
Jul 24 16:58:58 Finished compiler/backend/reg_alloc/proofs                     6m23s 870MB
Jul 24 16:58:59 Starting compiler/backend/proofs
Jul 24 18:04:15 Finished compiler/backend/proofs                            1h05m16s  11GB
Jul 24 18:04:15 Starting compiler/encoders/x64/proofs
Jul 24 18:22:31 Finished compiler/encoders/x64/proofs                         18m15s   5GB
Jul 24 18:22:32 Starting compiler/encoders/arm7/proofs
Jul 24 18:47:37 Finished compiler/encoders/arm7/proofs                        25m05s   8GB
Jul 24 18:47:38 Starting compiler/encoders/arm8/proofs
Jul 24 19:00:09 Finished compiler/encoders/arm8/proofs                        12m31s   1GB
Jul 24 19:00:10 Starting compiler/encoders/mips/proofs
Jul 24 19:18:25 Finished compiler/encoders/mips/proofs                        18m15s   3GB
Jul 24 19:18:25 Starting compiler/encoders/riscv/proofs
Jul 24 19:33:42 Finished compiler/encoders/riscv/proofs                       15m17s   1GB
Jul 24 19:33:43 Starting compiler/encoders/ag32/proofs
Jul 24 19:38:11 Finished compiler/encoders/ag32/proofs                         4m27s 883MB
Jul 24 19:38:11 Starting compiler/backend/x64/proofs
Jul 24 19:38:48 Finished compiler/backend/x64/proofs                             36s   1GB
Jul 24 19:38:48 Starting compiler/backend/arm7/proofs
Jul 24 19:39:26 Finished compiler/backend/arm7/proofs                            37s   1GB
Jul 24 19:39:26 Starting compiler/backend/arm8/proofs
Jul 24 19:40:01 Finished compiler/backend/arm8/proofs                            35s   1GB
Jul 24 19:40:02 Starting compiler/backend/mips/proofs
Jul 24 19:40:40 Finished compiler/backend/mips/proofs                            38s   1GB
Jul 24 19:40:40 Starting compiler/backend/riscv/proofs
Jul 24 19:41:19 Finished compiler/backend/riscv/proofs                           38s   1GB
Jul 24 19:41:19 Starting compiler/backend/ag32/proofs
Jul 24 19:57:47 Finished compiler/backend/ag32/proofs                         16m27s   9GB
Jul 24 19:57:47 Starting compiler/proofs
Jul 24 20:00:09 Finished compiler/proofs                                       2m21s   2GB
Jul 24 20:00:09 Starting candle/set-theory
Jul 24 20:00:57 Finished candle/set-theory                                       47s   1GB
Jul 24 20:00:57 Starting candle/syntax-lib
Jul 24 20:01:16 Finished candle/syntax-lib                                       18s 593MB
Jul 24 20:01:16 Starting candle/standard/syntax
Jul 24 20:04:28 Finished candle/standard/syntax                                3m12s   1GB
Jul 24 20:04:28 Starting candle/standard/semantics
Jul 24 20:07:41 Finished candle/standard/semantics                             3m12s   1GB
Jul 24 20:07:42 Starting candle/standard/monadic
Jul 24 20:10:26 Finished candle/standard/monadic                               2m44s   1GB
Jul 24 20:10:27 Starting candle/standard/ml_kernel
Jul 24 20:17:26 Finished candle/standard/ml_kernel                             6m58s   3GB
Jul 24 20:17:26 Starting candle/standard/opentheory
Jul 24 20:33:46 Finished candle/standard/opentheory                           16m20s   4GB
Jul 24 20:33:47 Starting candle/standard/opentheory/compilation
Jul 25 05:23:15 Finished candle/standard/opentheory/compilation             8h49m27s 486GB
Jul 25 05:23:15 Starting candle/standard/opentheory/compilation/proofs
Jul 25 05:24:26 Finished candle/standard/opentheory/compilation/proofs         1m10s   3GB
Jul 25 05:24:26 Starting characteristic/examples
Jul 25 05:27:25 Finished characteristic/examples                               2m58s   4GB
Jul 25 05:27:26 Starting tutorial/solutions
Jul 25 07:13:46 Finished tutorial/solutions                                 1h46m20s 197GB
Jul 25 07:13:46 Starting translator/monadic/examples
Jul 25 07:18:13 Finished translator/monadic/examples                           4m26s   2GB
Jul 25 07:18:13 Starting examples
Jul 25 07:33:03 Finished examples                                             14m49s  19GB
Jul 25 07:33:04 Starting examples/compilation/x64
Jul 26 11:51:10 Finished examples/compilation/x64                          28h18m06s 712GB
Jul 26 11:51:11 Starting examples/compilation/x64/proofs
Jul 26 11:53:51 Finished examples/compilation/x64/proofs                       2m39s   3GB
Jul 26 11:53:51 Starting examples/compilation/ag32
Jul 26 14:34:23 Finished examples/compilation/ag32                          2h40m32s 137GB
Jul 26 14:34:23 Starting examples/compilation/ag32/proofs
Jul 26 14:36:08 Finished examples/compilation/ag32/proofs                      1m44s   4GB
Jul 26 14:36:09 Starting translator/okasaki-examples
Jul 26 14:43:09 Finished translator/okasaki-examples                           7m00s   1GB
Jul 26 14:43:09 Starting translator/other-examples
Jul 26 14:49:44 Finished translator/other-examples                             6m34s   1GB
Jul 26 14:49:44 Starting compiler/parsing/tests
Jul 26 14:50:40 Finished compiler/parsing/tests                                  55s   2GB
Jul 26 14:50:41 Starting compiler/inference/tests
Jul 26 15:06:50 Finished compiler/inference/tests                             16m09s  26GB
Jul 26 15:06:50 Starting compiler/bootstrap/translation
Jul 26 19:45:13 Finished compiler/bootstrap/translation                     4h38m23s  80GB
Jul 26 19:45:14 Starting unverified/sexpr-bootstrap/x64/64
Jul 26 20:06:20 Finished unverified/sexpr-bootstrap/x64/64                    21m06s   7GB
Jul 26 20:06:21 Starting unverified/sexpr-bootstrap/x64/32
Jul 26 20:20:05 Finished unverified/sexpr-bootstrap/x64/32                    13m43s   7GB
Jul 26 20:20:05 Starting compiler/benchmarks
Jul 26 20:43:45 Finished compiler/benchmarks                                  23m39s   2GB
Jul 26 20:43:45 Starting compiler/bootstrap/compilation/x64/64 Jul 26 20:43:45 2663s