Job 1110

CakeML:71b306fb43e3ee260109a3bd41496a7873aed44f
  Avoid ARB in configs [Nov 28 10:05:57]
#707 (data-cost)
Merging into:c472a5c9eeea5c1d67e039697cb3e0f1c4e10831
  Fix a proof and some terrible indentation [Nov 28 06:33:56]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 28 15:07:26 Claimed job
Nov 28 15:07:30 Building HOL
Nov 28 15:16:57 Starting developers
Nov 28 15:16:59 Finished developers                                               2s 129MB
Nov 28 15:16:59 Starting developers/bin
Nov 28 15:17:03 Finished developers/bin                                           3s 164MB
Nov 28 15:17:03 Starting semantics/ffi
Nov 28 15:17:11 Finished semantics/ffi                                            7s 227MB
Nov 28 15:17:11 Starting semantics
Nov 28 15:18:37 Finished semantics                                             1m25s   1GB
Nov 28 15:18:37 Starting semantics/proofs
Nov 28 15:21:38 Finished semantics/proofs                                      2m59s 967MB
Nov 28 15:21:38 Starting semantics/alt_semantics
Nov 28 15:21:44 Finished semantics/alt_semantics                                  6s 292MB
Nov 28 15:21:45 Starting semantics/alt_semantics/proofs
Nov 28 15:23:35 Finished semantics/alt_semantics/proofs                        1m50s 812MB
Nov 28 15:23:35 Starting basis/pure
Nov 28 15:26:27 Finished basis/pure                                            2m51s 763MB
Nov 28 15:26:27 Starting translator
Nov 28 15:28:14 Finished translator                                            1m46s   1GB
Nov 28 15:28:14 Starting compiler/parsing
Nov 28 15:29:19 Finished compiler/parsing                                      1m04s   2GB
Nov 28 15:29:19 Starting characteristic
Nov 28 15:34:38 Finished characteristic                                        5m18s   1GB
Nov 28 15:34:38 Starting translator/monadic
Nov 28 15:36:07 Finished translator/monadic                                    1m28s   1GB
Nov 28 15:36:07 Starting basis
Nov 28 15:55:49 Finished basis                                                19m40s   2GB
Nov 28 15:55:49 Starting compiler/inference
Nov 28 15:57:33 Finished compiler/inference                                    1m44s   1GB
Nov 28 15:57:34 Starting compiler/backend/reg_alloc
Nov 28 15:58:34 Finished compiler/backend/reg_alloc                            1m00s   1GB
Nov 28 15:58:34 Starting compiler/backend/gc
Nov 28 16:01:44 Finished compiler/backend/gc                                   3m09s   2GB
Nov 28 16:01:44 Starting compiler/backend
Nov 28 16:05:28 Finished compiler/backend                                      3m44s   2GB
Nov 28 16:05:29 Starting compiler/encoders/asm
Nov 28 16:05:48 Finished compiler/encoders/asm                                   19s 697MB
Nov 28 16:05:49 Starting compiler/encoders/x64
Nov 28 16:06:41 Finished compiler/encoders/x64                                   51s 891MB
Nov 28 16:06:41 Starting compiler/encoders/arm7
Nov 28 16:08:19 Finished compiler/encoders/arm7                                1m37s   1GB
Nov 28 16:08:19 Starting compiler/encoders/arm8
Nov 28 16:08:49 Finished compiler/encoders/arm8                                  29s 579MB
Nov 28 16:08:49 Starting compiler/encoders/mips
Nov 28 16:09:55 Finished compiler/encoders/mips                                1m05s 957MB
Nov 28 16:09:55 Starting compiler/encoders/riscv
Nov 28 16:11:13 Finished compiler/encoders/riscv                               1m18s 818MB
Nov 28 16:11:14 Starting compiler/encoders/ag32
Nov 28 16:11:29 Finished compiler/encoders/ag32                                  15s 791MB
Nov 28 16:11:29 Starting compiler/backend/x64
Nov 28 16:11:47 Finished compiler/backend/x64                                    17s 964MB
Nov 28 16:11:47 Starting compiler/backend/arm7
Nov 28 16:12:06 Finished compiler/backend/arm7                                   18s   1GB
Nov 28 16:12:06 Starting compiler/backend/arm8
Nov 28 16:12:24 Finished compiler/backend/arm8                                   17s   1GB
Nov 28 16:12:24 Starting compiler/backend/mips
Nov 28 16:12:42 Finished compiler/backend/mips                                   17s   1GB
Nov 28 16:12:42 Starting compiler/backend/riscv
Nov 28 16:13:00 Finished compiler/backend/riscv                                  17s   1GB
Nov 28 16:13:00 Starting compiler/backend/ag32
Nov 28 16:14:06 Finished compiler/backend/ag32                                 1m05s   1GB
Nov 28 16:14:06 Starting compiler/parsing/proofs
Nov 28 16:19:43 Finished compiler/parsing/proofs                               5m36s 806MB
Nov 28 16:19:44 Starting compiler/inference/proofs
Nov 28 16:22:29 Finished compiler/inference/proofs                             2m45s   1GB
Nov 28 16:22:29 Starting compiler/backend/semantics
Nov 28 16:41:51 Finished compiler/backend/semantics                           19m21s   2GB
Nov 28 16:41:51 Starting compiler/backend/reg_alloc/proofs
Nov 28 16:45:11 Finished compiler/backend/reg_alloc/proofs                     3m19s 780MB
Nov 28 16:45:11 Starting compiler/backend/proofs
Nov 28 17:40:58 Finished compiler/backend/proofs                              55m46s  18GB
Nov 28 17:40:58 Starting compiler/encoders/x64/proofs
Nov 28 17:50:06 Finished compiler/encoders/x64/proofs                          9m07s   5GB
Nov 28 17:50:06 Starting compiler/encoders/arm7/proofs
Nov 28 18:02:28 Finished compiler/encoders/arm7/proofs                        12m21s   3GB
Nov 28 18:02:28 Starting compiler/encoders/arm8/proofs
Nov 28 18:08:44 Finished compiler/encoders/arm8/proofs                         6m15s   1GB
Nov 28 18:08:44 Starting compiler/encoders/mips/proofs
Nov 28 18:18:06 Finished compiler/encoders/mips/proofs                         9m21s   3GB
Nov 28 18:18:06 Starting compiler/encoders/riscv/proofs
Nov 28 18:26:27 Finished compiler/encoders/riscv/proofs                        8m21s   1GB
Nov 28 18:26:27 Starting compiler/encoders/ag32/proofs
Nov 28 18:28:52 Finished compiler/encoders/ag32/proofs                         2m24s 859MB
Nov 28 18:28:53 Starting compiler/backend/x64/proofs
Nov 28 18:29:10 Finished compiler/backend/x64/proofs                             17s   1GB
Nov 28 18:29:11 Starting compiler/backend/arm7/proofs
Nov 28 18:29:28 Finished compiler/backend/arm7/proofs                            17s   1GB
Nov 28 18:29:29 Starting compiler/backend/arm8/proofs
Nov 28 18:29:46 Finished compiler/backend/arm8/proofs                            16s   1GB
Nov 28 18:29:46 Starting compiler/backend/mips/proofs
Nov 28 18:30:04 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 28 18:30:05 Starting compiler/backend/riscv/proofs
Nov 28 18:30:23 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 28 18:30:23 Starting compiler/backend/ag32/proofs
Nov 28 18:39:28 Finished compiler/backend/ag32/proofs                          9m05s   3GB
Nov 28 18:39:29 Starting compiler/proofs
Nov 28 18:41:02 Finished compiler/proofs                                       1m32s   3GB
Nov 28 18:41:02 Starting candle/set-theory
Nov 28 18:41:29 Finished candle/set-theory                                       26s 726MB
Nov 28 18:41:30 Starting candle/syntax-lib
Nov 28 18:41:39 Finished candle/syntax-lib                                        9s 634MB
Nov 28 18:41:40 Starting candle/standard/syntax
Nov 28 18:43:22 Finished candle/standard/syntax                                1m42s   1GB
Nov 28 18:43:22 Starting candle/standard/semantics
Nov 28 18:44:58 Finished candle/standard/semantics                             1m35s   1GB
Nov 28 18:44:59 Starting candle/standard/monadic
Nov 28 18:46:35 Finished candle/standard/monadic                               1m35s   1GB
Nov 28 18:46:35 Starting candle/standard/ml_kernel
Nov 28 18:50:26 Finished candle/standard/ml_kernel                             3m50s   4GB
Nov 28 18:50:26 Starting candle/standard/opentheory
Nov 28 18:59:21 Finished candle/standard/opentheory                            8m54s   5GB
Nov 28 18:59:21 Starting candle/standard/opentheory/compilation
Nov 28 19:29:39 Finished candle/standard/opentheory/compilation               30m18s  15GB
Nov 28 19:29:40 Starting candle/standard/opentheory/compilation/proofs
Nov 28 19:30:27 Finished candle/standard/opentheory/compilation/proofs           47s   3GB
Nov 28 19:30:27 Starting characteristic/examples
Nov 28 19:31:57 Finished characteristic/examples                               1m29s   2GB
Nov 28 19:31:57 Starting tutorial/solutions
Nov 28 19:45:20 Finished tutorial/solutions                                   13m22s   7GB
Nov 28 19:45:20 Starting translator/monadic/examples
Nov 28 19:48:13 Finished translator/monadic/examples                           2m52s   3GB
Nov 28 19:48:13 Starting examples
Nov 28 19:57:14 Finished examples                                              9m00s   3GB
Nov 28 19:57:14 Starting examples/compilation/x64
Nov 28 22:04:07 Finished examples/compilation/x64                           2h06m51s  14GB
Nov 28 22:04:07 Starting examples/compilation/x64/proofs
Nov 28 22:05:42 Finished examples/compilation/x64/proofs                       1m34s   2GB
Nov 28 22:05:42 Starting examples/compilation/ag32
Nov 28 22:34:34 Finished examples/compilation/ag32                            28m51s   6GB
Nov 28 22:34:34 Starting examples/compilation/ag32/proofs
Nov 28 22:35:13 Finished examples/compilation/ag32/proofs                        39s   2GB
Nov 28 22:35:13 Starting examples/cost
Nov 28 22:56:44 Finished examples/cost                                        21m30s   7GB
Nov 28 22:56:44 Starting translator/okasaki-examples
Nov 28 23:00:51 Finished translator/okasaki-examples                           4m06s   1GB
Nov 28 23:00:51 Starting translator/other-examples
Nov 28 23:02:32 Finished translator/other-examples                             1m40s   1GB
Nov 28 23:02:32 Starting compiler/parsing/tests
Nov 28 23:02:55 Finished compiler/parsing/tests                                  23s 451MB
Nov 28 23:02:56 Starting compiler/inference/tests
Nov 28 23:07:18 Finished compiler/inference/tests                              4m21s   3GB
Nov 28 23:07:18 Starting compiler/bootstrap/translation
Nov 29 01:42:11 Finished compiler/bootstrap/translation                     2h34m52s  45GB
Nov 29 01:42:11 Starting unverified/sexpr-bootstrap/x64/64
Nov 29 01:57:13 Finished unverified/sexpr-bootstrap/x64/64                    15m00s   3GB
Nov 29 01:57:13 Starting unverified/sexpr-bootstrap/x64/32
Nov 29 02:07:26 Finished unverified/sexpr-bootstrap/x64/32                    10m12s   7GB
Nov 29 02:07:26 Starting compiler/benchmarks
Nov 29 02:46:03 Finished compiler/benchmarks                                  38m35s   1GB
Nov 29 02:46:03 Starting compiler/bootstrap/compilation/x64/64
Nov 29 15:00:14 Finished compiler/bootstrap/compilation/x64/64             12h14m09s  64GB
Nov 29 15:00:14 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 29 15:04:11 Finished compiler/bootstrap/compilation/x64/64/proofs          3m56s   5GB
Nov 29 15:04:11 Starting compiler/bootstrap/compilation/x64/32
Nov 30 03:17:29 Finished compiler/bootstrap/compilation/x64/32             12h13m17s  64GB
Nov 30 03:17:30 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 30 03:20:45 Finished compiler/bootstrap/compilation/x64/32/proofs          3m14s   5GB
Nov 30 03:20:45 Starting compiler/bootstrap/compilation/ag32/32
Nov 30 16:15:37 Finished compiler/bootstrap/compilation/ag32/32            12h54m51s  64GB
Nov 30 16:15:37 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 30 16:56:24 Finished compiler/bootstrap/compilation/ag32/32/proofs        40m46s  18GB
Nov 30 16:56:25 SUCCESS