Job 2183

CakeML:e6db84d62373636cd9788a3ebd3d245e4a58b720
  Fix errors caused by HOL deleting various quotient_*Theory [Jul 31 03:35:47]
HOL:86b636c26a48c10a3fb34f0cb2523c4331e97bd2
  Fix faults in a93d43e; extend tests to riscv_stepLib [Aug 04 00:42:15]
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

Aug 08 12:14:48 Claimed job
Aug 08 12:14:53 Building HOL
Aug 08 12:29:30 Starting developers
Aug 08 12:29:33 Finished developers                                               2s 209MB
Aug 08 12:29:34 Starting developers/bin
Aug 08 12:29:47 Finished developers/bin                                          11s   1GB
Aug 08 12:29:48 Starting compiler/proofs
Aug 08 14:13:47 Finished compiler/proofs                                    1h43m58s  31GB
Aug 08 14:13:48 Starting compiler/bootstrap/translation
Aug 08 22:04:19 Finished compiler/bootstrap/translation                     7h50m29s  67GB
Aug 08 22:04:20 Starting semantics/ffi
Aug 08 22:04:28 Finished semantics/ffi                                            7s 693MB
Aug 08 22:04:29 Starting semantics
Aug 08 22:04:30 Finished semantics                                                0s  65MB
Aug 08 22:04:31 Starting semantics/proofs
Aug 08 22:05:10 Finished semantics/proofs                                        37s   2GB
Aug 08 22:05:10 Starting semantics/alt_semantics
Aug 08 22:05:49 Finished semantics/alt_semantics                                 37s   1GB
Aug 08 22:05:50 Starting semantics/alt_semantics/proofs
Aug 08 22:16:47 Finished semantics/alt_semantics/proofs                       10m56s   5GB
Aug 08 22:16:48 Starting basis/pure
Aug 08 22:16:50 Finished basis/pure                                               0s  72MB
Aug 08 22:16:50 Starting translator
Aug 08 22:18:33 Finished translator                                            1m42s   3GB
Aug 08 22:18:34 Starting compiler/parsing
Aug 08 22:18:36 Finished compiler/parsing                                         0s  69MB
Aug 08 22:18:36 Starting characteristic
Aug 08 22:18:38 Finished characteristic                                           0s  89MB
Aug 08 22:18:39 Starting translator/monadic
Aug 08 22:18:40 Finished translator/monadic                                       0s  92MB
Aug 08 22:18:41 Starting basis
Aug 08 22:22:33 Finished basis                                                 3m50s   5GB
Aug 08 22:22:34 Starting compiler/inference
Aug 08 22:22:35 Finished compiler/inference                                       0s  79MB
Aug 08 22:22:36 Starting compiler/backend/reg_alloc
Aug 08 22:22:37 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 08 22:22:38 Starting compiler/backend/gc
Aug 08 22:22:39 Finished compiler/backend/gc                                      0s 134MB
Aug 08 22:22:40 Starting compiler/backend
Aug 08 22:22:58 Finished compiler/backend                                        16s   1GB
Aug 08 22:22:59 Starting compiler/encoders/asm
Aug 08 22:23:00 Finished compiler/encoders/asm                                    0s  82MB
Aug 08 22:23:01 Starting compiler/encoders/x64
Aug 08 22:23:02 Finished compiler/encoders/x64                                    0s  89MB
Aug 08 22:23:03 Starting compiler/encoders/arm7
Aug 08 22:23:05 Finished compiler/encoders/arm7                                   0s  95MB
Aug 08 22:23:05 Starting compiler/encoders/arm8
Aug 08 22:23:07 Finished compiler/encoders/arm8                                   0s  88MB
Aug 08 22:23:08 Starting compiler/encoders/arm8_asl
Aug 09 00:44:49 Finished compiler/encoders/arm8_asl                         2h21m37s  50GB
Aug 09 00:44:50 Starting compiler/encoders/mips
Aug 09 00:44:51 Finished compiler/encoders/mips                                   0s  85MB
Aug 09 00:44:52 Starting compiler/encoders/riscv
Aug 09 00:44:54 Finished compiler/encoders/riscv                                  0s  90MB
Aug 09 00:44:55 Starting compiler/encoders/ag32
Aug 09 00:44:56 Finished compiler/encoders/ag32                                   0s  85MB
Aug 09 00:44:57 Starting compiler/backend/x64
Aug 09 00:44:59 Finished compiler/backend/x64                                     0s 129MB
Aug 09 00:45:00 Starting compiler/backend/arm7
Aug 09 00:45:01 Finished compiler/backend/arm7                                    0s 128MB
Aug 09 00:45:02 Starting compiler/backend/arm8
Aug 09 00:45:04 Finished compiler/backend/arm8                                    0s 128MB
Aug 09 00:45:05 Starting compiler/backend/mips
Aug 09 00:45:07 Finished compiler/backend/mips                                    0s 128MB
Aug 09 00:45:07 Starting compiler/backend/riscv
Aug 09 00:45:09 Finished compiler/backend/riscv                                   0s 128MB
Aug 09 00:45:10 Starting compiler/backend/ag32
Aug 09 00:46:30 Finished compiler/backend/ag32                                 1m18s   2GB
Aug 09 00:46:31 Starting compiler/parsing/proofs
Aug 09 00:46:32 Finished compiler/parsing/proofs                                  0s  75MB
Aug 09 00:46:33 Starting compiler/inference/proofs
Aug 09 00:46:35 Finished compiler/inference/proofs                                0s  83MB
Aug 09 00:46:36 Starting compiler/backend/semantics
Aug 09 00:48:02 Finished compiler/backend/semantics                            1m25s   2GB
Aug 09 00:48:03 Starting compiler/backend/reg_alloc/proofs
Aug 09 00:48:04 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Aug 09 00:48:05 Starting compiler/backend/proofs
Aug 09 00:49:07 Finished compiler/backend/proofs                               1m01s   4GB
Aug 09 00:49:08 Starting compiler/backend/serialiser
Aug 09 00:49:10 Finished compiler/backend/serialiser                              1s 178MB
Aug 09 00:49:11 Starting compiler/encoders/x64/proofs
Aug 09 00:58:33 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Aug 09 00:58:34 Starting compiler/encoders/arm7/proofs
Aug 09 01:11:57 Finished compiler/encoders/arm7/proofs                        13m22s  11GB
Aug 09 01:11:58 Starting compiler/encoders/arm8/proofs
Aug 09 01:18:23 Finished compiler/encoders/arm8/proofs                         6m23s   6GB
Aug 09 01:18:24 Starting compiler/encoders/arm8_asl/proofs
Aug 09 02:06:11 Finished compiler/encoders/arm8_asl/proofs                    47m45s  11GB
Aug 09 02:06:12 Starting compiler/encoders/mips/proofs
Aug 09 02:16:22 Finished compiler/encoders/mips/proofs                        10m09s   7GB
Aug 09 02:16:23 Starting compiler/encoders/riscv/proofs
Aug 09 02:24:54 Finished compiler/encoders/riscv/proofs                        8m30s   4GB
Aug 09 02:24:55 Starting compiler/encoders/ag32/proofs
Aug 09 02:27:22 Finished compiler/encoders/ag32/proofs                         2m26s   3GB
Aug 09 02:27:23 Starting compiler/backend/x64/proofs
Aug 09 02:28:04 Finished compiler/backend/x64/proofs                             40s   2GB
Aug 09 02:28:05 Starting compiler/backend/arm7/proofs
Aug 09 02:28:51 Finished compiler/backend/arm7/proofs                            44s   3GB
Aug 09 02:28:52 Starting compiler/backend/arm8/proofs
Aug 09 02:29:31 Finished compiler/backend/arm8/proofs                            38s   3GB
Aug 09 02:29:32 Starting compiler/backend/arm8_asl
Aug 09 02:29:58 Finished compiler/backend/arm8_asl                               25s   2GB
Aug 09 02:29:59 Starting compiler/backend/mips/proofs
Aug 09 02:30:43 Finished compiler/backend/mips/proofs                            43s   3GB
Aug 09 02:30:44 Starting compiler/backend/riscv/proofs
Aug 09 02:31:32 Finished compiler/backend/riscv/proofs                           46s   4GB
Aug 09 02:31:33 Starting compiler/backend/ag32/proofs
Aug 09 02:44:37 Finished compiler/backend/ag32/proofs                         13m03s   6GB
Aug 09 02:44:38 Starting candle/set-theory
Aug 09 02:45:22 Finished candle/set-theory                                       42s   1GB
Aug 09 02:45:22 Starting candle/syntax-lib
Aug 09 02:45:24 Finished candle/syntax-lib                                        0s  72MB
Aug 09 02:45:24 Starting candle/standard/syntax
Aug 09 02:45:41 Finished candle/standard/syntax                                  15s   1GB
Aug 09 02:45:42 Starting candle/standard/semantics
Aug 09 02:48:08 Finished candle/standard/semantics                             2m25s   2GB
Aug 09 02:48:08 Starting candle/standard/monadic
Aug 09 02:48:10 Finished candle/standard/monadic                                  0s 100MB
Aug 09 02:48:11 Starting candle/standard/ml_kernel
Aug 09 02:49:58 Finished candle/standard/ml_kernel                             1m46s   5GB
Aug 09 02:49:59 Starting candle/overloading/syntax
Aug 09 02:53:20 Finished candle/overloading/syntax                             3m20s   3GB
Aug 09 02:53:21 Starting candle/overloading/semantics
Aug 09 03:04:41 Finished candle/overloading/semantics                         11m19s   5GB
Aug 09 03:04:42 Starting candle/overloading/monadic
Aug 09 03:07:14 Finished candle/overloading/monadic                            2m31s   2GB
Aug 09 03:07:15 Starting candle/overloading/ml_kernel
Aug 09 03:14:46 Finished candle/overloading/ml_kernel                          7m29s   7GB
Aug 09 03:14:47 Starting candle/overloading/ml_checker
Aug 09 03:17:19 Finished candle/overloading/ml_checker                         2m31s   6GB
Aug 09 03:17:20 Starting candle/prover
Aug 09 03:28:38 Finished candle/prover                                        11m17s   5GB
Aug 09 03:28:39 Starting pancake
Aug 09 03:29:35 Finished pancake                                                 55s   1GB
Aug 09 03:29:36 Starting pancake/ffi
Aug 09 03:29:37 Finished pancake/ffi                                              0s  20MB
Aug 09 03:29:37 Starting pancake/semantics
Aug 09 03:31:55 Finished pancake/semantics                                     2m16s   2GB
Aug 09 03:31:56 Starting pancake/parser
Aug 09 03:32:20 Finished pancake/parser                                          23s   1GB
Aug 09 03:32:21 Starting pancake/proofs
Aug 09 04:01:49 Finished pancake/proofs                                       29m27s   8GB
Aug 09 04:01:50 Starting characteristic/examples
Aug 09 04:03:23 Finished characteristic/examples                               1m31s   5GB
Aug 09 04:03:23 Starting tutorial/solutions
Aug 09 04:18:58 Finished tutorial/solutions                                   15m33s  13GB
Aug 09 04:18:59 Starting translator/monadic/examples
Aug 09 04:22:43 Finished translator/monadic/examples                           3m42s   5GB
Aug 09 04:22:44 Starting examples
Aug 09 04:37:19 Finished examples                                             14m33s   7GB
Aug 09 04:37:20 Starting examples/compilation/x64
Aug 09 06:34:08 Finished examples/compilation/x64                           1h56m45s  34GB
Aug 09 06:34:08 Starting examples/compilation/x64/proofs
Aug 09 06:37:52 Finished examples/compilation/x64/proofs                       3m42s   6GB
Aug 09 06:37:52 Starting examples/compilation/ag32
Aug 09 07:07:46 Finished examples/compilation/ag32                            29m52s  12GB
Aug 09 07:07:46 Starting examples/compilation/ag32/proofs
Aug 09 07:09:10 Finished examples/compilation/ag32/proofs                      1m22s   7GB
Aug 09 07:09:10 Starting examples/compilation/to_word
Aug 09 07:13:00 Finished examples/compilation/to_word                          3m48s  12GB
Aug 09 07:13:01 Starting examples/lpr_checker
Aug 09 07:14:15 Finished examples/lpr_checker                                  1m13s   2GB
Aug 09 07:14:16 Starting examples/lpr_checker/array
Aug 09 07:48:48 Finished examples/lpr_checker/array                           34m31s   9GB
Aug 09 07:48:49 Starting examples/lpr_checker/array/compilation
Aug 09 08:23:17 Finished examples/lpr_checker/array/compilation               34m27s  60GB
Aug 09 08:23:18 Starting examples/lpr_checker/array/compilation/proofs
Aug 09 08:25:10 Finished examples/lpr_checker/array/compilation/proofs         1m51s   9GB
Aug 09 08:25:11 Starting examples/opentheory
Aug 09 08:35:49 Finished examples/opentheory                                  10m37s   8GB
Aug 09 08:35:50 Starting examples/opentheory
Aug 09 08:35:52 Finished examples/opentheory                                      0s 132MB
Aug 09 08:35:53 Starting examples/opentheory/compilation
Aug 09 09:13:08 Finished examples/opentheory/compilation                      37m12s  70GB
Aug 09 09:13:09 Starting examples/opentheory/compilation/proofs
Aug 09 09:14:34 Finished examples/opentheory/compilation/proofs                1m23s   6GB
Aug 09 09:14:35 Starting examples/opentheory/compilation/ag32
Aug 09 09:47:07 Finished examples/opentheory/compilation/ag32                 32m30s  61GB
Aug 09 09:47:07 Starting examples/opentheory/compilation/ag32/proofs
Aug 09 09:49:23 Finished examples/opentheory/compilation/ag32/proofs           2m15s  11GB
Aug 09 09:49:24 Starting examples/sat_encodings
Aug 09 09:52:03 Finished examples/sat_encodings                                2m37s   1GB
Aug 09 09:52:04 Starting examples/sat_encodings/case_studies
Aug 09 09:54:00 Finished examples/sat_encodings/case_studies                   1m55s   2GB
Aug 09 09:54:01 Starting examples/sat_encodings/translation
Aug 09 10:00:05 Finished examples/sat_encodings/translation                    6m02s   7GB
Aug 09 10:00:06 Starting examples/sat_encodings/translation/compilation
Aug 09 10:34:24 Finished examples/sat_encodings/translation/compilation       34m15s  36GB
Aug 09 10:34:24 Starting examples/deflate
Aug 09 10:35:37 Finished examples/deflate                                      1m11s   1GB
Aug 09 10:35:38 Starting examples/deflate/translation
Aug 09 10:37:14 Finished examples/deflate/translation                          1m34s   7GB
Aug 09 10:37:14 Starting examples/deflate/translation/compilation
Aug 09 10:53:48 Finished examples/deflate/translation/compilation             16m33s  15GB
Aug 09 10:53:49 Starting examples/vipr
Aug 09 10:57:49 Finished examples/vipr                                         3m58s   5GB
Aug 09 10:57:50 Starting examples/vipr/compilation
Aug 09 11:17:32 Finished examples/vipr/compilation                            19m41s  31GB
Aug 09 11:17:33 Starting translator/okasaki-examples
Aug 09 11:22:31 Finished translator/okasaki-examples                           4m57s   4GB
Aug 09 11:22:31 Starting translator/other-examples
Aug 09 11:26:08 Finished translator/other-examples                             3m35s   3GB
Aug 09 11:26:09 Starting compiler/parsing/tests
Aug 09 11:26:42 Finished compiler/parsing/tests                                  32s   1GB
Aug 09 11:26:43 Starting compiler/inference/tests
Aug 09 11:34:07 Finished compiler/inference/tests                              7m23s   6GB
Aug 09 11:34:08 Starting compiler/printing/test
Aug 09 11:37:40 Finished compiler/printing/test                                3m29s   6GB
Aug 09 11:37:41 Starting icing/flover
Aug 09 12:13:24 Finished icing/flover                                         35m42s   4GB
Aug 09 12:13:25 Starting icing/
Aug 09 13:09:01 Finished icing/                                               55m29s  22GB
Aug 09 13:09:01 Starting icing/examples
Aug 09 13:10:41 Finished icing/examples                                        1m38s   8GB
Aug 09 13:10:42 Starting compiler/repl
Aug 09 13:19:25 Finished compiler/repl                                         8m41s  10GB
Aug 09 13:19:26 Starting unverified/sexpr-bootstrap/x64/64
Aug 09 13:30:47 Finished unverified/sexpr-bootstrap/x64/64                    10m51s  16GB
Aug 09 13:30:48 Starting unverified/sexpr-bootstrap/x64/32
Aug 09 13:40:05 Finished unverified/sexpr-bootstrap/x64/32                     9m00s  12GB
Aug 09 13:40:06 Starting compiler/benchmarks
Aug 09 13:40:51 Finished compiler/benchmarks                                     43s 713MB
Aug 09 13:40:52 Starting compiler/bootstrap/compilation/x64/64
Aug 10 04:07:47 Finished compiler/bootstrap/compilation/x64/64             14h26m42s 216GB
Aug 10 04:07:48 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 10 04:28:48 Finished compiler/bootstrap/compilation/x64/64/proofs         20m59s  45GB
Aug 10 04:28:49 Starting compiler/bootstrap/compilation/x64/32
Aug 10 11:27:02 Finished compiler/bootstrap/compilation/x64/32              6h57m56s 151GB
Aug 10 11:27:02 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 10 11:30:32 Finished compiler/bootstrap/compilation/x64/32/proofs          3m28s  19GB
Aug 10 11:30:33 Starting compiler/bootstrap/compilation/ag32/32
Aug 10 18:59:41 Finished compiler/bootstrap/compilation/ag32/32             7h29m06s 176GB
Aug 10 18:59:42 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 10 19:07:15 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m32s  48GB
Aug 10 19:07:16 SUCCESS