Job 2531

CakeML:61a425840bdc7fbd373ad4d382f80f15b91ee5a0
  Fix up some syntactic proofs in pan_to_word [Aug 06 07:16:55]
#1031 (talsewell:pancake_mul_to_exp)
Merging into:6eebd384c0cb34314a58957d79a6489087db8721
  Add arm8 tar.gz to artefacts [Aug 03 14:16:31]
HOL:21b98f6d58ea9a62a56b99031851951d5e3d7efd
  Fix generalised quotation syntax to handle underscore and apostrophes [Aug 01 01:59:57]
Machine:pavlova

Aug 06 12:17:26 Claimed job
Aug 06 12:17:37 Building HOL
Aug 06 12:31:51 Starting developers
Aug 06 12:31:54 Finished developers                                               2s 217MB
Aug 06 12:31:55 Starting developers/bin
Aug 06 12:32:05 Finished developers/bin                                           9s   1GB
Aug 06 12:32:06 Starting compiler/proofs
Aug 06 14:28:15 Finished compiler/proofs                                    1h56m07s  41GB
Aug 06 14:28:16 Starting compiler/bootstrap/translation
Aug 06 22:49:23 Finished compiler/bootstrap/translation                     8h21m05s  76GB
Aug 06 22:49:24 Starting semantics/ffi
Aug 06 22:49:33 Finished semantics/ffi                                            7s 656MB
Aug 06 22:49:33 Starting semantics
Aug 06 22:49:35 Finished semantics                                                0s  62MB
Aug 06 22:49:36 Starting semantics/proofs
Aug 06 22:50:12 Finished semantics/proofs                                        35s   1GB
Aug 06 22:50:13 Starting semantics/alt_semantics
Aug 06 22:50:55 Finished semantics/alt_semantics                                 40s   1GB
Aug 06 22:50:55 Starting semantics/alt_semantics/proofs
Aug 06 23:02:06 Finished semantics/alt_semantics/proofs                       11m09s   5GB
Aug 06 23:02:07 Starting basis/pure
Aug 06 23:02:08 Finished basis/pure                                               0s  71MB
Aug 06 23:02:09 Starting translator
Aug 06 23:03:59 Finished translator                                            1m49s   3GB
Aug 06 23:04:00 Starting compiler/parsing
Aug 06 23:04:01 Finished compiler/parsing                                         0s  73MB
Aug 06 23:04:02 Starting characteristic
Aug 06 23:04:04 Finished characteristic                                           0s  90MB
Aug 06 23:04:04 Starting translator/monadic
Aug 06 23:04:06 Finished translator/monadic                                       0s  94MB
Aug 06 23:04:07 Starting basis
Aug 06 23:07:43 Finished basis                                                 3m34s   5GB
Aug 06 23:07:44 Starting compiler/inference
Aug 06 23:07:45 Finished compiler/inference                                       0s  93MB
Aug 06 23:07:46 Starting compiler/backend/reg_alloc
Aug 06 23:07:47 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 06 23:07:48 Starting compiler/backend/gc
Aug 06 23:07:50 Finished compiler/backend/gc                                      0s 147MB
Aug 06 23:07:51 Starting compiler/backend
Aug 06 23:08:10 Finished compiler/backend                                        18s   1GB
Aug 06 23:08:11 Starting compiler/encoders/asm
Aug 06 23:08:13 Finished compiler/encoders/asm                                    0s  98MB
Aug 06 23:08:14 Starting compiler/encoders/x64
Aug 06 23:08:15 Finished compiler/encoders/x64                                    0s 103MB
Aug 06 23:08:16 Starting compiler/encoders/arm7
Aug 06 23:08:17 Finished compiler/encoders/arm7                                   0s 104MB
Aug 06 23:08:18 Starting compiler/encoders/arm8
Aug 06 23:08:20 Finished compiler/encoders/arm8                                   0s 100MB
Aug 06 23:08:21 Starting compiler/encoders/arm8_asl
Aug 07 01:34:45 Finished compiler/encoders/arm8_asl                         2h26m21s  44GB
Aug 07 01:34:46 Starting compiler/encoders/mips
Aug 07 01:34:47 Finished compiler/encoders/mips                                   0s 100MB
Aug 07 01:34:52 Starting compiler/encoders/riscv
Aug 07 01:34:54 Finished compiler/encoders/riscv                                  0s  95MB
Aug 07 01:34:55 Starting compiler/encoders/ag32
Aug 07 01:34:57 Finished compiler/encoders/ag32                                   0s  98MB
Aug 07 01:34:58 Starting compiler/backend/x64
Aug 07 01:35:00 Finished compiler/backend/x64                                     0s 145MB
Aug 07 01:35:01 Starting compiler/backend/arm7
Aug 07 01:35:03 Finished compiler/backend/arm7                                    0s 145MB
Aug 07 01:35:05 Starting compiler/backend/arm8
Aug 07 01:35:09 Finished compiler/backend/arm8                                    0s 139MB
Aug 07 01:35:11 Starting compiler/backend/mips
Aug 07 01:35:14 Finished compiler/backend/mips                                    0s 135MB
Aug 07 01:35:15 Starting compiler/backend/riscv
Aug 07 01:35:17 Finished compiler/backend/riscv                                   0s 134MB
Aug 07 01:35:18 Starting compiler/backend/ag32
Aug 07 01:36:41 Finished compiler/backend/ag32                                 1m20s   2GB
Aug 07 01:36:41 Starting compiler/parsing/proofs
Aug 07 01:36:43 Finished compiler/parsing/proofs                                  0s  75MB
Aug 07 01:36:44 Starting compiler/inference/proofs
Aug 07 01:36:46 Finished compiler/inference/proofs                                0s  92MB
Aug 07 01:36:48 Starting compiler/backend/semantics
Aug 07 01:40:36 Finished compiler/backend/semantics                            3m47s   3GB
Aug 07 01:40:37 Starting compiler/backend/reg_alloc/proofs
Aug 07 01:40:39 Finished compiler/backend/reg_alloc/proofs                        0s  98MB
Aug 07 01:40:41 Starting compiler/backend/proofs
Aug 07 01:41:46 Finished compiler/backend/proofs                               1m03s   2GB
Aug 07 01:41:47 Starting compiler/backend/serialiser
Aug 07 01:41:50 Finished compiler/backend/serialiser                              0s 141MB
Aug 07 01:41:51 Starting compiler/encoders/x64/proofs
Aug 07 01:51:32 Finished compiler/encoders/x64/proofs                          9m39s   6GB
Aug 07 01:51:33 Starting compiler/encoders/arm7/proofs
Aug 07 02:04:21 Finished compiler/encoders/arm7/proofs                        12m47s   5GB
Aug 07 02:04:22 Starting compiler/encoders/arm8/proofs
Aug 07 02:10:54 Finished compiler/encoders/arm8/proofs                         6m31s   5GB
Aug 07 02:10:55 Starting compiler/encoders/arm8_asl/proofs
Aug 07 02:58:53 Finished compiler/encoders/arm8_asl/proofs                    47m56s  11GB
Aug 07 02:58:53 Starting compiler/encoders/mips/proofs
Aug 07 03:09:03 Finished compiler/encoders/mips/proofs                        10m08s   7GB
Aug 07 03:09:03 Starting compiler/encoders/riscv/proofs
Aug 07 03:17:12 Finished compiler/encoders/riscv/proofs                        8m07s   4GB
Aug 07 03:17:13 Starting compiler/encoders/ag32/proofs
Aug 07 03:19:36 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
Aug 07 03:19:37 Starting compiler/backend/x64/proofs
Aug 07 03:20:20 Finished compiler/backend/x64/proofs                             42s   3GB
Aug 07 03:20:20 Starting compiler/backend/arm7/proofs
Aug 07 03:21:10 Finished compiler/backend/arm7/proofs                            48s   3GB
Aug 07 03:21:11 Starting compiler/backend/arm8/proofs
Aug 07 03:21:53 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 07 03:21:54 Starting compiler/backend/arm8_asl
Aug 07 03:22:24 Finished compiler/backend/arm8_asl                               28s   2GB
Aug 07 03:22:25 Starting compiler/backend/mips/proofs
Aug 07 03:23:10 Finished compiler/backend/mips/proofs                            44s   3GB
Aug 07 03:23:11 Starting compiler/backend/riscv/proofs
Aug 07 03:24:02 Finished compiler/backend/riscv/proofs                           50s   4GB
Aug 07 03:24:03 Starting compiler/backend/ag32/proofs
Aug 07 03:38:06 Finished compiler/backend/ag32/proofs                         14m01s   6GB
Aug 07 03:38:07 Starting compiler/backend/cv_compute
Aug 07 03:39:51 Finished compiler/backend/cv_compute                           1m43s   4GB
Aug 07 03:39:52 Starting cv_translator
Aug 07 03:59:00 Finished cv_translator                                        19m06s  12GB
Aug 07 03:59:01 Starting candle/set-theory
Aug 07 03:59:52 Finished candle/set-theory                                       50s   1GB
Aug 07 03:59:53 Starting candle/syntax-lib
Aug 07 03:59:54 Finished candle/syntax-lib                                        0s  74MB
Aug 07 03:59:55 Starting candle/standard/syntax
Aug 07 04:00:15 Finished candle/standard/syntax                                  18s   1GB
Aug 07 04:00:16 Starting candle/standard/semantics
Aug 07 04:02:53 Finished candle/standard/semantics                             2m36s   4GB
Aug 07 04:02:54 Starting candle/standard/monadic
Aug 07 04:02:56 Finished candle/standard/monadic                                  0s 108MB
Aug 07 04:02:56 Starting candle/standard/ml_kernel
Aug 07 04:04:50 Finished candle/standard/ml_kernel                             1m52s   5GB
Aug 07 04:04:51 Starting candle/overloading/syntax
Aug 07 04:08:27 Finished candle/overloading/syntax                             3m34s   2GB
Aug 07 04:08:28 Starting candle/overloading/semantics
Aug 07 04:19:47 Finished candle/overloading/semantics                         11m18s   4GB
Aug 07 04:19:48 Starting candle/overloading/monadic
Aug 07 04:22:28 Finished candle/overloading/monadic                            2m39s   2GB
Aug 07 04:22:29 Starting candle/overloading/ml_kernel
Aug 07 04:30:07 Finished candle/overloading/ml_kernel                          7m37s   6GB
Aug 07 04:30:08 Starting candle/overloading/ml_checker
Aug 07 04:32:43 Finished candle/overloading/ml_checker                         2m33s   6GB
Aug 07 04:32:44 Starting candle/prover
Aug 07 04:42:46 Finished candle/prover                                        10m01s   5GB
Aug 07 04:42:47 Starting pancake
Aug 07 04:43:55 Finished pancake                                               1m07s   1GB
Aug 07 04:43:56 Starting pancake/ffi
Aug 07 04:43:57 Finished pancake/ffi                                              0s  22MB
Aug 07 04:43:58 Starting pancake/semantics
Aug 07 04:46:45 Finished pancake/semantics                                     2m45s   3GB
Aug 07 04:46:46 Starting pancake/parser
Aug 07 04:47:21 Finished pancake/parser                                          34s   2GB
Aug 07 04:47:22 Starting pancake/proofs
Aug 07 05:18:25 Finished pancake/proofs                                       31m01s   8GB
Aug 07 05:18:26 Starting characteristic/examples
Aug 07 05:20:04 Finished characteristic/examples                               1m37s   6GB
Aug 07 05:20:05 Starting tutorial/solutions
Aug 07 07:40:39 Resuming tutorial/solutions
Aug 07 07:40:42 Finished tutorial/solutions                                       1s 270MB
Aug 07 07:40:43 Starting translator/monadic/examples
Aug 07 07:44:40 Finished translator/monadic/examples                           3m56s   5GB
Aug 07 07:44:40 Starting examples
Aug 07 07:59:55 Finished examples                                             15m13s   7GB
Aug 07 07:59:56 Starting examples/compilation/x64
Aug 07 08:09:19 Finished examples/compilation/x64                              9m22s   8GB
Aug 07 08:09:20 Starting examples/compilation/x64/proofs
Aug 07 08:14:03 Finished examples/compilation/x64/proofs                       4m42s   9GB
Aug 07 08:14:04 Starting examples/compilation/ag32
Aug 07 08:16:46 Finished examples/compilation/ag32                             2m40s   5GB
Aug 07 08:16:47 Starting examples/compilation/ag32/proofs
Aug 07 08:18:37 Finished examples/compilation/ag32/proofs                      1m48s  10GB
Aug 07 08:18:37 Starting examples/compilation/to_word
Aug 07 08:22:44 Finished examples/compilation/to_word                          4m05s  12GB
Aug 07 08:22:45 Starting examples/lpr_checker
Aug 07 08:24:06 Finished examples/lpr_checker                                  1m20s   2GB
Aug 07 08:24:07 Starting examples/lpr_checker/array
Aug 07 08:53:04 Finished examples/lpr_checker/array                           28m55s  11GB
Aug 07 08:53:05 Starting examples/lpr_checker/array/compilation
Aug 07 08:55:44 Finished examples/lpr_checker/array/compilation                2m37s  10GB
Aug 07 08:55:44 Starting examples/lpr_checker/array/compilation/proofs
Aug 07 08:57:54 Finished examples/lpr_checker/array/compilation/proofs         2m09s   7GB
Aug 07 08:57:55 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 07 08:59:43 Finished examples/lpr_checker/array/compilation/proofsARM8     1m47s   8GB
Aug 07 08:59:44 Starting examples/xlrup_checker
Aug 07 09:00:57 Finished examples/xlrup_checker                                1m11s   2GB
Aug 07 09:00:58 Starting examples/xlrup_checker/array
Aug 07 09:16:14 Finished examples/xlrup_checker/array                         15m14s   8GB
Aug 07 09:16:15 Starting examples/xlrup_checker/array/compilation
Aug 07 09:17:39 Finished examples/xlrup_checker/array/compilation              1m23s   7GB
Aug 07 09:17:40 Starting examples/xlrup_checker/array/compilation/proofs
Aug 07 09:19:16 Finished examples/xlrup_checker/array/compilation/proofs       1m34s   9GB
Aug 07 09:19:17 Starting examples/pseudo_bool
Aug 07 09:21:33 Finished examples/pseudo_bool                                  2m15s   2GB
Aug 07 09:21:34 Starting examples/pseudo_bool/cnf_encoding
Aug 07 09:22:14 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Aug 07 09:22:15 Starting examples/pseudo_bool/graph_encoding
Aug 07 09:23:11 Finished examples/pseudo_bool/graph_encoding                     55s   2GB
Aug 07 09:23:12 Starting examples/pseudo_bool/array
Aug 07 10:30:34 Finished examples/pseudo_bool/array                         1h07m20s  36GB
Aug 07 10:30:35 Starting examples/pseudo_bool/array/compilation
Aug 07 10:43:55 Finished examples/pseudo_bool/array/compilation               13m18s  28GB
Aug 07 10:43:56 Starting examples/pseudo_bool/array/compilation/proofs
Aug 07 10:47:53 Finished examples/pseudo_bool/array/compilation/proofs         3m56s  10GB
Aug 07 10:47:54 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 07 10:49:43 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m48s   8GB
Aug 07 10:49:44 Starting examples/opentheory
Aug 07 11:00:30 Finished examples/opentheory                                  10m45s   7GB
Aug 07 11:00:31 Starting examples/opentheory
Aug 07 11:00:33 Finished examples/opentheory                                      0s 133MB
Aug 07 11:00:34 Starting examples/opentheory/compilation
Aug 07 11:02:35 Finished examples/opentheory/compilation                       2m00s   8GB
Aug 07 11:02:36 Starting examples/opentheory/compilation/proofs
Aug 07 11:04:24 Finished examples/opentheory/compilation/proofs                1m46s   8GB
Aug 07 11:04:25 Starting examples/opentheory/compilation/ag32
Aug 07 11:06:30 Finished examples/opentheory/compilation/ag32                  2m04s   9GB
Aug 07 11:06:31 Starting examples/opentheory/compilation/ag32/proofs
Aug 07 11:08:54 Finished examples/opentheory/compilation/ag32/proofs           2m22s  12GB
Aug 07 11:08:55 Starting examples/sat_encodings
Aug 07 11:11:54 Finished examples/sat_encodings                                2m57s   2GB
Aug 07 11:11:55 Starting examples/sat_encodings/case_studies
Aug 07 11:14:05 Finished examples/sat_encodings/case_studies                   2m09s   2GB
Aug 07 11:14:06 Starting examples/sat_encodings/translation
Aug 07 11:20:32 Finished examples/sat_encodings/translation                    6m25s   8GB
Aug 07 11:20:32 Starting examples/sat_encodings/translation/compilation
Aug 07 11:22:56 Finished examples/sat_encodings/translation/compilation        2m22s   7GB
Aug 07 11:22:57 Starting examples/deflate
Aug 07 11:24:24 Finished examples/deflate                                      1m26s   1GB
Aug 07 11:24:25 Starting examples/deflate/translation
Aug 07 11:26:04 Finished examples/deflate/translation                          1m38s   7GB
Aug 07 11:26:05 Starting examples/deflate/translation/compilation
Aug 07 11:27:10 Finished examples/deflate/translation/compilation              1m04s   5GB
Aug 07 11:27:11 Starting examples/vipr
Aug 07 11:31:30 Finished examples/vipr                                         4m18s   8GB
Aug 07 11:31:31 Starting examples/vipr/compilation
Aug 07 11:32:48 Finished examples/vipr/compilation                             1m16s   6GB
Aug 07 11:32:49 Starting translator/okasaki-examples
Aug 07 11:38:05 Finished translator/okasaki-examples                           5m14s   4GB
Aug 07 11:38:06 Starting translator/other-examples
Aug 07 11:42:55 Finished translator/other-examples                             4m48s   3GB
Aug 07 11:42:56 Starting compiler/parsing/tests
Aug 07 11:43:30 Finished compiler/parsing/tests                                  33s   1GB
Aug 07 11:43:31 Starting compiler/inference/tests
Aug 07 11:44:14 Finished compiler/inference/tests                                41s   3GB
Aug 07 11:44:15 Starting compiler/printing/test
Aug 07 11:45:48 Finished compiler/printing/test                                1m32s   6GB
Aug 07 11:45:49 Starting icing/flover
Aug 07 12:22:56 Finished icing/flover                                         37m06s   3GB
Aug 07 12:22:57 Starting icing/
Aug 07 12:50:46 Finished icing/                                               27m47s   9GB
Aug 07 12:50:47 Starting icing/examples
Aug 07 12:52:34 Finished icing/examples                                        1m46s   8GB
Aug 07 12:52:35 Starting compiler/repl
Aug 07 13:01:32 Finished compiler/repl                                         8m55s  10GB
Aug 07 13:01:32 Starting unverified/sexpr-bootstrap/x64/64
Aug 07 13:13:24 Finished unverified/sexpr-bootstrap/x64/64                    11m50s  18GB
Aug 07 13:13:25 Starting unverified/sexpr-bootstrap/x64/32
Aug 07 13:22:49 Finished unverified/sexpr-bootstrap/x64/32                     9m23s  14GB
Aug 07 13:22:50 Starting compiler/benchmarks
Aug 07 13:23:34 Finished compiler/benchmarks                                     43s 713MB
Aug 07 13:23:35 Starting compiler/bootstrap/compilation/x64/64
Aug 07 14:07:05 Finished compiler/bootstrap/compilation/x64/64                43m29s 133GB
Aug 07 14:07:06 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 07 14:30:17 Finished compiler/bootstrap/compilation/x64/64/proofs         23m09s  52GB
Aug 07 14:30:18 Starting compiler/bootstrap/compilation/x64/32
Aug 07 15:08:59 Finished compiler/bootstrap/compilation/x64/32                38m40s 101GB
Aug 07 15:09:00 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 07 15:13:46 Finished compiler/bootstrap/compilation/x64/32/proofs          4m44s  24GB
Aug 07 15:13:47 Starting compiler/bootstrap/compilation/arm8/64
Aug 07 16:05:45 Finished compiler/bootstrap/compilation/arm8/64               51m56s 112GB
Aug 07 16:05:46 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 07 16:11:45 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m58s  29GB
Aug 07 16:11:46 Starting compiler/bootstrap/compilation/ag32/32
Aug 07 16:53:00 Finished compiler/bootstrap/compilation/ag32/32               41m12s 112GB
Aug 07 16:53:01 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 07 16:58:23 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m21s  32GB
Aug 07 16:58:24 SUCCESS