Job 710

CakeML:2d7c75fa02a5b1347dd76fa2b7150e0af74d940b
  Fix some uses of Theorem syntax [Jan 31 16:15:24]
HOL:e53c040a60b6ad258c99b0887434bda862eb81a8
  Build sequences must have src/finite_maps before src/integer [Jan 31 01:43:52]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 31 16:31:40 Claimed job
Jan 31 16:31:44 Reusing HOL
Jan 31 16:31:53 Starting developers
Jan 31 16:31:55 Finished developers                                               0s  30MB
Jan 31 16:31:55 Starting developers/bin
Jan 31 16:32:26 Finished developers/bin                                          29s 142MB
Jan 31 16:32:27 Starting semantics/ffi
Jan 31 16:32:35 Finished semantics/ffi                                            7s 216MB
Jan 31 16:32:36 Starting semantics
Jan 31 16:33:55 Finished semantics                                             1m18s   1GB
Jan 31 16:33:56 Starting semantics/proofs
Jan 31 16:37:08 Finished semantics/proofs                                      3m10s 986MB
Jan 31 16:37:08 Starting basis/pure
Jan 31 16:37:53 Finished basis/pure                                              43s 665MB
Jan 31 16:37:54 Starting translator
Jan 31 16:39:31 Finished translator                                            1m36s   1GB
Jan 31 16:39:32 Starting compiler/parsing
Jan 31 16:40:31 Finished compiler/parsing                                        58s   1GB
Jan 31 16:40:32 Starting characteristic
Jan 31 16:44:51 Finished characteristic                                        4m18s   1GB
Jan 31 16:44:52 Starting translator/monadic
Jan 31 16:46:17 Finished translator/monadic                                    1m24s   1GB
Jan 31 16:46:18 Starting basis
Jan 31 17:02:42 Finished basis                                                16m22s   2GB
Jan 31 17:02:42 Starting compiler/inference
Jan 31 17:04:13 Finished compiler/inference                                    1m29s   1GB
Jan 31 17:04:14 Starting compiler/backend/reg_alloc
Jan 31 17:05:06 Finished compiler/backend/reg_alloc                              51s   1GB
Jan 31 17:05:06 Starting compiler/backend/gc
Jan 31 17:13:55 Finished compiler/backend/gc                                   8m47s   1GB
Jan 31 17:13:55 Starting compiler/backend
Jan 31 17:13:58 Finished compiler/backend                                         1s  18MB
Jan 31 17:13:59 Starting compiler/encoders/asm
Jan 31 17:14:00 Finished compiler/encoders/asm                                    0s  16MB
Jan 31 17:14:01 Starting compiler/encoders/x64
Jan 31 17:15:00 Finished compiler/encoders/x64                                   58s 947MB
Jan 31 17:15:01 Starting compiler/encoders/arm6
Jan 31 17:16:49 Finished compiler/encoders/arm6                                1m46s   1GB
Jan 31 17:16:50 Starting compiler/encoders/arm8
Jan 31 17:17:19 Finished compiler/encoders/arm8                                  28s 563MB
Jan 31 17:17:20 Starting compiler/encoders/mips
Jan 31 17:18:24 Finished compiler/encoders/mips                                1m03s 930MB
Jan 31 17:18:25 Starting compiler/encoders/riscv
Jan 31 17:19:32 Finished compiler/encoders/riscv                               1m06s 754MB
Jan 31 17:19:33 Starting compiler/encoders/ag32
Jan 31 17:19:49 Finished compiler/encoders/ag32                                  15s 777MB
Jan 31 17:19:50 Starting compiler/backend/x64
Jan 31 17:20:08 Finished compiler/backend/x64                                    16s 869MB
Jan 31 17:20:08 Starting compiler/backend/arm6
Jan 31 17:20:28 Finished compiler/backend/arm6                                   18s   1GB
Jan 31 17:20:28 Starting compiler/backend/arm8
Jan 31 17:20:46 Finished compiler/backend/arm8                                   16s   1GB
Jan 31 17:20:47 Starting compiler/backend/mips
Jan 31 17:21:05 Finished compiler/backend/mips                                   17s 955MB
Jan 31 17:21:06 Starting compiler/backend/riscv
Jan 31 17:21:24 Finished compiler/backend/riscv                                  16s   1GB
Jan 31 17:21:25 Starting compiler/backend/ag32
Jan 31 17:22:32 Finished compiler/backend/ag32                                 1m06s   1GB
Jan 31 17:22:33 Starting compiler/parsing/proofs
Jan 31 17:28:08 Finished compiler/parsing/proofs                               5m33s 926MB
Jan 31 17:28:09 Starting compiler/inference/proofs
Jan 31 17:30:52 Finished compiler/inference/proofs                             2m42s   1GB
Jan 31 17:30:53 Starting compiler/backend/semantics
Jan 31 17:37:51 Finished compiler/backend/semantics                            6m56s   1GB
Jan 31 17:37:51 Starting compiler/backend/reg_alloc/proofs
Jan 31 17:40:29 Finished compiler/backend/reg_alloc/proofs                     2m36s 809MB
Jan 31 17:40:29 Starting compiler/backend/proofs
Feb 01 09:03:36 Resuming compiler/backend/proofs
Feb 01 09:03:40 Finished compiler/backend/proofs                                  2s  26MB
Feb 01 09:03:40 Starting compiler/encoders/x64/proofs
Feb 01 09:13:47 Finished compiler/encoders/x64/proofs                         10m06s   6GB
Feb 01 09:13:48 Starting compiler/encoders/arm6/proofs
Feb 01 09:27:21 Finished compiler/encoders/arm6/proofs                        13m31s   4GB
Feb 01 09:27:21 Starting compiler/encoders/arm8/proofs
Feb 01 09:33:12 Finished compiler/encoders/arm8/proofs                         5m49s   1GB
Feb 01 09:33:13 Starting compiler/encoders/mips/proofs
Feb 01 09:43:16 Finished compiler/encoders/mips/proofs                        10m02s   1GB
Feb 01 09:43:17 Starting compiler/encoders/riscv/proofs
Feb 01 09:51:05 Finished compiler/encoders/riscv/proofs                        7m47s 970MB
Feb 01 09:51:06 Starting compiler/encoders/ag32/proofs
Feb 01 09:53:37 Finished compiler/encoders/ag32/proofs                         2m30s 636MB
Feb 01 09:53:38 Starting compiler/backend/x64/proofs
Feb 01 09:53:57 Finished compiler/backend/x64/proofs                             18s   1GB
Feb 01 09:53:58 Starting compiler/backend/arm6/proofs
Feb 01 09:54:19 Finished compiler/backend/arm6/proofs                            20s 874MB
Feb 01 09:54:20 Starting compiler/backend/arm8/proofs
Feb 01 09:54:39 Finished compiler/backend/arm8/proofs                            18s   1GB
Feb 01 09:54:40 Starting compiler/backend/mips/proofs
Feb 01 09:55:00 Finished compiler/backend/mips/proofs                            19s   1GB
Feb 01 09:55:01 Starting compiler/backend/riscv/proofs
Feb 01 09:55:21 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 01 09:55:22 Starting compiler/backend/ag32/proofs
Feb 01 10:04:22 Finished compiler/backend/ag32/proofs                          8m59s   2GB
Feb 01 10:04:23 Starting compiler/proofs
Feb 01 10:05:43 Finished compiler/proofs                                       1m19s   4GB
Feb 01 10:05:44 Starting candle/set-theory
Feb 01 10:06:10 Finished candle/set-theory                                       24s 699MB
Feb 01 10:06:10 Starting candle/syntax-lib
Feb 01 10:06:21 Finished candle/syntax-lib                                       10s 469MB
Feb 01 10:06:22 Starting candle/standard/syntax
Feb 01 10:08:04 Finished candle/standard/syntax                                1m40s   1GB
Feb 01 10:08:04 Starting candle/standard/semantics
Feb 01 10:09:39 Finished candle/standard/semantics                             1m33s   1GB
Feb 01 10:09:39 Starting candle/standard/monadic
Feb 01 10:11:14 Finished candle/standard/monadic                               1m33s   1GB
Feb 01 10:11:14 Starting candle/standard/ml_kernel
Feb 01 10:15:04 Finished candle/standard/ml_kernel                             3m48s   4GB
Feb 01 10:15:04 Starting candle/standard/opentheory
Feb 01 10:23:32 Finished candle/standard/opentheory                            8m27s   5GB
Feb 01 10:23:33 Starting candle/standard/opentheory/compilation
Feb 01 10:52:43 Finished candle/standard/opentheory/compilation               29m09s  13GB
Feb 01 10:52:44 Starting candle/standard/opentheory/compilation/proofs
Feb 01 10:53:32 Finished candle/standard/opentheory/compilation/proofs           47s   5GB
Feb 01 10:53:33 Starting characteristic/examples
Feb 01 10:55:01 Finished characteristic/examples                               1m26s   2GB
Feb 01 10:55:01 Starting tutorial/solutions
Feb 01 11:08:12 Finished tutorial/solutions                                   13m10s   6GB
Feb 01 11:08:13 Starting translator/monadic/examples
Feb 01 11:10:26 Finished translator/monadic/examples                           2m11s   2GB
Feb 01 11:10:26 Starting examples
Feb 01 11:18:08 Finished examples                                              7m40s   3GB
Feb 01 11:18:09 Starting examples/compilation/x64
Feb 01 13:11:32 Finished examples/compilation/x64                           1h53m22s  24GB
Feb 01 13:11:33 Starting examples/compilation/x64/proofs
Feb 01 13:13:20 Finished examples/compilation/x64/proofs                       1m45s   4GB
Feb 01 13:13:20 Starting examples/compilation/ag32
Feb 01 13:41:25 Finished examples/compilation/ag32                            28m03s   6GB
Feb 01 13:41:25 Starting examples/compilation/ag32/proofs
Feb 01 13:42:12 Finished examples/compilation/ag32/proofs                        45s   4GB
Feb 01 13:42:13 Starting translator/okasaki-examples
Feb 01 13:46:24 Finished translator/okasaki-examples                           4m09s   1GB
Feb 01 13:46:25 Starting translator/other-examples
Feb 01 13:49:50 Finished translator/other-examples                             3m25s   1GB
Feb 01 13:49:51 Starting compiler/parsing/tests
Feb 01 13:50:17 Finished compiler/parsing/tests                                  25s 562MB
Feb 01 13:50:18 Starting compiler/inference/tests
Feb 01 13:54:29 Finished compiler/inference/tests                              4m10s   4GB
Feb 01 13:54:30 Starting compiler/bootstrap/translation
Feb 01 16:22:38 Finished compiler/bootstrap/translation                     2h28m07s  45GB
Feb 01 16:22:39 Starting unverified/sexpr-bootstrap/x64/64
Feb 01 16:31:19 Finished unverified/sexpr-bootstrap/x64/64                     8m38s  15GB
Feb 01 16:31:20 Starting unverified/sexpr-bootstrap/x64/32
Feb 01 16:36:42 Finished unverified/sexpr-bootstrap/x64/32                     5m20s  22GB
Feb 01 16:36:43 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Feb 01 16:37:14 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            30s   1GB
Feb 01 16:37:15 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Feb 01 16:38:03 Finished compiler/benchmarks/mlton_benchmarks/cakeml             47s   1GB
Feb 01 16:38:04 Starting compiler/bootstrap/compilation/x64/64
Feb 02 03:16:12 Finished compiler/bootstrap/compilation/x64/64             10h38m06s  64GB
Feb 02 03:16:12 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 02 03:22:26 Finished compiler/bootstrap/compilation/x64/64/proofs          6m12s  31GB
Feb 02 03:22:27 Starting compiler/bootstrap/compilation/x64/32
Feb 02 12:32:43 Finished compiler/bootstrap/compilation/x64/32              9h10m13s  64GB
Feb 02 12:32:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 02 12:38:29 Finished compiler/bootstrap/compilation/x64/32/proofs          5m43s  30GB
Feb 02 12:38:29 SUCCESS