Job 2354

CakeML:62d6b6509f4f15779b7bcb31490eb4ac9333d41a
  Merge pull request #986 from ShunyaoLiang/scope [Mar 24 06:08:46]
HOL:671b4b712f9e860a558393b4b0c6a15e3a52a754
  Updated HOL Description with higher mathematics contents promoted to  [Mar 18 23:15:32]
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

Mar 24 06:09:15 Claimed job
Mar 24 06:09:21 Reusing HOL
Mar 24 06:10:02 Starting developers
Mar 24 06:10:08 Finished developers                                               5s  97MB
Mar 24 06:10:08 Starting developers/bin
Mar 24 06:10:14 Finished developers/bin                                           6s   1GB
Mar 24 06:10:14 Starting compiler/proofs
Mar 24 08:09:51 Finished compiler/proofs                                    1h59m36s  20GB
Mar 24 08:09:51 Starting compiler/bootstrap/translation
Mar 24 16:30:36 Finished compiler/bootstrap/translation                     8h20m45s  34GB
Mar 24 16:30:36 Starting semantics/ffi
Mar 24 16:30:43 Finished semantics/ffi                                            5s 216MB
Mar 24 16:30:43 Starting semantics
Mar 24 16:30:44 Finished semantics                                                1s  19MB
Mar 24 16:30:44 Starting semantics/proofs
Mar 24 16:31:17 Finished semantics/proofs                                        33s 728MB
Mar 24 16:31:18 Starting semantics/alt_semantics
Mar 24 16:31:49 Finished semantics/alt_semantics                                 31s 683MB
Mar 24 16:31:50 Starting semantics/alt_semantics/proofs
Mar 24 16:43:44 Finished semantics/alt_semantics/proofs                       11m54s   1GB
Mar 24 16:43:44 Starting basis/pure
Mar 24 16:43:46 Finished basis/pure                                               1s  22MB
Mar 24 16:43:46 Starting translator
Mar 24 16:45:36 Finished translator                                            1m50s   1GB
Mar 24 16:45:36 Starting compiler/parsing
Mar 24 16:45:38 Finished compiler/parsing                                         1s  18MB
Mar 24 16:45:38 Starting characteristic
Mar 24 16:45:40 Finished characteristic                                           1s  24MB
Mar 24 16:45:40 Starting translator/monadic
Mar 24 16:45:42 Finished translator/monadic                                       1s  24MB
Mar 24 16:45:42 Starting basis
Mar 24 16:49:22 Finished basis                                                 3m39s   3GB
Mar 24 16:49:22 Starting compiler/inference
Mar 24 16:49:23 Finished compiler/inference                                       1s  25MB
Mar 24 16:49:23 Starting compiler/backend/reg_alloc
Mar 24 16:49:25 Finished compiler/backend/reg_alloc                               1s  22MB
Mar 24 16:49:25 Starting compiler/backend/gc
Mar 24 16:49:27 Finished compiler/backend/gc                                      2s  31MB
Mar 24 16:49:28 Starting compiler/backend
Mar 24 16:49:40 Finished compiler/backend                                        12s 725MB
Mar 24 16:49:41 Starting compiler/encoders/asm
Mar 24 16:49:42 Finished compiler/encoders/asm                                    1s  25MB
Mar 24 16:49:42 Starting compiler/encoders/x64
Mar 24 16:49:44 Finished compiler/encoders/x64                                    1s  26MB
Mar 24 16:49:44 Starting compiler/encoders/arm7
Mar 24 16:49:46 Finished compiler/encoders/arm7                                   1s  26MB
Mar 24 16:49:46 Starting compiler/encoders/arm8
Mar 24 16:49:48 Finished compiler/encoders/arm8                                   1s  23MB
Mar 24 16:49:48 Starting compiler/encoders/arm8_asl
Mar 24 16:53:02 Finished compiler/encoders/arm8_asl                            3m13s   1GB
Mar 24 16:53:02 Starting compiler/encoders/mips
Mar 24 16:53:04 Finished compiler/encoders/mips                                   1s  21MB
Mar 24 16:53:04 Starting compiler/encoders/riscv
Mar 24 16:53:06 Finished compiler/encoders/riscv                                  1s  25MB
Mar 24 16:53:06 Starting compiler/encoders/ag32
Mar 24 16:53:08 Finished compiler/encoders/ag32                                   1s  26MB
Mar 24 16:53:08 Starting compiler/backend/x64
Mar 24 16:53:10 Finished compiler/backend/x64                                     2s  29MB
Mar 24 16:53:10 Starting compiler/backend/arm7
Mar 24 16:53:12 Finished compiler/backend/arm7                                    2s  22MB
Mar 24 16:53:12 Starting compiler/backend/arm8
Mar 24 16:53:15 Finished compiler/backend/arm8                                    2s  27MB
Mar 24 16:53:15 Starting compiler/backend/mips
Mar 24 16:53:17 Finished compiler/backend/mips                                    2s  24MB
Mar 24 16:53:17 Starting compiler/backend/riscv
Mar 24 16:53:19 Finished compiler/backend/riscv                                   2s  24MB
Mar 24 16:53:19 Starting compiler/backend/ag32
Mar 24 16:54:45 Finished compiler/backend/ag32                                 1m25s   1GB
Mar 24 16:54:45 Starting compiler/parsing/proofs
Mar 24 16:54:47 Finished compiler/parsing/proofs                                  1s  19MB
Mar 24 16:54:47 Starting compiler/inference/proofs
Mar 24 16:54:49 Finished compiler/inference/proofs                                1s  20MB
Mar 24 16:54:49 Starting compiler/backend/semantics
Mar 24 16:58:39 Finished compiler/backend/semantics                            3m50s   1GB
Mar 24 16:58:39 Starting compiler/backend/reg_alloc/proofs
Mar 24 16:58:41 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Mar 24 16:58:41 Starting compiler/backend/proofs
Mar 24 16:59:42 Finished compiler/backend/proofs                               1m00s   3GB
Mar 24 16:59:42 Starting compiler/backend/serialiser
Mar 24 16:59:45 Finished compiler/backend/serialiser                              2s  31MB
Mar 24 16:59:45 Starting compiler/encoders/x64/proofs
Mar 24 17:09:41 Finished compiler/encoders/x64/proofs                          9m56s   4GB
Mar 24 17:09:41 Starting compiler/encoders/arm7/proofs
Mar 24 17:23:22 Finished compiler/encoders/arm7/proofs                        13m40s   3GB
Mar 24 17:23:22 Starting compiler/encoders/arm8/proofs
Mar 24 17:30:24 Finished compiler/encoders/arm8/proofs                         7m02s   1GB
Mar 24 17:30:25 Starting compiler/encoders/arm8_asl/proofs
Mar 24 17:46:12 Finished compiler/encoders/arm8_asl/proofs                    15m47s   2GB
Mar 24 17:46:12 Starting compiler/encoders/mips/proofs
Mar 24 17:56:57 Finished compiler/encoders/mips/proofs                        10m45s   2GB
Mar 24 17:56:58 Starting compiler/encoders/riscv/proofs
Mar 24 18:05:48 Finished compiler/encoders/riscv/proofs                        8m50s   2GB
Mar 24 18:05:48 Starting compiler/encoders/ag32/proofs
Mar 24 18:08:20 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Mar 24 18:08:20 Starting compiler/backend/x64/proofs
Mar 24 18:08:52 Finished compiler/backend/x64/proofs                             31s   2GB
Mar 24 18:08:52 Starting compiler/backend/arm7/proofs
Mar 24 18:09:24 Finished compiler/backend/arm7/proofs                            32s   1GB
Mar 24 18:09:24 Starting compiler/backend/arm8/proofs
Mar 24 18:09:54 Finished compiler/backend/arm8/proofs                            30s   1GB
Mar 24 18:09:54 Starting compiler/backend/arm8_asl
Mar 24 18:10:20 Finished compiler/backend/arm8_asl                               25s   2GB
Mar 24 18:10:20 Starting compiler/backend/mips/proofs
Mar 24 18:10:53 Finished compiler/backend/mips/proofs                            32s   2GB
Mar 24 18:10:53 Starting compiler/backend/riscv/proofs
Mar 24 18:11:29 Finished compiler/backend/riscv/proofs                           35s   2GB
Mar 24 18:11:29 Starting compiler/backend/ag32/proofs
Mar 24 18:26:01 Finished compiler/backend/ag32/proofs                         14m32s   2GB
Mar 24 18:26:02 Starting candle/set-theory
Mar 24 18:26:41 Finished candle/set-theory                                       39s   1GB
Mar 24 18:26:41 Starting candle/syntax-lib
Mar 24 18:26:43 Finished candle/syntax-lib                                        1s  19MB
Mar 24 18:26:43 Starting candle/standard/syntax
Mar 24 18:26:54 Finished candle/standard/syntax                                  11s 679MB
Mar 24 18:26:54 Starting candle/standard/semantics
Mar 24 18:28:54 Finished candle/standard/semantics                             1m59s   2GB
Mar 24 18:28:54 Starting candle/standard/monadic
Mar 24 18:28:56 Finished candle/standard/monadic                                  1s  20MB
Mar 24 18:28:56 Starting candle/standard/ml_kernel
Mar 24 18:30:40 Finished candle/standard/ml_kernel                             1m43s   3GB
Mar 24 18:30:40 Starting candle/overloading/syntax
Mar 24 18:34:02 Finished candle/overloading/syntax                             3m22s   1GB
Mar 24 18:34:02 Starting candle/overloading/semantics
Mar 24 18:46:22 Finished candle/overloading/semantics                         12m20s   3GB
Mar 24 18:46:23 Starting candle/overloading/monadic
Mar 24 18:49:09 Finished candle/overloading/monadic                            2m45s   1GB
Mar 24 18:49:09 Starting candle/overloading/ml_kernel
Mar 24 18:57:10 Finished candle/overloading/ml_kernel                          8m00s   3GB
Mar 24 18:57:10 Starting candle/overloading/ml_checker
Mar 24 18:59:55 Finished candle/overloading/ml_checker                         2m45s   2GB
Mar 24 18:59:55 Starting candle/prover
Mar 24 19:09:57 Finished candle/prover                                        10m02s   4GB
Mar 24 19:09:57 Starting pancake
Mar 24 19:10:43 Finished pancake                                                 45s 960MB
Mar 24 19:10:43 Starting pancake/ffi
Mar 24 19:10:43 Finished pancake/ffi                                              0s  13MB
Mar 24 19:10:43 Starting pancake/semantics
Mar 24 19:13:25 Finished pancake/semantics                                     2m41s   1GB
Mar 24 19:13:25 Starting pancake/parser
Mar 24 19:13:49 Finished pancake/parser                                          23s   1GB
Mar 24 19:13:49 Starting pancake/proofs
Mar 24 19:48:34 Finished pancake/proofs                                       34m44s   5GB
Mar 24 19:48:34 Starting characteristic/examples
Mar 24 19:50:26 Finished characteristic/examples                               1m51s   3GB
Mar 24 19:50:26 Starting tutorial/solutions
Mar 24 20:06:02 Finished tutorial/solutions                                   15m35s   9GB
Mar 24 20:06:02 Starting translator/monadic/examples
Mar 24 20:10:11 Finished translator/monadic/examples                           4m09s   3GB
Mar 24 20:10:12 Starting examples
Mar 24 20:26:25 Finished examples                                             16m13s   6GB
Mar 24 20:26:25 Starting examples/compilation/x64
Mar 24 22:28:17 Finished examples/compilation/x64                           2h01m51s  17GB
Mar 24 22:28:17 Starting examples/compilation/x64/proofs
Mar 24 22:30:57 Finished examples/compilation/x64/proofs                       2m39s   4GB
Mar 24 22:30:57 Starting examples/compilation/ag32
Mar 24 23:01:50 Finished examples/compilation/ag32                            30m52s   6GB
Mar 24 23:01:50 Starting examples/compilation/ag32/proofs
Mar 24 23:02:52 Finished examples/compilation/ag32/proofs                      1m02s   4GB
Mar 24 23:02:52 Starting examples/compilation/to_word
Mar 24 23:06:17 Finished examples/compilation/to_word                          3m24s   6GB
Mar 24 23:06:17 Starting examples/lpr_checker
Mar 24 23:07:22 Finished examples/lpr_checker                                  1m04s   1GB
Mar 24 23:07:22 Starting examples/lpr_checker/array
Mar 24 23:40:04 Finished examples/lpr_checker/array                           32m41s   6GB
Mar 24 23:40:04 Starting examples/lpr_checker/array/compilation
Mar 25 00:33:21 Finished examples/lpr_checker/array/compilation               53m17s  22GB
Mar 25 00:33:21 Starting examples/lpr_checker/array/compilation/proofs
Mar 25 00:35:07 Finished examples/lpr_checker/array/compilation/proofs         1m45s   3GB
Mar 25 00:35:07 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 25 00:40:59 Finished examples/lpr_checker/array/compilation/proofsARM8     5m52s  20GB
Mar 25 00:40:59 Starting examples/xlrup_checker
Mar 25 00:41:58 Finished examples/xlrup_checker                                  58s   1GB
Mar 25 00:41:58 Starting examples/xlrup_checker/array
Mar 25 00:59:05 Finished examples/xlrup_checker/array                         17m07s   4GB
Mar 25 00:59:05 Starting examples/xlrup_checker/array/compilation
Mar 25 01:21:43 Finished examples/xlrup_checker/array/compilation             22m37s  19GB
Mar 25 01:21:43 Starting examples/xlrup_checker/array/compilation/proofs
Mar 25 01:22:44 Finished examples/xlrup_checker/array/compilation/proofs       1m00s   4GB
Mar 25 01:22:44 Starting examples/pseudo_bool
Mar 25 01:24:42 Finished examples/pseudo_bool                                  1m58s   1GB
Mar 25 01:24:42 Starting examples/pseudo_bool/cnf_encoding
Mar 25 01:25:09 Finished examples/pseudo_bool/cnf_encoding                       26s 638MB
Mar 25 01:25:09 Starting examples/pseudo_bool/graph_encoding
Mar 25 01:25:52 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Mar 25 01:25:52 Starting examples/pseudo_bool/array
Mar 25 02:41:48 Finished examples/pseudo_bool/array                         1h15m56s   8GB
Mar 25 02:41:49 Starting examples/pseudo_bool/array/compilation
Mar 25 10:26:56 Finished examples/pseudo_bool/array/compilation             7h45m07s  61GB
Mar 25 10:26:56 Starting examples/pseudo_bool/array/compilation/proofs
Mar 25 10:29:57 Finished examples/pseudo_bool/array/compilation/proofs         3m00s   6GB
Mar 25 10:29:57 Starting examples/opentheory
Mar 25 10:41:03 Finished examples/opentheory                                  11m05s   4GB
Mar 25 10:41:03 Starting examples/opentheory
Mar 25 10:41:05 Finished examples/opentheory                                      1s  22MB
Mar 25 10:41:05 Starting examples/opentheory/compilation
Mar 25 11:19:11 Finished examples/opentheory/compilation                      38m06s  27GB
Mar 25 11:19:12 Starting examples/opentheory/compilation/proofs
Mar 25 11:20:18 Finished examples/opentheory/compilation/proofs                1m05s   4GB
Mar 25 11:20:18 Starting examples/opentheory/compilation/ag32
Mar 25 11:54:20 Finished examples/opentheory/compilation/ag32                 34m01s  30GB
Mar 25 11:54:20 Starting examples/opentheory/compilation/ag32/proofs
Mar 25 11:56:12 Finished examples/opentheory/compilation/ag32/proofs           1m52s   5GB
Mar 25 11:56:12 Starting examples/sat_encodings
Mar 25 11:58:18 Finished examples/sat_encodings                                2m05s 900MB
Mar 25 11:58:18 Starting examples/sat_encodings/case_studies
Mar 25 12:00:04 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Mar 25 12:00:04 Starting examples/sat_encodings/translation
Mar 25 12:06:15 Finished examples/sat_encodings/translation                    6m11s   3GB
Mar 25 12:06:15 Starting examples/sat_encodings/translation/compilation
Mar 25 12:54:17 Finished examples/sat_encodings/translation/compilation       48m01s  20GB
Mar 25 12:54:17 Starting examples/deflate
Mar 25 12:55:18 Finished examples/deflate                                      1m00s 982MB
Mar 25 12:55:18 Starting examples/deflate/translation
Mar 25 12:57:13 Finished examples/deflate/translation                          1m55s   3GB
Mar 25 12:57:13 Starting examples/deflate/translation/compilation
Mar 25 13:17:35 Finished examples/deflate/translation/compilation             20m21s  13GB
Mar 25 13:17:35 Starting examples/vipr
Mar 25 13:21:41 Finished examples/vipr                                         4m05s   3GB
Mar 25 13:21:41 Starting examples/vipr/compilation
Mar 25 13:42:55 Finished examples/vipr/compilation                            21m13s  16GB
Mar 25 13:42:55 Starting translator/okasaki-examples
Mar 25 13:48:06 Finished translator/okasaki-examples                           5m11s   2GB
Mar 25 13:48:06 Starting translator/other-examples
Mar 25 13:49:00 Finished translator/other-examples                               54s   1GB
Mar 25 13:49:00 Starting compiler/parsing/tests
Mar 25 13:49:33 Finished compiler/parsing/tests                                  32s 800MB
Mar 25 13:49:33 Starting compiler/inference/tests
Mar 25 13:58:05 Finished compiler/inference/tests                              8m31s   4GB
Mar 25 13:58:05 Starting compiler/printing/test
Mar 25 14:02:02 Finished compiler/printing/test                                3m56s   3GB
Mar 25 14:02:02 Starting icing/flover
Mar 25 14:46:05 Finished icing/flover                                         44m03s   2GB
Mar 25 14:46:05 Starting icing/
Mar 25 15:40:34 Finished icing/                                               54m28s   8GB
Mar 25 15:40:34 Starting icing/examples
Mar 25 15:42:09 Finished icing/examples                                        1m34s   4GB
Mar 25 15:42:09 Starting compiler/repl
Mar 25 15:50:55 Finished compiler/repl                                         8m46s   5GB
Mar 25 15:50:56 Starting unverified/sexpr-bootstrap/x64/64
Mar 25 16:04:33 Finished unverified/sexpr-bootstrap/x64/64                    13m36s  16GB
Mar 25 16:04:33 Starting unverified/sexpr-bootstrap/x64/32
Mar 25 16:15:53 Finished unverified/sexpr-bootstrap/x64/32                    11m19s  14GB
Mar 25 16:15:53 Starting compiler/benchmarks
Mar 25 16:31:30 Finished compiler/benchmarks                                  15m36s   2GB
Mar 25 16:31:30 Starting compiler/bootstrap/compilation/x64/64
Mar 26 04:50:04 Finished compiler/bootstrap/compilation/x64/64             12h18m34s  64GB
Mar 26 04:50:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 26 05:10:54 Finished compiler/bootstrap/compilation/x64/64/proofs         20m49s  31GB
Mar 26 05:10:54 Starting compiler/bootstrap/compilation/x64/32
Mar 26 12:32:52 Finished compiler/bootstrap/compilation/x64/32              7h21m57s  64GB
Mar 26 12:32:52 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 26 12:36:28 Finished compiler/bootstrap/compilation/x64/32/proofs          3m36s  18GB
Mar 26 12:36:29 Starting compiler/bootstrap/compilation/ag32/32
Mar 26 20:06:49 Finished compiler/bootstrap/compilation/ag32/32             7h30m19s  64GB
Mar 26 20:06:49 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 26 20:13:58 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m08s  40GB
Mar 26 20:13:58 SUCCESS