Job 1011

CakeML:7eeb111560567e646fd79d04919872dcfbc585c4
  Fix a silly typo from a previous fix [Aug 20 12:47:31]
#677 (clos-install)
Merging into:6217a49acea35e3698ec35c342033a1137a43768
  Fix compiler/encoders/monadic_enc for drule change [Aug 18 04:12:33]
HOL:8cc876e8e492e4f4045670ff53549a04cf1fdc65
  Further document drule breakage by linking to CakeML's old_drule [Aug 16 01:09:50]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 20 13:00:41 Claimed job
Aug 20 13:00:44 Reusing HOL
Aug 20 13:00:49 Starting developers
Aug 20 13:00:49 Finished developers                                               0s  39MB
Aug 20 13:00:50 Starting developers/bin
Aug 20 13:02:09 Finished developers/bin                                        1m18s 165MB
Aug 20 13:02:09 Starting semantics/ffi
Aug 20 13:02:18 Finished semantics/ffi                                            8s 206MB
Aug 20 13:02:18 Starting semantics
Aug 20 13:03:35 Finished semantics                                             1m16s   1GB
Aug 20 13:03:35 Starting semantics/proofs
Aug 20 13:06:32 Finished semantics/proofs                                      2m56s   1GB
Aug 20 13:06:32 Starting semantics/alt_semantics
Aug 20 13:06:39 Finished semantics/alt_semantics                                  6s 263MB
Aug 20 13:06:39 Starting semantics/alt_semantics/proofs
Aug 20 13:08:26 Finished semantics/alt_semantics/proofs                        1m46s 688MB
Aug 20 13:08:26 Starting basis/pure
Aug 20 13:09:10 Finished basis/pure                                              43s 737MB
Aug 20 13:09:10 Starting translator
Aug 20 13:10:54 Finished translator                                            1m43s   1GB
Aug 20 13:10:55 Starting compiler/parsing
Aug 20 13:11:52 Finished compiler/parsing                                        56s   1GB
Aug 20 13:11:52 Starting characteristic
Aug 20 13:16:55 Finished characteristic                                        5m02s   1GB
Aug 20 13:16:56 Starting translator/monadic
Aug 20 13:18:20 Finished translator/monadic                                    1m23s   1GB
Aug 20 13:18:20 Starting basis
Aug 20 13:36:22 Finished basis                                                18m00s   3GB
Aug 20 13:36:22 Starting compiler/inference
Aug 20 13:37:57 Finished compiler/inference                                    1m34s   1GB
Aug 20 13:37:57 Starting compiler/backend/reg_alloc
Aug 20 13:38:56 Finished compiler/backend/reg_alloc                              58s   1GB
Aug 20 13:38:56 Starting compiler/backend/gc
Aug 20 13:46:56 Finished compiler/backend/gc                                   7m59s   2GB
Aug 20 13:46:56 Starting compiler/backend
Aug 20 13:46:57 Finished compiler/backend                                         0s  45MB
Aug 20 13:46:58 Starting compiler/encoders/asm
Aug 20 13:46:58 Finished compiler/encoders/asm                                    0s  38MB
Aug 20 13:46:59 Starting compiler/encoders/x64
Aug 20 13:47:21 Finished compiler/encoders/x64                                   21s 958MB
Aug 20 13:47:21 Starting compiler/encoders/arm7
Aug 20 13:48:07 Finished compiler/encoders/arm7                                  45s 746MB
Aug 20 13:48:07 Starting compiler/encoders/arm8
Aug 20 13:48:19 Finished compiler/encoders/arm8                                  11s 557MB
Aug 20 13:48:19 Starting compiler/encoders/mips
Aug 20 13:48:35 Finished compiler/encoders/mips                                  15s   1GB
Aug 20 13:48:35 Starting compiler/encoders/riscv
Aug 20 13:48:48 Finished compiler/encoders/riscv                                 12s 730MB
Aug 20 13:48:49 Starting compiler/encoders/ag32
Aug 20 13:49:03 Finished compiler/encoders/ag32                                  14s 588MB
Aug 20 13:49:04 Starting compiler/backend/x64
Aug 20 13:49:20 Finished compiler/backend/x64                                    15s   1GB
Aug 20 13:49:20 Starting compiler/backend/arm7
Aug 20 13:49:38 Finished compiler/backend/arm7                                   17s   1GB
Aug 20 13:49:38 Starting compiler/backend/arm8
Aug 20 13:49:55 Finished compiler/backend/arm8                                   15s   1GB
Aug 20 13:49:55 Starting compiler/backend/mips
Aug 20 13:50:10 Finished compiler/backend/mips                                   15s 816MB
Aug 20 13:50:11 Starting compiler/backend/riscv
Aug 20 13:50:28 Finished compiler/backend/riscv                                  16s   1GB
Aug 20 13:50:28 Starting compiler/backend/ag32
Aug 20 13:51:34 Finished compiler/backend/ag32                                 1m05s   1GB
Aug 20 13:51:34 Starting compiler/parsing/proofs
Aug 20 13:57:03 Finished compiler/parsing/proofs                               5m27s 813MB
Aug 20 13:57:03 Starting compiler/inference/proofs
Aug 20 13:59:42 Finished compiler/inference/proofs                             2m38s 864MB
Aug 20 13:59:42 Starting compiler/backend/semantics
Aug 20 14:05:29 Finished compiler/backend/semantics                            5m47s   1GB
Aug 20 14:05:30 Starting compiler/backend/reg_alloc/proofs
Aug 20 14:08:41 Finished compiler/backend/reg_alloc/proofs                     3m10s 791MB
Aug 20 14:08:42 Starting compiler/backend/proofs
Aug 20 14:45:59 Finished compiler/backend/proofs                              37m16s   3GB
Aug 20 14:45:59 Starting compiler/encoders/x64/proofs
Aug 20 14:54:57 Finished compiler/encoders/x64/proofs                          8m57s   5GB
Aug 20 14:54:57 Starting compiler/encoders/arm7/proofs
Aug 20 15:07:03 Finished compiler/encoders/arm7/proofs                        12m04s   3GB
Aug 20 15:07:03 Starting compiler/encoders/arm8/proofs
Aug 20 15:13:30 Finished compiler/encoders/arm8/proofs                         6m26s   1GB
Aug 20 15:13:31 Starting compiler/encoders/mips/proofs
Aug 20 15:23:02 Finished compiler/encoders/mips/proofs                         9m30s   2GB
Aug 20 15:23:02 Starting compiler/encoders/riscv/proofs
Aug 20 15:31:10 Finished compiler/encoders/riscv/proofs                        8m07s   1GB
Aug 20 15:31:10 Starting compiler/encoders/ag32/proofs
Aug 20 15:33:39 Finished compiler/encoders/ag32/proofs                         2m27s 684MB
Aug 20 15:33:39 Starting compiler/backend/x64/proofs
Aug 20 15:33:56 Finished compiler/backend/x64/proofs                             16s   1GB
Aug 20 15:33:56 Starting compiler/backend/arm7/proofs
Aug 20 15:34:14 Finished compiler/backend/arm7/proofs                            16s 829MB
Aug 20 15:34:14 Starting compiler/backend/arm8/proofs
Aug 20 15:34:31 Finished compiler/backend/arm8/proofs                            15s   1GB
Aug 20 15:34:31 Starting compiler/backend/mips/proofs
Aug 20 15:34:49 Finished compiler/backend/mips/proofs                            17s   1GB
Aug 20 15:34:50 Starting compiler/backend/riscv/proofs
Aug 20 15:35:07 Finished compiler/backend/riscv/proofs                           16s   1GB
Aug 20 15:35:07 Starting compiler/backend/ag32/proofs
Aug 20 15:43:53 Finished compiler/backend/ag32/proofs                          8m44s   2GB
Aug 20 15:43:53 Starting compiler/proofs
Aug 20 15:45:07 Finished compiler/proofs                                       1m13s   3GB
Aug 20 15:45:08 Starting candle/set-theory
Aug 20 15:45:33 Finished candle/set-theory                                       24s 802MB
Aug 20 15:45:33 Starting candle/syntax-lib
Aug 20 15:45:42 Finished candle/syntax-lib                                        8s 599MB
Aug 20 15:45:43 Starting candle/standard/syntax
Aug 20 15:47:23 Finished candle/standard/syntax                                1m39s   1GB
Aug 20 15:47:23 Starting candle/standard/semantics
Aug 20 15:48:55 Finished candle/standard/semantics                             1m32s   1GB
Aug 20 15:48:56 Starting candle/standard/monadic
Aug 20 15:50:29 Finished candle/standard/monadic                               1m33s   1GB
Aug 20 15:50:30 Starting candle/standard/ml_kernel
Aug 20 15:54:11 Finished candle/standard/ml_kernel                             3m41s   4GB
Aug 20 15:54:12 Starting candle/standard/opentheory
Aug 20 16:02:45 Finished candle/standard/opentheory                            8m32s   4GB
Aug 20 16:02:45 Starting candle/standard/opentheory/compilation
Aug 20 16:32:14 Finished candle/standard/opentheory/compilation               29m28s  20GB
Aug 20 16:32:14 Starting candle/standard/opentheory/compilation/proofs
Aug 20 16:32:50 Finished candle/standard/opentheory/compilation/proofs           35s   3GB
Aug 20 16:32:51 Starting characteristic/examples
Aug 20 16:34:15 Finished characteristic/examples                               1m24s   2GB
Aug 20 16:34:16 Starting tutorial/solutions
Aug 20 16:47:18 Finished tutorial/solutions                                   13m01s   7GB
Aug 20 16:47:18 Starting translator/monadic/examples
Aug 20 16:50:07 Finished translator/monadic/examples                           2m49s   2GB
Aug 20 16:50:08 Starting examples
Aug 20 16:59:02 Finished examples                                              8m53s   3GB
Aug 20 16:59:02 Starting examples/compilation/x64
Aug 20 19:01:33 Finished examples/compilation/x64                           2h02m31s  13GB
Aug 20 19:01:34 Starting examples/compilation/x64/proofs
Aug 20 19:03:16 Finished examples/compilation/x64/proofs                       1m42s   3GB
Aug 20 19:03:17 Starting examples/compilation/ag32
Aug 20 19:31:21 Finished examples/compilation/ag32                            28m04s   6GB
Aug 20 19:31:22 Starting examples/compilation/ag32/proofs
Aug 20 19:31:59 Finished examples/compilation/ag32/proofs                        36s   3GB
Aug 20 19:32:00 Starting translator/okasaki-examples
Aug 20 19:36:06 Finished translator/okasaki-examples                           4m05s   1GB
Aug 20 19:36:06 Starting translator/other-examples
Aug 20 19:36:46 Finished translator/other-examples                               38s   1GB
Aug 20 19:36:46 Starting compiler/parsing/tests
Aug 20 19:37:11 Finished compiler/parsing/tests                                  23s 541MB
Aug 20 19:37:11 Starting compiler/inference/tests
Aug 20 19:41:23 Finished compiler/inference/tests                              4m11s   4GB
Aug 20 19:41:23 Starting compiler/bootstrap/translation
Aug 20 22:08:16 Finished compiler/bootstrap/translation                     2h26m52s  47GB
Aug 20 22:08:17 Starting unverified/sexpr-bootstrap/x64/64
Aug 20 22:19:53 Finished unverified/sexpr-bootstrap/x64/64                    11m36s   6GB
Aug 20 22:19:54 Starting unverified/sexpr-bootstrap/x64/32
Aug 20 22:28:27 Finished unverified/sexpr-bootstrap/x64/32                     8m33s   7GB
Aug 20 22:28:28 Starting compiler/benchmarks
Aug 20 23:05:07 Finished compiler/benchmarks                                  36m38s   2GB
Aug 20 23:05:07 Starting compiler/bootstrap/compilation/x64/64
Aug 21 10:53:02 Finished compiler/bootstrap/compilation/x64/64             11h47m55s  64GB
Aug 21 10:53:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 21 10:56:25 Finished compiler/bootstrap/compilation/x64/64/proofs          3m21s   6GB
Aug 21 10:56:25 Starting compiler/bootstrap/compilation/x64/32
Aug 21 22:21:08 Finished compiler/bootstrap/compilation/x64/32             11h24m42s  64GB
Aug 21 22:21:09 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 21 22:24:11 Finished compiler/bootstrap/compilation/x64/32/proofs          3m01s   5GB
Aug 21 22:24:11 Starting compiler/bootstrap/compilation/ag32/32
Aug 22 10:48:33 Finished compiler/bootstrap/compilation/ag32/32            12h24m20s  64GB
Aug 22 10:48:33 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 22 11:10:11 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m37s  16GB
Aug 22 11:10:12 SUCCESS