Job 2646

CakeML:98c4d6ad8ca77ba1ee9337863d031be6cf1268fa
  Remove some Define usages manually [Oct 08 18:20:21]
#1064 (remove-define)
Merging into:5dbca0ecc3929b5a56eadc76a2edd977f109ad1e
  Merge pull request #1066 from CakeML/remove-old-datatype [Oct 09 11:35:19]
HOL:277f6ad618617d462cd4ad2955206cb261828f87
  Add proofs about clock for fun-op-sem/imp (#1310) [Oct 03 07:36:31]
Machine:lammmington

Oct 09 11:37:42 Claimed job
Oct 09 11:37:46 Reusing HOL
Oct 09 11:37:58 Starting developers
Oct 09 11:38:02 Finished developers                                               3s 200MB
Oct 09 11:38:03 Starting developers/bin
Oct 09 11:38:24 Finished developers/bin                                          19s   1GB
Oct 09 11:38:25 Starting compiler/proofs
Oct 09 13:23:58 Finished compiler/proofs                                    1h45m31s  42GB
Oct 09 13:23:59 Starting compiler/bootstrap/translation
Oct 09 22:20:24 Finished compiler/bootstrap/translation                     8h56m24s  58GB
Oct 09 22:20:25 Starting semantics/ffi
Oct 09 22:20:35 Finished semantics/ffi                                            8s 644MB
Oct 09 22:20:36 Starting semantics
Oct 09 22:20:37 Finished semantics                                                0s  68MB
Oct 09 22:20:38 Starting semantics/proofs
Oct 09 22:21:02 Finished semantics/proofs                                        23s 823MB
Oct 09 22:21:03 Starting semantics/alt_semantics
Oct 09 22:21:26 Finished semantics/alt_semantics                                 22s 665MB
Oct 09 22:21:27 Starting semantics/alt_semantics/proofs
Oct 09 22:31:56 Finished semantics/alt_semantics/proofs                       10m28s   4GB
Oct 09 22:31:57 Starting basis/pure
Oct 09 22:31:59 Finished basis/pure                                               0s  70MB
Oct 09 22:31:59 Starting translator
Oct 09 22:33:36 Finished translator                                            1m35s   4GB
Oct 09 22:33:37 Starting compiler/parsing
Oct 09 22:33:39 Finished compiler/parsing                                         0s  72MB
Oct 09 22:33:39 Starting characteristic
Oct 09 22:33:41 Finished characteristic                                           0s  90MB
Oct 09 22:33:42 Starting translator/monadic
Oct 09 22:33:44 Finished translator/monadic                                       0s  93MB
Oct 09 22:33:45 Starting basis
Oct 09 22:36:23 Finished basis                                                 2m37s   9GB
Oct 09 22:36:24 Starting compiler/inference
Oct 09 22:36:26 Finished compiler/inference                                       0s 103MB
Oct 09 22:36:27 Starting compiler/backend/reg_alloc
Oct 09 22:36:28 Finished compiler/backend/reg_alloc                               0s  67MB
Oct 09 22:36:29 Starting compiler/backend/gc
Oct 09 22:36:31 Finished compiler/backend/gc                                      1s 140MB
Oct 09 22:36:32 Starting compiler/backend
Oct 09 22:36:38 Finished compiler/backend                                         4s 361MB
Oct 09 22:36:39 Starting compiler/encoders/asm
Oct 09 22:36:40 Finished compiler/encoders/asm                                    0s  93MB
Oct 09 22:36:41 Starting compiler/encoders/x64
Oct 09 22:36:43 Finished compiler/encoders/x64                                    0s 104MB
Oct 09 22:36:44 Starting compiler/encoders/arm7
Oct 09 22:36:46 Finished compiler/encoders/arm7                                   0s  98MB
Oct 09 22:36:47 Starting compiler/encoders/arm8
Oct 09 22:36:48 Finished compiler/encoders/arm8                                   0s 103MB
Oct 09 22:36:49 Starting compiler/encoders/arm8_asl
Oct 09 22:39:00 Finished compiler/encoders/arm8_asl                            2m10s   1GB
Oct 09 22:39:01 Starting compiler/encoders/mips
Oct 09 22:39:03 Finished compiler/encoders/mips                                   0s  98MB
Oct 09 22:39:04 Starting compiler/encoders/riscv
Oct 09 22:39:05 Finished compiler/encoders/riscv                                  0s  99MB
Oct 09 22:39:06 Starting compiler/encoders/ag32
Oct 09 22:39:08 Finished compiler/encoders/ag32                                   0s  98MB
Oct 09 22:39:09 Starting compiler/backend/x64
Oct 09 22:39:11 Finished compiler/backend/x64                                     1s 136MB
Oct 09 22:39:12 Starting compiler/backend/arm7
Oct 09 22:39:14 Finished compiler/backend/arm7                                    1s 143MB
Oct 09 22:39:15 Starting compiler/backend/arm8
Oct 09 22:39:17 Finished compiler/backend/arm8                                    1s 135MB
Oct 09 22:39:18 Starting compiler/backend/mips
Oct 09 22:39:20 Finished compiler/backend/mips                                    1s 131MB
Oct 09 22:39:21 Starting compiler/backend/riscv
Oct 09 22:39:23 Finished compiler/backend/riscv                                   1s 131MB
Oct 09 22:39:24 Starting compiler/backend/ag32
Oct 09 22:40:36 Finished compiler/backend/ag32                                 1m11s   2GB
Oct 09 22:40:37 Starting compiler/parsing/proofs
Oct 09 22:40:38 Finished compiler/parsing/proofs                                  0s  74MB
Oct 09 22:40:39 Starting compiler/inference/proofs
Oct 09 22:40:41 Finished compiler/inference/proofs                                0s  99MB
Oct 09 22:40:42 Starting compiler/backend/semantics
Oct 09 22:43:56 Finished compiler/backend/semantics                            3m13s   3GB
Oct 09 22:43:57 Starting compiler/backend/reg_alloc/proofs
Oct 09 22:43:59 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Oct 09 22:44:00 Starting compiler/backend/proofs
Oct 09 22:44:54 Finished compiler/backend/proofs                                 53s   2GB
Oct 09 22:44:55 Starting compiler/backend/serialiser
Oct 09 22:44:57 Finished compiler/backend/serialiser                              1s 148MB
Oct 09 22:44:58 Starting compiler/encoders/x64/proofs
Oct 09 22:55:09 Finished compiler/encoders/x64/proofs                         10m09s   5GB
Oct 09 22:55:10 Starting compiler/encoders/arm7/proofs
Oct 09 23:08:21 Finished compiler/encoders/arm7/proofs                        13m10s  12GB
Oct 09 23:08:22 Starting compiler/encoders/arm8/proofs
Oct 09 23:15:30 Finished compiler/encoders/arm8/proofs                         7m07s   5GB
Oct 09 23:15:31 Starting compiler/encoders/arm8_asl/proofs
Oct 09 23:30:50 Finished compiler/encoders/arm8_asl/proofs                    15m17s   4GB
Oct 09 23:30:50 Starting compiler/encoders/mips/proofs
Oct 09 23:41:14 Finished compiler/encoders/mips/proofs                        10m22s   7GB
Oct 09 23:41:15 Starting compiler/encoders/riscv/proofs
Oct 09 23:49:28 Finished compiler/encoders/riscv/proofs                        8m12s   3GB
Oct 09 23:49:29 Starting compiler/encoders/ag32/proofs
Oct 09 23:52:26 Finished compiler/encoders/ag32/proofs                         2m56s   2GB
Oct 09 23:52:27 Starting compiler/backend/x64/proofs
Oct 09 23:53:15 Finished compiler/backend/x64/proofs                             46s   3GB
Oct 09 23:53:16 Starting compiler/backend/arm7/proofs
Oct 09 23:54:03 Finished compiler/backend/arm7/proofs                            46s   3GB
Oct 09 23:54:04 Starting compiler/backend/arm8/proofs
Oct 09 23:54:48 Finished compiler/backend/arm8/proofs                            43s   3GB
Oct 09 23:54:49 Starting compiler/backend/arm8_asl
Oct 09 23:55:20 Finished compiler/backend/arm8_asl                               30s   2GB
Oct 09 23:55:21 Starting compiler/backend/mips/proofs
Oct 09 23:56:12 Finished compiler/backend/mips/proofs                            49s   3GB
Oct 09 23:56:13 Starting compiler/backend/riscv/proofs
Oct 09 23:57:08 Finished compiler/backend/riscv/proofs                           54s   3GB
Oct 09 23:57:09 Starting compiler/backend/ag32/proofs
Oct 10 00:11:49 Finished compiler/backend/ag32/proofs                         14m38s   7GB
Oct 10 00:11:50 Starting compiler/backend/cv_compute
Oct 10 00:13:43 Finished compiler/backend/cv_compute                           1m52s   3GB
Oct 10 00:13:44 Starting cv_translator
Oct 10 00:33:28 Finished cv_translator                                        19m42s   9GB
Oct 10 00:33:29 Starting candle/set-theory
Oct 10 00:34:19 Finished candle/set-theory                                       49s   1GB
Oct 10 00:34:19 Starting candle/syntax-lib
Oct 10 00:34:21 Finished candle/syntax-lib                                        0s  69MB
Oct 10 00:34:22 Starting candle/standard/syntax
Oct 10 00:34:42 Finished candle/standard/syntax                                  19s   1GB
Oct 10 00:34:43 Starting candle/standard/semantics
Oct 10 00:37:30 Finished candle/standard/semantics                             2m46s   3GB
Oct 10 00:37:31 Starting candle/standard/monadic
Oct 10 00:37:33 Finished candle/standard/monadic                                  0s 102MB
Oct 10 00:37:34 Starting candle/standard/ml_kernel
Oct 10 00:39:38 Finished candle/standard/ml_kernel                             2m03s   5GB
Oct 10 00:39:39 Starting candle/overloading/syntax
Oct 10 00:43:23 Finished candle/overloading/syntax                             3m42s   2GB
Oct 10 00:43:24 Starting candle/overloading/semantics
Oct 10 00:55:10 Finished candle/overloading/semantics                         11m45s   5GB
Oct 10 00:55:11 Starting candle/overloading/monadic
Oct 10 00:57:37 Finished candle/overloading/monadic                            2m25s   2GB
Oct 10 00:57:38 Starting candle/overloading/ml_kernel
Oct 10 01:05:44 Finished candle/overloading/ml_kernel                          8m05s   7GB
Oct 10 01:05:45 Starting candle/overloading/ml_checker
Oct 10 01:08:33 Finished candle/overloading/ml_checker                         2m47s   7GB
Oct 10 01:08:34 Starting candle/prover
Oct 10 01:19:09 Finished candle/prover                                        10m34s   6GB
Oct 10 01:19:10 Starting pancake
Oct 10 01:19:38 Finished pancake                                                 27s 994MB
Oct 10 01:19:39 Starting pancake/ffi
Oct 10 01:19:40 Finished pancake/ffi                                              0s  22MB
Oct 10 01:19:41 Starting pancake/semantics
Oct 10 01:21:49 Finished pancake/semantics                                     2m07s   2GB
Oct 10 01:21:50 Starting pancake/parser
Oct 10 01:22:13 Finished pancake/parser                                          22s 833MB
Oct 10 01:22:14 Starting pancake/proofs
Oct 10 01:38:19 Finished pancake/proofs                                       16m03s   7GB
Oct 10 01:38:20 Starting compiler/dafny
Oct 10 01:41:01 Finished compiler/dafny                                        2m40s  11GB
Oct 10 01:41:02 Starting compiler/dafny/translation
Oct 10 02:09:51 Finished compiler/dafny/translation                           28m47s  15GB
Oct 10 02:09:52 Starting compiler/dafny/compilation
Oct 10 02:13:27 Finished compiler/dafny/compilation                            3m34s  15GB
Oct 10 02:13:28 Starting compiler/dafny/semantics
Oct 10 02:14:06 Finished compiler/dafny/semantics                                37s   1GB
Oct 10 02:14:07 Starting characteristic/examples
Oct 10 02:15:38 Finished characteristic/examples                               1m29s   5GB
Oct 10 02:15:38 Starting tutorial/solutions
Oct 10 02:18:27 Finished tutorial/solutions                                    2m47s   5GB
Oct 10 02:18:28 Starting translator/monadic/examples
Oct 10 02:21:38 Finished translator/monadic/examples                           3m08s   4GB
Oct 10 02:21:39 Starting examples
Oct 10 02:34:01 Finished examples                                             12m20s   5GB
Oct 10 02:34:01 Starting examples/compilation/x64
Oct 10 02:44:02 Finished examples/compilation/x64                              9m59s   7GB
Oct 10 02:44:02 Starting examples/compilation/x64/proofs
Oct 10 02:48:59 Finished examples/compilation/x64/proofs                       4m55s   8GB
Oct 10 02:49:00 Starting examples/compilation/ag32
Oct 10 02:51:53 Finished examples/compilation/ag32                             2m52s   5GB
Oct 10 02:51:54 Starting examples/compilation/ag32/proofs
Oct 10 02:53:47 Finished examples/compilation/ag32/proofs                      1m52s  10GB
Oct 10 02:53:48 Starting examples/compilation/to_word
Oct 10 02:58:08 Finished examples/compilation/to_word                          4m18s  13GB
Oct 10 02:58:08 Starting examples/lpr_checker
Oct 10 02:58:40 Finished examples/lpr_checker                                    30s   1GB
Oct 10 02:58:41 Starting examples/lpr_checker/array
Oct 10 03:25:12 Finished examples/lpr_checker/array                           26m30s  25GB
Oct 10 03:25:13 Starting examples/lpr_checker/array/compilation
Oct 10 03:27:54 Finished examples/lpr_checker/array/compilation                2m39s  10GB
Oct 10 03:27:55 Starting examples/lpr_checker/array/compilation/proofs
Oct 10 03:29:56 Finished examples/lpr_checker/array/compilation/proofs         1m59s   8GB
Oct 10 03:29:57 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 10 03:31:52 Finished examples/lpr_checker/array/compilation/proofsARM8     1m54s   8GB
Oct 10 03:31:53 Starting examples/xlrup_checker
Oct 10 03:32:29 Finished examples/xlrup_checker                                  34s   1GB
Oct 10 03:32:30 Starting examples/xlrup_checker/array
Oct 10 03:45:54 Finished examples/xlrup_checker/array                         13m23s  11GB
Oct 10 03:45:55 Starting examples/xlrup_checker/array/compilation
Oct 10 03:47:25 Finished examples/xlrup_checker/array/compilation              1m29s   7GB
Oct 10 03:47:26 Starting examples/xlrup_checker/array/compilation/proofs
Oct 10 03:49:12 Finished examples/xlrup_checker/array/compilation/proofs       1m45s   7GB
Oct 10 03:49:13 Starting examples/pseudo_bool
Oct 10 03:50:41 Finished examples/pseudo_bool                                  1m26s   1GB
Oct 10 03:50:41 Starting examples/pseudo_bool/cnf_encoding
Oct 10 03:51:23 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Oct 10 03:51:24 Starting examples/pseudo_bool/graph_encoding
Oct 10 03:52:19 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 10 03:52:20 Starting examples/pseudo_bool/array
Oct 10 04:55:10 Finished examples/pseudo_bool/array                         1h02m48s  28GB
Oct 10 04:55:11 Starting examples/pseudo_bool/array/compilation
Oct 10 05:09:16 Finished examples/pseudo_bool/array/compilation               14m04s  29GB
Oct 10 05:09:17 Starting examples/pseudo_bool/array/compilation/proofs
Oct 10 05:13:46 Finished examples/pseudo_bool/array/compilation/proofs         4m28s  10GB
Oct 10 05:13:47 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 10 05:15:48 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m59s   9GB
Oct 10 05:15:49 Starting examples/opentheory
Oct 10 05:24:41 Finished examples/opentheory                                   8m51s   5GB
Oct 10 05:24:41 Starting examples/opentheory
Oct 10 05:24:43 Finished examples/opentheory                                      1s 133MB
Oct 10 05:24:44 Starting examples/opentheory/compilation
Oct 10 05:26:51 Finished examples/opentheory/compilation                       2m05s   9GB
Oct 10 05:26:52 Starting examples/opentheory/compilation/proofs
Oct 10 05:28:47 Finished examples/opentheory/compilation/proofs                1m54s   7GB
Oct 10 05:28:48 Starting examples/opentheory/compilation/ag32
Oct 10 05:30:59 Finished examples/opentheory/compilation/ag32                  2m10s   9GB
Oct 10 05:31:00 Starting examples/opentheory/compilation/ag32/proofs
Oct 10 05:33:37 Finished examples/opentheory/compilation/ag32/proofs           2m35s  13GB
Oct 10 05:33:38 Starting examples/sat_encodings
Oct 10 05:34:41 Finished examples/sat_encodings                                1m01s 946MB
Oct 10 05:34:42 Starting examples/sat_encodings/case_studies
Oct 10 05:36:55 Finished examples/sat_encodings/case_studies                   2m13s   2GB
Oct 10 05:36:56 Starting examples/sat_encodings/translation
Oct 10 05:40:43 Finished examples/sat_encodings/translation                    3m45s   3GB
Oct 10 05:40:44 Starting examples/sat_encodings/translation/compilation
Oct 10 05:43:16 Finished examples/sat_encodings/translation/compilation        2m30s   7GB
Oct 10 05:43:16 Starting examples/deflate
Oct 10 05:43:45 Finished examples/deflate                                        27s 765MB
Oct 10 05:43:46 Starting examples/deflate/translation
Oct 10 05:44:48 Finished examples/deflate/translation                          1m01s   2GB
Oct 10 05:44:49 Starting examples/deflate/translation/compilation
Oct 10 05:45:59 Finished examples/deflate/translation/compilation              1m08s   6GB
Oct 10 05:46:00 Starting examples/vipr
Oct 10 05:49:47 Finished examples/vipr                                         3m46s   7GB
Oct 10 05:49:48 Starting examples/vipr/compilation
Oct 10 05:51:08 Finished examples/vipr/compilation                             1m19s   6GB
Oct 10 05:51:09 Starting translator/okasaki-examples
Oct 10 05:55:23 Finished translator/okasaki-examples                           4m13s   4GB
Oct 10 05:55:24 Starting translator/other-examples
Oct 10 05:56:42 Finished translator/other-examples                             1m16s   3GB
Oct 10 05:56:43 Starting compiler/parsing/tests
Oct 10 05:57:22 Finished compiler/parsing/tests                                  37s   2GB
Oct 10 05:57:23 Starting compiler/inference/tests
Oct 10 05:58:10 Finished compiler/inference/tests                                46s   3GB
Oct 10 05:58:11 Starting compiler/printing/test
Oct 10 05:59:52 Finished compiler/printing/test                                1m40s   6GB
Oct 10 05:59:53 Starting icing/flover
Oct 10 06:36:52 Finished icing/flover                                         36m57s   4GB
Oct 10 06:36:53 Starting icing/
Oct 10 07:04:52 Finished icing/                                               27m58s   9GB
Oct 10 07:04:53 Starting icing/examples
Oct 10 07:06:51 Finished icing/examples                                        1m57s   9GB
Oct 10 07:06:52 Starting compiler/repl
Oct 10 07:16:07 Finished compiler/repl                                         9m14s  11GB
Oct 10 07:16:08 Starting unverified/sexpr-bootstrap/x64/64
Oct 10 07:29:59 Finished unverified/sexpr-bootstrap/x64/64                    13m50s  18GB
Oct 10 07:30:00 Starting unverified/sexpr-bootstrap/x64/32
Oct 10 07:41:20 Finished unverified/sexpr-bootstrap/x64/32                    11m18s  14GB
Oct 10 07:41:21 Starting compiler/benchmarks
Oct 10 07:42:06 Finished compiler/benchmarks                                     44s 712MB
Oct 10 07:42:07 Starting compiler/bootstrap/compilation/x64/64
Oct 10 08:26:24 Finished compiler/bootstrap/compilation/x64/64                44m15s 109GB
Oct 10 08:26:25 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 10 08:51:59 Finished compiler/bootstrap/compilation/x64/64/proofs         25m32s  52GB
Oct 10 08:51:59 Starting compiler/bootstrap/compilation/x64/32
Oct 10 09:33:44 Finished compiler/bootstrap/compilation/x64/32                41m43s 112GB
Oct 10 09:33:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 10 09:38:43 Finished compiler/bootstrap/compilation/x64/32/proofs          4m57s  24GB
Oct 10 09:38:44 Starting compiler/bootstrap/compilation/arm8/64
Oct 10 10:39:10 Finished compiler/bootstrap/compilation/arm8/64             1h00m25s 140GB
Oct 10 10:39:11 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 10 10:44:51 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m38s  31GB
Oct 10 10:44:52 Starting compiler/bootstrap/compilation/ag32/32
Oct 10 11:25:27 Finished compiler/bootstrap/compilation/ag32/32               40m34s 102GB
Oct 10 11:25:28 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 10 11:31:28 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m59s  32GB
Oct 10 11:31:29 SUCCESS