Job 718

CakeML:6bc8e267ebd128227cd90e1c9f9be4fd7f3bbb5a
  Merge remote-tracking branch 'origin/cleanup' [Feb 06 09:47:42]
HOL:ee2221d7ed25c0c6d29ff5d03002454814972116
  Document theorem syntaxes in the release notes [Feb 05 00:48:20]
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

Feb 06 09:51:32 Claimed job
Feb 06 09:51:40 Building HOL
Feb 06 09:59:14 Starting developers
Feb 06 09:59:16 Finished developers                                               0s  22MB
Feb 06 09:59:16 Starting developers/bin
Feb 06 09:59:50 Finished developers/bin                                          32s 142MB
Feb 06 09:59:51 Starting semantics/ffi
Feb 06 10:00:25 Finished semantics/ffi                                           33s 365MB
Feb 06 10:00:26 Starting semantics
Feb 06 10:01:55 Finished semantics                                             1m28s   1GB
Feb 06 10:01:55 Starting semantics/proofs
Feb 06 10:04:56 Finished semantics/proofs                                      3m00s   1GB
Feb 06 10:04:57 Starting basis/pure
Feb 06 10:08:25 Finished basis/pure                                            3m27s 724MB
Feb 06 10:08:26 Starting translator
Feb 06 10:10:03 Finished translator                                            1m35s   1GB
Feb 06 10:10:03 Starting compiler/parsing
Feb 06 10:11:01 Finished compiler/parsing                                        56s   2GB
Feb 06 10:11:01 Starting characteristic
Feb 06 10:15:16 Finished characteristic                                        4m13s   1GB
Feb 06 10:15:16 Starting translator/monadic
Feb 06 10:16:40 Finished translator/monadic                                    1m23s   1GB
Feb 06 10:16:41 Starting basis
Feb 06 10:32:56 Finished basis                                                16m14s   3GB
Feb 06 10:32:57 Starting compiler/inference
Feb 06 10:34:42 Finished compiler/inference                                    1m44s   1GB
Feb 06 10:34:43 Starting compiler/backend/reg_alloc
Feb 06 10:35:33 Finished compiler/backend/reg_alloc                              49s   1GB
Feb 06 10:35:34 Starting compiler/backend/gc
Feb 06 10:44:15 Finished compiler/backend/gc                                   8m39s   2GB
Feb 06 10:44:15 Starting compiler/backend
Feb 06 10:44:17 Finished compiler/backend                                         0s  41MB
Feb 06 10:44:17 Starting compiler/encoders/asm
Feb 06 10:44:18 Finished compiler/encoders/asm                                    0s  32MB
Feb 06 10:44:19 Starting compiler/encoders/x64
Feb 06 10:45:16 Finished compiler/encoders/x64                                   55s 707MB
Feb 06 10:45:17 Starting compiler/encoders/arm6
Feb 06 10:46:57 Finished compiler/encoders/arm6                                1m39s   1GB
Feb 06 10:46:58 Starting compiler/encoders/arm8
Feb 06 10:47:26 Finished compiler/encoders/arm8                                  27s 580MB
Feb 06 10:47:27 Starting compiler/encoders/mips
Feb 06 10:48:28 Finished compiler/encoders/mips                                1m00s 845MB
Feb 06 10:48:28 Starting compiler/encoders/riscv
Feb 06 10:49:32 Finished compiler/encoders/riscv                               1m02s 693MB
Feb 06 10:49:33 Starting compiler/encoders/ag32
Feb 06 10:49:48 Finished compiler/encoders/ag32                                  14s 781MB
Feb 06 10:49:49 Starting compiler/backend/x64
Feb 06 10:50:05 Finished compiler/backend/x64                                    14s   1GB
Feb 06 10:50:05 Starting compiler/backend/arm6
Feb 06 10:50:22 Finished compiler/backend/arm6                                   15s   1GB
Feb 06 10:50:22 Starting compiler/backend/arm8
Feb 06 10:50:39 Finished compiler/backend/arm8                                   15s   1GB
Feb 06 10:50:40 Starting compiler/backend/mips
Feb 06 10:50:57 Finished compiler/backend/mips                                   16s   1GB
Feb 06 10:50:57 Starting compiler/backend/riscv
Feb 06 10:51:14 Finished compiler/backend/riscv                                  15s   1GB
Feb 06 10:51:14 Starting compiler/backend/ag32
Feb 06 10:52:22 Finished compiler/backend/ag32                                 1m06s 930MB
Feb 06 10:52:23 Starting compiler/parsing/proofs
Feb 06 10:57:55 Finished compiler/parsing/proofs                               5m31s   1GB
Feb 06 10:57:56 Starting compiler/inference/proofs
Feb 06 11:00:38 Finished compiler/inference/proofs                             2m40s   1GB
Feb 06 11:00:38 Starting compiler/backend/semantics
Feb 06 11:08:25 Finished compiler/backend/semantics                            7m46s   1GB
Feb 06 11:08:26 Starting compiler/backend/reg_alloc/proofs
Feb 06 11:11:03 Finished compiler/backend/reg_alloc/proofs                     2m35s 782MB
Feb 06 11:11:03 Starting compiler/backend/proofs
Feb 06 11:51:18 Finished compiler/backend/proofs                              40m14s   3GB
Feb 06 11:51:19 Starting compiler/encoders/x64/proofs
Feb 06 12:01:11 Finished compiler/encoders/x64/proofs                          9m51s   5GB
Feb 06 12:01:12 Starting compiler/encoders/arm6/proofs
Feb 06 12:14:31 Finished compiler/encoders/arm6/proofs                        13m18s   3GB
Feb 06 12:14:32 Starting compiler/encoders/arm8/proofs
Feb 06 12:20:11 Finished compiler/encoders/arm8/proofs                         5m38s   1GB
Feb 06 12:20:12 Starting compiler/encoders/mips/proofs
Feb 06 12:30:05 Finished compiler/encoders/mips/proofs                         9m52s   2GB
Feb 06 12:30:06 Starting compiler/encoders/riscv/proofs
Feb 06 12:37:37 Finished compiler/encoders/riscv/proofs                        7m29s   1GB
Feb 06 12:37:37 Starting compiler/encoders/ag32/proofs
Feb 06 12:40:04 Finished compiler/encoders/ag32/proofs                         2m25s 849MB
Feb 06 12:40:05 Starting compiler/backend/x64/proofs
Feb 06 12:40:22 Finished compiler/backend/x64/proofs                             16s   1GB
Feb 06 12:40:23 Starting compiler/backend/arm6/proofs
Feb 06 12:40:42 Finished compiler/backend/arm6/proofs                            17s 929MB
Feb 06 12:40:42 Starting compiler/backend/arm8/proofs
Feb 06 12:41:00 Finished compiler/backend/arm8/proofs                            16s   1GB
Feb 06 12:41:00 Starting compiler/backend/mips/proofs
Feb 06 12:41:18 Finished compiler/backend/mips/proofs                            17s   1GB
Feb 06 12:41:19 Starting compiler/backend/riscv/proofs
Feb 06 12:41:36 Finished compiler/backend/riscv/proofs                           16s 951MB
Feb 06 12:41:37 Starting compiler/backend/ag32/proofs
Feb 06 12:50:25 Finished compiler/backend/ag32/proofs                          8m47s   2GB
Feb 06 12:50:26 Starting compiler/proofs
Feb 06 12:51:42 Finished compiler/proofs                                       1m15s   3GB
Feb 06 12:51:43 Starting candle/set-theory
Feb 06 12:52:08 Finished candle/set-theory                                       24s 693MB
Feb 06 12:52:09 Starting candle/syntax-lib
Feb 06 12:52:18 Finished candle/syntax-lib                                        8s 666MB
Feb 06 12:52:19 Starting candle/standard/syntax
Feb 06 12:54:00 Finished candle/standard/syntax                                1m40s   1GB
Feb 06 12:54:01 Starting candle/standard/semantics
Feb 06 12:55:34 Finished candle/standard/semantics                             1m32s   1GB
Feb 06 12:55:35 Starting candle/standard/monadic
Feb 06 12:57:07 Finished candle/standard/monadic                               1m31s   1GB
Feb 06 12:57:07 Starting candle/standard/ml_kernel
Feb 06 13:00:56 Finished candle/standard/ml_kernel                             3m47s   4GB
Feb 06 13:00:56 Starting candle/standard/opentheory
Feb 06 13:09:20 Finished candle/standard/opentheory                            8m22s   4GB
Feb 06 13:09:21 Starting candle/standard/opentheory/compilation
Feb 06 13:38:15 Finished candle/standard/opentheory/compilation               28m53s  24GB
Feb 06 13:38:16 Starting candle/standard/opentheory/compilation/proofs
Feb 06 13:39:01 Finished candle/standard/opentheory/compilation/proofs           44s   5GB
Feb 06 13:39:02 Starting characteristic/examples
Feb 06 13:40:27 Finished characteristic/examples                               1m24s   3GB
Feb 06 13:40:27 Starting tutorial/solutions
Feb 06 13:53:40 Finished tutorial/solutions                                   13m11s   6GB
Feb 06 13:53:40 Starting translator/monadic/examples
Feb 06 13:55:51 Finished translator/monadic/examples                           2m09s   2GB
Feb 06 13:55:52 Starting examples
Feb 06 14:03:26 Finished examples                                              7m33s   4GB
Feb 06 14:03:27 Starting examples/compilation/x64
Feb 06 15:55:49 Finished examples/compilation/x64                           1h52m21s  12GB
Feb 06 15:55:50 Starting examples/compilation/x64/proofs
Feb 06 15:57:36 Finished examples/compilation/x64/proofs                       1m45s   4GB
Feb 06 15:57:37 Starting examples/compilation/ag32
Feb 06 16:25:39 Finished examples/compilation/ag32                            28m01s   5GB
Feb 06 16:25:40 Starting examples/compilation/ag32/proofs
Feb 06 16:26:24 Finished examples/compilation/ag32/proofs                        43s   4GB
Feb 06 16:26:24 Starting translator/okasaki-examples
Feb 06 16:30:37 Finished translator/okasaki-examples                           4m11s   1GB
Feb 06 16:30:37 Starting translator/other-examples
Feb 06 16:34:18 Finished translator/other-examples                             3m39s   1GB
Feb 06 16:34:19 Starting compiler/parsing/tests
Feb 06 16:34:50 Finished compiler/parsing/tests                                  31s 578MB
Feb 06 16:34:51 Starting compiler/inference/tests
Feb 06 16:39:14 Finished compiler/inference/tests                              4m22s   5GB
Feb 06 16:39:15 Starting compiler/bootstrap/translation
Feb 06 19:07:38 Finished compiler/bootstrap/translation                     2h28m22s  44GB
Feb 06 19:07:39 Starting unverified/sexpr-bootstrap/x64/64
Feb 06 19:16:20 Finished unverified/sexpr-bootstrap/x64/64                     8m39s  15GB
Feb 06 19:16:21 Starting unverified/sexpr-bootstrap/x64/32
Feb 06 19:21:36 Finished unverified/sexpr-bootstrap/x64/32                     5m13s  23GB
Feb 06 19:21:37 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Feb 06 19:22:08 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            30s   1GB
Feb 06 19:22:09 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Feb 06 19:22:56 Finished compiler/benchmarks/mlton_benchmarks/cakeml             46s   1GB
Feb 06 19:22:57 Starting compiler/bootstrap/compilation/x64/64
Feb 07 05:27:44 Finished compiler/bootstrap/compilation/x64/64             10h04m45s  64GB
Feb 07 05:27:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 07 05:33:31 Finished compiler/bootstrap/compilation/x64/64/proofs          5m45s  31GB
Feb 07 05:33:31 Starting compiler/bootstrap/compilation/x64/32
Feb 07 14:43:12 Finished compiler/bootstrap/compilation/x64/32              9h09m38s  64GB
Feb 07 14:43:13 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 07 14:48:51 Finished compiler/bootstrap/compilation/x64/32/proofs          5m37s  28GB
Feb 07 14:48:52 SUCCESS