Job 2516

CakeML:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
  Merge pull request #1033 from CakeML/fix-translator-pair-type [Aug 01 15:02:04]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
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-arm8-64.tar.gz
cake-x64-32.tar.gz

Aug 01 16:20:41 Claimed job
Aug 01 16:20:42 Reusing HOL
Aug 01 16:21:26 Starting developers
Aug 01 16:21:31 Finished developers                                               5s 163MB
Aug 01 16:21:31 Starting developers/bin
Aug 01 16:21:37 Finished developers/bin                                           5s   1GB
Aug 01 16:21:38 Starting compiler/proofs
Aug 01 18:25:26 Finished compiler/proofs                                    2h03m48s  20GB
Aug 01 18:25:26 Starting compiler/bootstrap/translation
Aug 02 02:58:22 Finished compiler/bootstrap/translation                     8h32m55s  56GB
Aug 02 02:58:22 Starting semantics/ffi
Aug 02 02:58:28 Finished semantics/ffi                                            6s 380MB
Aug 02 02:58:28 Starting semantics
Aug 02 02:58:30 Finished semantics                                                1s  20MB
Aug 02 02:58:30 Starting semantics/proofs
Aug 02 02:59:10 Finished semantics/proofs                                        39s 859MB
Aug 02 02:59:10 Starting semantics/alt_semantics
Aug 02 02:59:49 Finished semantics/alt_semantics                                 39s 690MB
Aug 02 02:59:50 Starting semantics/alt_semantics/proofs
Aug 02 03:13:50 Finished semantics/alt_semantics/proofs                       14m00s   2GB
Aug 02 03:13:50 Starting basis/pure
Aug 02 03:13:52 Finished basis/pure                                               1s  19MB
Aug 02 03:13:52 Starting translator
Aug 02 03:16:17 Finished translator                                            2m24s   2GB
Aug 02 03:16:17 Starting compiler/parsing
Aug 02 03:16:19 Finished compiler/parsing                                         1s  25MB
Aug 02 03:16:19 Starting characteristic
Aug 02 03:16:21 Finished characteristic                                           2s  22MB
Aug 02 03:16:21 Starting translator/monadic
Aug 02 03:16:23 Finished translator/monadic                                       1s  36MB
Aug 02 03:16:23 Starting basis
Aug 02 03:21:23 Finished basis                                                 4m59s   3GB
Aug 02 03:21:23 Starting compiler/inference
Aug 02 03:21:25 Finished compiler/inference                                       1s  23MB
Aug 02 03:21:25 Starting compiler/backend/reg_alloc
Aug 02 03:21:27 Finished compiler/backend/reg_alloc                               1s  19MB
Aug 02 03:21:27 Starting compiler/backend/gc
Aug 02 03:21:29 Finished compiler/backend/gc                                      2s  36MB
Aug 02 03:21:29 Starting compiler/backend
Aug 02 03:21:46 Finished compiler/backend                                        16s 745MB
Aug 02 03:21:46 Starting compiler/encoders/asm
Aug 02 03:21:48 Finished compiler/encoders/asm                                    1s  23MB
Aug 02 03:21:48 Starting compiler/encoders/x64
Aug 02 03:21:50 Finished compiler/encoders/x64                                    1s  23MB
Aug 02 03:21:50 Starting compiler/encoders/arm7
Aug 02 03:21:52 Finished compiler/encoders/arm7                                   1s  23MB
Aug 02 03:21:53 Starting compiler/encoders/arm8
Aug 02 03:21:55 Finished compiler/encoders/arm8                                   1s  24MB
Aug 02 03:21:55 Starting compiler/encoders/arm8_asl
Aug 02 06:04:54 Finished compiler/encoders/arm8_asl                         2h42m59s  33GB
Aug 02 06:04:54 Starting compiler/encoders/mips
Aug 02 06:04:56 Finished compiler/encoders/mips                                   1s  28MB
Aug 02 06:04:56 Starting compiler/encoders/riscv
Aug 02 06:04:58 Finished compiler/encoders/riscv                                  1s  21MB
Aug 02 06:04:59 Starting compiler/encoders/ag32
Aug 02 06:05:00 Finished compiler/encoders/ag32                                   1s  24MB
Aug 02 06:05:01 Starting compiler/backend/x64
Aug 02 06:05:03 Finished compiler/backend/x64                                     2s  27MB
Aug 02 06:05:03 Starting compiler/backend/arm7
Aug 02 06:05:05 Finished compiler/backend/arm7                                    2s  30MB
Aug 02 06:05:05 Starting compiler/backend/arm8
Aug 02 06:05:08 Finished compiler/backend/arm8                                    2s  26MB
Aug 02 06:05:08 Starting compiler/backend/mips
Aug 02 06:05:10 Finished compiler/backend/mips                                    2s  24MB
Aug 02 06:05:10 Starting compiler/backend/riscv
Aug 02 06:05:13 Finished compiler/backend/riscv                                   2s  22MB
Aug 02 06:05:13 Starting compiler/backend/ag32
Aug 02 06:06:42 Finished compiler/backend/ag32                                 1m28s   1GB
Aug 02 06:06:42 Starting compiler/parsing/proofs
Aug 02 06:06:43 Finished compiler/parsing/proofs                                  1s  21MB
Aug 02 06:06:44 Starting compiler/inference/proofs
Aug 02 06:06:46 Finished compiler/inference/proofs                                1s  22MB
Aug 02 06:06:46 Starting compiler/backend/semantics
Aug 02 06:10:41 Finished compiler/backend/semantics                            3m54s   1GB
Aug 02 06:10:41 Starting compiler/backend/reg_alloc/proofs
Aug 02 06:10:43 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Aug 02 06:10:43 Starting compiler/backend/proofs
Aug 02 06:11:46 Finished compiler/backend/proofs                               1m02s   3GB
Aug 02 06:11:46 Starting compiler/backend/serialiser
Aug 02 06:11:48 Finished compiler/backend/serialiser                              2s  32MB
Aug 02 06:11:48 Starting compiler/encoders/x64/proofs
Aug 02 06:21:38 Finished compiler/encoders/x64/proofs                          9m50s   7GB
Aug 02 06:21:39 Starting compiler/encoders/arm7/proofs
Aug 02 06:35:23 Finished compiler/encoders/arm7/proofs                        13m44s   3GB
Aug 02 06:35:23 Starting compiler/encoders/arm8/proofs
Aug 02 06:42:21 Finished compiler/encoders/arm8/proofs                         6m57s   2GB
Aug 02 06:42:21 Starting compiler/encoders/arm8_asl/proofs
Aug 02 07:34:26 Finished compiler/encoders/arm8_asl/proofs                    52m05s  10GB
Aug 02 07:34:26 Starting compiler/encoders/mips/proofs
Aug 02 07:45:05 Finished compiler/encoders/mips/proofs                        10m38s   3GB
Aug 02 07:45:05 Starting compiler/encoders/riscv/proofs
Aug 02 07:54:01 Finished compiler/encoders/riscv/proofs                        8m55s   1GB
Aug 02 07:54:01 Starting compiler/encoders/ag32/proofs
Aug 02 07:56:38 Finished compiler/encoders/ag32/proofs                         2m36s   1GB
Aug 02 07:56:38 Starting compiler/backend/x64/proofs
Aug 02 07:57:10 Finished compiler/backend/x64/proofs                             32s   2GB
Aug 02 07:57:10 Starting compiler/backend/arm7/proofs
Aug 02 07:57:45 Finished compiler/backend/arm7/proofs                            34s   1GB
Aug 02 07:57:45 Starting compiler/backend/arm8/proofs
Aug 02 07:58:18 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 02 07:58:18 Starting compiler/backend/arm8_asl
Aug 02 07:58:42 Finished compiler/backend/arm8_asl                               24s   2GB
Aug 02 07:58:42 Starting compiler/backend/mips/proofs
Aug 02 07:59:17 Finished compiler/backend/mips/proofs                            34s   2GB
Aug 02 07:59:17 Starting compiler/backend/riscv/proofs
Aug 02 07:59:55 Finished compiler/backend/riscv/proofs                           38s   2GB
Aug 02 07:59:55 Starting compiler/backend/ag32/proofs
Aug 02 08:14:41 Finished compiler/backend/ag32/proofs                         14m46s   2GB
Aug 02 08:14:41 Starting compiler/backend/cv_compute
Aug 02 08:16:05 Finished compiler/backend/cv_compute                           1m24s   2GB
Aug 02 08:16:06 Starting cv_translator
Aug 02 08:36:42 Finished cv_translator                                        20m36s   6GB
Aug 02 08:36:42 Starting candle/set-theory
Aug 02 08:37:25 Finished candle/set-theory                                       43s   1GB
Aug 02 08:37:26 Starting candle/syntax-lib
Aug 02 08:37:27 Finished candle/syntax-lib                                        1s  22MB
Aug 02 08:37:27 Starting candle/standard/syntax
Aug 02 08:37:40 Finished candle/standard/syntax                                  12s 822MB
Aug 02 08:37:40 Starting candle/standard/semantics
Aug 02 08:39:50 Finished candle/standard/semantics                             2m10s   1GB
Aug 02 08:39:51 Starting candle/standard/monadic
Aug 02 08:39:53 Finished candle/standard/monadic                                  1s  32MB
Aug 02 08:39:53 Starting candle/standard/ml_kernel
Aug 02 08:41:37 Finished candle/standard/ml_kernel                             1m44s   3GB
Aug 02 08:41:37 Starting candle/overloading/syntax
Aug 02 08:45:13 Finished candle/overloading/syntax                             3m35s   1GB
Aug 02 08:45:13 Starting candle/overloading/semantics
Aug 02 08:57:42 Finished candle/overloading/semantics                         12m29s   2GB
Aug 02 08:57:42 Starting candle/overloading/monadic
Aug 02 09:00:36 Finished candle/overloading/monadic                            2m53s   1GB
Aug 02 09:00:36 Starting candle/overloading/ml_kernel
Aug 02 09:08:36 Finished candle/overloading/ml_kernel                          8m00s   3GB
Aug 02 09:08:36 Starting candle/overloading/ml_checker
Aug 02 09:11:16 Finished candle/overloading/ml_checker                         2m39s   3GB
Aug 02 09:11:16 Starting candle/prover
Aug 02 09:21:27 Finished candle/prover                                        10m10s   3GB
Aug 02 09:21:27 Starting pancake
Aug 02 09:22:18 Finished pancake                                                 51s   1GB
Aug 02 09:22:18 Starting pancake/ffi
Aug 02 09:22:19 Finished pancake/ffi                                              0s  13MB
Aug 02 09:22:19 Starting pancake/semantics
Aug 02 09:25:16 Finished pancake/semantics                                     2m56s   1GB
Aug 02 09:25:16 Starting pancake/parser
Aug 02 09:25:48 Finished pancake/parser                                          31s   1GB
Aug 02 09:25:48 Starting pancake/proofs
Aug 02 10:00:50 Finished pancake/proofs                                       35m02s   6GB
Aug 02 10:00:51 Starting characteristic/examples
Aug 02 10:02:28 Finished characteristic/examples                               1m36s   4GB
Aug 02 10:02:28 Starting tutorial/solutions
Aug 02 10:05:05 Finished tutorial/solutions                                    2m37s   2GB
Aug 02 10:05:05 Starting translator/monadic/examples
Aug 02 10:09:20 Finished translator/monadic/examples                           4m14s   3GB
Aug 02 10:09:20 Starting examples
Aug 02 10:25:50 Finished examples                                             16m29s   4GB
Aug 02 10:25:50 Starting examples/compilation/x64
Aug 02 10:34:32 Finished examples/compilation/x64                              8m41s   5GB
Aug 02 10:34:32 Starting examples/compilation/x64/proofs
Aug 02 10:37:26 Finished examples/compilation/x64/proofs                       2m54s   5GB
Aug 02 10:37:26 Starting examples/compilation/ag32
Aug 02 10:39:36 Finished examples/compilation/ag32                             2m09s   2GB
Aug 02 10:39:36 Starting examples/compilation/ag32/proofs
Aug 02 10:40:46 Finished examples/compilation/ag32/proofs                      1m09s   5GB
Aug 02 10:40:46 Starting examples/compilation/to_word
Aug 02 10:44:21 Finished examples/compilation/to_word                          3m34s   4GB
Aug 02 10:44:21 Starting examples/lpr_checker
Aug 02 10:45:33 Finished examples/lpr_checker                                  1m11s   1GB
Aug 02 10:45:33 Starting examples/lpr_checker/array
Aug 02 11:15:58 Finished examples/lpr_checker/array                           30m25s   5GB
Aug 02 11:15:58 Starting examples/lpr_checker/array/compilation
Aug 02 11:18:42 Finished examples/lpr_checker/array/compilation                2m43s   7GB
Aug 02 11:18:42 Starting examples/lpr_checker/array/compilation/proofs
Aug 02 11:20:01 Finished examples/lpr_checker/array/compilation/proofs         1m18s   6GB
Aug 02 11:20:01 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 02 11:21:14 Finished examples/lpr_checker/array/compilation/proofsARM8     1m13s   6GB
Aug 02 11:21:14 Starting examples/xlrup_checker
Aug 02 11:22:16 Finished examples/xlrup_checker                                1m01s   1GB
Aug 02 11:22:16 Starting examples/xlrup_checker/array
Aug 02 11:38:14 Finished examples/xlrup_checker/array                         15m58s   4GB
Aug 02 11:38:15 Starting examples/xlrup_checker/array/compilation
Aug 02 11:39:36 Finished examples/xlrup_checker/array/compilation              1m21s   4GB
Aug 02 11:39:36 Starting examples/xlrup_checker/array/compilation/proofs
Aug 02 11:40:48 Finished examples/xlrup_checker/array/compilation/proofs       1m11s   4GB
Aug 02 11:40:48 Starting examples/pseudo_bool
Aug 02 11:42:53 Finished examples/pseudo_bool                                  2m05s   1GB
Aug 02 11:42:53 Starting examples/pseudo_bool/cnf_encoding
Aug 02 11:43:23 Finished examples/pseudo_bool/cnf_encoding                       29s 901MB
Aug 02 11:43:23 Starting examples/pseudo_bool/graph_encoding
Aug 02 11:44:11 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Aug 02 11:44:12 Starting examples/pseudo_bool/array
Aug 02 12:53:35 Finished examples/pseudo_bool/array                         1h09m23s   9GB
Aug 02 12:53:36 Starting examples/pseudo_bool/array/compilation
Aug 02 13:08:33 Finished examples/pseudo_bool/array/compilation               14m56s  24GB
Aug 02 13:08:33 Starting examples/pseudo_bool/array/compilation/proofs
Aug 02 13:11:28 Finished examples/pseudo_bool/array/compilation/proofs         2m55s   7GB
Aug 02 13:11:29 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 02 13:12:44 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m15s   6GB
Aug 02 13:12:44 Starting examples/opentheory
Aug 02 13:23:47 Finished examples/opentheory                                  11m02s   4GB
Aug 02 13:23:47 Starting examples/opentheory
Aug 02 13:23:49 Finished examples/opentheory                                      1s  28MB
Aug 02 13:23:49 Starting examples/opentheory/compilation
Aug 02 13:25:51 Finished examples/opentheory/compilation                       2m01s   6GB
Aug 02 13:25:51 Starting examples/opentheory/compilation/proofs
Aug 02 13:26:57 Finished examples/opentheory/compilation/proofs                1m06s   4GB
Aug 02 13:26:57 Starting examples/opentheory/compilation/ag32
Aug 02 13:28:58 Finished examples/opentheory/compilation/ag32                  1m59s   6GB
Aug 02 13:28:58 Starting examples/opentheory/compilation/ag32/proofs
Aug 02 13:30:39 Finished examples/opentheory/compilation/ag32/proofs           1m41s   7GB
Aug 02 13:30:40 Starting examples/sat_encodings
Aug 02 13:33:00 Finished examples/sat_encodings                                2m20s   1GB
Aug 02 13:33:00 Starting examples/sat_encodings/case_studies
Aug 02 13:34:55 Finished examples/sat_encodings/case_studies                   1m54s   1GB
Aug 02 13:34:55 Starting examples/sat_encodings/translation
Aug 02 13:41:29 Finished examples/sat_encodings/translation                    6m33s   4GB
Aug 02 13:41:29 Starting examples/sat_encodings/translation/compilation
Aug 02 13:43:51 Finished examples/sat_encodings/translation/compilation        2m21s   5GB
Aug 02 13:43:51 Starting examples/deflate
Aug 02 13:44:59 Finished examples/deflate                                      1m08s   1GB
Aug 02 13:45:00 Starting examples/deflate/translation
Aug 02 13:46:49 Finished examples/deflate/translation                          1m49s   3GB
Aug 02 13:46:50 Starting examples/deflate/translation/compilation
Aug 02 13:47:57 Finished examples/deflate/translation/compilation              1m07s   3GB
Aug 02 13:47:57 Starting examples/vipr
Aug 02 13:52:11 Finished examples/vipr                                         4m13s   3GB
Aug 02 13:52:11 Starting examples/vipr/compilation
Aug 02 13:53:28 Finished examples/vipr/compilation                             1m16s   4GB
Aug 02 13:53:28 Starting translator/okasaki-examples
Aug 02 13:58:44 Finished translator/okasaki-examples                           5m16s   3GB
Aug 02 13:58:44 Starting translator/other-examples
Aug 02 14:02:35 Finished translator/other-examples                             3m49s   1GB
Aug 02 14:02:35 Starting compiler/parsing/tests
Aug 02 14:03:07 Finished compiler/parsing/tests                                  32s 822MB
Aug 02 14:03:08 Starting compiler/inference/tests
Aug 02 14:03:40 Finished compiler/inference/tests                                32s   1GB
Aug 02 14:03:40 Starting compiler/printing/test
Aug 02 14:05:07 Finished compiler/printing/test                                1m26s   3GB
Aug 02 14:05:07 Starting icing/flover
Aug 02 14:52:39 Finished icing/flover                                         47m31s   2GB
Aug 02 14:52:39 Starting icing/
Aug 02 15:22:40 Finished icing/                                               30m01s   3GB
Aug 02 15:22:40 Starting icing/examples
Aug 02 15:24:26 Finished icing/examples                                        1m45s   4GB
Aug 02 15:24:26 Starting compiler/repl
Aug 02 15:33:30 Finished compiler/repl                                         9m04s   7GB
Aug 02 15:33:30 Starting unverified/sexpr-bootstrap/x64/64
Aug 02 15:48:50 Finished unverified/sexpr-bootstrap/x64/64                    15m18s  17GB
Aug 02 15:48:50 Starting unverified/sexpr-bootstrap/x64/32
Aug 02 16:00:40 Finished unverified/sexpr-bootstrap/x64/32                    11m49s  14GB
Aug 02 16:00:40 Starting compiler/benchmarks
Aug 02 16:16:19 Finished compiler/benchmarks                                  15m39s   2GB
Aug 02 16:16:19 Starting compiler/bootstrap/compilation/x64/64
Aug 02 16:52:53 Finished compiler/bootstrap/compilation/x64/64                36m33s  63GB
Aug 02 16:52:53 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 02 17:15:42 Finished compiler/bootstrap/compilation/x64/64/proofs         22m48s  40GB
Aug 02 17:15:42 Starting compiler/bootstrap/compilation/x64/32
Aug 02 17:52:40 Finished compiler/bootstrap/compilation/x64/32                36m57s  63GB
Aug 02 17:52:40 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 02 17:58:24 Finished compiler/bootstrap/compilation/x64/32/proofs          5m44s  18GB
Aug 02 17:58:24 Starting compiler/bootstrap/compilation/arm8/64
Aug 02 18:47:44 Finished compiler/bootstrap/compilation/arm8/64               49m18s  63GB
Aug 02 18:47:44 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 02 18:52:40 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m56s  25GB
Aug 02 18:52:40 Starting compiler/bootstrap/compilation/ag32/32
Aug 02 19:27:07 Finished compiler/bootstrap/compilation/ag32/32               34m26s  63GB
Aug 02 19:27:07 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 02 19:33:42 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m34s  20GB
Aug 02 19:33:42 SUCCESS