Job 1122

CakeML:cba2304f48eaaede2d427419564f2c2e5d8b7e9a
  More CF fixes [Dec 10 22:02:09]
#692 (match-refactor-2)
Merging into:10943f8db35376f05a51dc0c63484da1b62abee6
  Merge pull request #708 from CakeML/lrat [Dec 09 23:25:17]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 10 22:02:37 Claimed job
Dec 10 22:02:40 Reusing HOL
Dec 10 22:02:45 Starting developers
Dec 10 22:02:46 Finished developers                                               0s  22MB
Dec 10 22:02:46 Starting developers/bin
Dec 10 22:02:50 Finished developers/bin                                           3s 238MB
Dec 10 22:02:50 Starting semantics/ffi
Dec 10 22:02:58 Finished semantics/ffi                                            7s 211MB
Dec 10 22:02:58 Starting semantics
Dec 10 22:04:14 Finished semantics                                             1m15s   1GB
Dec 10 22:04:14 Starting semantics/proofs
Dec 10 22:07:20 Finished semantics/proofs                                      3m06s   1GB
Dec 10 22:07:21 Starting semantics/alt_semantics
Dec 10 22:07:27 Finished semantics/alt_semantics                                  6s 292MB
Dec 10 22:07:28 Starting semantics/alt_semantics/proofs
Dec 10 22:09:25 Finished semantics/alt_semantics/proofs                        1m56s 808MB
Dec 10 22:09:25 Starting basis/pure
Dec 10 22:10:12 Finished basis/pure                                              46s 830MB
Dec 10 22:10:12 Starting translator
Dec 10 22:12:38 Finished translator                                            2m25s   1GB
Dec 10 22:12:38 Starting compiler/parsing
Dec 10 22:13:43 Finished compiler/parsing                                      1m04s   2GB
Dec 10 22:13:43 Starting characteristic
Dec 10 22:19:08 Finished characteristic                                        5m24s   1GB
Dec 10 22:19:09 Starting translator/monadic
Dec 10 22:20:39 Finished translator/monadic                                    1m30s   1GB
Dec 10 22:20:39 Starting basis
Dec 10 22:53:36 Finished basis                                                32m56s  25GB
Dec 10 22:53:36 Starting compiler/inference
Dec 10 22:55:14 Finished compiler/inference                                    1m36s   1GB
Dec 10 22:55:14 Starting compiler/backend/reg_alloc
Dec 10 22:56:18 Finished compiler/backend/reg_alloc                            1m03s   1GB
Dec 10 22:56:18 Starting compiler/backend/gc
Dec 10 22:59:29 Finished compiler/backend/gc                                   3m10s   1GB
Dec 10 22:59:29 Starting compiler/backend
Dec 10 23:03:15 Finished compiler/backend                                      3m45s   1GB
Dec 10 23:03:15 Starting compiler/encoders/asm
Dec 10 23:03:36 Finished compiler/encoders/asm                                   20s 859MB
Dec 10 23:03:36 Starting compiler/encoders/x64
Dec 10 23:04:00 Finished compiler/encoders/x64                                   23s 699MB
Dec 10 23:04:00 Starting compiler/encoders/arm7
Dec 10 23:04:46 Finished compiler/encoders/arm7                                  45s   1GB
Dec 10 23:04:46 Starting compiler/encoders/arm8
Dec 10 23:04:58 Finished compiler/encoders/arm8                                  11s 579MB
Dec 10 23:04:58 Starting compiler/encoders/mips
Dec 10 23:05:15 Finished compiler/encoders/mips                                  16s 947MB
Dec 10 23:05:15 Starting compiler/encoders/riscv
Dec 10 23:05:29 Finished compiler/encoders/riscv                                 13s 905MB
Dec 10 23:05:29 Starting compiler/encoders/ag32
Dec 10 23:05:45 Finished compiler/encoders/ag32                                  16s 545MB
Dec 10 23:05:46 Starting compiler/backend/x64
Dec 10 23:06:03 Finished compiler/backend/x64                                    17s   1GB
Dec 10 23:06:03 Starting compiler/backend/arm7
Dec 10 23:06:22 Finished compiler/backend/arm7                                   18s   1GB
Dec 10 23:06:22 Starting compiler/backend/arm8
Dec 10 23:06:39 Finished compiler/backend/arm8                                   16s   1GB
Dec 10 23:06:40 Starting compiler/backend/mips
Dec 10 23:06:58 Finished compiler/backend/mips                                   17s   1GB
Dec 10 23:06:58 Starting compiler/backend/riscv
Dec 10 23:07:16 Finished compiler/backend/riscv                                  17s   1GB
Dec 10 23:07:16 Starting compiler/backend/ag32
Dec 10 23:08:23 Finished compiler/backend/ag32                                 1m07s   1GB
Dec 10 23:08:24 Starting compiler/parsing/proofs
Dec 10 23:13:54 Finished compiler/parsing/proofs                               5m30s   1GB
Dec 10 23:13:54 Starting compiler/inference/proofs
Dec 10 23:16:47 Finished compiler/inference/proofs                             2m52s   1GB
Dec 10 23:16:47 Starting compiler/backend/semantics
Dec 10 23:36:31 Finished compiler/backend/semantics                           19m43s   2GB
Dec 10 23:36:32 Starting compiler/backend/reg_alloc/proofs
Dec 10 23:39:50 Finished compiler/backend/reg_alloc/proofs                     3m18s 799MB
Dec 10 23:39:51 Starting compiler/backend/proofs
Dec 11 00:40:46 Finished compiler/backend/proofs                            1h00m54s  14GB
Dec 11 00:40:46 Starting compiler/encoders/x64/proofs
Dec 11 00:49:54 Finished compiler/encoders/x64/proofs                          9m07s   5GB
Dec 11 00:49:55 Starting compiler/encoders/arm7/proofs
Dec 11 01:02:09 Finished compiler/encoders/arm7/proofs                        12m13s   3GB
Dec 11 01:02:09 Starting compiler/encoders/arm8/proofs
Dec 11 01:08:24 Finished compiler/encoders/arm8/proofs                         6m14s   1GB
Dec 11 01:08:24 Starting compiler/encoders/mips/proofs
Dec 11 01:18:12 Finished compiler/encoders/mips/proofs                         9m47s   2GB
Dec 11 01:18:12 Starting compiler/encoders/riscv/proofs
Dec 11 01:26:37 Finished compiler/encoders/riscv/proofs                        8m24s   1GB
Dec 11 01:26:37 Starting compiler/encoders/ag32/proofs
Dec 11 01:29:04 Finished compiler/encoders/ag32/proofs                         2m26s 732MB
Dec 11 01:29:04 Starting compiler/backend/x64/proofs
Dec 11 01:29:23 Finished compiler/backend/x64/proofs                             18s   1GB
Dec 11 01:29:24 Starting compiler/backend/arm7/proofs
Dec 11 01:29:43 Finished compiler/backend/arm7/proofs                            18s   1GB
Dec 11 01:29:43 Starting compiler/backend/arm8/proofs
Dec 11 01:30:00 Finished compiler/backend/arm8/proofs                            16s 764MB
Dec 11 01:30:00 Starting compiler/backend/mips/proofs
Dec 11 01:30:19 Finished compiler/backend/mips/proofs                            18s   1GB
Dec 11 01:30:20 Starting compiler/backend/riscv/proofs
Dec 11 01:30:38 Finished compiler/backend/riscv/proofs                           17s   1GB
Dec 11 01:30:38 Starting compiler/backend/ag32/proofs
Dec 11 01:39:38 Finished compiler/backend/ag32/proofs                          8m59s   2GB
Dec 11 01:39:38 Starting compiler/proofs
Dec 11 01:41:02 Finished compiler/proofs                                       1m23s   2GB
Dec 11 01:41:02 Starting candle/set-theory
Dec 11 01:41:29 Finished candle/set-theory                                       27s 756MB
Dec 11 01:41:31 Starting candle/syntax-lib
Dec 11 01:41:41 Finished candle/syntax-lib                                        9s 600MB
Dec 11 01:41:41 Starting candle/standard/syntax
Dec 11 01:43:24 Finished candle/standard/syntax                                1m42s   1GB
Dec 11 01:43:25 Starting candle/standard/semantics
Dec 11 01:45:02 Finished candle/standard/semantics                             1m36s   1GB
Dec 11 01:45:02 Starting candle/standard/monadic
Dec 11 01:46:37 Finished candle/standard/monadic                               1m34s   1GB
Dec 11 01:46:37 Starting candle/standard/ml_kernel
Dec 11 01:51:34 Finished candle/standard/ml_kernel                             4m56s   5GB
Dec 11 01:51:34 Starting candle/standard/opentheory
Dec 11 02:00:57 Finished candle/standard/opentheory                            9m23s   3GB
Dec 11 02:00:58 Starting candle/standard/opentheory/compilation
Dec 11 02:31:57 Finished candle/standard/opentheory/compilation               30m59s  14GB
Dec 11 02:31:57 Starting candle/standard/opentheory/compilation/proofs
Dec 11 02:32:44 Finished candle/standard/opentheory/compilation/proofs           45s   2GB
Dec 11 02:32:44 Starting characteristic/examples
Dec 11 02:34:14 Finished characteristic/examples                               1m29s   2GB
Dec 11 02:34:14 Starting tutorial/solutions
Dec 11 02:47:29 Finished tutorial/solutions                                   13m14s   7GB
Dec 11 02:47:29 Starting translator/monadic/examples
Dec 11 02:50:43 Finished translator/monadic/examples                           3m13s   2GB
Dec 11 02:50:43 Starting examples
Dec 11 03:01:05 Finished examples                                             10m21s   3GB
Dec 11 03:01:05 Starting examples/compilation/x64
Dec 11 05:08:53 Finished examples/compilation/x64                           2h07m47s  15GB
Dec 11 05:08:53 Starting examples/compilation/x64/proofs
Dec 11 05:10:51 Finished examples/compilation/x64/proofs                       1m57s   2GB
Dec 11 05:10:51 Starting examples/compilation/ag32
Dec 11 05:39:58 Finished examples/compilation/ag32                            29m06s   7GB
Dec 11 05:39:58 Starting examples/compilation/ag32/proofs
Dec 11 05:40:38 Finished examples/compilation/ag32/proofs                        38s   2GB
Dec 11 05:40:38 Starting examples/cost
Dec 11 06:02:30 Finished examples/cost                                        21m51s   8GB
Dec 11 06:02:30 Starting examples/lrat_checker
Dec 11 06:05:56 Finished examples/lrat_checker                                 3m24s   3GB
Dec 11 06:05:56 Starting examples/lrat_checker/compilation
Dec 11 06:21:36 Finished examples/lrat_checker/compilation                    15m39s   8GB
Dec 11 06:21:36 Starting examples/lrat_checker/compilation/proofs
Dec 11 06:22:10 Finished examples/lrat_checker/compilation/proofs                32s   3GB
Dec 11 06:22:10 Starting examples/lrat_checker/array
Dec 11 06:28:24 Finished examples/lrat_checker/array                           6m14s   2GB
Dec 11 06:28:25 Starting examples/lrat_checker/array/compilation
Dec 11 06:41:59 Finished examples/lrat_checker/array/compilation              13m33s   8GB
Dec 11 06:41:59 Starting examples/lrat_checker/array/compilation/proofs
Dec 11 06:42:37 Finished examples/lrat_checker/array/compilation/proofs          37s   2GB
Dec 11 06:42:37 Starting translator/okasaki-examples
Dec 11 06:46:49 Finished translator/okasaki-examples                           4m11s   1GB
Dec 11 06:46:49 Starting translator/other-examples
Dec 11 06:47:26 Finished translator/other-examples                               36s   1GB
Dec 11 06:47:26 Starting compiler/parsing/tests
Dec 11 06:47:51 Finished compiler/parsing/tests                                  24s 541MB
Dec 11 06:47:51 Starting compiler/inference/tests
Dec 11 06:52:18 Finished compiler/inference/tests                              4m26s   4GB
Dec 11 06:52:19 Starting compiler/bootstrap/translation
Dec 11 10:16:42 Finished compiler/bootstrap/translation                     3h24m23s  43GB
Dec 11 10:16:43 Starting unverified/sexpr-bootstrap/x64/64
Dec 11 10:32:26 Finished unverified/sexpr-bootstrap/x64/64                    15m42s   3GB
Dec 11 10:32:26 Starting unverified/sexpr-bootstrap/x64/32
Dec 11 10:43:19 Finished unverified/sexpr-bootstrap/x64/32                    10m52s   7GB
Dec 11 10:43:19 Starting compiler/benchmarks
Dec 11 11:21:07 Finished compiler/benchmarks                                  37m47s   2GB
Dec 11 11:21:07 Starting compiler/bootstrap/compilation/x64/64
Dec 12 01:10:17 Finished compiler/bootstrap/compilation/x64/64             13h49m08s  64GB
Dec 12 01:10:17 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 12 01:14:33 Finished compiler/bootstrap/compilation/x64/64/proofs          4m15s   5GB
Dec 12 01:14:33 Starting compiler/bootstrap/compilation/x64/32
Dec 12 14:44:44 Finished compiler/bootstrap/compilation/x64/32             13h30m10s  64GB
Dec 12 14:44:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 12 14:48:57 Finished compiler/bootstrap/compilation/x64/32/proofs          4m12s   5GB
Dec 12 14:48:58 Starting compiler/bootstrap/compilation/ag32/32
Dec 13 03:39:50 Finished compiler/bootstrap/compilation/ag32/32            12h50m52s  64GB
Dec 13 03:39:51 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 13 04:10:12 Finished compiler/bootstrap/compilation/ag32/32/proofs        30m20s  17GB
Dec 13 04:10:12 SUCCESS