Job 2178

CakeML:e6db84d62373636cd9788a3ebd3d245e4a58b720
  Fix errors caused by HOL deleting various quotient_*Theory [Jul 31 03:35:47]
HOL:cd25f914c1e642bc121101b8cc6d3de1bb6e8e6a
  Fixes after Num and Pair hidden [Jul 29 01:41:22]
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 31 03:37:42 Claimed job
Jul 31 03:37:47 Building HOL
Jul 31 03:52:21 Starting developers
Jul 31 03:52:24 Finished developers                                               2s 205MB
Jul 31 03:52:25 Starting developers/bin
Jul 31 03:52:36 Finished developers/bin                                           9s   1GB
Jul 31 03:52:37 Starting compiler/proofs
Jul 31 05:36:59 Finished compiler/proofs                                    1h44m20s  39GB
Jul 31 05:37:00 Starting compiler/bootstrap/translation
Jul 31 13:27:24 Finished compiler/bootstrap/translation                     7h50m22s  66GB
Jul 31 13:27:25 Starting semantics/ffi
Jul 31 13:27:33 Finished semantics/ffi                                            7s 690MB
Jul 31 13:27:34 Starting semantics
Jul 31 13:27:35 Finished semantics                                                0s  63MB
Jul 31 13:27:36 Starting semantics/proofs
Jul 31 13:28:10 Finished semantics/proofs                                        33s   2GB
Jul 31 13:28:11 Starting semantics/alt_semantics
Jul 31 13:28:53 Finished semantics/alt_semantics                                 40s   1GB
Jul 31 13:28:54 Starting semantics/alt_semantics/proofs
Jul 31 13:39:49 Finished semantics/alt_semantics/proofs                       10m54s   2GB
Jul 31 13:39:49 Starting basis/pure
Jul 31 13:39:51 Finished basis/pure                                               0s  72MB
Jul 31 13:39:51 Starting translator
Jul 31 13:41:35 Finished translator                                            1m42s   3GB
Jul 31 13:41:36 Starting compiler/parsing
Jul 31 13:41:37 Finished compiler/parsing                                         0s  70MB
Jul 31 13:41:38 Starting characteristic
Jul 31 13:41:40 Finished characteristic                                           0s  85MB
Jul 31 13:41:41 Starting translator/monadic
Jul 31 13:41:42 Finished translator/monadic                                       0s  92MB
Jul 31 13:41:43 Starting basis
Jul 31 13:45:36 Finished basis                                                 3m52s   5GB
Jul 31 13:45:37 Starting compiler/inference
Jul 31 13:45:38 Finished compiler/inference                                       0s  76MB
Jul 31 13:45:39 Starting compiler/backend/reg_alloc
Jul 31 13:45:40 Finished compiler/backend/reg_alloc                               0s  65MB
Jul 31 13:45:41 Starting compiler/backend/gc
Jul 31 13:45:43 Finished compiler/backend/gc                                      0s 133MB
Jul 31 13:45:44 Starting compiler/backend
Jul 31 13:46:01 Finished compiler/backend                                        16s   1GB
Jul 31 13:46:02 Starting compiler/encoders/asm
Jul 31 13:46:03 Finished compiler/encoders/asm                                    0s  91MB
Jul 31 13:46:04 Starting compiler/encoders/x64
Jul 31 13:46:05 Finished compiler/encoders/x64                                    0s  94MB
Jul 31 13:46:06 Starting compiler/encoders/arm7
Jul 31 13:46:08 Finished compiler/encoders/arm7                                   0s  92MB
Jul 31 13:46:08 Starting compiler/encoders/arm8
Jul 31 13:46:10 Finished compiler/encoders/arm8                                   0s  88MB
Jul 31 13:46:11 Starting compiler/encoders/arm8_asl
Jul 31 16:02:53 Finished compiler/encoders/arm8_asl                         2h16m41s  42GB
Jul 31 16:02:54 Starting compiler/encoders/mips
Jul 31 16:02:55 Finished compiler/encoders/mips                                   0s  87MB
Jul 31 16:02:56 Starting compiler/encoders/riscv
Jul 31 16:02:58 Finished compiler/encoders/riscv                                  0s  90MB
Jul 31 16:02:59 Starting compiler/encoders/ag32
Jul 31 16:03:00 Finished compiler/encoders/ag32                                   0s  90MB
Jul 31 16:03:01 Starting compiler/backend/x64
Jul 31 16:03:02 Finished compiler/backend/x64                                     0s 129MB
Jul 31 16:03:03 Starting compiler/backend/arm7
Jul 31 16:03:05 Finished compiler/backend/arm7                                    0s 128MB
Jul 31 16:03:06 Starting compiler/backend/arm8
Jul 31 16:03:07 Finished compiler/backend/arm8                                    0s 129MB
Jul 31 16:03:08 Starting compiler/backend/mips
Jul 31 16:03:10 Finished compiler/backend/mips                                    0s 129MB
Jul 31 16:03:11 Starting compiler/backend/riscv
Jul 31 16:03:12 Finished compiler/backend/riscv                                   0s 128MB
Jul 31 16:03:13 Starting compiler/backend/ag32
Jul 31 16:04:35 Finished compiler/backend/ag32                                 1m20s   2GB
Jul 31 16:04:36 Starting compiler/parsing/proofs
Jul 31 16:04:37 Finished compiler/parsing/proofs                                  0s  71MB
Jul 31 16:04:38 Starting compiler/inference/proofs
Jul 31 16:04:39 Finished compiler/inference/proofs                                0s  80MB
Jul 31 16:04:40 Starting compiler/backend/semantics
Jul 31 16:06:05 Finished compiler/backend/semantics                            1m23s   2GB
Jul 31 16:06:05 Starting compiler/backend/reg_alloc/proofs
Jul 31 16:06:07 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Jul 31 16:06:08 Starting compiler/backend/proofs
Jul 31 16:07:09 Finished compiler/backend/proofs                                 59s   3GB
Jul 31 16:07:09 Starting compiler/backend/serialiser
Jul 31 16:07:12 Finished compiler/backend/serialiser                              1s 182MB
Jul 31 16:07:12 Starting compiler/encoders/x64/proofs
Jul 31 16:16:32 Finished compiler/encoders/x64/proofs                          9m18s   5GB
Jul 31 16:16:32 Starting compiler/encoders/arm7/proofs
Jul 31 16:29:22 Finished compiler/encoders/arm7/proofs                        12m48s  11GB
Jul 31 16:29:23 Starting compiler/encoders/arm8/proofs
Jul 31 16:36:08 Finished compiler/encoders/arm8/proofs                         6m44s   5GB
Jul 31 16:36:09 Starting compiler/encoders/arm8_asl/proofs
Jul 31 17:24:01 Finished compiler/encoders/arm8_asl/proofs                    47m50s  10GB
Jul 31 17:24:02 Starting compiler/encoders/mips/proofs
Jul 31 17:34:15 Finished compiler/encoders/mips/proofs                        10m11s   7GB
Jul 31 17:34:15 Starting compiler/encoders/riscv/proofs
Jul 31 17:42:35 Finished compiler/encoders/riscv/proofs                        8m18s   3GB
Jul 31 17:42:36 Starting compiler/encoders/ag32/proofs
Jul 31 17:45:01 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Jul 31 17:45:02 Starting compiler/backend/x64/proofs
Jul 31 17:45:43 Finished compiler/backend/x64/proofs                             40s   3GB
Jul 31 17:45:43 Starting compiler/backend/arm7/proofs
Jul 31 17:46:30 Finished compiler/backend/arm7/proofs                            45s   3GB
Jul 31 17:46:31 Starting compiler/backend/arm8/proofs
Jul 31 17:47:11 Finished compiler/backend/arm8/proofs                            39s   2GB
Jul 31 17:47:11 Starting compiler/backend/arm8_asl
Jul 31 17:47:37 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 31 17:47:38 Starting compiler/backend/mips/proofs
Jul 31 17:48:21 Finished compiler/backend/mips/proofs                            42s   3GB
Jul 31 17:48:22 Starting compiler/backend/riscv/proofs
Jul 31 17:49:10 Finished compiler/backend/riscv/proofs                           47s   3GB
Jul 31 17:49:11 Starting compiler/backend/ag32/proofs
Jul 31 18:02:19 Finished compiler/backend/ag32/proofs                         13m07s   6GB
Jul 31 18:02:20 Starting candle/set-theory
Jul 31 18:03:07 Finished candle/set-theory                                       45s   1GB
Jul 31 18:03:07 Starting candle/syntax-lib
Jul 31 18:03:09 Finished candle/syntax-lib                                        0s  66MB
Jul 31 18:03:10 Starting candle/standard/syntax
Jul 31 18:03:25 Finished candle/standard/syntax                                  15s   1GB
Jul 31 18:03:26 Starting candle/standard/semantics
Jul 31 18:05:50 Finished candle/standard/semantics                             2m23s   2GB
Jul 31 18:05:51 Starting candle/standard/monadic
Jul 31 18:05:53 Finished candle/standard/monadic                                  0s  97MB
Jul 31 18:05:53 Starting candle/standard/ml_kernel
Jul 31 18:07:44 Finished candle/standard/ml_kernel                             1m49s   5GB
Jul 31 18:07:45 Starting candle/overloading/syntax
Jul 31 18:11:10 Finished candle/overloading/syntax                             3m24s   1GB
Jul 31 18:11:11 Starting candle/overloading/semantics
Jul 31 18:22:32 Finished candle/overloading/semantics                         11m20s   4GB
Jul 31 18:22:33 Starting candle/overloading/monadic
Jul 31 18:25:08 Finished candle/overloading/monadic                            2m33s   3GB
Jul 31 18:25:08 Starting candle/overloading/ml_kernel
Jul 31 18:32:34 Finished candle/overloading/ml_kernel                          7m24s   6GB
Jul 31 18:32:35 Starting candle/overloading/ml_checker
Jul 31 18:35:07 Finished candle/overloading/ml_checker                         2m31s   6GB
Jul 31 18:35:08 Starting candle/prover
Jul 31 18:45:00 Finished candle/prover                                         9m51s   5GB
Jul 31 18:45:01 Starting pancake
Jul 31 18:45:59 Finished pancake                                                 57s   1GB
Jul 31 18:46:00 Starting pancake/ffi
Jul 31 18:46:01 Finished pancake/ffi                                              0s  20MB
Jul 31 18:46:02 Starting pancake/semantics
Jul 31 18:48:20 Finished pancake/semantics                                     2m17s   2GB
Jul 31 18:48:21 Starting pancake/parser
Jul 31 18:48:45 Finished pancake/parser                                          23s   1GB
Jul 31 18:48:46 Starting pancake/proofs
Jul 31 19:18:16 Finished pancake/proofs                                       29m29s   8GB
Jul 31 19:18:17 Starting characteristic/examples
Jul 31 19:19:51 Finished characteristic/examples                               1m33s   5GB
Jul 31 19:19:52 Starting tutorial/solutions
Jul 31 19:35:34 Finished tutorial/solutions                                   15m39s  10GB
Jul 31 19:35:35 Starting translator/monadic/examples
Jul 31 19:39:18 Finished translator/monadic/examples                           3m42s   5GB
Jul 31 19:39:18 Starting examples
Jul 31 19:54:16 Finished examples                                             14m56s   7GB
Jul 31 19:54:16 Starting examples/compilation/x64
Jul 31 21:49:55 Finished examples/compilation/x64                           1h55m36s  27GB
Jul 31 21:49:55 Starting examples/compilation/x64/proofs
Jul 31 21:53:41 Finished examples/compilation/x64/proofs                       3m45s   6GB
Jul 31 21:53:42 Starting examples/compilation/ag32
Jul 31 22:23:51 Finished examples/compilation/ag32                            30m07s   9GB
Jul 31 22:23:52 Starting examples/compilation/ag32/proofs
Jul 31 22:25:19 Finished examples/compilation/ag32/proofs                      1m25s   6GB
Jul 31 22:25:20 Starting examples/compilation/to_word
Jul 31 22:29:12 Finished examples/compilation/to_word                          3m51s  11GB
Jul 31 22:29:13 Starting examples/lpr_checker
Jul 31 22:30:26 Finished examples/lpr_checker                                  1m12s   2GB
Jul 31 22:30:27 Starting examples/lpr_checker/array
Jul 31 23:04:42 Finished examples/lpr_checker/array                           34m13s   9GB
Jul 31 23:04:43 Starting examples/lpr_checker/array/compilation
Jul 31 23:38:29 Finished examples/lpr_checker/array/compilation               33m45s  41GB
Jul 31 23:38:30 Starting examples/lpr_checker/array/compilation/proofs
Jul 31 23:40:24 Finished examples/lpr_checker/array/compilation/proofs         1m52s  10GB
Jul 31 23:40:24 Starting examples/opentheory
Jul 31 23:51:12 Finished examples/opentheory                                  10m47s   8GB
Jul 31 23:51:13 Starting examples/opentheory
Jul 31 23:51:15 Finished examples/opentheory                                      0s 122MB
Jul 31 23:51:16 Starting examples/opentheory/compilation
Aug 01 00:27:20 Finished examples/opentheory/compilation                      36m01s  55GB
Aug 01 00:27:21 Starting examples/opentheory/compilation/proofs
Aug 01 00:28:48 Finished examples/opentheory/compilation/proofs                1m25s   6GB
Aug 01 00:28:49 Starting examples/opentheory/compilation/ag32
Aug 01 01:00:19 Finished examples/opentheory/compilation/ag32                 31m29s  38GB
Aug 01 01:00:20 Starting examples/opentheory/compilation/ag32/proofs
Aug 01 01:02:38 Finished examples/opentheory/compilation/ag32/proofs           2m16s  11GB
Aug 01 01:02:39 Starting examples/sat_encodings
Aug 01 01:05:14 Finished examples/sat_encodings                                2m34s   1GB
Aug 01 01:05:15 Starting examples/sat_encodings/case_studies
Aug 01 01:07:13 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Aug 01 01:07:14 Starting examples/sat_encodings/translation
Aug 01 01:13:18 Finished examples/sat_encodings/translation                    6m02s   7GB
Aug 01 01:13:18 Starting examples/sat_encodings/translation/compilation
Aug 01 01:47:31 Finished examples/sat_encodings/translation/compilation       34m11s  43GB
Aug 01 01:47:32 Starting examples/deflate
Aug 01 01:48:45 Finished examples/deflate                                      1m12s   1GB
Aug 01 01:48:46 Starting examples/deflate/translation
Aug 01 01:50:24 Finished examples/deflate/translation                          1m37s   7GB
Aug 01 01:50:25 Starting examples/deflate/translation/compilation
Aug 01 02:07:32 Finished examples/deflate/translation/compilation             17m06s  20GB
Aug 01 02:07:33 Starting examples/vipr
Aug 01 02:11:39 Finished examples/vipr                                         4m04s   7GB
Aug 01 02:11:40 Starting examples/vipr/compilation
Aug 01 02:31:27 Finished examples/vipr/compilation                            19m46s  33GB
Aug 01 02:31:28 Starting translator/okasaki-examples
Aug 01 02:36:27 Finished translator/okasaki-examples                           4m57s   4GB
Aug 01 02:36:27 Starting translator/other-examples
Aug 01 02:40:13 Finished translator/other-examples                             3m44s   3GB
Aug 01 02:40:14 Starting compiler/parsing/tests
Aug 01 02:40:48 Finished compiler/parsing/tests                                  32s   1GB
Aug 01 02:40:49 Starting compiler/inference/tests
Aug 01 02:48:10 Finished compiler/inference/tests                              7m20s   6GB
Aug 01 02:48:11 Starting compiler/printing/test
Aug 01 02:51:39 Finished compiler/printing/test                                3m26s   6GB
Aug 01 02:51:40 Starting icing/flover
Aug 01 03:27:26 Finished icing/flover                                         35m45s   4GB
Aug 01 03:27:27 Starting icing/
Aug 01 04:24:15 Finished icing/                                               56m46s  27GB
Aug 01 04:24:16 Starting icing/examples
Aug 01 04:25:57 Finished icing/examples                                        1m39s   8GB
Aug 01 04:25:58 Starting compiler/repl
Aug 01 04:34:42 Finished compiler/repl                                         8m43s   9GB
Aug 01 04:34:43 Starting unverified/sexpr-bootstrap/x64/64
Aug 01 04:46:02 Finished unverified/sexpr-bootstrap/x64/64                    10m57s  16GB
Aug 01 04:46:03 Starting unverified/sexpr-bootstrap/x64/32
Aug 01 04:55:22 Finished unverified/sexpr-bootstrap/x64/32                     9m01s  13GB
Aug 01 04:55:23 Starting compiler/benchmarks
Aug 01 04:56:08 Finished compiler/benchmarks                                     43s 713MB
Aug 01 04:56:08 Starting compiler/bootstrap/compilation/x64/64
Aug 01 18:44:04 Finished compiler/bootstrap/compilation/x64/64             13h47m43s 143GB
Aug 01 18:44:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 01 19:05:16 Finished compiler/bootstrap/compilation/x64/64/proofs         21m10s  43GB
Aug 01 19:05:17 Starting compiler/bootstrap/compilation/x64/32
Aug 02 01:52:57 Finished compiler/bootstrap/compilation/x64/32              6h47m23s 120GB
Aug 02 01:52:58 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 02 01:56:27 Finished compiler/bootstrap/compilation/x64/32/proofs          3m28s  18GB
Aug 02 01:56:28 Starting compiler/bootstrap/compilation/ag32/32
Aug 02 09:10:29 Finished compiler/bootstrap/compilation/ag32/32             7h13m58s 112GB
Aug 02 09:10:30 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 02 09:18:11 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m40s  48GB
Aug 02 09:18:12 SUCCESS