Job 1111

CakeML:1ac7dc2c330764836bfa3d58006aefbc591fc402
  Expose TextIO.input1 (used by catProg example) [Nov 30 13:30:45]
#702 (bufferedio)
Merging into:b42ce697adbe59d51cb59eb92a56fc360fa5ba4e
  Merge pull request #707 from CakeML/data-cost [Nov 30 23:36:35]
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 30 23:38:35 Claimed job
Nov 30 23:38:39 Reusing HOL
Nov 30 23:38:51 Starting developers
Nov 30 23:38:53 Finished developers                                               2s 102MB
Nov 30 23:38:53 Starting developers/bin
Nov 30 23:39:00 Finished developers/bin                                           5s 164MB
Nov 30 23:39:00 Starting semantics/ffi
Nov 30 23:39:08 Finished semantics/ffi                                            7s 208MB
Nov 30 23:39:08 Starting semantics
Nov 30 23:40:24 Finished semantics                                             1m15s   1GB
Nov 30 23:40:24 Starting semantics/proofs
Nov 30 23:43:23 Finished semantics/proofs                                      2m57s   1GB
Nov 30 23:43:23 Starting semantics/alt_semantics
Nov 30 23:43:29 Finished semantics/alt_semantics                                  6s 273MB
Nov 30 23:43:30 Starting semantics/alt_semantics/proofs
Nov 30 23:45:19 Finished semantics/alt_semantics/proofs                        1m48s 766MB
Nov 30 23:45:19 Starting basis/pure
Nov 30 23:46:06 Finished basis/pure                                              46s 708MB
Nov 30 23:46:06 Starting translator
Nov 30 23:47:54 Finished translator                                            1m47s   1GB
Nov 30 23:47:54 Starting compiler/parsing
Nov 30 23:48:59 Finished compiler/parsing                                      1m04s   1GB
Nov 30 23:48:59 Starting characteristic
Nov 30 23:54:17 Finished characteristic                                        5m18s   1GB
Nov 30 23:54:18 Starting translator/monadic
Nov 30 23:55:44 Finished translator/monadic                                    1m26s   1GB
Nov 30 23:55:45 Starting basis
Dec 01 00:28:01 Finished basis                                                32m16s  22GB
Dec 01 00:28:02 Starting compiler/inference
Dec 01 00:29:39 Finished compiler/inference                                    1m36s   1GB
Dec 01 00:29:39 Starting compiler/backend/reg_alloc
Dec 01 00:30:40 Finished compiler/backend/reg_alloc                            1m00s   1GB
Dec 01 00:30:40 Starting compiler/backend/gc
Dec 01 00:33:38 Finished compiler/backend/gc                                   2m57s   2GB
Dec 01 00:33:39 Starting compiler/backend
Dec 01 00:37:26 Finished compiler/backend                                      3m46s   2GB
Dec 01 00:37:26 Starting compiler/encoders/asm
Dec 01 00:37:46 Finished compiler/encoders/asm                                   19s 726MB
Dec 01 00:37:46 Starting compiler/encoders/x64
Dec 01 00:38:10 Finished compiler/encoders/x64                                   23s 703MB
Dec 01 00:38:10 Starting compiler/encoders/arm7
Dec 01 00:38:55 Finished compiler/encoders/arm7                                  45s 642MB
Dec 01 00:38:56 Starting compiler/encoders/arm8
Dec 01 00:39:07 Finished compiler/encoders/arm8                                  11s 590MB
Dec 01 00:39:08 Starting compiler/encoders/mips
Dec 01 00:39:24 Finished compiler/encoders/mips                                  16s 947MB
Dec 01 00:39:25 Starting compiler/encoders/riscv
Dec 01 00:39:38 Finished compiler/encoders/riscv                                 13s 905MB
Dec 01 00:39:38 Starting compiler/encoders/ag32
Dec 01 00:39:55 Finished compiler/encoders/ag32                                  16s 545MB
Dec 01 00:39:55 Starting compiler/backend/x64
Dec 01 00:40:12 Finished compiler/backend/x64                                    16s 958MB
Dec 01 00:40:13 Starting compiler/backend/arm7
Dec 01 00:40:31 Finished compiler/backend/arm7                                   17s   1GB
Dec 01 00:40:31 Starting compiler/backend/arm8
Dec 01 00:40:48 Finished compiler/backend/arm8                                   17s   1GB
Dec 01 00:40:49 Starting compiler/backend/mips
Dec 01 00:41:07 Finished compiler/backend/mips                                   17s   1GB
Dec 01 00:41:07 Starting compiler/backend/riscv
Dec 01 00:41:25 Finished compiler/backend/riscv                                  17s   1GB
Dec 01 00:41:25 Starting compiler/backend/ag32
Dec 01 00:42:31 Finished compiler/backend/ag32                                 1m06s   1GB
Dec 01 00:42:32 Starting compiler/parsing/proofs
Dec 01 00:48:03 Finished compiler/parsing/proofs                               5m30s 818MB
Dec 01 00:48:03 Starting compiler/inference/proofs
Dec 01 00:50:47 Finished compiler/inference/proofs                             2m43s   1GB
Dec 01 00:50:47 Starting compiler/backend/semantics
Dec 01 01:10:15 Finished compiler/backend/semantics                           19m27s   1GB
Dec 01 01:10:15 Starting compiler/backend/reg_alloc/proofs
Dec 01 01:13:30 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Dec 01 01:13:30 Starting compiler/backend/proofs
Dec 01 02:09:49 Finished compiler/backend/proofs                              56m18s  19GB
Dec 01 02:09:50 Starting compiler/encoders/x64/proofs
Dec 01 02:19:01 Finished compiler/encoders/x64/proofs                          9m10s   5GB
Dec 01 02:19:01 Starting compiler/encoders/arm7/proofs
Dec 01 02:31:32 Finished compiler/encoders/arm7/proofs                        12m30s   3GB
Dec 01 02:31:32 Starting compiler/encoders/arm8/proofs
Dec 01 02:37:47 Finished compiler/encoders/arm8/proofs                         6m14s   1GB
Dec 01 02:37:47 Starting compiler/encoders/mips/proofs
Dec 01 02:47:19 Finished compiler/encoders/mips/proofs                         9m31s   3GB
Dec 01 02:47:20 Starting compiler/encoders/riscv/proofs
Dec 01 02:55:50 Finished compiler/encoders/riscv/proofs                        8m30s   1GB
Dec 01 02:55:50 Starting compiler/encoders/ag32/proofs
Dec 01 02:58:13 Finished compiler/encoders/ag32/proofs                         2m22s 871MB
Dec 01 02:58:13 Starting compiler/backend/x64/proofs
Dec 01 02:58:31 Finished compiler/backend/x64/proofs                             17s   1GB
Dec 01 02:58:32 Starting compiler/backend/arm7/proofs
Dec 01 02:58:49 Finished compiler/backend/arm7/proofs                            17s   1GB
Dec 01 02:58:49 Starting compiler/backend/arm8/proofs
Dec 01 02:59:06 Finished compiler/backend/arm8/proofs                            16s 757MB
Dec 01 02:59:06 Starting compiler/backend/mips/proofs
Dec 01 02:59:24 Finished compiler/backend/mips/proofs                            17s   1GB
Dec 01 02:59:25 Starting compiler/backend/riscv/proofs
Dec 01 02:59:43 Finished compiler/backend/riscv/proofs                           17s   1GB
Dec 01 02:59:43 Starting compiler/backend/ag32/proofs
Dec 01 03:08:42 Finished compiler/backend/ag32/proofs                          8m59s   2GB
Dec 01 03:08:43 Starting compiler/proofs
Dec 01 03:10:10 Finished compiler/proofs                                       1m27s   3GB
Dec 01 03:10:11 Starting candle/set-theory
Dec 01 03:10:37 Finished candle/set-theory                                       25s 749MB
Dec 01 03:10:37 Starting candle/syntax-lib
Dec 01 03:10:47 Finished candle/syntax-lib                                        9s 516MB
Dec 01 03:10:47 Starting candle/standard/syntax
Dec 01 03:12:29 Finished candle/standard/syntax                                1m41s 877MB
Dec 01 03:12:29 Starting candle/standard/semantics
Dec 01 03:14:04 Finished candle/standard/semantics                             1m34s   1GB
Dec 01 03:14:04 Starting candle/standard/monadic
Dec 01 03:15:38 Finished candle/standard/monadic                               1m33s   1GB
Dec 01 03:15:39 Starting candle/standard/ml_kernel
Dec 01 03:19:43 Finished candle/standard/ml_kernel                             4m03s   3GB
Dec 01 03:19:43 Starting candle/standard/opentheory
Dec 01 03:28:32 Finished candle/standard/opentheory                            8m49s   4GB
Dec 01 03:28:33 Starting candle/standard/opentheory/compilation
Dec 01 03:58:35 Finished candle/standard/opentheory/compilation               30m01s  22GB
Dec 01 03:58:35 Starting candle/standard/opentheory/compilation/proofs
Dec 01 03:59:20 Finished candle/standard/opentheory/compilation/proofs           45s   2GB
Dec 01 03:59:20 Starting characteristic/examples
Dec 01 04:00:48 Finished characteristic/examples                               1m26s   2GB
Dec 01 04:00:48 Starting tutorial/solutions
Dec 01 04:14:33 Finished tutorial/solutions                                   13m44s   6GB
Dec 01 04:14:33 Starting translator/monadic/examples
Dec 01 04:17:28 Finished translator/monadic/examples                           2m54s   2GB
Dec 01 04:17:28 Starting examples
Dec 01 04:26:41 Finished examples                                              9m12s   3GB
Dec 01 04:26:42 Starting examples/compilation/x64
Dec 01 06:31:53 Finished examples/compilation/x64                           2h05m11s  19GB
Dec 01 06:31:54 Starting examples/compilation/x64/proofs
Dec 01 06:33:43 Finished examples/compilation/x64/proofs                       1m48s   2GB
Dec 01 06:33:43 Starting examples/compilation/ag32
Dec 01 07:02:28 Finished examples/compilation/ag32                            28m44s   7GB
Dec 01 07:02:28 Starting examples/compilation/ag32/proofs
Dec 01 07:03:20 Finished examples/compilation/ag32/proofs                        51s   3GB
Dec 01 07:03:20 Starting examples/cost
Dec 01 07:25:09 Finished examples/cost                                        21m48s   6GB
Dec 01 07:25:09 Starting translator/okasaki-examples
Dec 01 07:29:21 Finished translator/okasaki-examples                           4m11s   1GB
Dec 01 07:29:21 Starting translator/other-examples
Dec 01 07:29:58 Finished translator/other-examples                               37s   1GB
Dec 01 07:29:59 Starting compiler/parsing/tests
Dec 01 07:30:23 Finished compiler/parsing/tests                                  24s 409MB
Dec 01 07:30:23 Starting compiler/inference/tests
Dec 01 07:34:54 Finished compiler/inference/tests                              4m30s   6GB
Dec 01 07:34:54 Starting compiler/bootstrap/translation
Dec 01 10:09:53 Finished compiler/bootstrap/translation                     2h34m56s  43GB
Dec 01 10:09:53 Starting unverified/sexpr-bootstrap/x64/64
Dec 01 10:25:48 Finished unverified/sexpr-bootstrap/x64/64                    15m54s   3GB
Dec 01 10:25:48 Starting unverified/sexpr-bootstrap/x64/32
Dec 01 10:36:41 Finished unverified/sexpr-bootstrap/x64/32                    10m52s   7GB
Dec 01 10:36:41 Starting compiler/benchmarks
Dec 01 11:16:08 Finished compiler/benchmarks                                  39m26s   2GB
Dec 01 11:16:09 Starting compiler/bootstrap/compilation/x64/64
Dec 02 00:52:44 Finished compiler/bootstrap/compilation/x64/64             13h36m34s  64GB
Dec 02 00:52:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 02 00:57:08 Finished compiler/bootstrap/compilation/x64/64/proofs          4m23s   5GB
Dec 02 00:57:09 Starting compiler/bootstrap/compilation/x64/32
Dec 02 13:44:37 Finished compiler/bootstrap/compilation/x64/32             12h47m28s  64GB
Dec 02 13:44:38 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 02 13:49:03 Finished compiler/bootstrap/compilation/x64/32/proofs          4m24s   5GB
Dec 02 13:49:03 Starting compiler/bootstrap/compilation/ag32/32
Dec 03 02:54:57 Finished compiler/bootstrap/compilation/ag32/32            13h05m53s  64GB
Dec 03 02:54:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 03 03:14:23 Finished compiler/bootstrap/compilation/ag32/32/proofs        19m25s  18GB
Dec 03 03:14:23 SUCCESS