Job 2315

CakeML:82012f90a7ee71dd8a07de33c92304ae526fe758
  Remove unused arg from closLang's ByteArray [Feb 10 23:41:50]
#982 (contexts)
Merging into: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:lammington

Mar 01 00:00:37 Claimed job
Mar 01 00:00:42 Reusing HOL
Mar 01 00:00:52 Starting developers
Mar 01 00:00:56 Finished developers                                               2s 218MB
Mar 01 00:00:57 Starting developers/bin
Mar 01 00:01:07 Finished developers/bin                                           9s   1GB
Mar 01 00:01:08 Starting compiler/proofs
Mar 01 01:44:29 Finished compiler/proofs                                    1h43m20s  23GB
Mar 01 01:44:30 Starting compiler/bootstrap/translation
Mar 01 09:43:01 Finished compiler/bootstrap/translation                     7h58m29s  63GB
Mar 01 09:43:01 Starting semantics/ffi
Mar 01 09:43:10 Finished semantics/ffi                                            7s 701MB
Mar 01 09:43:10 Starting semantics
Mar 01 09:43:12 Finished semantics                                                0s  67MB
Mar 01 09:43:13 Starting semantics/proofs
Mar 01 09:43:47 Finished semantics/proofs                                        33s   1GB
Mar 01 09:43:48 Starting semantics/alt_semantics
Mar 01 09:44:27 Finished semantics/alt_semantics                                 37s   1GB
Mar 01 09:44:28 Starting semantics/alt_semantics/proofs
Mar 01 09:55:24 Finished semantics/alt_semantics/proofs                       10m55s   5GB
Mar 01 09:55:25 Starting basis/pure
Mar 01 09:55:27 Finished basis/pure                                               0s  68MB
Mar 01 09:55:27 Starting translator
Mar 01 09:57:11 Finished translator                                            1m42s   4GB
Mar 01 09:57:12 Starting compiler/parsing
Mar 01 09:57:13 Finished compiler/parsing                                         0s  72MB
Mar 01 09:57:14 Starting characteristic
Mar 01 09:57:16 Finished characteristic                                           0s  91MB
Mar 01 09:57:16 Starting translator/monadic
Mar 01 09:57:18 Finished translator/monadic                                       0s  90MB
Mar 01 09:57:19 Starting basis
Mar 01 10:00:57 Finished basis                                                 3m37s   5GB
Mar 01 10:00:58 Starting compiler/inference
Mar 01 10:00:59 Finished compiler/inference                                       0s  83MB
Mar 01 10:01:00 Starting compiler/backend/reg_alloc
Mar 01 10:01:02 Finished compiler/backend/reg_alloc                               0s  65MB
Mar 01 10:01:02 Starting compiler/backend/gc
Mar 01 10:01:04 Finished compiler/backend/gc                                      0s 141MB
Mar 01 10:01:05 Starting compiler/backend
Mar 01 10:01:23 Finished compiler/backend                                        17s   1GB
Mar 01 10:01:24 Starting compiler/encoders/asm
Mar 01 10:01:26 Finished compiler/encoders/asm                                    0s  85MB
Mar 01 10:01:26 Starting compiler/encoders/x64
Mar 01 10:01:28 Finished compiler/encoders/x64                                    0s  97MB
Mar 01 10:01:29 Starting compiler/encoders/arm7
Mar 01 10:01:30 Finished compiler/encoders/arm7                                   0s  93MB
Mar 01 10:01:31 Starting compiler/encoders/arm8
Mar 01 10:01:33 Finished compiler/encoders/arm8                                   0s  93MB
Mar 01 10:01:34 Starting compiler/encoders/arm8_asl
Mar 01 10:03:50 Finished compiler/encoders/arm8_asl                            2m15s   1GB
Mar 01 10:03:51 Starting compiler/encoders/mips
Mar 01 10:03:53 Finished compiler/encoders/mips                                   0s  93MB
Mar 01 10:03:54 Starting compiler/encoders/riscv
Mar 01 10:03:55 Finished compiler/encoders/riscv                                  0s  97MB
Mar 01 10:03:56 Starting compiler/encoders/ag32
Mar 01 10:03:58 Finished compiler/encoders/ag32                                   0s  93MB
Mar 01 10:03:58 Starting compiler/backend/x64
Mar 01 10:04:00 Finished compiler/backend/x64                                     0s 129MB
Mar 01 10:04:01 Starting compiler/backend/arm7
Mar 01 10:04:03 Finished compiler/backend/arm7                                    0s 133MB
Mar 01 10:04:04 Starting compiler/backend/arm8
Mar 01 10:04:05 Finished compiler/backend/arm8                                    0s 133MB
Mar 01 10:04:06 Starting compiler/backend/mips
Mar 01 10:04:08 Finished compiler/backend/mips                                    0s 133MB
Mar 01 10:04:09 Starting compiler/backend/riscv
Mar 01 10:04:11 Finished compiler/backend/riscv                                   0s 126MB
Mar 01 10:04:12 Starting compiler/backend/ag32
Mar 01 10:05:31 Finished compiler/backend/ag32                                 1m18s   3GB
Mar 01 10:05:32 Starting compiler/parsing/proofs
Mar 01 10:05:33 Finished compiler/parsing/proofs                                  0s  76MB
Mar 01 10:05:34 Starting compiler/inference/proofs
Mar 01 10:05:36 Finished compiler/inference/proofs                                0s  89MB
Mar 01 10:05:37 Starting compiler/backend/semantics
Mar 01 10:07:03 Finished compiler/backend/semantics                            1m25s   2GB
Mar 01 10:07:04 Starting compiler/backend/reg_alloc/proofs
Mar 01 10:07:05 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Mar 01 10:07:06 Starting compiler/backend/proofs
Mar 01 10:08:08 Finished compiler/backend/proofs                               1m00s   3GB
Mar 01 10:08:08 Starting compiler/backend/serialiser
Mar 01 10:08:11 Finished compiler/backend/serialiser                              1s 194MB
Mar 01 10:08:12 Starting compiler/encoders/x64/proofs
Mar 01 10:17:34 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Mar 01 10:17:35 Starting compiler/encoders/arm7/proofs
Mar 01 10:30:22 Finished compiler/encoders/arm7/proofs                        12m45s   7GB
Mar 01 10:30:23 Starting compiler/encoders/arm8/proofs
Mar 01 10:36:51 Finished compiler/encoders/arm8/proofs                         6m26s   4GB
Mar 01 10:36:51 Starting compiler/encoders/arm8_asl/proofs
Mar 01 10:50:42 Finished compiler/encoders/arm8_asl/proofs                    13m49s   5GB
Mar 01 10:50:43 Starting compiler/encoders/mips/proofs
Mar 01 11:00:45 Finished compiler/encoders/mips/proofs                        10m00s   6GB
Mar 01 11:00:46 Starting compiler/encoders/riscv/proofs
Mar 01 11:09:03 Finished compiler/encoders/riscv/proofs                        8m15s   3GB
Mar 01 11:09:04 Starting compiler/encoders/ag32/proofs
Mar 01 11:11:25 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 01 11:11:26 Starting compiler/backend/x64/proofs
Mar 01 11:12:05 Finished compiler/backend/x64/proofs                             37s   3GB
Mar 01 11:12:06 Starting compiler/backend/arm7/proofs
Mar 01 11:12:49 Finished compiler/backend/arm7/proofs                            41s   2GB
Mar 01 11:12:49 Starting compiler/backend/arm8/proofs
Mar 01 11:13:31 Finished compiler/backend/arm8/proofs                            40s   3GB
Mar 01 11:13:31 Starting compiler/backend/arm8_asl
Mar 01 11:14:00 Finished compiler/backend/arm8_asl                               27s   2GB
Mar 01 11:14:01 Starting compiler/backend/mips/proofs
Mar 01 11:14:46 Finished compiler/backend/mips/proofs                            44s   3GB
Mar 01 11:14:47 Starting compiler/backend/riscv/proofs
Mar 01 11:15:38 Finished compiler/backend/riscv/proofs                           49s   3GB
Mar 01 11:15:39 Starting compiler/backend/ag32/proofs
Mar 01 11:28:47 Finished compiler/backend/ag32/proofs                         13m07s   6GB
Mar 01 11:28:48 Starting candle/set-theory
Mar 01 11:29:33 Finished candle/set-theory                                       43s   1GB
Mar 01 11:29:33 Starting candle/syntax-lib
Mar 01 11:29:35 Finished candle/syntax-lib                                        0s  75MB
Mar 01 11:29:36 Starting candle/standard/syntax
Mar 01 11:29:52 Finished candle/standard/syntax                                  15s   1GB
Mar 01 11:29:53 Starting candle/standard/semantics
Mar 01 11:32:19 Finished candle/standard/semantics                             2m25s   2GB
Mar 01 11:32:20 Starting candle/standard/monadic
Mar 01 11:32:21 Finished candle/standard/monadic                                  0s  97MB
Mar 01 11:32:22 Starting candle/standard/ml_kernel
Mar 01 11:34:13 Finished candle/standard/ml_kernel                             1m50s   6GB
Mar 01 11:34:14 Starting candle/overloading/syntax
Mar 01 11:37:43 Finished candle/overloading/syntax                             3m27s   3GB
Mar 01 11:37:44 Starting candle/overloading/semantics
Mar 01 11:48:56 Finished candle/overloading/semantics                         11m10s   3GB
Mar 01 11:48:56 Starting candle/overloading/monadic
Mar 01 11:51:27 Finished candle/overloading/monadic                            2m29s   2GB
Mar 01 11:51:28 Starting candle/overloading/ml_kernel
Mar 01 11:58:58 Finished candle/overloading/ml_kernel                          7m28s   6GB
Mar 01 11:58:59 Starting candle/overloading/ml_checker
Mar 01 12:01:30 Finished candle/overloading/ml_checker                         2m29s   7GB
Mar 01 12:01:31 Starting candle/prover
Mar 01 12:11:23 Finished candle/prover                                         9m51s   5GB
Mar 01 12:11:23 Starting pancake
Mar 01 12:12:25 Finished pancake                                               1m00s   1GB
Mar 01 12:12:26 Starting pancake/ffi
Mar 01 12:12:27 Finished pancake/ffi                                              0s  20MB
Mar 01 12:12:28 Starting pancake/semantics
Mar 01 12:14:45 Finished pancake/semantics                                     2m15s   2GB
Mar 01 12:14:46 Starting pancake/parser
Mar 01 12:15:12 Finished pancake/parser                                          25s   2GB
Mar 01 12:15:13 Starting pancake/proofs
Mar 01 12:44:48 Finished pancake/proofs                                       29m33s   8GB
Mar 01 12:44:49 Starting characteristic/examples
Mar 01 12:46:32 Finished characteristic/examples                               1m42s   6GB
Mar 01 12:46:33 Starting tutorial/solutions
Mar 01 13:02:00 Finished tutorial/solutions                                   15m25s  11GB
Mar 01 13:02:01 Starting translator/monadic/examples
Mar 01 13:05:47 Finished translator/monadic/examples                           3m45s   5GB
Mar 01 13:05:48 Starting examples
Mar 01 13:20:05 Finished examples                                             14m16s   7GB
Mar 01 13:20:06 Starting examples/compilation/x64
Mar 01 15:16:15 Finished examples/compilation/x64                           1h56m08s  41GB
Mar 01 15:16:16 Starting examples/compilation/x64/proofs
Mar 01 15:20:00 Finished examples/compilation/x64/proofs                       3m42s   6GB
Mar 01 15:20:01 Starting examples/compilation/ag32
Mar 01 15:49:15 Finished examples/compilation/ag32                            29m13s  10GB
Mar 01 15:49:16 Starting examples/compilation/ag32/proofs
Mar 01 15:50:44 Finished examples/compilation/ag32/proofs                      1m27s   7GB
Mar 01 15:50:45 Starting examples/compilation/to_word
Mar 01 15:54:35 Finished examples/compilation/to_word                          3m49s  11GB
Mar 01 15:54:36 Starting examples/lpr_checker
Mar 01 15:55:51 Finished examples/lpr_checker                                  1m14s   2GB
Mar 01 15:55:52 Starting examples/lpr_checker/array
Mar 01 16:24:33 Finished examples/lpr_checker/array                           28m40s   8GB
Mar 01 16:24:34 Starting examples/lpr_checker/array/compilation
Mar 01 16:58:40 Finished examples/lpr_checker/array/compilation               34m04s  69GB
Mar 01 16:58:41 Starting examples/lpr_checker/array/compilation/proofs
Mar 01 17:00:32 Finished examples/lpr_checker/array/compilation/proofs         1m50s   9GB
Mar 01 17:00:33 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 01 17:09:24 Finished examples/lpr_checker/array/compilation/proofsARM8     8m50s  47GB
Mar 01 17:09:25 Starting examples/xlrup_checker
Mar 01 17:10:34 Finished examples/xlrup_checker                                1m07s   1GB
Mar 01 17:10:35 Starting examples/xlrup_checker/array
Mar 01 17:26:44 Finished examples/xlrup_checker/array                         16m08s   5GB
Mar 01 17:26:45 Starting examples/xlrup_checker/array/compilation
Mar 01 17:47:32 Finished examples/xlrup_checker/array/compilation             20m45s  33GB
Mar 01 17:47:33 Starting examples/xlrup_checker/array/compilation/proofs
Mar 01 17:49:00 Finished examples/xlrup_checker/array/compilation/proofs       1m25s   6GB
Mar 01 17:49:00 Starting examples/pseudo_bool
Mar 01 17:51:01 Finished examples/pseudo_bool                                  1m59s   2GB
Mar 01 17:51:02 Starting examples/pseudo_bool/cnf_encoding
Mar 01 17:51:38 Finished examples/pseudo_bool/cnf_encoding                       35s   1GB
Mar 01 17:51:39 Starting examples/pseudo_bool/graph_encoding
Mar 01 17:52:29 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Mar 01 17:52:30 Starting examples/pseudo_bool/array
Mar 01 18:55:44 Finished examples/pseudo_bool/array                         1h03m13s  40GB
Mar 01 18:55:45 Starting examples/pseudo_bool/array/compilation
Mar 02 02:14:36 Finished examples/pseudo_bool/array/compilation             7h18m49s 123GB
Mar 02 02:14:37 Starting examples/pseudo_bool/array/compilation/proofs
Mar 02 02:17:55 Finished examples/pseudo_bool/array/compilation/proofs         3m17s   7GB
Mar 02 02:17:56 Starting examples/opentheory
Mar 02 02:28:36 Finished examples/opentheory                                  10m39s   8GB
Mar 02 02:28:37 Starting examples/opentheory
Mar 02 02:28:39 Finished examples/opentheory                                      0s 123MB
Mar 02 02:28:39 Starting examples/opentheory/compilation
Mar 02 03:03:58 Finished examples/opentheory/compilation                      35m17s  49GB
Mar 02 03:03:59 Starting examples/opentheory/compilation/proofs
Mar 02 03:05:25 Finished examples/opentheory/compilation/proofs                1m24s   6GB
Mar 02 03:05:26 Starting examples/opentheory/compilation/ag32
Mar 02 03:36:43 Finished examples/opentheory/compilation/ag32                 31m16s  47GB
Mar 02 03:36:44 Starting examples/opentheory/compilation/ag32/proofs
Mar 02 03:39:05 Finished examples/opentheory/compilation/ag32/proofs           2m20s  11GB
Mar 02 03:39:06 Starting examples/sat_encodings
Mar 02 03:41:41 Finished examples/sat_encodings                                2m33s   1GB
Mar 02 03:41:42 Starting examples/sat_encodings/case_studies
Mar 02 03:43:39 Finished examples/sat_encodings/case_studies                   1m55s   1GB
Mar 02 03:43:39 Starting examples/sat_encodings/translation
Mar 02 03:49:43 Finished examples/sat_encodings/translation                    6m02s   7GB
Mar 02 03:49:44 Starting examples/sat_encodings/translation/compilation
Mar 02 04:25:10 Finished examples/sat_encodings/translation/compilation       35m25s  35GB
Mar 02 04:25:11 Starting examples/deflate
Mar 02 04:26:26 Finished examples/deflate                                      1m14s   1GB
Mar 02 04:26:27 Starting examples/deflate/translation
Mar 02 04:28:06 Finished examples/deflate/translation                          1m37s   7GB
Mar 02 04:28:07 Starting examples/deflate/translation/compilation
Mar 02 04:44:48 Finished examples/deflate/translation/compilation             16m40s  14GB
Mar 02 04:44:49 Starting examples/vipr
Mar 02 04:48:52 Finished examples/vipr                                         4m01s   7GB
Mar 02 04:48:53 Starting examples/vipr/compilation
Mar 02 05:08:50 Finished examples/vipr/compilation                            19m56s  41GB
Mar 02 05:08:51 Starting translator/okasaki-examples
Mar 02 05:13:50 Finished translator/okasaki-examples                           4m57s   4GB
Mar 02 05:13:51 Starting translator/other-examples
Mar 02 05:14:58 Finished translator/other-examples                             1m06s   3GB
Mar 02 05:14:59 Starting compiler/parsing/tests
Mar 02 05:15:33 Finished compiler/parsing/tests                                  32s   1GB
Mar 02 05:15:33 Starting compiler/inference/tests
Mar 02 05:23:06 Finished compiler/inference/tests                              7m31s   7GB
Mar 02 05:23:07 Starting compiler/printing/test
Mar 02 05:26:35 Finished compiler/printing/test                                3m27s   6GB
Mar 02 05:26:36 Starting icing/flover
Mar 02 06:02:31 Finished icing/flover                                         35m53s   4GB
Mar 02 06:02:32 Starting icing/
Mar 02 06:57:10 Finished icing/                                               54m37s  32GB
Mar 02 06:57:11 Starting icing/examples
Mar 02 06:58:55 Finished icing/examples                                        1m42s   8GB
Mar 02 06:58:55 Starting compiler/repl
Mar 02 07:07:39 Finished compiler/repl                                         8m42s   9GB
Mar 02 07:07:40 Starting unverified/sexpr-bootstrap/x64/64
Mar 02 07:18:27 Finished unverified/sexpr-bootstrap/x64/64                    10m46s  16GB
Mar 02 07:18:28 Starting unverified/sexpr-bootstrap/x64/32
Mar 02 07:27:23 Finished unverified/sexpr-bootstrap/x64/32                     8m53s  14GB
Mar 02 07:27:24 Starting compiler/benchmarks
Mar 02 07:28:08 Finished compiler/benchmarks                                     43s 713MB
Mar 02 07:28:09 Starting compiler/bootstrap/compilation/x64/64
Mar 02 22:23:05 Finished compiler/bootstrap/compilation/x64/64             14h54m54s 157GB
Mar 02 22:23:06 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 02 22:44:20 Finished compiler/bootstrap/compilation/x64/64/proofs         21m13s  47GB
Mar 02 22:44:21 Starting compiler/bootstrap/compilation/x64/32
Mar 03 06:25:27 Finished compiler/bootstrap/compilation/x64/32              7h41m04s 175GB
Mar 03 06:25:28 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 03 06:28:56 Finished compiler/bootstrap/compilation/x64/32/proofs          3m27s  19GB
Mar 03 06:28:57 Starting compiler/bootstrap/compilation/ag32/32
Mar 03 14:22:15 Finished compiler/bootstrap/compilation/ag32/32             7h53m16s 146GB
Mar 03 14:22:16 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 03 14:30:00 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m43s  50GB
Mar 03 14:30:01 SUCCESS