Job 2313

CakeML:2dfec7f3c046be832517dafc6084be45d55e7082
  Merge pull request #983 from CakeML/fromsexpfix [Feb 29 22:18:07]
HOL:525694a1f1c7016dea954894bea6e6e396f7d6b3
  HolSmt: add unit tests for circular definitions [Feb 21 23:04:33]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Feb 29 22:22:50 Claimed job
Feb 29 22:22:52 Reusing HOL
Feb 29 22:23:33 Starting developers
Feb 29 22:23:38 Finished developers                                               5s 118MB
Feb 29 22:23:38 Starting developers/bin
Feb 29 22:23:46 Finished developers/bin                                           8s   1GB
Feb 29 22:23:46 Starting compiler/proofs
Mar 01 00:13:56 Finished compiler/proofs                                    1h50m09s  23GB
Mar 01 00:13:56 Starting compiler/bootstrap/translation
Mar 01 09:06:42 Finished compiler/bootstrap/translation                     8h52m46s  48GB
Mar 01 09:06:42 Starting semantics/ffi
Mar 01 09:06:48 Finished semantics/ffi                                            5s 214MB
Mar 01 09:06:48 Starting semantics
Mar 01 09:06:50 Finished semantics                                                1s  19MB
Mar 01 09:06:50 Starting semantics/proofs
Mar 01 09:07:24 Finished semantics/proofs                                        34s   1GB
Mar 01 09:07:24 Starting semantics/alt_semantics
Mar 01 09:07:56 Finished semantics/alt_semantics                                 31s 672MB
Mar 01 09:07:57 Starting semantics/alt_semantics/proofs
Mar 01 09:19:57 Finished semantics/alt_semantics/proofs                       12m00s   1GB
Mar 01 09:19:57 Starting basis/pure
Mar 01 09:19:59 Finished basis/pure                                               1s  19MB
Mar 01 09:19:59 Starting translator
Mar 01 09:21:50 Finished translator                                            1m50s   1GB
Mar 01 09:21:50 Starting compiler/parsing
Mar 01 09:21:51 Finished compiler/parsing                                         1s  19MB
Mar 01 09:21:51 Starting characteristic
Mar 01 09:21:53 Finished characteristic                                           1s  22MB
Mar 01 09:21:54 Starting translator/monadic
Mar 01 09:21:55 Finished translator/monadic                                       1s  25MB
Mar 01 09:21:56 Starting basis
Mar 01 09:25:37 Finished basis                                                 3m41s   3GB
Mar 01 09:25:37 Starting compiler/inference
Mar 01 09:25:39 Finished compiler/inference                                       1s  22MB
Mar 01 09:25:39 Starting compiler/backend/reg_alloc
Mar 01 09:25:41 Finished compiler/backend/reg_alloc                               1s  21MB
Mar 01 09:25:41 Starting compiler/backend/gc
Mar 01 09:25:43 Finished compiler/backend/gc                                      2s  31MB
Mar 01 09:25:43 Starting compiler/backend
Mar 01 09:25:56 Finished compiler/backend                                        12s 822MB
Mar 01 09:25:56 Starting compiler/encoders/asm
Mar 01 09:25:58 Finished compiler/encoders/asm                                    1s  23MB
Mar 01 09:25:58 Starting compiler/encoders/x64
Mar 01 09:26:00 Finished compiler/encoders/x64                                    1s  20MB
Mar 01 09:26:00 Starting compiler/encoders/arm7
Mar 01 09:26:02 Finished compiler/encoders/arm7                                   1s  25MB
Mar 01 09:26:02 Starting compiler/encoders/arm8
Mar 01 09:26:04 Finished compiler/encoders/arm8                                   1s  21MB
Mar 01 09:26:04 Starting compiler/encoders/arm8_asl
Mar 01 09:29:19 Finished compiler/encoders/arm8_asl                            3m15s   1GB
Mar 01 09:29:19 Starting compiler/encoders/mips
Mar 01 09:29:21 Finished compiler/encoders/mips                                   1s  23MB
Mar 01 09:29:21 Starting compiler/encoders/riscv
Mar 01 09:29:23 Finished compiler/encoders/riscv                                  1s  21MB
Mar 01 09:29:23 Starting compiler/encoders/ag32
Mar 01 09:29:25 Finished compiler/encoders/ag32                                   1s  24MB
Mar 01 09:29:25 Starting compiler/backend/x64
Mar 01 09:29:27 Finished compiler/backend/x64                                     2s  32MB
Mar 01 09:29:27 Starting compiler/backend/arm7
Mar 01 09:29:30 Finished compiler/backend/arm7                                    2s  22MB
Mar 01 09:29:30 Starting compiler/backend/arm8
Mar 01 09:29:32 Finished compiler/backend/arm8                                    2s  23MB
Mar 01 09:29:32 Starting compiler/backend/mips
Mar 01 09:29:34 Finished compiler/backend/mips                                    2s  29MB
Mar 01 09:29:34 Starting compiler/backend/riscv
Mar 01 09:29:37 Finished compiler/backend/riscv                                   2s  25MB
Mar 01 09:29:37 Starting compiler/backend/ag32
Mar 01 09:31:01 Finished compiler/backend/ag32                                 1m23s   1GB
Mar 01 09:31:01 Starting compiler/parsing/proofs
Mar 01 09:31:02 Finished compiler/parsing/proofs                                  1s  19MB
Mar 01 09:31:03 Starting compiler/inference/proofs
Mar 01 09:31:04 Finished compiler/inference/proofs                                1s  25MB
Mar 01 09:31:04 Starting compiler/backend/semantics
Mar 01 09:32:20 Finished compiler/backend/semantics                            1m15s   1GB
Mar 01 09:32:20 Starting compiler/backend/reg_alloc/proofs
Mar 01 09:32:22 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Mar 01 09:32:22 Starting compiler/backend/proofs
Mar 01 09:33:20 Finished compiler/backend/proofs                                 57s   2GB
Mar 01 09:33:20 Starting compiler/backend/serialiser
Mar 01 09:33:23 Finished compiler/backend/serialiser                              2s  29MB
Mar 01 09:33:23 Starting compiler/encoders/x64/proofs
Mar 01 09:43:13 Finished compiler/encoders/x64/proofs                          9m50s   6GB
Mar 01 09:43:13 Starting compiler/encoders/arm7/proofs
Mar 01 09:56:57 Finished compiler/encoders/arm7/proofs                        13m43s   8GB
Mar 01 09:56:57 Starting compiler/encoders/arm8/proofs
Mar 01 10:03:53 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Mar 01 10:03:53 Starting compiler/encoders/arm8_asl/proofs
Mar 01 10:19:30 Finished compiler/encoders/arm8_asl/proofs                    15m36s   2GB
Mar 01 10:19:30 Starting compiler/encoders/mips/proofs
Mar 01 10:30:27 Finished compiler/encoders/mips/proofs                        10m56s   2GB
Mar 01 10:30:27 Starting compiler/encoders/riscv/proofs
Mar 01 10:39:29 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Mar 01 10:39:29 Starting compiler/encoders/ag32/proofs
Mar 01 10:42:03 Finished compiler/encoders/ag32/proofs                         2m33s 965MB
Mar 01 10:42:03 Starting compiler/backend/x64/proofs
Mar 01 10:42:33 Finished compiler/backend/x64/proofs                             30s   2GB
Mar 01 10:42:33 Starting compiler/backend/arm7/proofs
Mar 01 10:43:05 Finished compiler/backend/arm7/proofs                            31s   1GB
Mar 01 10:43:05 Starting compiler/backend/arm8/proofs
Mar 01 10:43:36 Finished compiler/backend/arm8/proofs                            30s   2GB
Mar 01 10:43:36 Starting compiler/backend/arm8_asl
Mar 01 10:44:02 Finished compiler/backend/arm8_asl                               25s   1GB
Mar 01 10:44:02 Starting compiler/backend/mips/proofs
Mar 01 10:44:34 Finished compiler/backend/mips/proofs                            31s   2GB
Mar 01 10:44:34 Starting compiler/backend/riscv/proofs
Mar 01 10:45:07 Finished compiler/backend/riscv/proofs                           32s   2GB
Mar 01 10:45:07 Starting compiler/backend/ag32/proofs
Mar 01 10:58:59 Finished compiler/backend/ag32/proofs                         13m51s   2GB
Mar 01 10:58:59 Starting candle/set-theory
Mar 01 10:59:38 Finished candle/set-theory                                       39s   1GB
Mar 01 10:59:38 Starting candle/syntax-lib
Mar 01 10:59:40 Finished candle/syntax-lib                                        1s  20MB
Mar 01 10:59:40 Starting candle/standard/syntax
Mar 01 10:59:51 Finished candle/standard/syntax                                  10s 768MB
Mar 01 10:59:51 Starting candle/standard/semantics
Mar 01 11:01:51 Finished candle/standard/semantics                             2m00s   1GB
Mar 01 11:01:51 Starting candle/standard/monadic
Mar 01 11:01:53 Finished candle/standard/monadic                                  1s  20MB
Mar 01 11:01:54 Starting candle/standard/ml_kernel
Mar 01 11:03:31 Finished candle/standard/ml_kernel                             1m37s   2GB
Mar 01 11:03:31 Starting candle/overloading/syntax
Mar 01 11:06:57 Finished candle/overloading/syntax                             3m25s   1GB
Mar 01 11:06:57 Starting candle/overloading/semantics
Mar 01 11:19:25 Finished candle/overloading/semantics                         12m28s   2GB
Mar 01 11:19:25 Starting candle/overloading/monadic
Mar 01 11:22:13 Finished candle/overloading/monadic                            2m47s   1GB
Mar 01 11:22:13 Starting candle/overloading/ml_kernel
Mar 01 11:30:11 Finished candle/overloading/ml_kernel                          7m58s   3GB
Mar 01 11:30:11 Starting candle/overloading/ml_checker
Mar 01 11:32:48 Finished candle/overloading/ml_checker                         2m36s   2GB
Mar 01 11:32:48 Starting candle/prover
Mar 01 11:42:56 Finished candle/prover                                        10m08s   2GB
Mar 01 11:42:56 Starting pancake
Mar 01 11:43:42 Finished pancake                                                 46s 868MB
Mar 01 11:43:42 Starting pancake/ffi
Mar 01 11:43:43 Finished pancake/ffi                                              0s  13MB
Mar 01 11:43:43 Starting pancake/semantics
Mar 01 11:46:10 Finished pancake/semantics                                     2m27s   1GB
Mar 01 11:46:10 Starting pancake/parser
Mar 01 11:46:33 Finished pancake/parser                                          22s 649MB
Mar 01 11:46:33 Starting pancake/proofs
Mar 01 12:20:09 Finished pancake/proofs                                       33m35s   6GB
Mar 01 12:20:09 Starting characteristic/examples
Mar 01 12:21:43 Finished characteristic/examples                               1m33s   2GB
Mar 01 12:21:43 Starting tutorial/solutions
Mar 01 12:36:41 Finished tutorial/solutions                                   14m57s  11GB
Mar 01 12:36:41 Starting translator/monadic/examples
Mar 01 12:40:46 Finished translator/monadic/examples                           4m05s   3GB
Mar 01 12:40:46 Starting examples
Mar 01 12:56:53 Finished examples                                             16m07s   4GB
Mar 01 12:56:53 Starting examples/compilation/x64
Mar 01 14:56:46 Finished examples/compilation/x64                           1h59m51s  19GB
Mar 01 14:56:46 Starting examples/compilation/x64/proofs
Mar 01 14:59:21 Finished examples/compilation/x64/proofs                       2m34s   4GB
Mar 01 14:59:21 Starting examples/compilation/ag32
Mar 01 15:30:09 Finished examples/compilation/ag32                            30m47s   7GB
Mar 01 15:30:09 Starting examples/compilation/ag32/proofs
Mar 01 15:31:11 Finished examples/compilation/ag32/proofs                      1m02s   5GB
Mar 01 15:31:11 Starting examples/compilation/to_word
Mar 01 15:34:34 Finished examples/compilation/to_word                          3m22s   6GB
Mar 01 15:34:34 Starting examples/lpr_checker
Mar 01 15:35:38 Finished examples/lpr_checker                                  1m04s   1GB
Mar 01 15:35:38 Starting examples/lpr_checker/array
Mar 01 16:06:47 Finished examples/lpr_checker/array                           31m08s   5GB
Mar 01 16:06:47 Starting examples/lpr_checker/array/compilation
Mar 01 16:59:43 Finished examples/lpr_checker/array/compilation               52m55s  32GB
Mar 01 16:59:43 Starting examples/lpr_checker/array/compilation/proofs
Mar 01 17:01:45 Finished examples/lpr_checker/array/compilation/proofs         2m01s   3GB
Mar 01 17:01:45 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 01 17:11:37 Finished examples/lpr_checker/array/compilation/proofsARM8     9m51s  25GB
Mar 01 17:11:37 Starting examples/xlrup_checker
Mar 01 17:12:35 Finished examples/xlrup_checker                                  57s   1GB
Mar 01 17:12:35 Starting examples/xlrup_checker/array
Mar 01 17:30:11 Finished examples/xlrup_checker/array                         17m35s   3GB
Mar 01 17:30:11 Starting examples/xlrup_checker/array/compilation
Mar 01 17:52:14 Finished examples/xlrup_checker/array/compilation             22m03s  16GB
Mar 01 17:52:14 Starting examples/xlrup_checker/array/compilation/proofs
Mar 01 17:53:16 Finished examples/xlrup_checker/array/compilation/proofs       1m01s   4GB
Mar 01 17:53:16 Starting examples/pseudo_bool
Mar 01 17:55:11 Finished examples/pseudo_bool                                  1m55s   1GB
Mar 01 17:55:12 Starting examples/pseudo_bool/cnf_encoding
Mar 01 17:55:38 Finished examples/pseudo_bool/cnf_encoding                       26s 600MB
Mar 01 17:55:38 Starting examples/pseudo_bool/graph_encoding
Mar 01 17:56:20 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Mar 01 17:56:20 Starting examples/pseudo_bool/array
Mar 01 19:03:56 Finished examples/pseudo_bool/array                         1h07m35s   8GB
Mar 01 19:03:56 Starting examples/pseudo_bool/array/compilation
Mar 02 02:25:33 Finished examples/pseudo_bool/array/compilation             7h21m37s  64GB
Mar 02 02:25:33 Starting examples/pseudo_bool/array/compilation/proofs
Mar 02 02:28:09 Finished examples/pseudo_bool/array/compilation/proofs         2m35s   6GB
Mar 02 02:28:09 Starting examples/opentheory
Mar 02 02:39:08 Finished examples/opentheory                                  10m58s   4GB
Mar 02 02:39:08 Starting examples/opentheory
Mar 02 02:39:10 Finished examples/opentheory                                      1s  24MB
Mar 02 02:39:10 Starting examples/opentheory/compilation
Mar 02 03:16:03 Finished examples/opentheory/compilation                      36m52s  33GB
Mar 02 03:16:03 Starting examples/opentheory/compilation/proofs
Mar 02 03:17:09 Finished examples/opentheory/compilation/proofs                1m05s   4GB
Mar 02 03:17:09 Starting examples/opentheory/compilation/ag32
Mar 02 03:50:42 Finished examples/opentheory/compilation/ag32                 33m33s  29GB
Mar 02 03:50:42 Starting examples/opentheory/compilation/ag32/proofs
Mar 02 03:52:37 Finished examples/opentheory/compilation/ag32/proofs           1m54s   7GB
Mar 02 03:52:37 Starting examples/sat_encodings
Mar 02 03:54:41 Finished examples/sat_encodings                                2m03s   1GB
Mar 02 03:54:41 Starting examples/sat_encodings/case_studies
Mar 02 03:56:25 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Mar 02 03:56:25 Starting examples/sat_encodings/translation
Mar 02 04:02:37 Finished examples/sat_encodings/translation                    6m11s   3GB
Mar 02 04:02:37 Starting examples/sat_encodings/translation/compilation
Mar 02 04:48:59 Finished examples/sat_encodings/translation/compilation       46m21s  20GB
Mar 02 04:48:59 Starting examples/deflate
Mar 02 04:50:01 Finished examples/deflate                                      1m01s 844MB
Mar 02 04:50:01 Starting examples/deflate/translation
Mar 02 04:51:44 Finished examples/deflate/translation                          1m42s   3GB
Mar 02 04:51:45 Starting examples/deflate/translation/compilation
Mar 02 05:12:00 Finished examples/deflate/translation/compilation             20m15s  15GB
Mar 02 05:12:00 Starting examples/vipr
Mar 02 05:16:07 Finished examples/vipr                                         4m06s   3GB
Mar 02 05:16:07 Starting examples/vipr/compilation
Mar 02 05:36:48 Finished examples/vipr/compilation                            20m41s  20GB
Mar 02 05:36:48 Starting translator/okasaki-examples
Mar 02 05:42:02 Finished translator/okasaki-examples                           5m13s   2GB
Mar 02 05:42:02 Starting translator/other-examples
Mar 02 05:45:37 Finished translator/other-examples                             3m35s   1GB
Mar 02 05:45:38 Starting compiler/parsing/tests
Mar 02 05:46:09 Finished compiler/parsing/tests                                  31s 832MB
Mar 02 05:46:10 Starting compiler/inference/tests
Mar 02 05:54:40 Finished compiler/inference/tests                              8m30s   5GB
Mar 02 05:54:40 Starting compiler/printing/test
Mar 02 05:58:33 Finished compiler/printing/test                                3m52s   3GB
Mar 02 05:58:33 Starting icing/flover
Mar 02 06:43:26 Finished icing/flover                                         44m52s   2GB
Mar 02 06:43:26 Starting icing/
Mar 02 07:38:28 Finished icing/                                               55m01s   7GB
Mar 02 07:38:28 Starting icing/examples
Mar 02 07:40:05 Finished icing/examples                                        1m36s   5GB
Mar 02 07:40:05 Starting compiler/repl
Mar 02 07:48:57 Finished compiler/repl                                         8m51s   6GB
Mar 02 07:48:57 Starting unverified/sexpr-bootstrap/x64/64
Mar 02 08:02:35 Finished unverified/sexpr-bootstrap/x64/64                    13m37s  16GB
Mar 02 08:02:35 Starting unverified/sexpr-bootstrap/x64/32
Mar 02 08:13:33 Finished unverified/sexpr-bootstrap/x64/32                    10m57s  12GB
Mar 02 08:13:33 Starting compiler/benchmarks
Mar 02 08:29:11 Finished compiler/benchmarks                                  15m37s   2GB
Mar 02 08:29:12 Starting compiler/bootstrap/compilation/x64/64
Mar 02 21:01:45 Finished compiler/bootstrap/compilation/x64/64             12h32m32s  64GB
Mar 02 21:01:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 02 21:24:22 Finished compiler/bootstrap/compilation/x64/64/proofs         22m36s  34GB
Mar 02 21:24:22 Starting compiler/bootstrap/compilation/x64/32
Mar 03 04:32:21 Finished compiler/bootstrap/compilation/x64/32              7h07m58s  64GB
Mar 03 04:32:21 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 03 04:35:47 Finished compiler/bootstrap/compilation/x64/32/proofs          3m25s  18GB
Mar 03 04:35:48 Starting compiler/bootstrap/compilation/ag32/32
Mar 03 11:54:58 Finished compiler/bootstrap/compilation/ag32/32             7h19m10s  64GB
Mar 03 11:54:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 03 12:02:01 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m02s  36GB
Mar 03 12:02:01 SUCCESS