Job 1009

CakeML: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
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Aug 18 04:20:23 Claimed job
Aug 18 04:20:27 Reusing HOL
Aug 18 04:20:31 Starting developers
Aug 18 04:20:32 Finished developers                                               0s  29MB
Aug 18 04:20:33 Starting developers/bin
Aug 18 04:21:54 Finished developers/bin                                        1m20s 237MB
Aug 18 04:21:54 Starting semantics/ffi
Aug 18 04:22:02 Finished semantics/ffi                                            7s 205MB
Aug 18 04:22:02 Starting semantics
Aug 18 04:23:19 Finished semantics                                             1m16s   1GB
Aug 18 04:23:19 Starting semantics/proofs
Aug 18 04:26:18 Finished semantics/proofs                                      2m58s   1GB
Aug 18 04:26:19 Starting semantics/alt_semantics
Aug 18 04:26:25 Finished semantics/alt_semantics                                  6s 287MB
Aug 18 04:26:26 Starting semantics/alt_semantics/proofs
Aug 18 04:28:14 Finished semantics/alt_semantics/proofs                        1m48s 742MB
Aug 18 04:28:14 Starting basis/pure
Aug 18 04:28:59 Finished basis/pure                                              44s 785MB
Aug 18 04:28:59 Starting translator
Aug 18 04:30:42 Finished translator                                            1m42s   1GB
Aug 18 04:30:43 Starting compiler/parsing
Aug 18 04:31:39 Finished compiler/parsing                                        56s   1GB
Aug 18 04:31:40 Starting characteristic
Aug 18 04:36:49 Finished characteristic                                        5m08s   1GB
Aug 18 04:36:49 Starting translator/monadic
Aug 18 04:38:15 Finished translator/monadic                                    1m25s   1GB
Aug 18 04:38:15 Starting basis
Aug 18 04:58:11 Finished basis                                                19m55s   2GB
Aug 18 04:58:12 Starting compiler/inference
Aug 18 04:59:52 Finished compiler/inference                                    1m39s   1GB
Aug 18 04:59:52 Starting compiler/backend/reg_alloc
Aug 18 05:00:52 Finished compiler/backend/reg_alloc                            1m00s   1GB
Aug 18 05:00:53 Starting compiler/backend/gc
Aug 18 05:09:42 Finished compiler/backend/gc                                   8m48s   2GB
Aug 18 05:09:42 Starting compiler/backend
Aug 18 05:09:43 Finished compiler/backend                                         0s  44MB
Aug 18 05:09:43 Starting compiler/encoders/asm
Aug 18 05:09:44 Finished compiler/encoders/asm                                    0s  38MB
Aug 18 05:09:44 Starting compiler/encoders/x64
Aug 18 05:10:07 Finished compiler/encoders/x64                                   22s 939MB
Aug 18 05:10:08 Starting compiler/encoders/arm7
Aug 18 05:10:55 Finished compiler/encoders/arm7                                  47s 719MB
Aug 18 05:10:56 Starting compiler/encoders/arm8
Aug 18 05:11:08 Finished compiler/encoders/arm8                                  11s 724MB
Aug 18 05:11:08 Starting compiler/encoders/mips
Aug 18 05:11:24 Finished compiler/encoders/mips                                  15s   1GB
Aug 18 05:11:25 Starting compiler/encoders/riscv
Aug 18 05:11:38 Finished compiler/encoders/riscv                                 13s 787MB
Aug 18 05:11:39 Starting compiler/encoders/ag32
Aug 18 05:11:54 Finished compiler/encoders/ag32                                  14s 501MB
Aug 18 05:11:54 Starting compiler/backend/x64
Aug 18 05:12:10 Finished compiler/backend/x64                                    15s 842MB
Aug 18 05:12:11 Starting compiler/backend/arm7
Aug 18 05:12:29 Finished compiler/backend/arm7                                   18s   1GB
Aug 18 05:12:30 Starting compiler/backend/arm8
Aug 18 05:12:47 Finished compiler/backend/arm8                                   17s   1GB
Aug 18 05:12:47 Starting compiler/backend/mips
Aug 18 05:13:05 Finished compiler/backend/mips                                   17s   1GB
Aug 18 05:13:06 Starting compiler/backend/riscv
Aug 18 05:13:22 Finished compiler/backend/riscv                                  16s   1GB
Aug 18 05:13:23 Starting compiler/backend/ag32
Aug 18 05:14:32 Finished compiler/backend/ag32                                 1m08s   1GB
Aug 18 05:14:32 Starting compiler/parsing/proofs
Aug 18 05:20:12 Finished compiler/parsing/proofs                               5m39s 979MB
Aug 18 05:20:13 Starting compiler/inference/proofs
Aug 18 05:23:02 Finished compiler/inference/proofs                             2m49s   1GB
Aug 18 05:23:03 Starting compiler/backend/semantics
Aug 18 05:31:03 Finished compiler/backend/semantics                            8m00s   2GB
Aug 18 05:31:04 Starting compiler/backend/reg_alloc/proofs
Aug 18 05:34:25 Finished compiler/backend/reg_alloc/proofs                     3m20s 743MB
Aug 18 05:34:26 Starting compiler/backend/proofs
Aug 18 06:17:58 Finished compiler/backend/proofs                              43m31s   4GB
Aug 18 06:17:58 Starting compiler/encoders/x64/proofs
Aug 18 06:27:30 Finished compiler/encoders/x64/proofs                          9m31s   5GB
Aug 18 06:27:30 Starting compiler/encoders/arm7/proofs
Aug 18 06:40:47 Finished compiler/encoders/arm7/proofs                        13m17s   3GB
Aug 18 06:40:48 Starting compiler/encoders/arm8/proofs
Aug 18 06:47:33 Finished compiler/encoders/arm8/proofs                         6m45s   1GB
Aug 18 06:47:34 Starting compiler/encoders/mips/proofs
Aug 18 06:57:48 Finished compiler/encoders/mips/proofs                        10m13s   3GB
Aug 18 06:57:48 Starting compiler/encoders/riscv/proofs
Aug 18 07:07:19 Finished compiler/encoders/riscv/proofs                        9m30s 980MB
Aug 18 07:07:19 Starting compiler/encoders/ag32/proofs
Aug 18 07:09:55 Finished compiler/encoders/ag32/proofs                         2m35s   1GB
Aug 18 07:09:56 Starting compiler/backend/x64/proofs
Aug 18 07:10:14 Finished compiler/backend/x64/proofs                             17s 990MB
Aug 18 07:10:14 Starting compiler/backend/arm7/proofs
Aug 18 07:10:35 Finished compiler/backend/arm7/proofs                            19s   1GB
Aug 18 07:10:35 Starting compiler/backend/arm8/proofs
Aug 18 07:10:54 Finished compiler/backend/arm8/proofs                            19s 879MB
Aug 18 07:10:55 Starting compiler/backend/mips/proofs
Aug 18 07:11:13 Finished compiler/backend/mips/proofs                            18s 914MB
Aug 18 07:11:14 Starting compiler/backend/riscv/proofs
Aug 18 07:11:33 Finished compiler/backend/riscv/proofs                           18s   1GB
Aug 18 07:11:33 Starting compiler/backend/ag32/proofs
Aug 18 07:21:44 Finished compiler/backend/ag32/proofs                         10m10s   2GB
Aug 18 07:21:45 Starting compiler/proofs
Aug 18 07:23:05 Finished compiler/proofs                                       1m19s   2GB
Aug 18 07:23:05 Starting candle/set-theory
Aug 18 07:23:34 Finished candle/set-theory                                       28s 757MB
Aug 18 07:23:34 Starting candle/syntax-lib
Aug 18 07:23:44 Finished candle/syntax-lib                                        9s 619MB
Aug 18 07:23:45 Starting candle/standard/syntax
Aug 18 07:25:35 Finished candle/standard/syntax                                1m50s 875MB
Aug 18 07:25:36 Starting candle/standard/semantics
Aug 18 07:27:19 Finished candle/standard/semantics                             1m42s   1GB
Aug 18 07:27:19 Starting candle/standard/monadic
Aug 18 07:29:00 Finished candle/standard/monadic                               1m40s   1GB
Aug 18 07:29:00 Starting candle/standard/ml_kernel
Aug 18 07:33:19 Finished candle/standard/ml_kernel                             4m19s   4GB
Aug 18 07:33:20 Starting candle/standard/opentheory
Aug 18 07:43:24 Finished candle/standard/opentheory                           10m03s   4GB
Aug 18 07:43:24 Starting candle/standard/opentheory/compilation
Aug 18 08:15:46 Finished candle/standard/opentheory/compilation               32m21s   8GB
Aug 18 08:15:46 Starting candle/standard/opentheory/compilation/proofs
Aug 18 08:16:29 Finished candle/standard/opentheory/compilation/proofs           42s   2GB
Aug 18 08:16:29 Starting characteristic/examples
Aug 18 08:17:58 Finished characteristic/examples                               1m28s   2GB
Aug 18 08:17:58 Starting tutorial/solutions
Aug 18 08:30:44 Finished tutorial/solutions                                   12m45s   7GB
Aug 18 08:30:44 Starting translator/monadic/examples
Aug 18 08:33:35 Finished translator/monadic/examples                           2m49s   2GB
Aug 18 08:33:35 Starting examples
Aug 18 08:42:21 Finished examples                                              8m45s   3GB
Aug 18 08:42:22 Starting examples/compilation/x64
Aug 18 10:44:21 Finished examples/compilation/x64                           2h01m59s  10GB
Aug 18 10:44:22 Starting examples/compilation/x64/proofs
Aug 18 10:45:47 Finished examples/compilation/x64/proofs                       1m25s   2GB
Aug 18 10:45:48 Starting examples/compilation/ag32
Aug 18 11:14:04 Finished examples/compilation/ag32                            28m15s   6GB
Aug 18 11:14:04 Starting examples/compilation/ag32/proofs
Aug 18 11:14:52 Finished examples/compilation/ag32/proofs                        46s   3GB
Aug 18 11:14:52 Starting translator/okasaki-examples
Aug 18 11:18:57 Finished translator/okasaki-examples                           4m04s   1GB
Aug 18 11:18:57 Starting translator/other-examples
Aug 18 11:19:38 Finished translator/other-examples                               39s   1GB
Aug 18 11:19:38 Starting compiler/parsing/tests
Aug 18 11:20:02 Finished compiler/parsing/tests                                  23s 526MB
Aug 18 11:20:02 Starting compiler/inference/tests
Aug 18 11:24:13 Finished compiler/inference/tests                              4m10s   5GB
Aug 18 11:24:14 Starting compiler/bootstrap/translation
Aug 18 13:52:03 Finished compiler/bootstrap/translation                     2h27m48s  31GB
Aug 18 13:52:03 Starting unverified/sexpr-bootstrap/x64/64
Aug 18 14:03:32 Finished unverified/sexpr-bootstrap/x64/64                    11m27s   6GB
Aug 18 14:03:32 Starting unverified/sexpr-bootstrap/x64/32
Aug 18 14:12:09 Finished unverified/sexpr-bootstrap/x64/32                     8m35s   5GB
Aug 18 14:12:09 Starting compiler/benchmarks
Aug 18 14:49:41 Finished compiler/benchmarks                                  37m31s   1GB
Aug 18 14:49:42 Starting compiler/bootstrap/compilation/x64/64
Aug 19 02:41:15 Finished compiler/bootstrap/compilation/x64/64             11h51m31s  64GB
Aug 19 02:41:15 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 19 02:44:34 Finished compiler/bootstrap/compilation/x64/64/proofs          3m17s   5GB
Aug 19 02:44:34 Starting compiler/bootstrap/compilation/x64/32
Aug 19 13:35:56 Finished compiler/bootstrap/compilation/x64/32             10h51m20s  64GB
Aug 19 13:35:56 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 19 13:38:26 Finished compiler/bootstrap/compilation/x64/32/proofs          2m29s  10GB
Aug 19 13:38:26 Starting compiler/bootstrap/compilation/ag32/32
Aug 20 02:31:44 Finished compiler/bootstrap/compilation/ag32/32            12h53m16s  64GB
Aug 20 02:31:44 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 20 02:54:33 Finished compiler/bootstrap/compilation/ag32/32/proofs        22m48s  17GB
Aug 20 02:54:33 SUCCESS