Job 2213

CakeML:2f2213e5f93cc3ba42f9b63ce1f03f5720a71481
  byteTheory: remove a duplicate [Sep 02 09:28:25]
#972 (byte)
Merging into:d72802c88994d8eaec084c06e52f7d4ca8fa3d00
  Merge pull request #973 from CakeML/arm8_bootstrap [Sep 06 05:48:43]
HOL:56875629a42860effd84a80abd66e63a4c7a4961
  [rational] Weaken RAT_MINV_LES's precondition [Aug 28 06:33:33]
Machine:lammington

Sep 06 05:51:53 Claimed job
Sep 06 05:51:57 Reusing HOL
Sep 06 05:52:06 Starting developers
Sep 06 05:52:10 Finished developers                                               2s 200MB
Sep 06 05:52:11 Starting developers/bin
Sep 06 05:52:21 Finished developers/bin                                           9s   1GB
Sep 06 05:52:21 Starting compiler/proofs
Sep 06 07:34:02 Finished compiler/proofs                                    1h41m38s  36GB
Sep 06 07:34:03 Starting compiler/bootstrap/translation
Sep 06 15:30:25 Finished compiler/bootstrap/translation                     7h56m20s  67GB
Sep 06 15:30:26 Starting semantics/ffi
Sep 06 15:30:34 Finished semantics/ffi                                            7s 569MB
Sep 06 15:30:35 Starting semantics
Sep 06 15:30:36 Finished semantics                                                0s  65MB
Sep 06 15:30:37 Starting semantics/proofs
Sep 06 15:31:12 Finished semantics/proofs                                        33s   1GB
Sep 06 15:31:12 Starting semantics/alt_semantics
Sep 06 15:31:52 Finished semantics/alt_semantics                                 38s   1GB
Sep 06 15:31:53 Starting semantics/alt_semantics/proofs
Sep 06 15:42:57 Finished semantics/alt_semantics/proofs                       11m04s   4GB
Sep 06 15:42:58 Starting basis/pure
Sep 06 15:42:59 Finished basis/pure                                               0s  68MB
Sep 06 15:43:00 Starting translator
Sep 06 15:44:42 Finished translator                                            1m41s   4GB
Sep 06 15:44:43 Starting compiler/parsing
Sep 06 15:44:44 Finished compiler/parsing                                         0s  70MB
Sep 06 15:44:45 Starting characteristic
Sep 06 15:44:47 Finished characteristic                                           0s  93MB
Sep 06 15:44:48 Starting translator/monadic
Sep 06 15:44:49 Finished translator/monadic                                       0s  97MB
Sep 06 15:44:50 Starting basis
Sep 06 15:48:48 Finished basis                                                 3m57s   5GB
Sep 06 15:48:49 Starting compiler/inference
Sep 06 15:48:51 Finished compiler/inference                                       0s  80MB
Sep 06 15:48:51 Starting compiler/backend/reg_alloc
Sep 06 15:48:53 Finished compiler/backend/reg_alloc                               0s  65MB
Sep 06 15:48:53 Starting compiler/backend/gc
Sep 06 15:48:55 Finished compiler/backend/gc                                      0s 137MB
Sep 06 15:48:56 Starting compiler/backend
Sep 06 15:49:13 Finished compiler/backend                                        16s   1GB
Sep 06 15:49:14 Starting compiler/encoders/asm
Sep 06 15:49:15 Finished compiler/encoders/asm                                    0s  84MB
Sep 06 15:49:16 Starting compiler/encoders/x64
Sep 06 15:49:18 Finished compiler/encoders/x64                                    0s  95MB
Sep 06 15:49:18 Starting compiler/encoders/arm7
Sep 06 15:49:20 Finished compiler/encoders/arm7                                   0s  94MB
Sep 06 15:49:21 Starting compiler/encoders/arm8
Sep 06 15:49:22 Finished compiler/encoders/arm8                                   0s  89MB
Sep 06 15:49:23 Starting compiler/encoders/arm8_asl
Sep 06 15:51:34 Finished compiler/encoders/arm8_asl                            2m10s   1GB
Sep 06 15:51:35 Starting compiler/encoders/mips
Sep 06 15:51:37 Finished compiler/encoders/mips                                   0s  89MB
Sep 06 15:51:37 Starting compiler/encoders/riscv
Sep 06 15:51:39 Finished compiler/encoders/riscv                                  0s  89MB
Sep 06 15:51:40 Starting compiler/encoders/ag32
Sep 06 15:51:41 Finished compiler/encoders/ag32                                   0s  85MB
Sep 06 15:51:42 Starting compiler/backend/x64
Sep 06 15:51:43 Finished compiler/backend/x64                                     0s 127MB
Sep 06 15:51:44 Starting compiler/backend/arm7
Sep 06 15:51:46 Finished compiler/backend/arm7                                    0s 126MB
Sep 06 15:51:47 Starting compiler/backend/arm8
Sep 06 15:51:48 Finished compiler/backend/arm8                                    0s 127MB
Sep 06 15:51:49 Starting compiler/backend/mips
Sep 06 15:51:51 Finished compiler/backend/mips                                    0s 127MB
Sep 06 15:51:52 Starting compiler/backend/riscv
Sep 06 15:51:53 Finished compiler/backend/riscv                                   0s 127MB
Sep 06 15:51:54 Starting compiler/backend/ag32
Sep 06 15:53:18 Finished compiler/backend/ag32                                 1m22s   3GB
Sep 06 15:53:19 Starting compiler/parsing/proofs
Sep 06 15:53:20 Finished compiler/parsing/proofs                                  0s  73MB
Sep 06 15:53:21 Starting compiler/inference/proofs
Sep 06 15:53:22 Finished compiler/inference/proofs                                0s  89MB
Sep 06 15:53:23 Starting compiler/backend/semantics
Sep 06 15:54:47 Finished compiler/backend/semantics                            1m23s   2GB
Sep 06 15:54:48 Starting compiler/backend/reg_alloc/proofs
Sep 06 15:54:49 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Sep 06 15:54:50 Starting compiler/backend/proofs
Sep 06 15:55:54 Finished compiler/backend/proofs                               1m03s   5GB
Sep 06 15:55:55 Starting compiler/backend/serialiser
Sep 06 15:55:57 Finished compiler/backend/serialiser                              1s 193MB
Sep 06 15:55:58 Starting compiler/encoders/x64/proofs
Sep 06 16:05:27 Finished compiler/encoders/x64/proofs                          9m27s   5GB
Sep 06 16:05:27 Starting compiler/encoders/arm7/proofs
Sep 06 16:18:39 Finished compiler/encoders/arm7/proofs                        13m11s   8GB
Sep 06 16:18:40 Starting compiler/encoders/arm8/proofs
Sep 06 16:25:00 Finished compiler/encoders/arm8/proofs                         6m19s   4GB
Sep 06 16:25:01 Starting compiler/encoders/arm8_asl/proofs
Sep 06 16:39:00 Finished compiler/encoders/arm8_asl/proofs                    13m57s   4GB
Sep 06 16:39:01 Starting compiler/encoders/mips/proofs
Sep 06 16:49:09 Finished compiler/encoders/mips/proofs                        10m06s   6GB
Sep 06 16:49:10 Starting compiler/encoders/riscv/proofs
Sep 06 16:57:32 Finished compiler/encoders/riscv/proofs                        8m21s   7GB
Sep 06 16:57:33 Starting compiler/encoders/ag32/proofs
Sep 06 16:59:59 Finished compiler/encoders/ag32/proofs                         2m25s   2GB
Sep 06 17:00:00 Starting compiler/backend/x64/proofs
Sep 06 17:00:41 Finished compiler/backend/x64/proofs                             39s   2GB
Sep 06 17:00:42 Starting compiler/backend/arm7/proofs
Sep 06 17:01:26 Finished compiler/backend/arm7/proofs                            43s   2GB
Sep 06 17:01:27 Starting compiler/backend/arm8/proofs
Sep 06 17:02:07 Finished compiler/backend/arm8/proofs                            39s   3GB
Sep 06 17:02:08 Starting compiler/backend/arm8_asl
Sep 06 17:02:36 Finished compiler/backend/arm8_asl                               27s   2GB
Sep 06 17:02:37 Starting compiler/backend/mips/proofs
Sep 06 17:03:21 Finished compiler/backend/mips/proofs                            42s   3GB
Sep 06 17:03:22 Starting compiler/backend/riscv/proofs
Sep 06 17:04:11 Finished compiler/backend/riscv/proofs                           48s   4GB
Sep 06 17:04:12 Starting compiler/backend/ag32/proofs
Sep 06 17:17:18 Finished compiler/backend/ag32/proofs                         13m04s   6GB
Sep 06 17:17:19 Starting candle/set-theory
Sep 06 17:18:03 Finished candle/set-theory                                       43s   1GB
Sep 06 17:18:04 Starting candle/syntax-lib
Sep 06 17:18:05 Finished candle/syntax-lib                                        0s  73MB
Sep 06 17:18:06 Starting candle/standard/syntax
Sep 06 17:18:22 Finished candle/standard/syntax                                  15s   1GB
Sep 06 17:18:23 Starting candle/standard/semantics
Sep 06 17:20:50 Finished candle/standard/semantics                             2m25s   2GB
Sep 06 17:20:50 Starting candle/standard/monadic
Sep 06 17:20:52 Finished candle/standard/monadic                                  0s 100MB
Sep 06 17:20:53 Starting candle/standard/ml_kernel
Sep 06 17:22:43 Finished candle/standard/ml_kernel                             1m49s   5GB
Sep 06 17:22:44 Starting candle/overloading/syntax
Sep 06 17:26:12 Finished candle/overloading/syntax                             3m26s   2GB
Sep 06 17:26:13 Starting candle/overloading/semantics
Sep 06 17:37:31 Finished candle/overloading/semantics                         11m17s   5GB
Sep 06 17:37:32 Starting candle/overloading/monadic
Sep 06 17:40:05 Finished candle/overloading/monadic                            2m31s   2GB
Sep 06 17:40:06 Starting candle/overloading/ml_kernel
Sep 06 17:47:35 Finished candle/overloading/ml_kernel                          7m28s   6GB
Sep 06 17:47:36 Starting candle/overloading/ml_checker
Sep 06 17:50:09 Finished candle/overloading/ml_checker                         2m31s   6GB
Sep 06 17:50:09 Starting candle/prover
Sep 06 18:00:03 Finished candle/prover                                         9m53s   5GB
Sep 06 18:00:04 Starting pancake
Sep 06 18:01:04 Finished pancake                                                 59s   1GB
Sep 06 18:01:05 Starting pancake/ffi
Sep 06 18:01:06 Finished pancake/ffi                                              0s  20MB
Sep 06 18:01:07 Starting pancake/semantics
Sep 06 18:03:23 Finished pancake/semantics                                     2m15s   2GB
Sep 06 18:03:23 Starting pancake/parser
Sep 06 18:03:51 Finished pancake/parser                                          26s   1GB
Sep 06 18:03:52 Starting pancake/proofs
Sep 06 18:33:30 Finished pancake/proofs                                       29m37s   9GB
Sep 06 18:33:31 Starting characteristic/examples
Sep 06 18:35:05 Finished characteristic/examples                               1m33s   6GB
Sep 06 18:35:06 Starting tutorial/solutions
Sep 06 18:50:29 Finished tutorial/solutions                                   15m19s  10GB
Sep 06 18:50:30 Starting translator/monadic/examples
Sep 06 18:54:14 Finished translator/monadic/examples                           3m43s   5GB
Sep 06 18:54:15 Starting examples
Sep 06 19:08:30 Finished examples                                             14m14s   7GB
Sep 06 19:08:31 Starting examples/compilation/x64
Sep 06 21:05:13 Finished examples/compilation/x64                           1h56m39s  21GB
Sep 06 21:05:14 Starting examples/compilation/x64/proofs
Sep 06 21:09:03 Finished examples/compilation/x64/proofs                       3m47s   5GB
Sep 06 21:09:04 Starting examples/compilation/ag32
Sep 06 21:38:42 Finished examples/compilation/ag32                            29m37s  16GB
Sep 06 21:38:43 Starting examples/compilation/ag32/proofs
Sep 06 21:40:08 Finished examples/compilation/ag32/proofs                      1m24s   7GB
Sep 06 21:40:09 Starting examples/compilation/to_word
Sep 06 21:43:56 Finished examples/compilation/to_word                          3m46s  11GB
Sep 06 21:43:57 Starting examples/lpr_checker
Sep 06 21:45:15 Finished examples/lpr_checker                                  1m16s   2GB
Sep 06 21:45:15 Starting examples/lpr_checker/array
Sep 06 22:19:59 Finished examples/lpr_checker/array                           34m41s  13GB
Sep 06 22:20:00 Starting examples/lpr_checker/array/compilation
Sep 06 22:54:57 Finished examples/lpr_checker/array/compilation               34m56s  64GB
Sep 06 22:54:58 Starting examples/lpr_checker/array/compilation/proofs
Sep 06 22:56:51 Finished examples/lpr_checker/array/compilation/proofs         1m52s  10GB
Sep 06 22:56:52 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 06 23:05:40 Finished examples/lpr_checker/array/compilation/proofsARM8     8m47s  45GB
Sep 06 23:05:41 Starting examples/opentheory
Sep 06 23:16:22 Finished examples/opentheory                                  10m40s   7GB
Sep 06 23:16:23 Starting examples/opentheory
Sep 06 23:16:24 Finished examples/opentheory                                      0s 123MB
Sep 06 23:16:25 Starting examples/opentheory/compilation
Sep 06 23:52:18 Finished examples/opentheory/compilation                      35m52s  52GB
Sep 06 23:52:19 Starting examples/opentheory/compilation/proofs
Sep 06 23:53:45 Finished examples/opentheory/compilation/proofs                1m25s   6GB
Sep 06 23:53:46 Starting examples/opentheory/compilation/ag32
Sep 07 00:25:38 Finished examples/opentheory/compilation/ag32                 31m51s  36GB
Sep 07 00:25:39 Starting examples/opentheory/compilation/ag32/proofs
Sep 07 00:27:53 Finished examples/opentheory/compilation/ag32/proofs           2m13s  12GB
Sep 07 00:27:54 Starting examples/sat_encodings
Sep 07 00:30:27 Finished examples/sat_encodings                                2m32s   1GB
Sep 07 00:30:28 Starting examples/sat_encodings/case_studies
Sep 07 00:32:27 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Sep 07 00:32:28 Starting examples/sat_encodings/translation
Sep 07 00:38:33 Finished examples/sat_encodings/translation                    6m04s   7GB
Sep 07 00:38:34 Starting examples/sat_encodings/translation/compilation
Sep 07 01:13:25 Finished examples/sat_encodings/translation/compilation       34m50s  36GB
Sep 07 01:13:26 Starting examples/deflate
Sep 07 01:14:40 Finished examples/deflate                                      1m13s   1GB
Sep 07 01:14:41 Starting examples/deflate/translation
Sep 07 01:16:13 Finished examples/deflate/translation                          1m31s   6GB
Sep 07 01:16:14 Starting examples/deflate/translation/compilation
Sep 07 01:32:41 Finished examples/deflate/translation/compilation             16m26s  23GB
Sep 07 01:32:42 Starting examples/vipr
Sep 07 01:36:46 Finished examples/vipr                                         4m03s   7GB
Sep 07 01:36:47 Starting examples/vipr/compilation
Sep 07 01:57:08 Finished examples/vipr/compilation                            20m20s  37GB
Sep 07 01:57:09 Starting translator/okasaki-examples
Sep 07 02:02:05 Finished translator/okasaki-examples                           4m55s   3GB
Sep 07 02:02:06 Starting translator/other-examples
Sep 07 02:03:15 Finished translator/other-examples                             1m08s   3GB
Sep 07 02:03:16 Starting compiler/parsing/tests
Sep 07 02:03:50 Finished compiler/parsing/tests                                  32s   1GB
Sep 07 02:03:51 Starting compiler/inference/tests
Sep 07 02:11:18 Finished compiler/inference/tests                              7m26s   7GB
Sep 07 02:11:19 Starting compiler/printing/test
Sep 07 02:14:48 Finished compiler/printing/test                                3m27s   6GB
Sep 07 02:14:49 Starting icing/flover
Sep 07 02:50:54 Finished icing/flover                                         36m04s   4GB
Sep 07 02:50:55 Starting icing/
Sep 07 03:47:00 Finished icing/                                               56m03s  30GB
Sep 07 03:47:01 Starting icing/examples
Sep 07 03:48:43 Finished icing/examples                                        1m40s   8GB
Sep 07 03:48:43 Starting compiler/repl
Sep 07 03:57:25 Finished compiler/repl                                         8m41s   8GB
Sep 07 03:57:26 Starting unverified/sexpr-bootstrap/x64/64
Sep 07 04:08:28 Finished unverified/sexpr-bootstrap/x64/64                    11m01s  16GB
Sep 07 04:08:29 Starting unverified/sexpr-bootstrap/x64/32
Sep 07 04:37:13 Finished unverified/sexpr-bootstrap/x64/32                    27m58s  16GB
Sep 07 04:37:17 Starting compiler/benchmarks
Sep 07 04:38:10 Finished compiler/benchmarks                                     48s 713MB
Sep 07 04:38:13 Starting compiler/bootstrap/compilation/x64/64
Sep 07 19:16:14 Finished compiler/bootstrap/compilation/x64/64             14h37m58s 201GB
Sep 07 19:16:14 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 07 19:37:12 Finished compiler/bootstrap/compilation/x64/64/proofs         20m56s  42GB
Sep 07 19:37:12 Starting compiler/bootstrap/compilation/x64/32
Sep 14 01:00:12 Resuming compiler/bootstrap/compilation/x64/32
Sep 14 01:00:15 Finished compiler/bootstrap/compilation/x64/32                    2s 263MB
Sep 14 01:00:15 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 14 01:03:53 Finished compiler/bootstrap/compilation/x64/32/proofs          3m36s  18GB
Sep 14 01:03:54 Starting compiler/bootstrap/compilation/ag32/32
Sep 14 08:37:02 Finished compiler/bootstrap/compilation/ag32/32             7h33m06s 126GB
Sep 14 08:37:03 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 14 08:44:54 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m50s  49GB
Sep 14 08:44:55 SUCCESS