Job 2161

CakeML:23b458869d6cee82f5c6fb8f93f3ca797267490b
  Merge pull request #958 from CakeML/pan_compose [Jul 05 12:35:24]
HOL:39d587ce28156b9b533d088a721d072e3271ddfb
  Fix another proof broken by automatic {DIV,MOD}_0 [Jul 03 07:06:39]
Machine:pavlova
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jul 05 12:44:25 Claimed job
Jul 05 12:44:31 Building HOL
Jul 05 12:57:24 Starting developers
Jul 05 12:57:27 Finished developers                                               2s 188MB
Jul 05 12:57:28 Starting developers/bin
Jul 05 12:57:38 Finished developers/bin                                           9s   1GB
Jul 05 12:57:39 Starting compiler/proofs
Jul 05 14:41:34 Finished compiler/proofs                                    1h43m54s  39GB
Jul 05 14:41:35 Starting compiler/bootstrap/translation
Jul 05 22:46:39 Finished compiler/bootstrap/translation                     8h05m01s  90GB
Jul 05 22:46:40 Starting semantics/ffi
Jul 05 22:46:48 Finished semantics/ffi                                            7s 617MB
Jul 05 22:46:49 Starting semantics
Jul 05 22:46:50 Finished semantics                                                0s  63MB
Jul 05 22:46:51 Starting semantics/proofs
Jul 05 22:47:27 Finished semantics/proofs                                        34s   2GB
Jul 05 22:47:27 Starting semantics/alt_semantics
Jul 05 22:48:07 Finished semantics/alt_semantics                                 39s   1GB
Jul 05 22:48:08 Starting semantics/alt_semantics/proofs
Jul 05 22:59:03 Finished semantics/alt_semantics/proofs                       10m54s   5GB
Jul 05 22:59:04 Starting basis/pure
Jul 05 22:59:06 Finished basis/pure                                               0s  72MB
Jul 05 22:59:06 Starting translator
Jul 05 23:00:47 Finished translator                                            1m40s   3GB
Jul 05 23:00:48 Starting compiler/parsing
Jul 05 23:00:49 Finished compiler/parsing                                         0s  69MB
Jul 05 23:00:50 Starting characteristic
Jul 05 23:00:52 Finished characteristic                                           0s  93MB
Jul 05 23:00:53 Starting translator/monadic
Jul 05 23:00:54 Finished translator/monadic                                       0s  90MB
Jul 05 23:00:55 Starting basis
Jul 05 23:04:46 Finished basis                                                 3m49s   5GB
Jul 05 23:04:47 Starting compiler/inference
Jul 05 23:04:48 Finished compiler/inference                                       0s  85MB
Jul 05 23:04:49 Starting compiler/backend/reg_alloc
Jul 05 23:04:50 Finished compiler/backend/reg_alloc                               0s  68MB
Jul 05 23:04:51 Starting compiler/backend/gc
Jul 05 23:04:53 Finished compiler/backend/gc                                      0s 138MB
Jul 05 23:04:53 Starting compiler/backend
Jul 05 23:05:11 Finished compiler/backend                                        16s   1GB
Jul 05 23:05:12 Starting compiler/encoders/asm
Jul 05 23:05:13 Finished compiler/encoders/asm                                    0s  89MB
Jul 05 23:05:14 Starting compiler/encoders/x64
Jul 05 23:05:15 Finished compiler/encoders/x64                                    0s  90MB
Jul 05 23:05:16 Starting compiler/encoders/arm7
Jul 05 23:05:17 Finished compiler/encoders/arm7                                   0s  90MB
Jul 05 23:05:18 Starting compiler/encoders/arm8
Jul 05 23:05:20 Finished compiler/encoders/arm8                                   0s  90MB
Jul 05 23:05:21 Starting compiler/encoders/arm8_asl
Jul 06 01:13:30 Finished compiler/encoders/arm8_asl                         2h08m08s  39GB
Jul 06 01:13:31 Starting compiler/encoders/mips
Jul 06 01:13:32 Finished compiler/encoders/mips                                   0s  90MB
Jul 06 01:13:33 Starting compiler/encoders/riscv
Jul 06 01:13:34 Finished compiler/encoders/riscv                                  0s  93MB
Jul 06 01:13:35 Starting compiler/encoders/ag32
Jul 06 01:13:36 Finished compiler/encoders/ag32                                   0s  89MB
Jul 06 01:13:37 Starting compiler/backend/x64
Jul 06 01:13:39 Finished compiler/backend/x64                                     0s 130MB
Jul 06 01:13:40 Starting compiler/backend/arm7
Jul 06 01:13:41 Finished compiler/backend/arm7                                    0s 130MB
Jul 06 01:13:42 Starting compiler/backend/arm8
Jul 06 01:13:44 Finished compiler/backend/arm8                                    0s 130MB
Jul 06 01:13:45 Starting compiler/backend/mips
Jul 06 01:13:47 Finished compiler/backend/mips                                    0s 130MB
Jul 06 01:13:47 Starting compiler/backend/riscv
Jul 06 01:13:49 Finished compiler/backend/riscv                                   0s 130MB
Jul 06 01:13:50 Starting compiler/backend/ag32
Jul 06 01:15:14 Finished compiler/backend/ag32                                 1m23s   4GB
Jul 06 01:15:15 Starting compiler/parsing/proofs
Jul 06 01:15:16 Finished compiler/parsing/proofs                                  0s  72MB
Jul 06 01:15:17 Starting compiler/inference/proofs
Jul 06 01:15:18 Finished compiler/inference/proofs                                0s  80MB
Jul 06 01:15:19 Starting compiler/backend/semantics
Jul 06 01:16:47 Finished compiler/backend/semantics                            1m26s   3GB
Jul 06 01:16:47 Starting compiler/backend/reg_alloc/proofs
Jul 06 01:16:49 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Jul 06 01:16:50 Starting compiler/backend/proofs
Jul 06 01:17:53 Finished compiler/backend/proofs                               1m01s   3GB
Jul 06 01:17:53 Starting compiler/backend/serialiser
Jul 06 01:17:56 Finished compiler/backend/serialiser                              1s 181MB
Jul 06 01:17:56 Starting compiler/encoders/x64/proofs
Jul 06 01:27:20 Finished compiler/encoders/x64/proofs                          9m22s   5GB
Jul 06 01:27:21 Starting compiler/encoders/arm7/proofs
Jul 06 01:40:10 Finished compiler/encoders/arm7/proofs                        12m48s   8GB
Jul 06 01:40:11 Starting compiler/encoders/arm8/proofs
Jul 06 01:46:41 Finished compiler/encoders/arm8/proofs                         6m29s   5GB
Jul 06 01:46:42 Starting compiler/encoders/arm8_asl/proofs
Jul 06 02:35:07 Finished compiler/encoders/arm8_asl/proofs                    48m24s  10GB
Jul 06 02:35:08 Starting compiler/encoders/mips/proofs
Jul 06 02:45:12 Finished compiler/encoders/mips/proofs                        10m03s   6GB
Jul 06 02:45:13 Starting compiler/encoders/riscv/proofs
Jul 06 02:53:39 Finished compiler/encoders/riscv/proofs                        8m25s   5GB
Jul 06 02:53:40 Starting compiler/encoders/ag32/proofs
Jul 06 02:56:05 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Jul 06 02:56:05 Starting compiler/backend/x64/proofs
Jul 06 02:56:46 Finished compiler/backend/x64/proofs                             39s   2GB
Jul 06 02:56:47 Starting compiler/backend/arm7/proofs
Jul 06 02:57:32 Finished compiler/backend/arm7/proofs                            44s   2GB
Jul 06 02:57:33 Starting compiler/backend/arm8/proofs
Jul 06 02:58:13 Finished compiler/backend/arm8/proofs                            39s   2GB
Jul 06 02:58:14 Starting compiler/backend/arm8_asl
Jul 06 02:58:42 Finished compiler/backend/arm8_asl                               26s   2GB
Jul 06 02:58:43 Starting compiler/backend/mips/proofs
Jul 06 02:59:27 Finished compiler/backend/mips/proofs                            43s   3GB
Jul 06 02:59:28 Starting compiler/backend/riscv/proofs
Jul 06 03:00:17 Finished compiler/backend/riscv/proofs                           48s   4GB
Jul 06 03:00:18 Starting compiler/backend/ag32/proofs
Jul 06 03:13:38 Finished compiler/backend/ag32/proofs                         13m19s   6GB
Jul 06 03:13:39 Starting candle/set-theory
Jul 06 03:14:21 Finished candle/set-theory                                       41s   1GB
Jul 06 03:14:22 Starting candle/syntax-lib
Jul 06 03:14:24 Finished candle/syntax-lib                                        0s  70MB
Jul 06 03:14:24 Starting candle/standard/syntax
Jul 06 03:14:40 Finished candle/standard/syntax                                  15s   1GB
Jul 06 03:14:41 Starting candle/standard/semantics
Jul 06 03:17:05 Finished candle/standard/semantics                             2m22s   2GB
Jul 06 03:17:06 Starting candle/standard/monadic
Jul 06 03:17:07 Finished candle/standard/monadic                                  0s 105MB
Jul 06 03:17:08 Starting candle/standard/ml_kernel
Jul 06 03:18:55 Finished candle/standard/ml_kernel                             1m46s   5GB
Jul 06 03:18:56 Starting candle/overloading/syntax
Jul 06 03:22:21 Finished candle/overloading/syntax                             3m24s   3GB
Jul 06 03:22:22 Starting candle/overloading/semantics
Jul 06 03:33:33 Finished candle/overloading/semantics                         11m10s   4GB
Jul 06 03:33:34 Starting candle/overloading/monadic
Jul 06 03:36:09 Finished candle/overloading/monadic                            2m33s   3GB
Jul 06 03:36:09 Starting candle/overloading/ml_kernel
Jul 06 03:43:38 Finished candle/overloading/ml_kernel                          7m28s   6GB
Jul 06 03:43:39 Starting candle/overloading/ml_checker
Jul 06 03:46:12 Finished candle/overloading/ml_checker                         2m31s   7GB
Jul 06 03:46:13 Starting candle/prover
Jul 06 03:56:11 Finished candle/prover                                         9m57s   5GB
Jul 06 03:56:11 Starting pancake
Jul 06 03:57:10 Finished pancake                                                 57s   1GB
Jul 06 03:57:11 Starting pancake/ffi
Jul 06 03:57:11 Finished pancake/ffi                                              0s  20MB
Jul 06 03:57:12 Starting pancake/semantics
Jul 06 03:59:29 Finished pancake/semantics                                     2m15s   2GB
Jul 06 03:59:30 Starting pancake/proofs
Jul 06 04:29:19 Finished pancake/proofs                                       29m48s   8GB
Jul 06 04:29:20 Starting characteristic/examples
Jul 06 04:30:54 Finished characteristic/examples                               1m33s   5GB
Jul 06 04:30:55 Starting tutorial/solutions
Jul 06 04:46:21 Finished tutorial/solutions                                   15m24s  11GB
Jul 06 04:46:21 Starting translator/monadic/examples
Jul 06 04:50:06 Finished translator/monadic/examples                           3m43s   5GB
Jul 06 04:50:07 Starting examples
Jul 06 05:04:41 Finished examples                                             14m33s   7GB
Jul 06 05:04:41 Starting examples/compilation/x64
Jul 06 07:00:22 Finished examples/compilation/x64                           1h55m38s  15GB
Jul 06 07:00:23 Starting examples/compilation/x64/proofs
Jul 06 07:04:09 Finished examples/compilation/x64/proofs                       3m45s   6GB
Jul 06 07:04:10 Starting examples/compilation/ag32
Jul 06 07:33:29 Finished examples/compilation/ag32                            29m17s  10GB
Jul 06 07:33:29 Starting examples/compilation/ag32/proofs
Jul 06 07:34:59 Finished examples/compilation/ag32/proofs                      1m28s   6GB
Jul 06 07:35:00 Starting examples/compilation/to_word
Jul 06 07:38:48 Finished examples/compilation/to_word                          3m47s  11GB
Jul 06 07:38:49 Starting examples/lpr_checker
Jul 06 07:40:02 Finished examples/lpr_checker                                  1m12s   2GB
Jul 06 07:40:03 Starting examples/lpr_checker/array
Jul 06 08:14:58 Finished examples/lpr_checker/array                           34m52s   9GB
Jul 06 08:14:58 Starting examples/lpr_checker/array/compilation
Jul 06 08:49:10 Finished examples/lpr_checker/array/compilation               34m11s  45GB
Jul 06 08:49:11 Starting examples/lpr_checker/array/compilation/proofs
Jul 06 08:51:05 Finished examples/lpr_checker/array/compilation/proofs         1m52s   9GB
Jul 06 08:51:06 Starting examples/opentheory
Jul 06 09:01:50 Finished examples/opentheory                                  10m43s   7GB
Jul 06 09:01:51 Starting examples/opentheory
Jul 06 09:01:53 Finished examples/opentheory                                      0s 128MB
Jul 06 09:01:53 Starting examples/opentheory/compilation
Jul 06 09:37:33 Finished examples/opentheory/compilation                      35m37s  48GB
Jul 06 09:37:34 Starting examples/opentheory/compilation/proofs
Jul 06 09:39:05 Finished examples/opentheory/compilation/proofs                1m30s   6GB
Jul 06 09:39:06 Starting examples/opentheory/compilation/ag32
Jul 06 10:12:28 Finished examples/opentheory/compilation/ag32                 33m21s  48GB
Jul 06 10:12:29 Starting examples/opentheory/compilation/ag32/proofs
Jul 06 10:14:50 Finished examples/opentheory/compilation/ag32/proofs           2m19s  11GB
Jul 06 10:14:51 Starting examples/sat_encodings
Jul 06 10:17:27 Finished examples/sat_encodings                                2m35s   1GB
Jul 06 10:17:28 Starting examples/sat_encodings/case_studies
Jul 06 10:19:28 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Jul 06 10:19:29 Starting examples/sat_encodings/translation
Jul 06 10:25:36 Finished examples/sat_encodings/translation                    6m06s   7GB
Jul 06 10:25:37 Starting examples/sat_encodings/translation/compilation
Jul 06 10:59:46 Finished examples/sat_encodings/translation/compilation       34m04s  27GB
Jul 06 10:59:46 Starting examples/deflate
Jul 06 11:01:02 Finished examples/deflate                                      1m14s   1GB
Jul 06 11:01:02 Starting examples/deflate/translation
Jul 06 11:02:39 Finished examples/deflate/translation                          1m36s   7GB
Jul 06 11:02:40 Starting examples/deflate/translation/compilation
Jul 06 11:18:27 Finished examples/deflate/translation/compilation             15m45s  15GB
Jul 06 11:18:27 Starting examples/vipr
Jul 06 11:22:32 Finished examples/vipr                                         4m03s   7GB
Jul 06 11:22:33 Starting examples/vipr/compilation
Jul 06 11:42:29 Finished examples/vipr/compilation                            19m54s  20GB
Jul 06 11:42:30 Starting translator/okasaki-examples
Jul 06 11:47:25 Finished translator/okasaki-examples                           4m54s   5GB
Jul 06 11:47:26 Starting translator/other-examples
Jul 06 11:51:03 Finished translator/other-examples                             3m36s   3GB
Jul 06 11:51:04 Starting compiler/parsing/tests
Jul 06 11:51:38 Finished compiler/parsing/tests                                  33s   1GB
Jul 06 11:51:39 Starting compiler/inference/tests
Jul 06 11:59:09 Finished compiler/inference/tests                              7m29s   8GB
Jul 06 11:59:10 Starting compiler/printing/test
Jul 06 12:02:44 Finished compiler/printing/test                                3m32s   4GB
Jul 06 12:02:45 Starting icing/flover
Jul 06 12:37:59 Finished icing/flover                                         35m12s   4GB
Jul 06 12:38:00 Starting icing/
Jul 06 13:34:01 Finished icing/                                               56m00s  30GB
Jul 06 13:34:02 Starting icing/examples
Jul 06 13:35:43 Finished icing/examples                                        1m40s   8GB
Jul 06 13:35:44 Starting compiler/repl
Jul 06 13:44:29 Finished compiler/repl                                         8m44s  10GB
Jul 06 13:44:30 Starting unverified/sexpr-bootstrap/x64/64
Jul 06 13:55:40 Finished unverified/sexpr-bootstrap/x64/64                    10m48s  15GB
Jul 06 13:55:41 Starting unverified/sexpr-bootstrap/x64/32
Jul 06 14:04:56 Finished unverified/sexpr-bootstrap/x64/32                     8m58s  13GB
Jul 06 14:04:57 Starting compiler/benchmarks
Jul 06 14:05:42 Finished compiler/benchmarks                                     43s 713MB
Jul 06 14:05:42 Starting compiler/bootstrap/compilation/x64/64
Jul 07 05:02:31 Finished compiler/bootstrap/compilation/x64/64             14h56m36s 148GB
Jul 07 05:02:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 07 05:23:53 Finished compiler/bootstrap/compilation/x64/64/proofs         21m20s  48GB
Jul 07 05:23:54 Starting compiler/bootstrap/compilation/x64/32
Jul 07 12:13:49 Finished compiler/bootstrap/compilation/x64/32              6h49m47s 102GB
Jul 07 12:13:50 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 07 12:17:16 Finished compiler/bootstrap/compilation/x64/32/proofs          3m26s  18GB
Jul 07 12:17:17 Starting compiler/bootstrap/compilation/ag32/32
Jul 07 19:30:01 Finished compiler/bootstrap/compilation/ag32/32             7h12m42s 134GB
Jul 07 19:30:01 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 07 19:37:09 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m06s  36GB
Jul 07 19:37:10 SUCCESS