Job 2641

CakeML:7dfdee9e4a6033677097060c39aede7421e85286
  Remove some Define usages manually [Oct 06 07:15:12]
#1064 (remove-define)
Merging into:95fcf67a782508c8452388d720098fe2bd4a4a3a
  Merge pull request #1063 from CakeML/remove-xdefine [Oct 05 18:51:32]
HOL:277f6ad618617d462cd4ad2955206cb261828f87
  Add proofs about clock for fun-op-sem/imp (#1310) [Oct 03 07:36:31]
Machine:lammmington

Oct 06 18:40:52 Claimed job
Oct 06 18:40:55 Reusing HOL
Oct 06 18:41:07 Starting developers
Oct 06 18:41:11 Finished developers                                               2s 212MB
Oct 06 18:41:12 Starting developers/bin
Oct 06 18:41:33 Finished developers/bin                                          20s   1GB
Oct 06 18:41:34 Starting compiler/proofs
Oct 06 20:26:36 Finished compiler/proofs                                    1h45m00s  34GB
Oct 06 20:26:36 Starting compiler/bootstrap/translation
Oct 07 05:21:57 Finished compiler/bootstrap/translation                     8h55m18s  83GB
Oct 07 05:21:57 Starting semantics/ffi
Oct 07 05:22:07 Finished semantics/ffi                                            8s 644MB
Oct 07 05:22:08 Starting semantics
Oct 07 05:22:09 Finished semantics                                                0s  70MB
Oct 07 05:22:10 Starting semantics/proofs
Oct 07 05:22:35 Finished semantics/proofs                                        23s 818MB
Oct 07 05:22:35 Starting semantics/alt_semantics
Oct 07 05:22:58 Finished semantics/alt_semantics                                 21s 618MB
Oct 07 05:22:59 Starting semantics/alt_semantics/proofs
Oct 07 05:33:17 Finished semantics/alt_semantics/proofs                       10m16s   3GB
Oct 07 05:33:17 Starting basis/pure
Oct 07 05:33:19 Finished basis/pure                                               0s  70MB
Oct 07 05:33:20 Starting translator
Oct 07 05:34:57 Finished translator                                            1m35s   4GB
Oct 07 05:34:57 Starting compiler/parsing
Oct 07 05:34:59 Finished compiler/parsing                                         0s  72MB
Oct 07 05:35:00 Starting characteristic
Oct 07 05:35:02 Finished characteristic                                           0s  89MB
Oct 07 05:35:02 Starting translator/monadic
Oct 07 05:35:04 Finished translator/monadic                                       0s  93MB
Oct 07 05:35:05 Starting basis
Oct 07 05:37:32 Finished basis                                                 2m25s   3GB
Oct 07 05:37:32 Starting compiler/inference
Oct 07 05:37:34 Finished compiler/inference                                       0s 103MB
Oct 07 05:37:35 Starting compiler/backend/reg_alloc
Oct 07 05:37:37 Finished compiler/backend/reg_alloc                               0s  67MB
Oct 07 05:37:37 Starting compiler/backend/gc
Oct 07 05:37:40 Finished compiler/backend/gc                                      1s 147MB
Oct 07 05:37:40 Starting compiler/backend
Oct 07 05:37:46 Finished compiler/backend                                         4s 318MB
Oct 07 05:37:46 Starting compiler/encoders/asm
Oct 07 05:37:48 Finished compiler/encoders/asm                                    0s  94MB
Oct 07 05:37:49 Starting compiler/encoders/x64
Oct 07 05:37:51 Finished compiler/encoders/x64                                    0s 104MB
Oct 07 05:37:52 Starting compiler/encoders/arm7
Oct 07 05:37:53 Finished compiler/encoders/arm7                                   0s  98MB
Oct 07 05:37:54 Starting compiler/encoders/arm8
Oct 07 05:37:56 Finished compiler/encoders/arm8                                   0s 103MB
Oct 07 05:37:57 Starting compiler/encoders/arm8_asl
Oct 07 05:40:07 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Oct 07 05:40:08 Starting compiler/encoders/mips
Oct 07 05:40:10 Finished compiler/encoders/mips                                   0s  98MB
Oct 07 05:40:10 Starting compiler/encoders/riscv
Oct 07 05:40:12 Finished compiler/encoders/riscv                                  0s  99MB
Oct 07 05:40:13 Starting compiler/encoders/ag32
Oct 07 05:40:15 Finished compiler/encoders/ag32                                   0s  98MB
Oct 07 05:40:16 Starting compiler/backend/x64
Oct 07 05:40:18 Finished compiler/backend/x64                                     1s 137MB
Oct 07 05:40:19 Starting compiler/backend/arm7
Oct 07 05:40:21 Finished compiler/backend/arm7                                    1s 141MB
Oct 07 05:40:21 Starting compiler/backend/arm8
Oct 07 05:40:24 Finished compiler/backend/arm8                                    1s 133MB
Oct 07 05:40:24 Starting compiler/backend/mips
Oct 07 05:40:26 Finished compiler/backend/mips                                    1s 130MB
Oct 07 05:40:27 Starting compiler/backend/riscv
Oct 07 05:40:29 Finished compiler/backend/riscv                                   1s 129MB
Oct 07 05:40:30 Starting compiler/backend/ag32
Oct 07 05:41:42 Finished compiler/backend/ag32                                 1m10s   2GB
Oct 07 05:41:43 Starting compiler/parsing/proofs
Oct 07 05:41:45 Finished compiler/parsing/proofs                                  0s  74MB
Oct 07 05:41:45 Starting compiler/inference/proofs
Oct 07 05:41:47 Finished compiler/inference/proofs                                0s  99MB
Oct 07 05:41:48 Starting compiler/backend/semantics
Oct 07 05:45:02 Finished compiler/backend/semantics                            3m12s   4GB
Oct 07 05:45:03 Starting compiler/backend/reg_alloc/proofs
Oct 07 05:45:04 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Oct 07 05:45:05 Starting compiler/backend/proofs
Oct 07 05:46:00 Finished compiler/backend/proofs                                 53s   2GB
Oct 07 05:46:01 Starting compiler/backend/serialiser
Oct 07 05:46:03 Finished compiler/backend/serialiser                              1s 140MB
Oct 07 05:46:04 Starting compiler/encoders/x64/proofs
Oct 07 05:56:17 Finished compiler/encoders/x64/proofs                         10m12s   6GB
Oct 07 05:56:18 Starting compiler/encoders/arm7/proofs
Oct 07 06:09:24 Finished compiler/encoders/arm7/proofs                        13m05s  10GB
Oct 07 06:09:25 Starting compiler/encoders/arm8/proofs
Oct 07 06:16:17 Finished compiler/encoders/arm8/proofs                         6m50s   6GB
Oct 07 06:16:18 Starting compiler/encoders/arm8_asl/proofs
Oct 07 06:31:53 Finished compiler/encoders/arm8_asl/proofs                    15m33s   4GB
Oct 07 06:31:54 Starting compiler/encoders/mips/proofs
Oct 07 06:42:21 Finished compiler/encoders/mips/proofs                        10m26s  10GB
Oct 07 06:42:22 Starting compiler/encoders/riscv/proofs
Oct 07 06:50:37 Finished compiler/encoders/riscv/proofs                        8m13s   3GB
Oct 07 06:50:38 Starting compiler/encoders/ag32/proofs
Oct 07 06:53:35 Finished compiler/encoders/ag32/proofs                         2m56s   2GB
Oct 07 06:53:36 Starting compiler/backend/x64/proofs
Oct 07 06:54:22 Finished compiler/backend/x64/proofs                             45s   3GB
Oct 07 06:54:23 Starting compiler/backend/arm7/proofs
Oct 07 06:55:10 Finished compiler/backend/arm7/proofs                            45s   3GB
Oct 07 06:55:11 Starting compiler/backend/arm8/proofs
Oct 07 06:55:56 Finished compiler/backend/arm8/proofs                            44s   3GB
Oct 07 06:55:57 Starting compiler/backend/arm8_asl
Oct 07 06:56:28 Finished compiler/backend/arm8_asl                               30s   2GB
Oct 07 06:56:29 Starting compiler/backend/mips/proofs
Oct 07 06:57:19 Finished compiler/backend/mips/proofs                            48s   3GB
Oct 07 06:57:20 Starting compiler/backend/riscv/proofs
Oct 07 06:58:18 Finished compiler/backend/riscv/proofs                           57s   4GB
Oct 07 06:58:19 Starting compiler/backend/ag32/proofs
Oct 07 07:12:40 Finished compiler/backend/ag32/proofs                         14m20s   6GB
Oct 07 07:12:41 Starting compiler/backend/cv_compute
Oct 07 07:14:34 Finished compiler/backend/cv_compute                           1m51s   3GB
Oct 07 07:14:35 Starting cv_translator
Oct 07 07:34:25 Finished cv_translator                                        19m48s  13GB
Oct 07 07:34:26 Starting candle/set-theory
Oct 07 07:35:15 Finished candle/set-theory                                       48s   1GB
Oct 07 07:35:16 Starting candle/syntax-lib
Oct 07 07:35:18 Finished candle/syntax-lib                                        0s  69MB
Oct 07 07:35:19 Starting candle/standard/syntax
Oct 07 07:35:39 Finished candle/standard/syntax                                  19s   1GB
Oct 07 07:35:40 Starting candle/standard/semantics
Oct 07 07:38:31 Finished candle/standard/semantics                             2m50s   3GB
Oct 07 07:38:32 Starting candle/standard/monadic
Oct 07 07:38:33 Finished candle/standard/monadic                                  0s 102MB
Oct 07 07:38:34 Starting candle/standard/ml_kernel
Oct 07 07:40:43 Finished candle/standard/ml_kernel                             2m07s   5GB
Oct 07 07:40:44 Starting candle/overloading/syntax
Oct 07 07:44:28 Finished candle/overloading/syntax                             3m42s   2GB
Oct 07 07:44:28 Starting candle/overloading/semantics
Oct 07 07:56:20 Finished candle/overloading/semantics                         11m50s   6GB
Oct 07 07:56:21 Starting candle/overloading/monadic
Oct 07 07:58:47 Finished candle/overloading/monadic                            2m25s   2GB
Oct 07 07:58:48 Starting candle/overloading/ml_kernel
Oct 07 08:06:54 Finished candle/overloading/ml_kernel                          8m04s   7GB
Oct 07 08:06:55 Starting candle/overloading/ml_checker
Oct 07 08:09:41 Finished candle/overloading/ml_checker                         2m45s   7GB
Oct 07 08:09:42 Starting candle/prover
Oct 07 08:20:22 Finished candle/prover                                        10m39s   5GB
Oct 07 08:20:23 Starting pancake
Oct 07 08:20:50 Finished pancake                                                 26s 951MB
Oct 07 08:20:51 Starting pancake/ffi
Oct 07 08:20:52 Finished pancake/ffi                                              0s  23MB
Oct 07 08:20:53 Starting pancake/semantics
Oct 07 08:23:09 Finished pancake/semantics                                     2m15s   3GB
Oct 07 08:23:10 Starting pancake/parser
Oct 07 08:23:34 Finished pancake/parser                                          22s 789MB
Oct 07 08:23:35 Starting pancake/proofs
Oct 07 08:39:42 Finished pancake/proofs                                       16m06s   7GB
Oct 07 08:39:43 Starting compiler/dafny
Oct 07 08:42:14 Finished compiler/dafny                                        2m29s   8GB
Oct 07 08:42:15 Starting compiler/dafny/translation
Oct 07 09:11:04 Finished compiler/dafny/translation                           28m48s  21GB
Oct 07 09:11:05 Starting compiler/dafny/compilation
Oct 07 09:14:36 Finished compiler/dafny/compilation                            3m30s  14GB
Oct 07 09:14:37 Starting compiler/dafny/semantics
Oct 07 09:15:15 Finished compiler/dafny/semantics                                36s   1GB
Oct 07 09:15:16 Starting characteristic/examples
Oct 07 09:16:49 Finished characteristic/examples                               1m32s   4GB
Oct 07 09:16:50 Starting tutorial/solutions
Oct 07 09:19:39 Finished tutorial/solutions                                    2m48s   5GB
Oct 07 09:19:40 Starting translator/monadic/examples
Oct 07 09:22:58 Finished translator/monadic/examples                           3m16s   4GB
Oct 07 09:22:59 Starting examples
Oct 07 09:35:19 Finished examples                                             12m19s   5GB
Oct 07 09:35:20 Starting examples/compilation/x64
Oct 07 09:45:33 Finished examples/compilation/x64                             10m12s   7GB
Oct 07 09:45:34 Starting examples/compilation/x64/proofs
Oct 07 09:50:40 Finished examples/compilation/x64/proofs                       5m05s   8GB
Oct 07 09:50:41 Starting examples/compilation/ag32
Oct 07 09:53:29 Finished examples/compilation/ag32                             2m47s   5GB
Oct 07 09:53:30 Starting examples/compilation/ag32/proofs
Oct 07 09:55:23 Finished examples/compilation/ag32/proofs                      1m52s  10GB
Oct 07 09:55:24 Starting examples/compilation/to_word
Oct 07 09:59:43 Finished examples/compilation/to_word                          4m17s  14GB
Oct 07 09:59:44 Starting examples/lpr_checker
Oct 07 10:00:16 Finished examples/lpr_checker                                    30s   1GB
Oct 07 10:00:17 Starting examples/lpr_checker/array
Oct 07 10:26:44 Finished examples/lpr_checker/array                           26m26s  23GB
Oct 07 10:26:45 Starting examples/lpr_checker/array/compilation
Oct 07 10:29:28 Finished examples/lpr_checker/array/compilation                2m42s   9GB
Oct 07 10:29:29 Starting examples/lpr_checker/array/compilation/proofs
Oct 07 10:31:29 Finished examples/lpr_checker/array/compilation/proofs         1m58s   8GB
Oct 07 10:31:30 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 07 10:33:26 Finished examples/lpr_checker/array/compilation/proofsARM8     1m55s  10GB
Oct 07 10:33:26 Starting examples/xlrup_checker
Oct 07 10:34:02 Finished examples/xlrup_checker                                  34s   1GB
Oct 07 10:34:03 Starting examples/xlrup_checker/array
Oct 07 10:47:29 Finished examples/xlrup_checker/array                         13m24s  11GB
Oct 07 10:47:30 Starting examples/xlrup_checker/array/compilation
Oct 07 10:48:56 Finished examples/xlrup_checker/array/compilation              1m26s   6GB
Oct 07 10:48:57 Starting examples/xlrup_checker/array/compilation/proofs
Oct 07 10:50:47 Finished examples/xlrup_checker/array/compilation/proofs       1m48s   8GB
Oct 07 10:50:48 Starting examples/pseudo_bool
Oct 07 10:52:16 Finished examples/pseudo_bool                                  1m27s   1GB
Oct 07 10:52:17 Starting examples/pseudo_bool/cnf_encoding
Oct 07 10:52:59 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Oct 07 10:53:00 Starting examples/pseudo_bool/graph_encoding
Oct 07 10:53:58 Finished examples/pseudo_bool/graph_encoding                     56s   1GB
Oct 07 10:53:58 Starting examples/pseudo_bool/array
Oct 07 11:57:17 Finished examples/pseudo_bool/array                         1h03m17s  34GB
Oct 07 11:57:18 Starting examples/pseudo_bool/array/compilation
Oct 07 12:11:02 Finished examples/pseudo_bool/array/compilation               13m43s  32GB
Oct 07 12:11:03 Starting examples/pseudo_bool/array/compilation/proofs
Oct 07 12:15:22 Finished examples/pseudo_bool/array/compilation/proofs         4m18s   9GB
Oct 07 12:15:23 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 07 12:17:15 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m51s   8GB
Oct 07 12:17:16 Starting examples/opentheory
Oct 07 12:25:58 Finished examples/opentheory                                   8m41s   5GB
Oct 07 12:25:59 Starting examples/opentheory
Oct 07 12:26:01 Finished examples/opentheory                                      1s 134MB
Oct 07 12:26:02 Starting examples/opentheory/compilation
Oct 07 12:28:11 Finished examples/opentheory/compilation                       2m07s   9GB
Oct 07 12:28:12 Starting examples/opentheory/compilation/proofs
Oct 07 12:30:06 Finished examples/opentheory/compilation/proofs                1m53s   7GB
Oct 07 12:30:07 Starting examples/opentheory/compilation/ag32
Oct 07 12:32:19 Finished examples/opentheory/compilation/ag32                  2m11s   9GB
Oct 07 12:32:20 Starting examples/opentheory/compilation/ag32/proofs
Oct 07 12:34:51 Finished examples/opentheory/compilation/ag32/proofs           2m30s  13GB
Oct 07 12:34:52 Starting examples/sat_encodings
Oct 07 12:35:55 Finished examples/sat_encodings                                1m01s 935MB
Oct 07 12:35:56 Starting examples/sat_encodings/case_studies
Oct 07 12:38:09 Finished examples/sat_encodings/case_studies                   2m12s   2GB
Oct 07 12:38:10 Starting examples/sat_encodings/translation
Oct 07 12:41:53 Finished examples/sat_encodings/translation                    3m42s   3GB
Oct 07 12:41:54 Starting examples/sat_encodings/translation/compilation
Oct 07 12:44:27 Finished examples/sat_encodings/translation/compilation        2m31s   7GB
Oct 07 12:44:28 Starting examples/deflate
Oct 07 12:44:56 Finished examples/deflate                                        27s 746MB
Oct 07 12:44:57 Starting examples/deflate/translation
Oct 07 12:45:56 Finished examples/deflate/translation                            58s   2GB
Oct 07 12:45:57 Starting examples/deflate/translation/compilation
Oct 07 12:47:06 Finished examples/deflate/translation/compilation              1m07s   5GB
Oct 07 12:47:07 Starting examples/vipr
Oct 07 12:50:53 Finished examples/vipr                                         3m45s   8GB
Oct 07 12:50:54 Starting examples/vipr/compilation
Oct 07 12:52:14 Finished examples/vipr/compilation                             1m19s   6GB
Oct 07 12:52:15 Starting translator/okasaki-examples
Oct 07 12:56:37 Finished translator/okasaki-examples                           4m20s   3GB
Oct 07 12:56:38 Starting translator/other-examples
Oct 07 12:57:55 Finished translator/other-examples                             1m16s   3GB
Oct 07 12:57:56 Starting compiler/parsing/tests
Oct 07 12:58:35 Finished compiler/parsing/tests                                  38s   2GB
Oct 07 12:58:36 Starting compiler/inference/tests
Oct 07 12:59:24 Finished compiler/inference/tests                                46s   3GB
Oct 07 12:59:25 Starting compiler/printing/test
Oct 07 13:01:08 Finished compiler/printing/test                                1m42s   6GB
Oct 07 13:01:09 Starting icing/flover
Oct 07 13:38:40 Finished icing/flover                                         37m30s   4GB
Oct 07 13:38:41 Starting icing/
Oct 07 14:06:37 Finished icing/                                               27m54s   9GB
Oct 07 14:06:38 Starting icing/examples
Oct 07 14:08:26 Finished icing/examples                                        1m47s   5GB
Oct 07 14:08:27 Starting compiler/repl
Oct 07 14:17:46 Finished compiler/repl                                         9m17s  12GB
Oct 07 14:17:47 Starting unverified/sexpr-bootstrap/x64/64
Oct 07 14:31:47 Finished unverified/sexpr-bootstrap/x64/64                    13m59s  17GB
Oct 07 14:31:48 Starting unverified/sexpr-bootstrap/x64/32 Oct 07 14:31:48 697s