Job 1676

CakeML:d917c7a9f34970d38dc8c798bfed0c0d67fc23b8
  Make evaluateScript.sml more readable [Dec 06 07:32:14]
#849 (delete_terminationTheory)
Merging into:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6
  Merge pull request #847 from CakeML/clos-smart-op [Nov 30 09:57:02]
HOL:6dcb52a09341deda5c5068c06f92c6eaa2af36b6
  emacs-mode: display *Holmake* buffer better when it does its thing [Nov 26 04:28:46]
Machine:oven3 4.19.67.1.amd64-smp

Dec 06 08:11:57 Claimed job
Dec 06 08:12:18 Reusing HOL
Dec 06 08:13:16 Starting developers
Dec 06 08:13:24 Finished developers                                               7s 153MB
Dec 06 08:13:24 Starting developers/bin
Dec 06 08:13:37 Finished developers/bin                                          12s   1GB
Dec 06 08:13:37 Starting semantics/ffi
Dec 06 08:13:56 Finished semantics/ffi                                           18s 247MB
Dec 06 08:13:57 Starting semantics
Dec 06 08:16:45 Finished semantics                                             2m47s   1GB
Dec 06 08:16:45 Starting semantics/proofs
Dec 06 08:24:30 Finished semantics/proofs                                      7m44s   1GB
Dec 06 08:24:30 Starting semantics/alt_semantics
Dec 06 08:24:55 Finished semantics/alt_semantics                                 25s 382MB
Dec 06 08:24:56 Starting semantics/alt_semantics/proofs
Dec 06 08:30:05 Finished semantics/alt_semantics/proofs                        5m09s   1GB
Dec 06 08:30:05 Starting basis/pure
Dec 06 08:31:54 Finished basis/pure                                            1m48s 860MB
Dec 06 08:31:55 Starting translator
Dec 06 08:37:48 Finished translator                                            5m53s   2GB
Dec 06 08:37:49 Starting compiler/parsing
Dec 06 08:40:33 Finished compiler/parsing                                      2m44s   2GB
Dec 06 08:40:33 Starting characteristic
Dec 06 08:52:33 Finished characteristic                                       11m59s   1GB
Dec 06 08:52:34 Starting translator/monadic
Dec 06 08:56:05 Finished translator/monadic                                    3m31s   1GB
Dec 06 08:56:06 Starting basis
Dec 06 10:35:14 Finished basis                                              1h39m08s  15GB
Dec 06 10:35:15 Starting compiler/inference
Dec 06 10:37:40 Finished compiler/inference                                    2m24s   1GB
Dec 06 10:37:40 Starting compiler/backend/reg_alloc
Dec 06 10:39:48 Finished compiler/backend/reg_alloc                            2m07s   1GB
Dec 06 10:39:48 Starting compiler/backend/gc
Dec 06 10:46:28 Finished compiler/backend/gc                                   6m40s   2GB
Dec 06 10:46:29 Starting compiler/backend
Dec 06 10:55:12 Finished compiler/backend                                      8m42s   2GB
Dec 06 10:55:12 Starting compiler/encoders/asm
Dec 06 10:56:04 Finished compiler/encoders/asm                                   51s 686MB
Dec 06 10:56:04 Starting compiler/encoders/x64
Dec 06 10:57:00 Finished compiler/encoders/x64                                   56s 986MB
Dec 06 10:57:01 Starting compiler/encoders/arm7
Dec 06 10:59:35 Finished compiler/encoders/arm7                                2m34s 885MB
Dec 06 10:59:35 Starting compiler/encoders/arm8
Dec 06 11:00:06 Finished compiler/encoders/arm8                                  30s 971MB
Dec 06 11:00:06 Starting compiler/encoders/mips
Dec 06 11:00:43 Finished compiler/encoders/mips                                  37s   1GB
Dec 06 11:00:44 Starting compiler/encoders/riscv
Dec 06 11:01:20 Finished compiler/encoders/riscv                                 36s 794MB
Dec 06 11:01:21 Starting compiler/encoders/ag32
Dec 06 11:02:00 Finished compiler/encoders/ag32                                  39s 689MB
Dec 06 11:02:00 Starting compiler/backend/x64
Dec 06 11:02:40 Finished compiler/backend/x64                                    39s   1GB
Dec 06 11:02:40 Starting compiler/backend/arm7
Dec 06 11:03:28 Finished compiler/backend/arm7                                   47s   1GB
Dec 06 11:03:28 Starting compiler/backend/arm8
Dec 06 11:04:12 Finished compiler/backend/arm8                                   43s   1GB
Dec 06 11:04:12 Starting compiler/backend/mips
Dec 06 11:04:54 Finished compiler/backend/mips                                   41s   1GB
Dec 06 11:04:54 Starting compiler/backend/riscv
Dec 06 11:05:38 Finished compiler/backend/riscv                                  43s   1GB
Dec 06 11:05:39 Starting compiler/backend/ag32
Dec 06 11:08:03 Finished compiler/backend/ag32                                 2m24s   1GB
Dec 06 11:08:04 Starting compiler/parsing/proofs
Dec 06 11:16:16 Finished compiler/parsing/proofs                               8m11s   1GB
Dec 06 11:16:16 Starting compiler/inference/proofs
Dec 06 11:21:30 Finished compiler/inference/proofs                             5m14s   1GB
Dec 06 11:21:30 Starting compiler/backend/semantics
Dec 06 12:22:48 Finished compiler/backend/semantics                         1h01m17s   2GB
Dec 06 12:22:49 Starting compiler/backend/reg_alloc/proofs
Dec 06 12:30:28 Finished compiler/backend/reg_alloc/proofs                     7m38s 979MB
Dec 06 12:30:28 Starting compiler/backend/proofs
Dec 06 14:10:48 Finished compiler/backend/proofs                            1h40m19s  10GB
Dec 06 14:10:48 Starting compiler/backend/serialiser
Dec 06 14:13:19 Finished compiler/backend/serialiser                           2m31s   1GB
Dec 06 14:13:19 Starting compiler/encoders/x64/proofs
Dec 06 14:34:51 Finished compiler/encoders/x64/proofs                         21m31s   5GB
Dec 06 14:34:51 Starting compiler/encoders/arm7/proofs
Dec 06 15:04:19 Finished compiler/encoders/arm7/proofs                        29m27s   3GB
Dec 06 15:04:20 Starting compiler/encoders/arm8/proofs
Dec 06 15:19:54 Finished compiler/encoders/arm8/proofs                        15m32s   1GB
Dec 06 15:19:54 Starting compiler/encoders/mips/proofs
Dec 06 15:42:31 Finished compiler/encoders/mips/proofs                        22m36s   2GB
Dec 06 15:42:31 Starting compiler/encoders/riscv/proofs
Dec 06 16:03:02 Finished compiler/encoders/riscv/proofs                       20m30s   1GB
Dec 06 16:03:03 Starting compiler/encoders/ag32/proofs
Dec 06 16:08:45 Finished compiler/encoders/ag32/proofs                         5m42s 799MB
Dec 06 16:08:46 Starting compiler/backend/x64/proofs
Dec 06 16:09:37 Finished compiler/backend/x64/proofs                             51s   1GB
Dec 06 16:09:37 Starting compiler/backend/arm7/proofs
Dec 06 16:10:30 Finished compiler/backend/arm7/proofs                            52s   1GB
Dec 06 16:10:30 Starting compiler/backend/arm8/proofs
Dec 06 16:11:21 Finished compiler/backend/arm8/proofs                            50s   1GB
Dec 06 16:11:21 Starting compiler/backend/mips/proofs
Dec 06 16:12:12 Finished compiler/backend/mips/proofs                            50s   1GB
Dec 06 16:12:12 Starting compiler/backend/riscv/proofs
Dec 06 16:13:04 Finished compiler/backend/riscv/proofs                           51s   1GB
Dec 06 16:13:04 Starting compiler/backend/ag32/proofs
Dec 06 16:40:46 Finished compiler/backend/ag32/proofs                         27m41s   2GB
Dec 06 16:40:46 Starting compiler/proofs
Dec 06 16:44:33 Finished compiler/proofs                                       3m46s   4GB
Dec 06 16:44:33 Starting candle/set-theory
Dec 06 16:45:31 Finished candle/set-theory                                       57s 755MB
Dec 06 16:45:31 Starting candle/syntax-lib
Dec 06 16:45:56 Finished candle/syntax-lib                                       24s 451MB
Dec 06 16:45:56 Starting candle/standard/syntax
Dec 06 16:49:42 Finished candle/standard/syntax                                3m45s   1GB
Dec 06 16:49:42 Starting candle/standard/semantics
Dec 06 16:53:37 Finished candle/standard/semantics                             3m54s   1GB
Dec 06 16:53:37 Starting candle/standard/monadic
Dec 06 16:57:22 Finished candle/standard/monadic                               3m44s   1GB
Dec 06 16:57:22 Starting candle/standard/ml_kernel
Dec 06 17:08:48 Finished candle/standard/ml_kernel                            11m25s   3GB
Dec 06 17:08:48 Starting candle/overloading/syntax
Dec 06 17:15:23 Finished candle/overloading/syntax                             6m34s   1GB
Dec 06 17:15:23 Starting candle/overloading/semantics
Dec 06 17:41:22 Finished candle/overloading/semantics                         25m58s   2GB
Dec 06 17:41:22 Starting pancake
Dec 06 17:45:15 Finished pancake                                               3m53s   2GB
Dec 06 17:45:15 Starting pancake/ffi
Dec 06 17:45:16 Finished pancake/ffi                                              0s   7MB
Dec 06 17:45:16 Starting pancake/semantics
Dec 06 17:50:04 Finished pancake/semantics                                     4m47s   1GB
Dec 06 17:50:04 Starting pancake/proofs
Dec 06 18:15:48 Finished pancake/proofs                                       25m43s   6GB
Dec 06 18:15:48 Starting characteristic/examples
Dec 06 18:18:48 Finished characteristic/examples                               3m00s   3GB
Dec 06 18:18:48 Starting tutorial/solutions
Dec 06 18:54:47 Finished tutorial/solutions                                   35m58s   9GB
Dec 06 18:54:47 Starting translator/monadic/examples
Dec 06 19:00:44 Finished translator/monadic/examples                           5m56s   2GB
Dec 06 19:00:44 Starting examples
Dec 06 19:18:07 Finished examples                                             17m23s   4GB
Dec 06 19:18:08 Starting examples/compilation/x64
Dec 07 00:48:40 Finished examples/compilation/x64                           5h30m30s  18GB
Dec 07 00:48:40 Starting examples/compilation/x64/proofs
Dec 07 00:52:07 Finished examples/compilation/x64/proofs                       3m26s   3GB
Dec 07 00:52:07 Starting examples/compilation/ag32
Dec 07 02:10:17 Finished examples/compilation/ag32                          1h18m09s  10GB
Dec 07 02:10:17 Starting examples/compilation/ag32/proofs
Dec 07 02:12:00 Finished examples/compilation/ag32/proofs                      1m42s   2GB
Dec 07 02:12:00 Starting examples/cost
Dec 07 04:09:23 Finished examples/cost                                      1h57m22s   8GB
Dec 07 04:09:23 Starting examples/lpr_checker
Dec 07 04:11:06 Finished examples/lpr_checker                                  1m42s   1GB
Dec 07 04:11:07 Starting examples/lpr_checker/array
Dec 07 05:14:45 Finished examples/lpr_checker/array                         1h03m37s   6GB
Dec 07 05:14:45 Starting examples/lpr_checker/array/compilation
Dec 07 08:26:19 Finished examples/lpr_checker/array/compilation             3h11m33s  44GB
Dec 07 08:26:19 Starting examples/lpr_checker/array/compilation/proofs
Dec 07 08:28:50 Finished examples/lpr_checker/array/compilation/proofs         2m30s   6GB
Dec 07 08:28:50 Starting examples/opentheory
Dec 07 08:48:52 Finished examples/opentheory                                  20m02s   5GB
Dec 07 08:48:53 Starting examples/opentheory
Dec 07 08:48:55 Finished examples/opentheory                                      2s  34MB
Dec 07 08:48:55 Starting examples/opentheory/compilation
Dec 07 10:12:50 Finished examples/opentheory/compilation                    1h23m54s  41GB
Dec 07 10:12:50 Starting examples/opentheory/compilation/proofs
Dec 07 10:14:21 Finished examples/opentheory/compilation/proofs                1m30s   4GB
Dec 07 10:14:22 Starting examples/opentheory/compilation/ag32
Dec 07 11:43:52 Finished examples/opentheory/compilation/ag32               1h29m29s  41GB
Dec 07 11:43:52 Starting examples/opentheory/compilation/ag32/proofs
Dec 07 11:47:17 Finished examples/opentheory/compilation/ag32/proofs           3m24s   4GB
Dec 07 11:47:17 Starting examples/sat_encodings
Dec 07 11:51:09 Finished examples/sat_encodings                                3m51s   1GB
Dec 07 11:51:10 Starting examples/sat_encodings/case_studies
Dec 07 11:54:31 Finished examples/sat_encodings/case_studies                   3m21s 780MB
Dec 07 11:54:32 Starting examples/sat_encodings/translation
Dec 07 12:06:02 Finished examples/sat_encodings/translation                   11m29s   4GB
Dec 07 12:06:02 Starting examples/sat_encodings/translation/compilation
Dec 07 13:34:18 Finished examples/sat_encodings/translation/compilation     1h28m15s  22GB
Dec 07 13:34:18 Starting translator/okasaki-examples
Dec 07 13:43:38 Finished translator/okasaki-examples                           9m19s   1GB
Dec 07 13:43:38 Starting translator/other-examples
Dec 07 13:45:00 Finished translator/other-examples                             1m21s   1GB
Dec 07 13:45:01 Starting compiler/parsing/tests
Dec 07 13:46:04 Finished compiler/parsing/tests                                1m03s 596MB
Dec 07 13:46:04 Starting compiler/inference/tests
Dec 07 14:02:09 Finished compiler/inference/tests                             16m04s   5GB
Dec 07 14:02:10 Starting compiler/bootstrap/translation
Dec 07 19:32:56 Finished compiler/bootstrap/translation                     5h30m45s  26GB
Dec 07 19:32:56 Starting unverified/sexpr-bootstrap/x64/64
Dec 07 19:57:28 Finished unverified/sexpr-bootstrap/x64/64                    24m31s   8GB
Dec 07 19:57:28 Starting unverified/sexpr-bootstrap/x64/32
Dec 07 20:18:23 Finished unverified/sexpr-bootstrap/x64/32                    20m54s   8GB
Dec 07 20:18:23 Starting compiler/benchmarks
Dec 07 20:18:27 Finished compiler/benchmarks                                      4s  34MB
Dec 07 20:18:28 Starting compiler/bootstrap/compilation/x64/64
Dec 09 03:59:32 Finished compiler/bootstrap/compilation/x64/64             31h41m03s 116GB
Dec 09 03:59:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 09 04:04:11 Finished compiler/bootstrap/compilation/x64/64/proofs          4m38s  15GB
Dec 09 04:04:11 Starting compiler/bootstrap/compilation/x64/32
Dec 10 05:14:56 Finished compiler/bootstrap/compilation/x64/32             25h10m43s 110GB
Dec 10 05:14:56 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 10 05:19:20 Finished compiler/bootstrap/compilation/x64/32/proofs          4m24s  18GB
Dec 10 05:19:21 Starting compiler/bootstrap/compilation/ag32/32
Dec 11 06:00:59 Finished compiler/bootstrap/compilation/ag32/32            24h41m37s  96GB
Dec 11 06:01:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 11 06:21:27 Finished compiler/bootstrap/compilation/ag32/32/proofs        20m27s  41GB
Dec 11 06:21:28 SUCCESS