Job 1890

CakeML:f49dcaf134cf3038907bd8cfe02a1dc5849938f2
  Fix some more REPL-related proofs [May 06 07:53:04]
#865 (Iced_cake)
Merging into:d49028c882e2061b0b85fe1f775e9d1c157b9b23
  Merge pull request #882 from mktnk3/time_to_pan_cleanup [May 02 07:00:59]
HOL:9ef7738eaecdb725492f0929f6b270d1f4e63a40
  Teach Holmake and Parse.sml about the tmux terminal [Apr 28 21:56:05]
Machine:oven3

May 06 07:53:56 Claimed job
May 06 07:53:58 Reusing HOL
May 06 07:54:51 Starting developers
May 06 07:55:01 Finished developers                                               9s 177MB
May 06 07:55:01 Starting developers/bin
May 06 07:55:14 Finished developers/bin                                          12s   1GB
May 06 07:55:14 Starting semantics/ffi
May 06 07:55:39 Finished semantics/ffi                                           24s 242MB
May 06 07:55:39 Starting semantics
May 06 08:00:38 Finished semantics                                             4m58s   1GB
May 06 08:00:39 Starting semantics/proofs
May 06 08:16:14 Finished semantics/proofs                                     15m35s   1GB
May 06 08:16:14 Starting semantics/alt_semantics
May 06 08:17:13 Finished semantics/alt_semantics                                 58s 548MB
May 06 08:17:13 Starting semantics/alt_semantics/proofs
May 06 08:42:44 Finished semantics/alt_semantics/proofs                       25m30s   1GB
May 06 08:42:44 Starting basis/pure
May 06 08:44:56 Finished basis/pure                                            2m11s   1GB
May 06 08:44:56 Starting translator
May 06 08:52:55 Finished translator                                            7m59s   1GB
May 06 08:52:56 Starting compiler/parsing
May 06 08:55:47 Finished compiler/parsing                                      2m50s   4GB
May 06 08:55:47 Starting characteristic
May 06 09:10:36 Finished characteristic                                       14m48s   1GB
May 06 09:10:36 Starting translator/monadic
May 06 09:14:51 Finished translator/monadic                                    4m14s   1GB
May 06 09:14:51 Starting basis
May 06 11:08:47 Finished basis                                              1h53m55s  15GB
May 06 11:08:48 Starting compiler/inference
May 06 11:11:58 Finished compiler/inference                                    3m10s   1GB
May 06 11:11:58 Starting compiler/backend/reg_alloc
May 06 11:15:14 Finished compiler/backend/reg_alloc                            3m16s   1GB
May 06 11:15:14 Starting compiler/backend/gc
May 06 11:23:45 Finished compiler/backend/gc                                   8m30s   2GB
May 06 11:23:45 Starting compiler/backend
May 06 11:35:10 Finished compiler/backend                                     11m24s   2GB
May 06 11:35:10 Starting compiler/encoders/asm
May 06 11:36:16 Finished compiler/encoders/asm                                 1m05s 745MB
May 06 11:36:16 Starting compiler/encoders/x64
May 06 11:37:20 Finished compiler/encoders/x64                                 1m03s 989MB
May 06 11:37:20 Starting compiler/encoders/arm7
May 06 11:39:25 Finished compiler/encoders/arm7                                2m04s 837MB
May 06 11:39:26 Starting compiler/encoders/arm8
May 06 11:40:02 Finished compiler/encoders/arm8                                  36s 706MB
May 06 11:40:02 Starting compiler/encoders/arm8_asl
May 06 11:47:37 Finished compiler/encoders/arm8_asl                            7m34s   1GB
May 06 11:47:37 Starting compiler/encoders/mips
May 06 11:48:21 Finished compiler/encoders/mips                                  43s   1GB
May 06 11:48:21 Starting compiler/encoders/riscv
May 06 11:49:00 Finished compiler/encoders/riscv                                 39s 889MB
May 06 11:49:01 Starting compiler/encoders/ag32
May 06 11:49:51 Finished compiler/encoders/ag32                                  50s 637MB
May 06 11:49:51 Starting compiler/backend/x64
May 06 11:50:39 Finished compiler/backend/x64                                    47s   1GB
May 06 11:50:39 Starting compiler/backend/arm7
May 06 11:51:33 Finished compiler/backend/arm7                                   54s   1GB
May 06 11:51:34 Starting compiler/backend/arm8
May 06 11:52:23 Finished compiler/backend/arm8                                   49s   1GB
May 06 11:52:23 Starting compiler/backend/mips
May 06 11:53:14 Finished compiler/backend/mips                                   51s   1GB
May 06 11:53:15 Starting compiler/backend/riscv
May 06 11:54:05 Finished compiler/backend/riscv                                  50s   1GB
May 06 11:54:05 Starting compiler/backend/ag32
May 06 11:57:05 Finished compiler/backend/ag32                                 2m59s   1GB
May 06 11:57:05 Starting compiler/parsing/proofs
May 06 12:05:33 Finished compiler/parsing/proofs                               8m27s   1GB
May 06 12:05:33 Starting compiler/inference/proofs
May 06 12:11:31 Finished compiler/inference/proofs                             5m56s   1GB
May 06 12:11:31 Starting compiler/backend/semantics
May 06 13:22:41 Finished compiler/backend/semantics                         1h11m08s   2GB
May 06 13:22:41 Starting compiler/backend/reg_alloc/proofs
May 06 13:30:34 Finished compiler/backend/reg_alloc/proofs                     7m52s   1GB
May 06 13:30:34 Starting compiler/backend/proofs
May 06 15:17:45 Finished compiler/backend/proofs                            1h47m10s  15GB
May 06 15:17:46 Starting compiler/backend/serialiser
May 06 15:21:12 Finished compiler/backend/serialiser                           3m26s   1GB
May 06 15:21:13 Starting compiler/encoders/x64/proofs
May 06 15:42:38 Finished compiler/encoders/x64/proofs                         21m25s   4GB
May 06 15:42:39 Starting compiler/encoders/arm7/proofs
May 06 16:12:01 Finished compiler/encoders/arm7/proofs                        29m22s   3GB
May 06 16:12:01 Starting compiler/encoders/arm8/proofs
May 06 16:27:42 Finished compiler/encoders/arm8/proofs                        15m40s   1GB
May 06 16:27:42 Starting compiler/encoders/arm8_asl/proofs
May 06 17:03:32 Finished compiler/encoders/arm8_asl/proofs                    35m49s   1GB
May 06 17:03:32 Starting compiler/encoders/mips/proofs
May 06 17:26:27 Finished compiler/encoders/mips/proofs                        22m54s   3GB
May 06 17:26:27 Starting compiler/encoders/riscv/proofs
May 06 17:46:36 Finished compiler/encoders/riscv/proofs                       20m08s   1GB
May 06 17:46:36 Starting compiler/encoders/ag32/proofs
May 06 17:52:26 Finished compiler/encoders/ag32/proofs                         5m49s 860MB
May 06 17:52:26 Starting compiler/backend/x64/proofs
May 06 17:53:29 Finished compiler/backend/x64/proofs                           1m02s   1GB
May 06 17:53:29 Starting compiler/backend/arm7/proofs
May 06 17:54:36 Finished compiler/backend/arm7/proofs                          1m06s   1GB
May 06 17:54:36 Starting compiler/backend/arm8/proofs
May 06 17:55:38 Finished compiler/backend/arm8/proofs                          1m01s   1GB
May 06 17:55:38 Starting compiler/backend/arm8_asl
May 06 17:56:30 Finished compiler/backend/arm8_asl                               51s   1GB
May 06 17:56:30 Starting compiler/backend/mips/proofs
May 06 17:57:30 Finished compiler/backend/mips/proofs                            59s   1GB
May 06 17:57:31 Starting compiler/backend/riscv/proofs
May 06 17:58:33 Finished compiler/backend/riscv/proofs                         1m01s   2GB
May 06 17:58:33 Starting compiler/backend/ag32/proofs
May 06 18:29:11 Finished compiler/backend/ag32/proofs                         30m38s   2GB
May 06 18:29:11 Starting compiler/proofs
May 06 18:33:52 Finished compiler/proofs                                       4m40s   3GB
May 06 18:33:52 Starting candle/set-theory
May 06 18:35:03 Finished candle/set-theory                                     1m10s 894MB
May 06 18:35:03 Starting candle/syntax-lib
May 06 18:35:32 Finished candle/syntax-lib                                       28s 696MB
May 06 18:35:32 Starting candle/standard/syntax
May 06 18:39:52 Finished candle/standard/syntax                                4m19s   1GB
May 06 18:39:52 Starting candle/standard/semantics
May 06 18:43:57 Finished candle/standard/semantics                             4m04s   1GB
May 06 18:43:57 Starting candle/standard/monadic
May 06 18:47:57 Finished candle/standard/monadic                               3m59s   1GB
May 06 18:47:57 Starting candle/standard/ml_kernel
May 06 19:01:50 Finished candle/standard/ml_kernel                            13m52s   4GB
May 06 19:01:50 Starting candle/overloading/syntax
May 06 19:08:51 Finished candle/overloading/syntax                             7m00s   1GB
May 06 19:08:51 Starting candle/overloading/semantics
May 06 19:35:01 Finished candle/overloading/semantics                         26m10s   2GB
May 06 19:35:02 Starting candle/overloading/monadic
May 06 19:40:30 Finished candle/overloading/monadic                            5m28s   1GB
May 06 19:40:30 Starting candle/overloading/ml_kernel
May 06 19:56:32 Finished candle/overloading/ml_kernel                         16m00s   4GB
May 06 19:56:32 Starting candle/overloading/ml_checker
May 06 20:01:53 Finished candle/overloading/ml_checker                         5m20s   3GB
May 06 20:01:53 Starting candle/prover
May 06 20:29:38 Finished candle/prover                                        27m45s   3GB
May 06 20:29:38 Starting pancake
May 06 20:37:18 Finished pancake                                               7m39s   2GB
May 06 20:37:18 Starting pancake/ffi
May 06 20:37:19 Finished pancake/ffi                                              0s  29MB
May 06 20:37:19 Starting pancake/semantics
May 06 20:42:48 Finished pancake/semantics                                     5m28s   1GB
May 06 20:42:48 Starting pancake/proofs
May 06 21:09:30 Finished pancake/proofs                                       26m41s   6GB
May 06 21:09:30 Starting characteristic/examples
May 06 21:12:30 Finished characteristic/examples                               2m59s   3GB
May 06 21:12:30 Starting tutorial/solutions
May 06 21:50:05 Finished tutorial/solutions                                   37m33s  11GB
May 06 21:50:05 Starting translator/monadic/examples
May 06 21:57:05 Finished translator/monadic/examples                           7m00s   2GB
May 06 21:57:06 Starting examples
May 06 22:16:40 Finished examples                                             19m34s   4GB
May 06 22:16:40 Starting examples/compilation/x64
May 07 03:54:41 Finished examples/compilation/x64                           5h38m00s  22GB
May 07 03:54:42 Starting examples/compilation/x64/proofs
May 07 03:59:39 Finished examples/compilation/x64/proofs                       4m56s   3GB
May 07 03:59:39 Starting examples/compilation/ag32
May 07 05:18:04 Finished examples/compilation/ag32                          1h18m24s   9GB
May 07 05:18:05 Starting examples/compilation/ag32/proofs
May 07 05:20:01 Finished examples/compilation/ag32/proofs                      1m56s   2GB
May 07 05:20:02 Starting examples/cost
May 07 07:26:38 Finished examples/cost                                      2h06m36s   8GB
May 07 07:26:38 Starting examples/lpr_checker
May 07 07:28:50 Finished examples/lpr_checker                                  2m11s   1GB
May 07 07:28:50 Starting examples/lpr_checker/array
May 07 08:44:06 Finished examples/lpr_checker/array                         1h15m16s   5GB
May 07 08:44:07 Starting examples/lpr_checker/array/compilation
May 07 11:44:24 Finished examples/lpr_checker/array/compilation             3h00m16s  35GB
May 07 11:44:24 Starting examples/lpr_checker/array/compilation/proofs
May 07 11:47:33 Finished examples/lpr_checker/array/compilation/proofs         3m08s   7GB
May 07 11:47:33 Starting examples/opentheory
May 07 12:10:24 Finished examples/opentheory                                  22m50s   5GB
May 07 12:10:24 Starting examples/opentheory
May 07 12:10:27 Finished examples/opentheory                                      2s  34MB
May 07 12:10:28 Starting examples/opentheory/compilation
May 07 13:46:26 Finished examples/opentheory/compilation                    1h35m57s  37GB
May 07 13:46:26 Starting examples/opentheory/compilation/proofs
May 07 13:48:21 Finished examples/opentheory/compilation/proofs                1m54s   4GB
May 07 13:48:21 Starting examples/opentheory/compilation/ag32
May 07 15:17:13 Finished examples/opentheory/compilation/ag32               1h28m50s  40GB
May 07 15:17:13 Starting examples/opentheory/compilation/ag32/proofs
May 07 15:21:18 Finished examples/opentheory/compilation/ag32/proofs           4m05s   6GB
May 07 15:21:19 Starting examples/sat_encodings
May 07 15:25:40 Finished examples/sat_encodings                                4m21s 776MB
May 07 15:25:40 Starting examples/sat_encodings/case_studies
May 07 15:29:20 Finished examples/sat_encodings/case_studies                   3m39s 893MB
May 07 15:29:20 Starting examples/sat_encodings/translation
May 07 15:41:18 Finished examples/sat_encodings/translation                   11m57s   3GB
May 07 15:41:18 Starting examples/sat_encodings/translation/compilation
May 07 17:08:39 Finished examples/sat_encodings/translation/compilation     1h27m20s  20GB
May 07 17:08:39 Starting translator/okasaki-examples
May 07 17:19:08 Finished translator/okasaki-examples                          10m28s   2GB
May 07 17:19:09 Starting translator/other-examples
May 07 17:20:42 Finished translator/other-examples                             1m33s   1GB
May 07 17:20:43 Starting compiler/parsing/tests
May 07 17:21:52 Finished compiler/parsing/tests                                1m09s 596MB
May 07 17:21:52 Starting compiler/inference/tests
May 07 17:38:24 Finished compiler/inference/tests                             16m31s   6GB
May 07 17:38:24 Starting compiler/printing/test
May 07 17:46:02 Finished compiler/printing/test                                7m37s   3GB
May 07 17:46:02 Starting icing/flover
May 07 18:13:44 Finished icing/flover                                         27m41s   1GB
May 07 18:13:44 Starting icing/
May 07 20:27:42 Finished icing/                                             2h13m57s   7GB
May 07 20:27:42 Starting icing/examples
May 07 20:30:44 Finished icing/examples                                        3m02s   3GB
May 07 20:30:45 Starting compiler/repl
May 07 20:56:49 Finished compiler/repl                                        26m04s   6GB
May 07 20:56:49 Starting compiler/bootstrap/translation
May 08 06:12:00 Finished compiler/bootstrap/translation                     9h15m08s  52GB
May 08 06:12:00 Starting unverified/sexpr-bootstrap/x64/64
May 08 06:35:35 Finished unverified/sexpr-bootstrap/x64/64                    23m35s  12GB
May 08 06:35:35 Starting unverified/sexpr-bootstrap/x64/32
May 08 06:54:26 Finished unverified/sexpr-bootstrap/x64/32                    18m50s  10GB
May 08 06:54:26 Starting compiler/benchmarks
May 08 06:54:32 Finished compiler/benchmarks                                      5s  56MB
May 08 06:54:32 Starting compiler/bootstrap/compilation/x64/64 May 08 06:54:32 2641s