Job 1619

CakeML:11ce5f9be7a62a7a9d1e8fc232d385c48c16d833
  Hook up decoder to bootstrap translation [Oct 21 06:45:24]
#841 (eval)
Merging into:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
  Merge pull request #839 from CakeML/lpr_transform [Oct 03 11:04:50]
HOL:56617180468ec5da8a1c0cfa582a16877f54a29b
  Make Theorem/Definition syntax slightly more liberal [Nov 03 04:51:40]
Machine:oven3 4.19.67.1.amd64-smp

Nov 04 19:19:13 Claimed job
Nov 04 19:19:27 Building HOL
Nov 04 19:44:06 Starting developers
Nov 04 19:44:15 Finished developers                                               8s 129MB
Nov 04 19:44:15 Starting developers/bin
Nov 04 19:44:27 Finished developers/bin                                          12s   1GB
Nov 04 19:44:28 Starting semantics/ffi
Nov 04 19:44:53 Finished semantics/ffi                                           25s 263MB
Nov 04 19:44:53 Starting semantics
Nov 04 19:48:06 Finished semantics                                             3m12s   1GB
Nov 04 19:48:06 Starting semantics/proofs
Nov 04 19:56:37 Finished semantics/proofs                                      8m31s   1GB
Nov 04 19:56:37 Starting semantics/alt_semantics
Nov 04 19:57:03 Finished semantics/alt_semantics                                 25s 391MB
Nov 04 19:57:03 Starting semantics/alt_semantics/proofs
Nov 04 20:02:23 Finished semantics/alt_semantics/proofs                        5m19s 965MB
Nov 04 20:02:23 Starting basis/pure
Nov 04 20:08:24 Finished basis/pure                                            6m01s 905MB
Nov 04 20:08:24 Starting translator
Nov 04 20:15:11 Finished translator                                            6m46s   1GB
Nov 04 20:15:11 Starting compiler/parsing
Nov 04 20:17:50 Finished compiler/parsing                                      2m38s   2GB
Nov 04 20:17:51 Starting characteristic
Nov 04 20:30:00 Finished characteristic                                       12m09s   2GB
Nov 04 20:30:00 Starting translator/monadic
Nov 04 20:33:40 Finished translator/monadic                                    3m40s   1GB
Nov 04 20:33:41 Starting basis
Nov 04 22:13:26 Finished basis                                              1h39m43s  15GB
Nov 04 22:13:27 Starting compiler/inference
Nov 04 22:16:11 Finished compiler/inference                                    2m44s   1GB
Nov 04 22:16:12 Starting compiler/backend/reg_alloc
Nov 04 22:18:22 Finished compiler/backend/reg_alloc                            2m10s   1GB
Nov 04 22:18:22 Starting compiler/backend/gc
Nov 04 22:25:22 Finished compiler/backend/gc                                   6m59s   2GB
Nov 04 22:25:22 Starting compiler/backend
Nov 04 22:35:21 Finished compiler/backend                                      9m59s   4GB
Nov 04 22:35:21 Starting compiler/encoders/asm
Nov 04 22:36:11 Finished compiler/encoders/asm                                   49s 797MB
Nov 04 22:36:11 Starting compiler/encoders/x64
Nov 04 22:38:28 Finished compiler/encoders/x64                                 2m16s 789MB
Nov 04 22:38:28 Starting compiler/encoders/arm7
Nov 04 22:43:03 Finished compiler/encoders/arm7                                4m34s   1GB
Nov 04 22:43:04 Starting compiler/encoders/arm8
Nov 04 22:44:27 Finished compiler/encoders/arm8                                1m22s 996MB
Nov 04 22:44:27 Starting compiler/encoders/mips
Nov 04 22:47:37 Finished compiler/encoders/mips                                3m09s   1GB
Nov 04 22:47:37 Starting compiler/encoders/riscv
Nov 04 22:51:30 Finished compiler/encoders/riscv                               3m52s   1GB
Nov 04 22:51:30 Starting compiler/encoders/ag32
Nov 04 22:52:11 Finished compiler/encoders/ag32                                  40s 765MB
Nov 04 22:52:11 Starting compiler/backend/x64
Nov 04 22:52:51 Finished compiler/backend/x64                                    39s   1GB
Nov 04 22:52:51 Starting compiler/backend/arm7
Nov 04 22:53:35 Finished compiler/backend/arm7                                   44s   1GB
Nov 04 22:53:36 Starting compiler/backend/arm8
Nov 04 22:54:18 Finished compiler/backend/arm8                                   41s   1GB
Nov 04 22:54:18 Starting compiler/backend/mips
Nov 04 22:55:00 Finished compiler/backend/mips                                   41s   1GB
Nov 04 22:55:00 Starting compiler/backend/riscv
Nov 04 22:55:43 Finished compiler/backend/riscv                                  42s   1GB
Nov 04 22:55:43 Starting compiler/backend/ag32
Nov 04 22:58:13 Finished compiler/backend/ag32                                 2m29s   1GB
Nov 04 22:58:13 Starting compiler/parsing/proofs
Nov 04 23:12:43 Finished compiler/parsing/proofs                              14m29s   1GB
Nov 04 23:12:43 Starting compiler/inference/proofs
Nov 04 23:18:16 Finished compiler/inference/proofs                             5m32s   1GB
Nov 04 23:18:16 Starting compiler/backend/semantics
Nov 05 00:19:16 Finished compiler/backend/semantics                         1h00m59s   3GB
Nov 05 00:19:17 Starting compiler/backend/reg_alloc/proofs
Nov 05 00:27:02 Finished compiler/backend/reg_alloc/proofs                     7m45s   1GB
Nov 05 00:27:02 Starting compiler/backend/proofs
Nov 05 02:07:46 Finished compiler/backend/proofs                            1h40m43s  12GB
Nov 05 02:07:46 Starting compiler/backend/serialiser
Nov 05 02:10:13 Finished compiler/backend/serialiser                           2m26s   1GB
Nov 05 02:10:13 Starting compiler/encoders/x64/proofs
Nov 05 02:31:25 Finished compiler/encoders/x64/proofs                         21m11s   4GB
Nov 05 02:31:25 Starting compiler/encoders/arm7/proofs
Nov 05 03:00:41 Finished compiler/encoders/arm7/proofs                        29m16s   3GB
Nov 05 03:00:41 Starting compiler/encoders/arm8/proofs
Nov 05 03:15:40 Finished compiler/encoders/arm8/proofs                        14m57s   1GB
Nov 05 03:15:40 Starting compiler/encoders/mips/proofs
Nov 05 03:37:58 Finished compiler/encoders/mips/proofs                        22m17s   3GB
Nov 05 03:37:58 Starting compiler/encoders/riscv/proofs
Nov 05 03:57:57 Finished compiler/encoders/riscv/proofs                       19m58s   1GB
Nov 05 03:57:57 Starting compiler/encoders/ag32/proofs
Nov 05 04:03:40 Finished compiler/encoders/ag32/proofs                         5m43s 784MB
Nov 05 04:03:40 Starting compiler/backend/x64/proofs
Nov 05 04:04:32 Finished compiler/backend/x64/proofs                             51s   1GB
Nov 05 04:04:32 Starting compiler/backend/arm7/proofs
Nov 05 04:05:24 Finished compiler/backend/arm7/proofs                            51s   1GB
Nov 05 04:05:24 Starting compiler/backend/arm8/proofs
Nov 05 04:06:13 Finished compiler/backend/arm8/proofs                            49s   1GB
Nov 05 04:06:14 Starting compiler/backend/mips/proofs
Nov 05 04:07:03 Finished compiler/backend/mips/proofs                            49s   1GB
Nov 05 04:07:03 Starting compiler/backend/riscv/proofs
Nov 05 04:07:54 Finished compiler/backend/riscv/proofs                           50s   1GB
Nov 05 04:07:54 Starting compiler/backend/ag32/proofs
Nov 05 04:35:10 Finished compiler/backend/ag32/proofs                         27m15s   3GB
Nov 05 04:35:10 Starting compiler/proofs
Nov 05 04:39:38 Finished compiler/proofs                                       4m27s   5GB
Nov 05 04:39:38 Starting candle/set-theory
Nov 05 04:40:38 Finished candle/set-theory                                     1m00s 801MB
Nov 05 04:40:39 Starting candle/syntax-lib
Nov 05 04:41:02 Finished candle/syntax-lib                                       22s 455MB
Nov 05 04:41:02 Starting candle/standard/syntax
Nov 05 04:45:00 Finished candle/standard/syntax                                3m57s   1GB
Nov 05 04:45:00 Starting candle/standard/semantics