Job 2238

CakeML:8ac36a22c960a9f4aaae14aa89dabaf177cd63fa
  Merge pull request #974 from CakeML/dominance [Nov 15 15:00:12]
HOL:e7f2e175666a4f2e69629143d260e17e1817b475
  Minor additions to cv<->term transfer theorems [Nov 13 06:11:30]
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

Nov 15 15:17:25 Claimed job
Nov 15 15:17:30 Building HOL
Nov 15 15:32:04 Starting developers
Nov 15 15:32:08 Finished developers                                               2s 190MB
Nov 15 15:32:08 Starting developers/bin
Nov 15 15:32:19 Finished developers/bin                                           9s   1GB
Nov 15 15:32:20 Starting compiler/proofs
Nov 15 17:17:30 Finished compiler/proofs                                    1h45m09s  47GB
Nov 15 17:17:31 Starting compiler/bootstrap/translation
Nov 16 01:28:47 Finished compiler/bootstrap/translation                     8h11m14s  76GB
Nov 16 01:28:48 Starting semantics/ffi
Nov 16 01:28:56 Finished semantics/ffi                                            7s 655MB
Nov 16 01:28:57 Starting semantics
Nov 16 01:28:58 Finished semantics                                                0s  66MB
Nov 16 01:28:59 Starting semantics/proofs
Nov 16 01:29:37 Finished semantics/proofs                                        36s   1GB
Nov 16 01:29:38 Starting semantics/alt_semantics
Nov 16 01:30:17 Finished semantics/alt_semantics                                 38s   1GB
Nov 16 01:30:18 Starting semantics/alt_semantics/proofs
Nov 16 01:41:15 Finished semantics/alt_semantics/proofs                       10m56s   3GB
Nov 16 01:41:16 Starting basis/pure
Nov 16 01:41:17 Finished basis/pure                                               0s  67MB
Nov 16 01:41:18 Starting translator
Nov 16 01:43:03 Finished translator                                            1m43s   3GB
Nov 16 01:43:03 Starting compiler/parsing
Nov 16 01:43:05 Finished compiler/parsing                                         0s  70MB
Nov 16 01:43:06 Starting characteristic
Nov 16 01:43:07 Finished characteristic                                           0s  90MB
Nov 16 01:43:08 Starting translator/monadic
Nov 16 01:43:09 Finished translator/monadic                                       0s  95MB
Nov 16 01:43:10 Starting basis
Nov 16 01:46:50 Finished basis                                                 3m38s   5GB
Nov 16 01:46:51 Starting compiler/inference
Nov 16 01:46:52 Finished compiler/inference                                       0s  80MB
Nov 16 01:46:53 Starting compiler/backend/reg_alloc
Nov 16 01:46:54 Finished compiler/backend/reg_alloc                               0s  66MB
Nov 16 01:46:55 Starting compiler/backend/gc
Nov 16 01:46:57 Finished compiler/backend/gc                                      0s 131MB
Nov 16 01:46:58 Starting compiler/backend
Nov 16 01:47:15 Finished compiler/backend                                        16s   1GB
Nov 16 01:47:16 Starting compiler/encoders/asm
Nov 16 01:47:18 Finished compiler/encoders/asm                                    0s  90MB
Nov 16 01:47:19 Starting compiler/encoders/x64
Nov 16 01:47:20 Finished compiler/encoders/x64                                    0s  89MB
Nov 16 01:47:21 Starting compiler/encoders/arm7
Nov 16 01:47:22 Finished compiler/encoders/arm7                                   0s  92MB
Nov 16 01:47:23 Starting compiler/encoders/arm8
Nov 16 01:47:25 Finished compiler/encoders/arm8                                   0s  87MB
Nov 16 01:47:25 Starting compiler/encoders/arm8_asl
Nov 16 03:56:47 Finished compiler/encoders/arm8_asl                         2h09m21s  41GB
Nov 16 03:56:48 Starting compiler/encoders/mips
Nov 16 03:56:50 Finished compiler/encoders/mips                                   0s  87MB
Nov 16 03:56:50 Starting compiler/encoders/riscv
Nov 16 03:56:52 Finished compiler/encoders/riscv                                  0s  90MB
Nov 16 03:56:53 Starting compiler/encoders/ag32
Nov 16 03:56:54 Finished compiler/encoders/ag32                                   0s  90MB
Nov 16 03:56:55 Starting compiler/backend/x64
Nov 16 03:56:57 Finished compiler/backend/x64                                     0s 129MB
Nov 16 03:56:58 Starting compiler/backend/arm7
Nov 16 03:56:59 Finished compiler/backend/arm7                                    0s 129MB
Nov 16 03:57:00 Starting compiler/backend/arm8
Nov 16 03:57:02 Finished compiler/backend/arm8                                    0s 129MB
Nov 16 03:57:03 Starting compiler/backend/mips
Nov 16 03:57:04 Finished compiler/backend/mips                                    0s 129MB
Nov 16 03:57:05 Starting compiler/backend/riscv
Nov 16 03:57:07 Finished compiler/backend/riscv                                   0s 129MB
Nov 16 03:57:08 Starting compiler/backend/ag32
Nov 16 03:58:27 Finished compiler/backend/ag32                                 1m18s   2GB
Nov 16 03:58:28 Starting compiler/parsing/proofs
Nov 16 03:58:29 Finished compiler/parsing/proofs                                  0s  73MB
Nov 16 03:58:30 Starting compiler/inference/proofs
Nov 16 03:58:32 Finished compiler/inference/proofs                                0s  87MB
Nov 16 03:58:32 Starting compiler/backend/semantics
Nov 16 04:00:02 Finished compiler/backend/semantics                            1m28s   2GB
Nov 16 04:00:03 Starting compiler/backend/reg_alloc/proofs
Nov 16 04:00:04 Finished compiler/backend/reg_alloc/proofs                        0s  96MB
Nov 16 04:00:05 Starting compiler/backend/proofs
Nov 16 04:01:09 Finished compiler/backend/proofs                               1m02s   4GB
Nov 16 04:01:09 Starting compiler/backend/serialiser
Nov 16 04:01:12 Finished compiler/backend/serialiser                              1s 188MB
Nov 16 04:01:13 Starting compiler/encoders/x64/proofs
Nov 16 04:10:36 Finished compiler/encoders/x64/proofs                          9m22s   5GB
Nov 16 04:10:37 Starting compiler/encoders/arm7/proofs
Nov 16 04:23:36 Finished compiler/encoders/arm7/proofs                        12m58s   7GB
Nov 16 04:23:37 Starting compiler/encoders/arm8/proofs
Nov 16 04:30:06 Finished compiler/encoders/arm8/proofs                         6m28s   4GB
Nov 16 04:30:07 Starting compiler/encoders/arm8_asl/proofs
Nov 16 05:18:19 Finished compiler/encoders/arm8_asl/proofs                    48m10s   8GB
Nov 16 05:18:20 Starting compiler/encoders/mips/proofs
Nov 16 05:28:30 Finished compiler/encoders/mips/proofs                        10m09s   7GB
Nov 16 05:28:31 Starting compiler/encoders/riscv/proofs
Nov 16 05:37:02 Finished compiler/encoders/riscv/proofs                        8m29s   3GB
Nov 16 05:37:03 Starting compiler/encoders/ag32/proofs
Nov 16 05:39:24 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Nov 16 05:39:25 Starting compiler/backend/x64/proofs
Nov 16 05:40:05 Finished compiler/backend/x64/proofs                             39s   3GB
Nov 16 05:40:06 Starting compiler/backend/arm7/proofs
Nov 16 05:40:49 Finished compiler/backend/arm7/proofs                            42s   2GB
Nov 16 05:40:50 Starting compiler/backend/arm8/proofs
Nov 16 05:41:29 Finished compiler/backend/arm8/proofs                            38s   3GB
Nov 16 05:41:30 Starting compiler/backend/arm8_asl
Nov 16 05:41:59 Finished compiler/backend/arm8_asl                               27s   2GB
Nov 16 05:41:59 Starting compiler/backend/mips/proofs
Nov 16 05:42:43 Finished compiler/backend/mips/proofs                            42s   3GB
Nov 16 05:42:43 Starting compiler/backend/riscv/proofs
Nov 16 05:43:33 Finished compiler/backend/riscv/proofs                           48s   3GB
Nov 16 05:43:34 Starting compiler/backend/ag32/proofs
Nov 16 05:56:39 Finished compiler/backend/ag32/proofs                         13m04s   6GB
Nov 16 05:56:40 Starting candle/set-theory
Nov 16 05:57:23 Finished candle/set-theory                                       42s   1GB
Nov 16 05:57:24 Starting candle/syntax-lib
Nov 16 05:57:25 Finished candle/syntax-lib                                        0s  67MB
Nov 16 05:57:26 Starting candle/standard/syntax
Nov 16 05:57:42 Finished candle/standard/syntax                                  15s   1GB
Nov 16 05:57:43 Starting candle/standard/semantics
Nov 16 06:00:04 Finished candle/standard/semantics                             2m20s   2GB
Nov 16 06:00:05 Starting candle/standard/monadic
Nov 16 06:00:06 Finished candle/standard/monadic                                  0s 102MB
Nov 16 06:00:07 Starting candle/standard/ml_kernel
Nov 16 06:01:56 Finished candle/standard/ml_kernel                             1m48s   5GB
Nov 16 06:01:57 Starting candle/overloading/syntax
Nov 16 06:05:26 Finished candle/overloading/syntax                             3m28s   2GB
Nov 16 06:05:27 Starting candle/overloading/semantics
Nov 16 06:16:52 Finished candle/overloading/semantics                         11m23s   5GB
Nov 16 06:16:53 Starting candle/overloading/monadic
Nov 16 06:19:27 Finished candle/overloading/monadic                            2m32s   3GB
Nov 16 06:19:28 Starting candle/overloading/ml_kernel
Nov 16 06:26:56 Finished candle/overloading/ml_kernel                          7m27s   6GB
Nov 16 06:26:57 Starting candle/overloading/ml_checker
Nov 16 06:29:31 Finished candle/overloading/ml_checker                         2m32s   7GB
Nov 16 06:29:32 Starting candle/prover
Nov 16 06:39:21 Finished candle/prover                                         9m48s   5GB
Nov 16 06:39:22 Starting pancake
Nov 16 06:40:23 Finished pancake                                                 59s   1GB
Nov 16 06:40:23 Starting pancake/ffi
Nov 16 06:40:24 Finished pancake/ffi                                              0s  21MB
Nov 16 06:40:25 Starting pancake/semantics
Nov 16 06:42:43 Finished pancake/semantics                                     2m17s   2GB
Nov 16 06:42:44 Starting pancake/parser
Nov 16 06:43:12 Finished pancake/parser                                          26s   2GB
Nov 16 06:43:12 Starting pancake/proofs
Nov 16 07:12:57 Finished pancake/proofs                                       29m43s   8GB
Nov 16 07:12:58 Starting characteristic/examples
Nov 16 07:14:34 Finished characteristic/examples                               1m35s   6GB
Nov 16 07:14:35 Starting tutorial/solutions
Nov 16 07:30:04 Finished tutorial/solutions                                   15m27s  12GB
Nov 16 07:30:05 Starting translator/monadic/examples
Nov 16 07:33:49 Finished translator/monadic/examples                           3m42s   5GB
Nov 16 07:33:49 Starting examples
Nov 16 07:48:22 Finished examples                                             14m31s   7GB
Nov 16 07:48:23 Starting examples/compilation/x64
Nov 16 09:45:04 Finished examples/compilation/x64                           1h56m40s  24GB
Nov 16 09:45:05 Starting examples/compilation/x64/proofs
Nov 16 09:48:48 Finished examples/compilation/x64/proofs                       3m42s   6GB
Nov 16 09:48:49 Starting examples/compilation/ag32
Nov 16 10:18:46 Finished examples/compilation/ag32                            29m56s  12GB
Nov 16 10:18:47 Starting examples/compilation/ag32/proofs
Nov 16 10:20:13 Finished examples/compilation/ag32/proofs                      1m25s   7GB
Nov 16 10:20:14 Starting examples/compilation/to_word
Nov 16 10:24:05 Finished examples/compilation/to_word                          3m50s  12GB
Nov 16 10:24:06 Starting examples/lpr_checker
Nov 16 10:25:20 Finished examples/lpr_checker                                  1m13s   2GB
Nov 16 10:25:21 Starting examples/lpr_checker/array
Nov 16 10:54:05 Finished examples/lpr_checker/array                           28m42s  10GB
Nov 16 10:54:06 Starting examples/lpr_checker/array/compilation
Nov 16 11:28:44 Finished examples/lpr_checker/array/compilation               34m37s  42GB
Nov 16 11:28:45 Starting examples/lpr_checker/array/compilation/proofs
Nov 16 11:30:48 Finished examples/lpr_checker/array/compilation/proofs         2m02s   9GB
Nov 16 11:30:49 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 16 11:39:45 Finished examples/lpr_checker/array/compilation/proofsARM8     8m55s  48GB
Nov 16 11:39:46 Starting examples/pseudo_bool
Nov 16 11:41:45 Finished examples/pseudo_bool                                  1m58s   2GB
Nov 16 11:41:46 Starting examples/pseudo_bool/cnf_encoding
Nov 16 11:42:23 Finished examples/pseudo_bool/cnf_encoding                       35s   1GB
Nov 16 11:42:23 Starting examples/pseudo_bool/graph_encoding
Nov 16 11:43:12 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Nov 16 11:43:13 Starting examples/pseudo_bool/array
Nov 16 12:33:34 Finished examples/pseudo_bool/array                           50m19s  12GB
Nov 16 12:33:35 Starting examples/pseudo_bool/array/compilation
Nov 16 14:22:08 Finished examples/pseudo_bool/array/compilation             1h48m31s 122GB
Nov 16 14:22:09 Starting examples/pseudo_bool/array/compilation/proofs
Nov 16 14:25:10 Finished examples/pseudo_bool/array/compilation/proofs         3m00s   7GB
Nov 16 14:25:11 Starting examples/opentheory
Nov 16 14:35:59 Finished examples/opentheory                                  10m47s   7GB
Nov 16 14:36:00 Starting examples/opentheory
Nov 16 14:36:02 Finished examples/opentheory                                      0s 123MB
Nov 16 14:36:03 Starting examples/opentheory/compilation
Nov 16 15:12:15 Finished examples/opentheory/compilation                      36m11s  46GB
Nov 16 15:12:16 Starting examples/opentheory/compilation/proofs
Nov 16 15:13:47 Finished examples/opentheory/compilation/proofs                1m29s   6GB
Nov 16 15:13:47 Starting examples/opentheory/compilation/ag32
Nov 16 15:45:51 Finished examples/opentheory/compilation/ag32                 32m02s  49GB
Nov 16 15:45:52 Starting examples/opentheory/compilation/ag32/proofs
Nov 16 15:48:10 Finished examples/opentheory/compilation/ag32/proofs           2m17s  11GB
Nov 16 15:48:11 Starting examples/sat_encodings
Nov 16 15:50:45 Finished examples/sat_encodings                                2m33s   1GB
Nov 16 15:50:46 Starting examples/sat_encodings/case_studies
Nov 16 15:52:45 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Nov 16 15:52:46 Starting examples/sat_encodings/translation
Nov 16 15:58:53 Finished examples/sat_encodings/translation                    6m06s   7GB
Nov 16 15:58:54 Starting examples/sat_encodings/translation/compilation
Nov 16 16:34:31 Finished examples/sat_encodings/translation/compilation       35m36s  36GB
Nov 16 16:34:32 Starting examples/deflate
Nov 16 16:35:47 Finished examples/deflate                                      1m13s   2GB
Nov 16 16:35:48 Starting examples/deflate/translation
Nov 16 16:37:24 Finished examples/deflate/translation                          1m35s   7GB
Nov 16 16:37:25 Starting examples/deflate/translation/compilation
Nov 16 16:54:01 Finished examples/deflate/translation/compilation             16m35s  22GB
Nov 16 16:54:02 Starting examples/vipr
Nov 16 16:58:02 Finished examples/vipr                                         3m59s   7GB
Nov 16 16:58:03 Starting examples/vipr/compilation
Nov 16 17:18:09 Finished examples/vipr/compilation                            20m04s  28GB
Nov 16 17:18:10 Starting translator/okasaki-examples
Nov 16 17:23:07 Finished translator/okasaki-examples                           4m56s   4GB
Nov 16 17:23:08 Starting translator/other-examples
Nov 16 17:26:50 Finished translator/other-examples                             3m41s   3GB
Nov 16 17:26:51 Starting compiler/parsing/tests
Nov 16 17:27:25 Finished compiler/parsing/tests                                  32s   1GB
Nov 16 17:27:26 Starting compiler/inference/tests
Nov 16 17:35:00 Finished compiler/inference/tests                              7m33s   5GB
Nov 16 17:35:01 Starting compiler/printing/test
Nov 16 17:38:29 Finished compiler/printing/test                                3m27s   6GB
Nov 16 17:38:30 Starting icing/flover
Nov 16 18:14:28 Finished icing/flover                                         35m56s   3GB
Nov 16 18:14:29 Starting icing/
Nov 16 19:10:09 Finished icing/                                               55m39s  31GB
Nov 16 19:10:10 Starting icing/examples
Nov 16 19:11:52 Finished icing/examples                                        1m41s   8GB
Nov 16 19:11:53 Starting compiler/repl
Nov 16 19:20:39 Finished compiler/repl                                         8m44s  10GB
Nov 16 19:20:40 Starting unverified/sexpr-bootstrap/x64/64
Nov 16 19:32:04 Finished unverified/sexpr-bootstrap/x64/64                    11m01s  17GB
Nov 16 19:32:05 Starting unverified/sexpr-bootstrap/x64/32
Nov 16 19:41:25 Finished unverified/sexpr-bootstrap/x64/32                     9m02s  14GB
Nov 16 19:41:26 Starting compiler/benchmarks
Nov 16 19:42:11 Finished compiler/benchmarks                                     43s 713MB
Nov 16 19:42:12 Starting compiler/bootstrap/compilation/x64/64
Nov 17 10:28:21 Finished compiler/bootstrap/compilation/x64/64             14h45m56s 146GB
Nov 17 10:28:22 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 17 10:49:27 Finished compiler/bootstrap/compilation/x64/64/proofs         21m04s  39GB
Nov 17 10:49:28 Starting compiler/bootstrap/compilation/x64/32
Nov 17 18:05:14 Finished compiler/bootstrap/compilation/x64/32              7h15m38s 103GB
Nov 17 18:05:15 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 17 18:08:58 Finished compiler/bootstrap/compilation/x64/32/proofs          3m42s  17GB
Nov 17 18:08:59 Starting compiler/bootstrap/compilation/ag32/32
Nov 18 01:49:07 Finished compiler/bootstrap/compilation/ag32/32             7h40m07s 142GB
Nov 18 01:49:08 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 18 01:56:47 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m37s  49GB
Nov 18 01:56:48 SUCCESS