Job 2333

CakeML:98d0d03c9e52b27a9895186563d385583deb75a2
  Merge pull request #984 from CakeML/compression [Mar 10 14:36:06]
HOL:772a64a23fab01445886a113b810bd3c02930e63
  Tweak tailrecLib to allow function terms that are composite [Mar 04 00:41:36]
Machine:lammington
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Mar 11 08:02:12 Claimed job
Mar 11 08:02:16 Reusing HOL
Mar 11 08:02:26 Starting developers
Mar 11 08:02:30 Finished developers                                               2s 218MB
Mar 11 08:02:30 Starting developers/bin
Mar 11 08:02:41 Finished developers/bin                                           9s   1GB
Mar 11 08:02:42 Starting compiler/proofs
Mar 11 09:46:20 Finished compiler/proofs                                    1h43m36s  42GB
Mar 11 09:46:21 Starting compiler/bootstrap/translation
Mar 11 17:46:06 Finished compiler/bootstrap/translation                     7h59m43s  66GB
Mar 11 17:46:06 Starting semantics/ffi
Mar 11 17:46:15 Finished semantics/ffi                                            7s 636MB
Mar 11 17:46:16 Starting semantics
Mar 11 17:46:17 Finished semantics                                                0s  62MB
Mar 11 17:46:18 Starting semantics/proofs
Mar 11 17:46:52 Finished semantics/proofs                                        33s   1GB
Mar 11 17:46:53 Starting semantics/alt_semantics
Mar 11 17:47:32 Finished semantics/alt_semantics                                 38s   1GB
Mar 11 17:47:33 Starting semantics/alt_semantics/proofs
Mar 11 17:58:29 Finished semantics/alt_semantics/proofs                       10m54s   5GB
Mar 11 17:58:30 Starting basis/pure
Mar 11 17:58:31 Finished basis/pure                                               0s  68MB
Mar 11 17:58:32 Starting translator
Mar 11 18:00:15 Finished translator                                            1m42s   3GB
Mar 11 18:00:16 Starting compiler/parsing
Mar 11 18:00:17 Finished compiler/parsing                                         0s  73MB
Mar 11 18:00:18 Starting characteristic
Mar 11 18:00:20 Finished characteristic                                           0s  94MB
Mar 11 18:00:20 Starting translator/monadic
Mar 11 18:00:22 Finished translator/monadic                                       0s  90MB
Mar 11 18:00:23 Starting basis
Mar 11 18:04:02 Finished basis                                                 3m37s   5GB
Mar 11 18:04:02 Starting compiler/inference
Mar 11 18:04:04 Finished compiler/inference                                       0s  83MB
Mar 11 18:04:05 Starting compiler/backend/reg_alloc
Mar 11 18:04:06 Finished compiler/backend/reg_alloc                               0s  65MB
Mar 11 18:04:07 Starting compiler/backend/gc
Mar 11 18:04:09 Finished compiler/backend/gc                                      0s 135MB
Mar 11 18:04:10 Starting compiler/backend
Mar 11 18:04:27 Finished compiler/backend                                        17s   1GB
Mar 11 18:04:28 Starting compiler/encoders/asm
Mar 11 18:04:30 Finished compiler/encoders/asm                                    0s  85MB
Mar 11 18:04:31 Starting compiler/encoders/x64
Mar 11 18:04:32 Finished compiler/encoders/x64                                    0s  93MB
Mar 11 18:04:33 Starting compiler/encoders/arm7
Mar 11 18:04:35 Finished compiler/encoders/arm7                                   0s  93MB
Mar 11 18:04:35 Starting compiler/encoders/arm8
Mar 11 18:04:37 Finished compiler/encoders/arm8                                   0s  97MB
Mar 11 18:04:38 Starting compiler/encoders/arm8_asl
Mar 11 18:06:55 Finished compiler/encoders/arm8_asl                            2m16s   1GB
Mar 11 18:06:56 Starting compiler/encoders/mips
Mar 11 18:06:57 Finished compiler/encoders/mips                                   0s  93MB
Mar 11 18:06:58 Starting compiler/encoders/riscv
Mar 11 18:06:59 Finished compiler/encoders/riscv                                  0s  97MB
Mar 11 18:07:00 Starting compiler/encoders/ag32
Mar 11 18:07:02 Finished compiler/encoders/ag32                                   0s  92MB
Mar 11 18:07:03 Starting compiler/backend/x64
Mar 11 18:07:04 Finished compiler/backend/x64                                     0s 133MB
Mar 11 18:07:05 Starting compiler/backend/arm7
Mar 11 18:07:07 Finished compiler/backend/arm7                                    0s 133MB
Mar 11 18:07:08 Starting compiler/backend/arm8
Mar 11 18:07:10 Finished compiler/backend/arm8                                    0s 133MB
Mar 11 18:07:11 Starting compiler/backend/mips
Mar 11 18:07:12 Finished compiler/backend/mips                                    0s 133MB
Mar 11 18:07:13 Starting compiler/backend/riscv
Mar 11 18:07:15 Finished compiler/backend/riscv                                   0s 133MB
Mar 11 18:07:16 Starting compiler/backend/ag32
Mar 11 18:08:36 Finished compiler/backend/ag32                                 1m19s   2GB
Mar 11 18:08:37 Starting compiler/parsing/proofs
Mar 11 18:08:38 Finished compiler/parsing/proofs                                  0s  76MB
Mar 11 18:08:39 Starting compiler/inference/proofs
Mar 11 18:08:41 Finished compiler/inference/proofs                                0s  89MB
Mar 11 18:08:42 Starting compiler/backend/semantics
Mar 11 18:10:08 Finished compiler/backend/semantics                            1m25s   2GB
Mar 11 18:10:09 Starting compiler/backend/reg_alloc/proofs
Mar 11 18:10:10 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Mar 11 18:10:11 Starting compiler/backend/proofs
Mar 11 18:11:17 Finished compiler/backend/proofs                               1m04s   4GB
Mar 11 18:11:17 Starting compiler/backend/serialiser
Mar 11 18:11:20 Finished compiler/backend/serialiser                              1s 194MB
Mar 11 18:11:21 Starting compiler/encoders/x64/proofs
Mar 11 18:20:42 Finished compiler/encoders/x64/proofs                          9m20s   5GB
Mar 11 18:20:43 Starting compiler/encoders/arm7/proofs
Mar 11 18:33:32 Finished compiler/encoders/arm7/proofs                        12m48s   8GB
Mar 11 18:33:33 Starting compiler/encoders/arm8/proofs
Mar 11 18:40:08 Finished compiler/encoders/arm8/proofs                         6m33s   5GB
Mar 11 18:40:09 Starting compiler/encoders/arm8_asl/proofs
Mar 11 18:53:55 Finished compiler/encoders/arm8_asl/proofs                    13m45s   4GB
Mar 11 18:53:56 Starting compiler/encoders/mips/proofs
Mar 11 19:03:58 Finished compiler/encoders/mips/proofs                        10m00s   7GB
Mar 11 19:03:59 Starting compiler/encoders/riscv/proofs
Mar 11 19:12:17 Finished compiler/encoders/riscv/proofs                        8m17s   5GB
Mar 11 19:12:18 Starting compiler/encoders/ag32/proofs
Mar 11 19:14:40 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 11 19:14:41 Starting compiler/backend/x64/proofs
Mar 11 19:15:19 Finished compiler/backend/x64/proofs                             37s   3GB
Mar 11 19:15:20 Starting compiler/backend/arm7/proofs
Mar 11 19:16:01 Finished compiler/backend/arm7/proofs                            40s   2GB
Mar 11 19:16:02 Starting compiler/backend/arm8/proofs
Mar 11 19:16:41 Finished compiler/backend/arm8/proofs                            38s   3GB
Mar 11 19:16:42 Starting compiler/backend/arm8_asl
Mar 11 19:17:11 Finished compiler/backend/arm8_asl                               28s   2GB
Mar 11 19:17:12 Starting compiler/backend/mips/proofs
Mar 11 19:17:56 Finished compiler/backend/mips/proofs                            43s   3GB
Mar 11 19:17:57 Starting compiler/backend/riscv/proofs
Mar 11 19:18:45 Finished compiler/backend/riscv/proofs                           47s   4GB
Mar 11 19:18:46 Starting compiler/backend/ag32/proofs
Mar 11 19:31:59 Finished compiler/backend/ag32/proofs                         13m11s   6GB
Mar 11 19:32:00 Starting candle/set-theory
Mar 11 19:32:43 Finished candle/set-theory                                       43s   1GB
Mar 11 19:32:44 Starting candle/syntax-lib
Mar 11 19:32:46 Finished candle/syntax-lib                                        0s  74MB
Mar 11 19:32:47 Starting candle/standard/syntax
Mar 11 19:33:03 Finished candle/standard/syntax                                  15s   1GB
Mar 11 19:33:04 Starting candle/standard/semantics
Mar 11 19:35:28 Finished candle/standard/semantics                             2m23s   2GB
Mar 11 19:35:29 Starting candle/standard/monadic
Mar 11 19:35:30 Finished candle/standard/monadic                                  0s  97MB
Mar 11 19:35:31 Starting candle/standard/ml_kernel
Mar 11 19:37:23 Finished candle/standard/ml_kernel                             1m50s   6GB
Mar 11 19:37:24 Starting candle/overloading/syntax
Mar 11 19:40:48 Finished candle/overloading/syntax                             3m23s   2GB
Mar 11 19:40:49 Starting candle/overloading/semantics
Mar 11 19:52:08 Finished candle/overloading/semantics                         11m17s   6GB
Mar 11 19:52:09 Starting candle/overloading/monadic
Mar 11 19:54:42 Finished candle/overloading/monadic                            2m32s   2GB
Mar 11 19:54:43 Starting candle/overloading/ml_kernel
Mar 11 20:02:16 Finished candle/overloading/ml_kernel                          7m32s   7GB
Mar 11 20:02:17 Starting candle/overloading/ml_checker
Mar 11 20:04:49 Finished candle/overloading/ml_checker                         2m30s   7GB
Mar 11 20:04:49 Starting candle/prover
Mar 11 20:14:42 Finished candle/prover                                         9m51s   5GB
Mar 11 20:14:43 Starting pancake
Mar 11 20:15:42 Finished pancake                                                 58s   1GB
Mar 11 20:15:42 Starting pancake/ffi
Mar 11 20:15:43 Finished pancake/ffi                                              0s  20MB
Mar 11 20:15:44 Starting pancake/semantics
Mar 11 20:18:04 Finished pancake/semantics                                     2m18s   2GB
Mar 11 20:18:05 Starting pancake/parser
Mar 11 20:18:32 Finished pancake/parser                                          25s   2GB
Mar 11 20:18:32 Starting pancake/proofs
Mar 11 20:48:30 Finished pancake/proofs                                       29m56s   9GB
Mar 11 20:48:31 Starting characteristic/examples
Mar 11 20:50:08 Finished characteristic/examples                               1m36s   6GB
Mar 11 20:50:09 Starting tutorial/solutions
Mar 11 21:05:42 Finished tutorial/solutions                                   15m32s  12GB
Mar 11 21:05:43 Starting translator/monadic/examples
Mar 11 21:09:26 Finished translator/monadic/examples                           3m42s   5GB
Mar 11 21:09:27 Starting examples
Mar 11 21:23:52 Finished examples                                             14m23s   7GB
Mar 11 21:23:53 Starting examples/compilation/x64
Mar 11 23:21:13 Finished examples/compilation/x64                           1h57m19s  35GB
Mar 11 23:21:14 Starting examples/compilation/x64/proofs
Mar 11 23:25:07 Finished examples/compilation/x64/proofs                       3m52s   5GB
Mar 11 23:25:08 Starting examples/compilation/ag32
Mar 11 23:54:37 Finished examples/compilation/ag32                            29m27s   9GB
Mar 11 23:54:38 Starting examples/compilation/ag32/proofs
Mar 11 23:56:05 Finished examples/compilation/ag32/proofs                      1m26s   7GB
Mar 11 23:56:06 Starting examples/compilation/to_word
Mar 11 23:59:58 Finished examples/compilation/to_word                          3m51s  12GB
Mar 11 23:59:59 Starting examples/lpr_checker
Mar 12 00:01:14 Finished examples/lpr_checker                                  1m14s   2GB
Mar 12 00:01:15 Starting examples/lpr_checker/array
Mar 12 00:31:29 Finished examples/lpr_checker/array                           30m11s  10GB
Mar 12 00:31:30 Starting examples/lpr_checker/array/compilation
Mar 12 01:09:43 Finished examples/lpr_checker/array/compilation               38m12s  75GB
Mar 12 01:09:44 Starting examples/lpr_checker/array/compilation/proofs
Mar 12 01:11:22 Finished examples/lpr_checker/array/compilation/proofs         1m36s   7GB
Mar 12 01:11:23 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 12 01:23:06 Finished examples/lpr_checker/array/compilation/proofsARM8    11m42s  41GB
Mar 12 01:23:07 Starting examples/xlrup_checker
Mar 12 01:24:16 Finished examples/xlrup_checker                                1m08s   1GB
Mar 12 01:24:17 Starting examples/xlrup_checker/array
Mar 12 01:40:48 Finished examples/xlrup_checker/array                         16m30s   6GB
Mar 12 01:40:49 Starting examples/xlrup_checker/array/compilation
Mar 12 02:02:24 Finished examples/xlrup_checker/array/compilation             21m33s  47GB
Mar 12 02:02:24 Starting examples/xlrup_checker/array/compilation/proofs
Mar 12 02:03:56 Finished examples/xlrup_checker/array/compilation/proofs       1m30s   6GB
Mar 12 02:03:57 Starting examples/pseudo_bool
Mar 12 02:05:59 Finished examples/pseudo_bool                                  2m01s   2GB
Mar 12 02:06:00 Starting examples/pseudo_bool/cnf_encoding
Mar 12 02:06:38 Finished examples/pseudo_bool/cnf_encoding                       36s   1GB
Mar 12 02:06:39 Starting examples/pseudo_bool/graph_encoding
Mar 12 02:07:27 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Mar 12 02:07:28 Starting examples/pseudo_bool/array
Mar 12 03:12:42 Finished examples/pseudo_bool/array                         1h05m13s  34GB
Mar 12 03:12:43 Starting examples/pseudo_bool/array/compilation
Mar 12 10:24:14 Finished examples/pseudo_bool/array/compilation             7h11m29s 114GB
Mar 12 10:24:15 Starting examples/pseudo_bool/array/compilation/proofs
Mar 12 10:27:33 Finished examples/pseudo_bool/array/compilation/proofs         3m17s   8GB
Mar 12 10:27:34 Starting examples/opentheory
Mar 12 10:38:07 Finished examples/opentheory                                  10m32s   8GB
Mar 12 10:38:08 Starting examples/opentheory
Mar 12 10:38:10 Finished examples/opentheory                                      0s 122MB
Mar 12 10:38:11 Starting examples/opentheory/compilation
Mar 12 11:13:49 Finished examples/opentheory/compilation                      35m37s  49GB
Mar 12 11:13:50 Starting examples/opentheory/compilation/proofs
Mar 12 11:15:19 Finished examples/opentheory/compilation/proofs                1m28s   6GB
Mar 12 11:15:20 Starting examples/opentheory/compilation/ag32
Mar 12 11:46:53 Finished examples/opentheory/compilation/ag32                 31m31s  43GB
Mar 12 11:46:54 Starting examples/opentheory/compilation/ag32/proofs
Mar 12 11:49:14 Finished examples/opentheory/compilation/ag32/proofs           2m19s  11GB
Mar 12 11:49:15 Starting examples/sat_encodings
Mar 12 11:51:49 Finished examples/sat_encodings                                2m33s   1GB
Mar 12 11:51:50 Starting examples/sat_encodings/case_studies
Mar 12 11:53:46 Finished examples/sat_encodings/case_studies                   1m55s   1GB
Mar 12 11:53:47 Starting examples/sat_encodings/translation
Mar 12 11:59:58 Finished examples/sat_encodings/translation                    6m10s   7GB
Mar 12 11:59:59 Starting examples/sat_encodings/translation/compilation
Mar 12 12:34:56 Finished examples/sat_encodings/translation/compilation       34m55s  20GB
Mar 12 12:34:57 Starting examples/deflate
Mar 12 12:36:10 Finished examples/deflate                                      1m12s   1GB
Mar 12 12:36:11 Starting examples/deflate/translation
Mar 12 12:37:48 Finished examples/deflate/translation                          1m35s   7GB
Mar 12 12:37:48 Starting examples/deflate/translation/compilation
Mar 12 12:55:04 Finished examples/deflate/translation/compilation             17m14s  35GB
Mar 12 12:55:05 Starting examples/vipr
Mar 12 12:59:12 Finished examples/vipr                                         4m06s   7GB
Mar 12 12:59:13 Starting examples/vipr/compilation
Mar 12 13:18:34 Finished examples/vipr/compilation                            19m19s  30GB
Mar 12 13:18:35 Starting translator/okasaki-examples
Mar 12 13:23:34 Finished translator/okasaki-examples                           4m58s   3GB
Mar 12 13:23:35 Starting translator/other-examples
Mar 12 13:24:43 Finished translator/other-examples                             1m07s   3GB
Mar 12 13:24:44 Starting compiler/parsing/tests
Mar 12 13:25:17 Finished compiler/parsing/tests                                  32s   1GB
Mar 12 13:25:18 Starting compiler/inference/tests
Mar 12 13:32:45 Finished compiler/inference/tests                              7m26s   6GB
Mar 12 13:32:46 Starting compiler/printing/test
Mar 12 13:36:16 Finished compiler/printing/test                                3m29s   6GB
Mar 12 13:36:17 Starting icing/flover
Mar 12 14:11:31 Finished icing/flover                                         35m12s   3GB
Mar 12 14:11:32 Starting icing/
Mar 12 15:06:32 Finished icing/                                               54m58s  23GB
Mar 12 15:06:33 Starting icing/examples
Mar 12 15:08:14 Finished icing/examples                                        1m40s   8GB
Mar 12 15:08:15 Starting compiler/repl
Mar 12 15:16:57 Finished compiler/repl                                         8m41s   9GB
Mar 12 15:16:58 Starting unverified/sexpr-bootstrap/x64/64
Mar 12 15:28:15 Finished unverified/sexpr-bootstrap/x64/64                    10m54s  15GB
Mar 12 15:28:16 Starting unverified/sexpr-bootstrap/x64/32
Mar 12 15:37:34 Finished unverified/sexpr-bootstrap/x64/32                     8m59s  13GB
Mar 12 15:37:35 Starting compiler/benchmarks
Mar 12 15:38:20 Finished compiler/benchmarks                                     43s 713MB
Mar 12 15:38:20 Starting compiler/bootstrap/compilation/x64/64
Mar 13 06:06:17 Finished compiler/bootstrap/compilation/x64/64             14h27m44s 149GB
Mar 13 06:06:18 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 13 06:27:11 Finished compiler/bootstrap/compilation/x64/64/proofs         20m52s  44GB
Mar 13 06:27:12 Starting compiler/bootstrap/compilation/x64/32
Mar 13 13:42:43 Finished compiler/bootstrap/compilation/x64/32              7h15m23s 112GB
Mar 13 13:42:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 13 13:46:24 Finished compiler/bootstrap/compilation/x64/32/proofs          3m39s  18GB
Mar 13 13:46:25 Starting compiler/bootstrap/compilation/ag32/32
Mar 13 21:41:30 Finished compiler/bootstrap/compilation/ag32/32             7h55m04s 151GB
Mar 13 21:41:31 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 13 21:49:10 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m38s  50GB
Mar 13 21:49:11 SUCCESS