Job 3422

CakeML:d4ce405e105cef3b7901d0f89694c41597bb8b22
  Merge pull request #1431 from CakeML/pb_str_to_core [Jul 04 16:05:56]
HOL:1d9f33ad168d3823cc070223d83ea660d86dcb58
  Invert ParoundPrec, and use it to bracket stacked suffixes [Jun 24 01:00:44]
Machine:pavlova

Jul 04 16:20:07 Claimed job
Jul 04 16:20:11 Reusing HOL
Jul 04 16:21:06 Starting developers
Jul 04 16:21:11 Finished developers                                               4s 159MB
Jul 04 16:21:12 Starting developers/bin
Jul 04 16:21:15 Finished developers/bin                                           2s  93MB
Jul 04 16:21:16 Starting misc
Jul 04 16:21:59 Finished misc                                                    42s   1GB
Jul 04 16:22:00 Starting compiler/proofs
Jul 04 17:33:04 Finished compiler/proofs                                    1h11m02s  11GB
Jul 04 17:33:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 05 00:16:19 Finished compiler/bootstrap/compilation/x64/64/proofs       6h43m13s  85GB
Jul 05 00:16:20 Starting semantics/ffi
Jul 05 00:16:32 Finished semantics/ffi                                           11s 538MB
Jul 05 00:16:32 Starting semantics
Jul 05 00:16:34 Finished semantics                                                0s  87MB
Jul 05 00:16:35 Starting semantics/proofs
Jul 05 00:16:59 Finished semantics/proofs                                        22s 722MB
Jul 05 00:16:59 Starting semantics/alt_semantics
Jul 05 00:17:16 Finished semantics/alt_semantics                                 15s 574MB
Jul 05 00:17:17 Starting semantics/alt_semantics/proofs
Jul 05 00:21:04 Finished semantics/alt_semantics/proofs                        3m46s   1GB
Jul 05 00:21:05 Starting basis/pure
Jul 05 00:21:06 Finished basis/pure                                               0s  79MB
Jul 05 00:21:07 Starting translator
Jul 05 00:22:16 Finished translator                                            1m07s   2GB
Jul 05 00:22:16 Starting compiler/parsing
Jul 05 00:23:02 Finished compiler/parsing                                        45s   2GB
Jul 05 00:23:03 Starting characteristic
Jul 05 00:23:05 Finished characteristic                                           1s 118MB
Jul 05 00:23:06 Starting translator/monadic
Jul 05 00:23:08 Finished translator/monadic                                       0s 112MB
Jul 05 00:23:09 Starting translator/monadic/monad_base
Jul 05 00:23:10 Finished translator/monadic/monad_base                            0s  86MB
Jul 05 00:23:11 Starting profiler
Jul 05 00:23:40 Finished profiler                                                28s   1GB
Jul 05 00:23:41 Starting basis
Jul 05 00:25:25 Finished basis                                                 1m42s   4GB
Jul 05 00:25:25 Starting compiler
Jul 05 00:25:28 Finished compiler                                                 1s 228MB
Jul 05 00:25:29 Starting compiler/inference
Jul 05 00:25:31 Finished compiler/inference                                       0s 117MB
Jul 05 00:25:31 Starting compiler/backend/reg_alloc
Jul 05 00:25:33 Finished compiler/backend/reg_alloc                               0s  86MB
Jul 05 00:25:34 Starting compiler/backend/gc
Jul 05 00:25:36 Finished compiler/backend/gc                                      1s 134MB
Jul 05 00:25:37 Starting compiler/backend
Jul 05 00:25:39 Finished compiler/backend                                         1s 133MB
Jul 05 00:25:39 Starting compiler/encoders/asm
Jul 05 00:25:41 Finished compiler/encoders/asm                                    0s 100MB
Jul 05 00:25:42 Starting compiler/encoders/x64
Jul 05 00:25:44 Finished compiler/encoders/x64                                    0s 103MB
Jul 05 00:25:44 Starting compiler/encoders/arm7
Jul 05 00:25:46 Finished compiler/encoders/arm7                                   0s 106MB
Jul 05 00:25:47 Starting compiler/encoders/arm8
Jul 05 00:25:49 Finished compiler/encoders/arm8                                   0s  95MB
Jul 05 00:25:49 Starting compiler/encoders/arm8_asl
Jul 05 00:26:07 Finished compiler/encoders/arm8_asl                              16s   1GB
Jul 05 00:26:08 Starting compiler/encoders/mips
Jul 05 00:26:10 Finished compiler/encoders/mips                                   0s  99MB
Jul 05 00:26:10 Starting compiler/encoders/riscv
Jul 05 00:26:12 Finished compiler/encoders/riscv                                  0s  99MB
Jul 05 00:26:13 Starting compiler/encoders/ag32
Jul 05 00:26:15 Finished compiler/encoders/ag32                                   0s 101MB
Jul 05 00:26:16 Starting compiler/encoders/tests
Jul 05 00:26:17 Finished compiler/encoders/tests                                  1s 126MB
Jul 05 00:26:18 Starting compiler/encoders/monadic_enc
Jul 05 00:26:41 Finished compiler/encoders/monadic_enc                           21s   1GB
Jul 05 00:26:41 Starting compiler/backend/x64
Jul 05 00:26:43 Finished compiler/backend/x64                                     1s 133MB
Jul 05 00:26:44 Starting compiler/backend/arm7
Jul 05 00:26:46 Finished compiler/backend/arm7                                    1s 132MB
Jul 05 00:26:47 Starting compiler/backend/arm8
Jul 05 00:26:49 Finished compiler/backend/arm8                                    1s 133MB
Jul 05 00:26:50 Starting compiler/backend/mips
Jul 05 00:26:52 Finished compiler/backend/mips                                    1s 133MB
Jul 05 00:26:52 Starting compiler/backend/riscv
Jul 05 00:26:54 Finished compiler/backend/riscv                                   1s 134MB
Jul 05 00:26:55 Starting compiler/backend/ag32
Jul 05 00:27:57 Finished compiler/backend/ag32                                 1m00s   1GB
Jul 05 00:27:58 Starting compiler/backend/pattern_matching
Jul 05 00:27:59 Finished compiler/backend/pattern_matching                        0s  91MB
Jul 05 00:28:00 Starting compiler/parsing/ocaml
Jul 05 00:30:08 Finished compiler/parsing/ocaml                                2m07s   1GB
Jul 05 00:30:09 Starting compiler/printing
Jul 05 00:31:05 Finished compiler/printing                                       55s   1GB
Jul 05 00:31:06 Starting compiler/parsing/proofs
Jul 05 00:31:08 Finished compiler/parsing/proofs                                  0s  98MB
Jul 05 00:31:09 Starting compiler/inference/proofs
Jul 05 00:31:11 Finished compiler/inference/proofs                                0s 114MB
Jul 05 00:31:12 Starting compiler/backend/semantics
Jul 05 00:34:17 Finished compiler/backend/semantics                            3m04s   3GB
Jul 05 00:34:17 Starting compiler/backend/reg_alloc/proofs
Jul 05 00:34:19 Finished compiler/backend/reg_alloc/proofs                        1s 116MB
Jul 05 00:34:20 Starting compiler/backend/proofs
Jul 05 00:35:03 Finished compiler/backend/proofs                                 41s   1GB
Jul 05 00:35:04 Starting compiler/backend/serialiser
Jul 05 00:35:06 Finished compiler/backend/serialiser                              1s 144MB
Jul 05 00:35:07 Starting compiler/encoders/x64/proofs
Jul 05 00:35:09 Finished compiler/encoders/x64/proofs                             0s 108MB
Jul 05 00:35:09 Starting compiler/encoders/arm7/proofs
Jul 05 00:47:30 Finished compiler/encoders/arm7/proofs                        12m20s   5GB
Jul 05 00:47:31 Starting compiler/encoders/arm8/proofs
Jul 05 00:55:25 Finished compiler/encoders/arm8/proofs                         7m52s   3GB
Jul 05 00:55:25 Starting compiler/encoders/arm8_asl/proofs
Jul 05 01:12:48 Finished compiler/encoders/arm8_asl/proofs                    17m21s   3GB
Jul 05 01:12:49 Starting compiler/encoders/mips/proofs
Jul 05 01:23:36 Finished compiler/encoders/mips/proofs                        10m44s   8GB
Jul 05 01:23:36 Starting compiler/encoders/riscv/proofs
Jul 05 01:33:04 Finished compiler/encoders/riscv/proofs                        9m26s   4GB
Jul 05 01:33:05 Starting compiler/encoders/ag32/proofs
Jul 05 01:36:12 Finished compiler/encoders/ag32/proofs                         3m06s   1GB
Jul 05 01:36:12 Starting compiler/backend/x64/proofs
Jul 05 01:36:15 Finished compiler/backend/x64/proofs                              1s 216MB
Jul 05 01:36:16 Starting compiler/backend/arm7/proofs
Jul 05 01:36:53 Finished compiler/backend/arm7/proofs                            36s   2GB
Jul 05 01:36:54 Starting compiler/backend/arm8/proofs
Jul 05 01:37:33 Finished compiler/backend/arm8/proofs                            37s   2GB
Jul 05 01:37:33 Starting compiler/backend/arm8_asl
Jul 05 01:37:58 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 05 01:37:59 Starting compiler/backend/mips/proofs
Jul 05 01:38:41 Finished compiler/backend/mips/proofs                            41s   2GB
Jul 05 01:38:42 Starting compiler/backend/riscv/proofs
Jul 05 01:39:23 Finished compiler/backend/riscv/proofs                           39s   2GB
Jul 05 01:39:24 Starting compiler/backend/ag32/proofs
Jul 05 01:48:55 Finished compiler/backend/ag32/proofs                          9m30s   5GB
Jul 05 01:48:56 Starting compiler/backend/cv_compute
Jul 05 01:49:26 Finished compiler/backend/cv_compute                             29s   1GB
Jul 05 01:49:27 Starting cv_translator
Jul 05 01:54:23 Finished cv_translator                                         4m55s   3GB
Jul 05 01:54:24 Starting candle
Jul 05 01:54:25 Finished candle                                                   0s   7MB
Jul 05 01:54:26 Starting candle/set-theory
Jul 05 01:54:57 Finished candle/set-theory                                       30s 937MB
Jul 05 01:54:57 Starting candle/syntax-lib
Jul 05 01:54:59 Finished candle/syntax-lib                                        0s  78MB
Jul 05 01:55:00 Starting candle/standard
Jul 05 01:55:01 Finished candle/standard                                          0s   7MB
Jul 05 01:55:01 Starting candle/standard/syntax
Jul 05 01:55:16 Finished candle/standard/syntax                                  14s 811MB
Jul 05 01:55:17 Starting candle/standard/syntax/little_theories
Jul 05 01:56:29 Finished candle/standard/syntax/little_theories                1m11s 985MB
Jul 05 01:56:30 Starting candle/standard/semantics
Jul 05 01:58:44 Finished candle/standard/semantics                             2m13s   1GB
Jul 05 01:58:45 Starting candle/standard/monadic
Jul 05 01:58:47 Finished candle/standard/monadic                                  0s 122MB
Jul 05 01:58:48 Starting candle/standard/ml_kernel
Jul 05 02:01:14 Finished candle/standard/ml_kernel                             2m25s   3GB
Jul 05 02:01:15 Starting candle/overloading
Jul 05 02:01:16 Finished candle/overloading                                       0s   6MB
Jul 05 02:01:17 Starting candle/overloading/syntax
Jul 05 02:04:26 Finished candle/overloading/syntax                             3m08s   2GB
Jul 05 02:04:27 Starting candle/overloading/semantics
Jul 05 02:14:05 Finished candle/overloading/semantics                          9m37s   4GB
Jul 05 02:14:06 Starting candle/overloading/monadic
Jul 05 02:16:09 Finished candle/overloading/monadic                            2m02s   1GB
Jul 05 02:16:10 Starting candle/overloading/ml_kernel
Jul 05 02:22:52 Finished candle/overloading/ml_kernel                          6m41s   6GB
Jul 05 02:22:53 Starting candle/overloading/ml_checker
Jul 05 02:25:36 Finished candle/overloading/ml_checker                         2m42s   6GB
Jul 05 02:25:37 Starting candle/prover
Jul 05 02:25:39 Finished candle/prover                                            1s 183MB
Jul 05 02:25:40 Starting candle/prover/compute
Jul 05 02:25:42 Finished candle/prover/compute                                    1s 157MB
Jul 05 02:25:43 Starting pancake
Jul 05 02:25:45 Finished pancake                                                  1s 148MB
Jul 05 02:25:46 Starting pancake/semantics
Jul 05 02:28:41 Finished pancake/semantics                                     2m54s   2GB
Jul 05 02:28:42 Starting pancake/parser
Jul 05 02:29:24 Finished pancake/parser                                          41s 487MB
Jul 05 02:29:25 Starting pancake/static_checker
Jul 05 02:31:58 Finished pancake/static_checker                                2m33s   1GB
Jul 05 02:31:59 Starting pancake/proofs
Jul 05 02:49:22 Finished pancake/proofs                                       17m22s   4GB
Jul 05 02:49:23 Starting compiler/dafny
Jul 05 02:49:46 Finished compiler/dafny                                          22s 664MB
Jul 05 02:49:47 Starting compiler/dafny/translation
Jul 05 03:00:51 Finished compiler/dafny/translation                           11m02s   7GB
Jul 05 03:00:52 Starting compiler/dafny/compilation
Jul 05 03:02:39 Finished compiler/dafny/compilation                            1m46s   6GB
Jul 05 03:02:40 Starting compiler/dafny/semantics
Jul 05 03:03:19 Finished compiler/dafny/semantics                                37s 492MB
Jul 05 03:03:20 Starting compiler/dafny/proofs
Jul 05 03:04:59 Finished compiler/dafny/proofs                                 1m37s   1GB
Jul 05 03:04:59 Starting compiler/dafny/vcg
Jul 05 03:05:01 Finished compiler/dafny/vcg                                       0s  98MB
Jul 05 03:05:02 Starting compiler/dafny/vcg/examples
Jul 05 03:05:31 Finished compiler/dafny/vcg/examples                             28s   1GB
Jul 05 03:05:32 Starting compiler/scheme
Jul 05 03:05:58 Finished compiler/scheme                                         25s   1GB
Jul 05 03:05:59 Starting compiler/scheme/translation
Jul 05 03:12:42 Finished compiler/scheme/translation                           6m42s   7GB
Jul 05 03:12:43 Starting compiler/scheme/compilation
Jul 05 03:14:08 Finished compiler/scheme/compilation                           1m23s   4GB
Jul 05 03:14:09 Starting compiler/scheme/proofs
Jul 05 03:20:59 Finished compiler/scheme/proofs                                6m49s   2GB
Jul 05 03:21:00 Starting characteristic/examples
Jul 05 03:22:32 Finished characteristic/examples                               1m30s   5GB
Jul 05 03:22:32 Starting tutorial/solutions
Jul 05 03:25:15 Finished tutorial/solutions                                    2m42s   3GB
Jul 05 03:25:16 Starting translator/monadic/examples Jul 05 03:25:16 174s