Job 2633

CakeML:d053dbf34ff2e972ac57481f98cf12dcd5a6e28f
  Remove xDefine usages manually [Oct 03 19:14:05]
#1063 (remove-xdefine)
Merging into:f75fcbe801e04eaa9ba012a65a23b09ddb54203a
  Fix proof broken by recent HOL change [Oct 03 03:30:59]
HOL:277f6ad618617d462cd4ad2955206cb261828f87
  Add proofs about clock for fun-op-sem/imp (#1310) [Oct 03 07:36:31]
Machine:lammmington

Oct 04 15:29:30 Claimed job
Oct 04 15:29:36 Building HOL
Oct 04 15:44:33 Starting developers
Oct 04 15:44:37 Finished developers                                               2s 198MB
Oct 04 15:44:38 Starting developers/bin
Oct 04 15:44:58 Finished developers/bin                                          19s   1GB
Oct 04 15:44:59 Starting compiler/proofs
Oct 04 17:33:20 Finished compiler/proofs                                    1h48m20s  47GB
Oct 04 17:33:21 Starting compiler/bootstrap/translation
Oct 05 02:24:48 Finished compiler/bootstrap/translation                     8h51m24s  57GB
Oct 05 02:24:48 Starting semantics/ffi
Oct 05 02:24:58 Finished semantics/ffi                                            8s 686MB
Oct 05 02:24:59 Starting semantics
Oct 05 02:25:00 Finished semantics                                                0s  69MB
Oct 05 02:25:01 Starting semantics/proofs
Oct 05 02:25:26 Finished semantics/proofs                                        23s 795MB
Oct 05 02:25:27 Starting semantics/alt_semantics
Oct 05 02:25:51 Finished semantics/alt_semantics                                 23s 930MB
Oct 05 02:25:52 Starting semantics/alt_semantics/proofs
Oct 05 02:36:08 Finished semantics/alt_semantics/proofs                       10m15s   3GB
Oct 05 02:36:09 Starting basis/pure
Oct 05 02:36:10 Finished basis/pure                                               0s  70MB
Oct 05 02:36:11 Starting translator
Oct 05 02:37:46 Finished translator                                            1m34s   4GB
Oct 05 02:37:47 Starting compiler/parsing
Oct 05 02:37:49 Finished compiler/parsing                                         0s  72MB
Oct 05 02:37:49 Starting characteristic
Oct 05 02:37:51 Finished characteristic                                           0s  91MB
Oct 05 02:37:52 Starting translator/monadic
Oct 05 02:37:54 Finished translator/monadic                                       0s  99MB
Oct 05 02:37:55 Starting basis
Oct 05 02:40:31 Finished basis                                                 2m35s   9GB
Oct 05 02:40:32 Starting compiler/inference
Oct 05 02:40:34 Finished compiler/inference                                       0s  93MB
Oct 05 02:40:35 Starting compiler/backend/reg_alloc
Oct 05 02:40:36 Finished compiler/backend/reg_alloc                               0s  67MB
Oct 05 02:40:37 Starting compiler/backend/gc
Oct 05 02:40:39 Finished compiler/backend/gc                                      1s 149MB
Oct 05 02:40:40 Starting compiler/backend
Oct 05 02:40:45 Finished compiler/backend                                         4s 319MB
Oct 05 02:40:46 Starting compiler/encoders/asm
Oct 05 02:40:48 Finished compiler/encoders/asm                                    0s  98MB
Oct 05 02:40:49 Starting compiler/encoders/x64
Oct 05 02:40:50 Finished compiler/encoders/x64                                    0s  99MB
Oct 05 02:40:51 Starting compiler/encoders/arm7
Oct 05 02:40:53 Finished compiler/encoders/arm7                                   0s  98MB
Oct 05 02:40:54 Starting compiler/encoders/arm8
Oct 05 02:40:56 Finished compiler/encoders/arm8                                   0s  98MB
Oct 05 02:40:57 Starting compiler/encoders/arm8_asl
Oct 05 04:56:13 Finished compiler/encoders/arm8_asl                         2h15m15s  42GB
Oct 05 04:56:14 Starting compiler/encoders/mips
Oct 05 04:56:16 Finished compiler/encoders/mips                                   0s 103MB
Oct 05 04:56:17 Starting compiler/encoders/riscv
Oct 05 04:56:18 Finished compiler/encoders/riscv                                  0s  99MB
Oct 05 04:56:19 Starting compiler/encoders/ag32
Oct 05 04:56:21 Finished compiler/encoders/ag32                                   0s  89MB
Oct 05 04:56:22 Starting compiler/backend/x64
Oct 05 04:56:24 Finished compiler/backend/x64                                     1s 140MB
Oct 05 04:56:25 Starting compiler/backend/arm7
Oct 05 04:56:27 Finished compiler/backend/arm7                                    1s 139MB
Oct 05 04:56:28 Starting compiler/backend/arm8
Oct 05 04:56:30 Finished compiler/backend/arm8                                    1s 139MB
Oct 05 04:56:31 Starting compiler/backend/mips
Oct 05 04:56:33 Finished compiler/backend/mips                                    1s 139MB
Oct 05 04:56:34 Starting compiler/backend/riscv
Oct 05 04:56:36 Finished compiler/backend/riscv                                   1s 139MB
Oct 05 04:56:36 Starting compiler/backend/ag32
Oct 05 04:57:48 Finished compiler/backend/ag32                                 1m10s   2GB
Oct 05 04:57:49 Starting compiler/parsing/proofs
Oct 05 04:57:50 Finished compiler/parsing/proofs                                  0s  73MB
Oct 05 04:57:51 Starting compiler/inference/proofs
Oct 05 04:57:53 Finished compiler/inference/proofs                                0s  92MB
Oct 05 04:57:54 Starting compiler/backend/semantics
Oct 05 05:01:04 Finished compiler/backend/semantics                            3m09s   3GB
Oct 05 05:01:05 Starting compiler/backend/reg_alloc/proofs
Oct 05 05:01:07 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Oct 05 05:01:08 Starting compiler/backend/proofs
Oct 05 05:02:02 Finished compiler/backend/proofs                                 53s   2GB
Oct 05 05:02:03 Starting compiler/backend/serialiser
Oct 05 05:02:05 Finished compiler/backend/serialiser                              1s 141MB
Oct 05 05:02:06 Starting compiler/encoders/x64/proofs
Oct 05 05:12:23 Finished compiler/encoders/x64/proofs                         10m16s   5GB
Oct 05 05:12:24 Starting compiler/encoders/arm7/proofs
Oct 05 05:25:40 Finished compiler/encoders/arm7/proofs                        13m14s  12GB
Oct 05 05:25:41 Starting compiler/encoders/arm8/proofs
Oct 05 05:32:43 Finished compiler/encoders/arm8/proofs                         7m00s   6GB
Oct 05 05:32:44 Starting compiler/encoders/arm8_asl/proofs
Oct 05 06:23:39 Finished compiler/encoders/arm8_asl/proofs                    50m54s  13GB
Oct 05 06:23:40 Starting compiler/encoders/mips/proofs
Oct 05 06:33:57 Finished compiler/encoders/mips/proofs                        10m16s   7GB
Oct 05 06:33:58 Starting compiler/encoders/riscv/proofs
Oct 05 06:42:30 Finished compiler/encoders/riscv/proofs                        8m31s   3GB
Oct 05 06:42:31 Starting compiler/encoders/ag32/proofs
Oct 05 06:45:30 Finished compiler/encoders/ag32/proofs                         2m57s   2GB
Oct 05 06:45:31 Starting compiler/backend/x64/proofs
Oct 05 06:46:18 Finished compiler/backend/x64/proofs                             46s   3GB
Oct 05 06:46:19 Starting compiler/backend/arm7/proofs
Oct 05 06:47:07 Finished compiler/backend/arm7/proofs                            47s   3GB
Oct 05 06:47:08 Starting compiler/backend/arm8/proofs
Oct 05 06:47:54 Finished compiler/backend/arm8/proofs                            45s   3GB
Oct 05 06:47:55 Starting compiler/backend/arm8_asl
Oct 05 06:48:27 Finished compiler/backend/arm8_asl                               31s   2GB
Oct 05 06:48:28 Starting compiler/backend/mips/proofs
Oct 05 06:49:18 Finished compiler/backend/mips/proofs                            49s   3GB
Oct 05 06:49:19 Starting compiler/backend/riscv/proofs
Oct 05 06:50:16 Finished compiler/backend/riscv/proofs                           56s   3GB
Oct 05 06:50:17 Starting compiler/backend/ag32/proofs
Oct 05 07:04:41 Finished compiler/backend/ag32/proofs                         14m22s   6GB
Oct 05 07:04:42 Starting compiler/backend/cv_compute
Oct 05 07:06:39 Finished compiler/backend/cv_compute                           1m56s   3GB
Oct 05 07:06:40 Starting cv_translator
Oct 05 07:26:34 Finished cv_translator                                        19m52s  10GB
Oct 05 07:26:34 Starting candle/set-theory
Oct 05 07:27:25 Finished candle/set-theory                                       49s   1GB
Oct 05 07:27:25 Starting candle/syntax-lib
Oct 05 07:27:27 Finished candle/syntax-lib                                        0s  69MB
Oct 05 07:27:28 Starting candle/standard/syntax
Oct 05 07:27:49 Finished candle/standard/syntax                                  19s   1GB
Oct 05 07:27:49 Starting candle/standard/semantics
Oct 05 07:30:38 Finished candle/standard/semantics                             2m47s   3GB
Oct 05 07:30:39 Starting candle/standard/monadic
Oct 05 07:30:41 Finished candle/standard/monadic                                  0s 106MB
Oct 05 07:30:41 Starting candle/standard/ml_kernel
Oct 05 07:32:45 Finished candle/standard/ml_kernel                             2m02s   5GB
Oct 05 07:32:46 Starting candle/overloading/syntax
Oct 05 07:36:30 Finished candle/overloading/syntax                             3m43s   3GB
Oct 05 07:36:31 Starting candle/overloading/semantics
Oct 05 07:48:37 Finished candle/overloading/semantics                         12m05s   8GB
Oct 05 07:48:38 Starting candle/overloading/monadic
Oct 05 07:51:04 Finished candle/overloading/monadic                            2m25s   2GB
Oct 05 07:51:05 Starting candle/overloading/ml_kernel
Oct 05 07:59:21 Finished candle/overloading/ml_kernel                          8m14s   7GB
Oct 05 07:59:22 Starting candle/overloading/ml_checker
Oct 05 08:02:08 Finished candle/overloading/ml_checker                         2m45s   7GB
Oct 05 08:02:09 Starting candle/prover
Oct 05 08:12:39 Finished candle/prover                                        10m29s   5GB
Oct 05 08:12:40 Starting pancake
Oct 05 08:13:08 Finished pancake                                                 26s 994MB
Oct 05 08:13:08 Starting pancake/ffi
Oct 05 08:13:09 Finished pancake/ffi                                              0s  23MB
Oct 05 08:13:10 Starting pancake/semantics
Oct 05 08:15:23 Finished pancake/semantics                                     2m11s   3GB
Oct 05 08:15:24 Starting pancake/parser
Oct 05 08:15:48 Finished pancake/parser                                          23s 816MB
Oct 05 08:15:49 Starting pancake/proofs
Oct 05 08:31:56 Finished pancake/proofs                                       16m05s   7GB
Oct 05 08:31:56 Starting compiler/dafny
Oct 05 08:34:36 Finished compiler/dafny                                        2m38s   8GB
Oct 05 08:34:37 Starting compiler/dafny/translation
Oct 05 09:03:15 Finished compiler/dafny/translation                           28m37s  14GB
Oct 05 09:03:16 Starting compiler/dafny/compilation
Oct 05 09:06:54 Finished compiler/dafny/compilation                            3m37s  15GB
Oct 05 09:06:55 Starting compiler/dafny/semantics
Oct 05 09:07:33 Finished compiler/dafny/semantics                                36s   1GB
Oct 05 09:07:34 Starting characteristic/examples
Oct 05 09:09:09 Finished characteristic/examples                               1m33s   5GB
Oct 05 09:09:10 Starting tutorial/solutions
Oct 05 09:12:01 Finished tutorial/solutions                                    2m50s   5GB
Oct 05 09:12:02 Starting translator/monadic/examples
Oct 05 09:15:21 Finished translator/monadic/examples                           3m17s   4GB
Oct 05 09:15:22 Starting examples
Oct 05 09:27:40 Finished examples                                             12m17s   6GB
Oct 05 09:27:41 Starting examples/compilation/x64
Oct 05 09:37:44 Finished examples/compilation/x64                             10m02s   7GB
Oct 05 09:37:45 Starting examples/compilation/x64/proofs
Oct 05 09:42:40 Finished examples/compilation/x64/proofs                       4m53s   9GB
Oct 05 09:42:41 Starting examples/compilation/ag32
Oct 05 09:45:25 Finished examples/compilation/ag32                             2m43s   5GB
Oct 05 09:45:26 Starting examples/compilation/ag32/proofs
Oct 05 09:47:21 Finished examples/compilation/ag32/proofs                      1m54s   8GB
Oct 05 09:47:22 Starting examples/compilation/to_word
Oct 05 09:51:39 Finished examples/compilation/to_word                          4m16s  12GB
Oct 05 09:51:40 Starting examples/lpr_checker
Oct 05 09:52:12 Finished examples/lpr_checker                                    30s   1GB
Oct 05 09:52:12 Starting examples/lpr_checker/array
Oct 05 10:19:17 Finished examples/lpr_checker/array                           27m03s  29GB
Oct 05 10:19:18 Starting examples/lpr_checker/array/compilation
Oct 05 10:21:58 Finished examples/lpr_checker/array/compilation                2m38s  10GB
Oct 05 10:21:59 Starting examples/lpr_checker/array/compilation/proofs
Oct 05 10:24:03 Finished examples/lpr_checker/array/compilation/proofs         2m03s   7GB
Oct 05 10:24:04 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 05 10:26:00 Finished examples/lpr_checker/array/compilation/proofsARM8     1m55s   8GB
Oct 05 10:26:01 Starting examples/xlrup_checker
Oct 05 10:26:37 Finished examples/xlrup_checker                                  34s   1GB
Oct 05 10:26:38 Starting examples/xlrup_checker/array
Oct 05 10:39:58 Finished examples/xlrup_checker/array                         13m19s  12GB
Oct 05 10:39:59 Starting examples/xlrup_checker/array/compilation
Oct 05 10:41:26 Finished examples/xlrup_checker/array/compilation              1m26s   6GB
Oct 05 10:41:27 Starting examples/xlrup_checker/array/compilation/proofs
Oct 05 10:43:17 Finished examples/xlrup_checker/array/compilation/proofs       1m49s   8GB
Oct 05 10:43:18 Starting examples/pseudo_bool
Oct 05 10:44:45 Finished examples/pseudo_bool                                  1m25s   1GB
Oct 05 10:44:45 Starting examples/pseudo_bool/cnf_encoding
Oct 05 10:45:27 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Oct 05 10:45:28 Starting examples/pseudo_bool/graph_encoding
Oct 05 10:46:23 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 05 10:46:24 Starting examples/pseudo_bool/array
Oct 05 11:49:52 Finished examples/pseudo_bool/array                         1h03m26s  33GB
Oct 05 11:49:53 Starting examples/pseudo_bool/array/compilation
Oct 05 12:03:37 Finished examples/pseudo_bool/array/compilation               13m42s  31GB
Oct 05 12:03:38 Starting examples/pseudo_bool/array/compilation/proofs
Oct 05 12:08:04 Finished examples/pseudo_bool/array/compilation/proofs         4m25s  10GB
Oct 05 12:08:05 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 05 12:10:00 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m54s   9GB
Oct 05 12:10:01 Starting examples/opentheory
Oct 05 12:18:52 Finished examples/opentheory                                   8m49s   6GB
Oct 05 12:18:53 Starting examples/opentheory
Oct 05 12:18:55 Finished examples/opentheory                                      1s 134MB
Oct 05 12:18:55 Starting examples/opentheory/compilation
Oct 05 12:21:03 Finished examples/opentheory/compilation                       2m06s   9GB
Oct 05 12:21:04 Starting examples/opentheory/compilation/proofs
Oct 05 12:22:59 Finished examples/opentheory/compilation/proofs                1m53s   6GB
Oct 05 12:23:00 Starting examples/opentheory/compilation/ag32
Oct 05 12:25:17 Finished examples/opentheory/compilation/ag32                  2m16s   8GB
Oct 05 12:25:18 Starting examples/opentheory/compilation/ag32/proofs
Oct 05 12:27:59 Finished examples/opentheory/compilation/ag32/proofs           2m40s   6GB
Oct 05 12:28:00 Starting examples/sat_encodings
Oct 05 12:29:03 Finished examples/sat_encodings                                1m02s 934MB
Oct 05 12:29:04 Starting examples/sat_encodings/case_studies
Oct 05 12:31:17 Finished examples/sat_encodings/case_studies                   2m12s   2GB
Oct 05 12:31:18 Starting examples/sat_encodings/translation
Oct 05 12:35:01 Finished examples/sat_encodings/translation                    3m41s   4GB
Oct 05 12:35:02 Starting examples/sat_encodings/translation/compilation
Oct 05 12:37:38 Finished examples/sat_encodings/translation/compilation        2m35s   7GB
Oct 05 12:37:39 Starting examples/deflate
Oct 05 12:38:08 Finished examples/deflate                                        27s 741MB
Oct 05 12:38:09 Starting examples/deflate/translation
Oct 05 12:39:10 Finished examples/deflate/translation                            59s   2GB
Oct 05 12:39:11 Starting examples/deflate/translation/compilation
Oct 05 12:40:20 Finished examples/deflate/translation/compilation              1m08s   5GB
Oct 05 12:40:21 Starting examples/vipr
Oct 05 12:44:05 Finished examples/vipr                                         3m43s   5GB
Oct 05 12:44:06 Starting examples/vipr/compilation
Oct 05 12:45:28 Finished examples/vipr/compilation                             1m21s   6GB
Oct 05 12:45:29 Starting translator/okasaki-examples
Oct 05 12:49:45 Finished translator/okasaki-examples                           4m14s   4GB
Oct 05 12:49:46 Starting translator/other-examples
Oct 05 12:54:52 Finished translator/other-examples                             5m05s   3GB
Oct 05 12:54:53 Starting compiler/parsing/tests
Oct 05 12:55:33 Finished compiler/parsing/tests                                  38s   2GB
Oct 05 12:55:33 Starting compiler/inference/tests
Oct 05 12:56:21 Finished compiler/inference/tests                                46s   2GB
Oct 05 12:56:22 Starting compiler/printing/test
Oct 05 12:58:04 Finished compiler/printing/test                                1m41s   6GB
Oct 05 12:58:05 Starting icing/flover
Oct 05 13:35:20 Finished icing/flover                                         37m13s   4GB
Oct 05 13:35:20 Starting icing/
Oct 05 14:03:18 Finished icing/                                               27m56s  10GB
Oct 05 14:03:19 Starting icing/examples
Oct 05 14:05:14 Finished icing/examples                                        1m54s   9GB
Oct 05 14:05:15 Starting compiler/repl
Oct 05 14:14:39 Finished compiler/repl                                         9m22s  10GB
Oct 05 14:14:40 Starting unverified/sexpr-bootstrap/x64/64
Oct 05 14:28:35 Finished unverified/sexpr-bootstrap/x64/64                    13m53s  17GB
Oct 05 14:28:36 Starting unverified/sexpr-bootstrap/x64/32
Oct 05 14:39:59 Finished unverified/sexpr-bootstrap/x64/32                    11m22s  14GB
Oct 05 14:40:00 Starting compiler/benchmarks
Oct 05 14:40:46 Finished compiler/benchmarks                                     44s 712MB
Oct 05 14:40:46 Starting compiler/bootstrap/compilation/x64/64
Oct 05 15:27:15 Finished compiler/bootstrap/compilation/x64/64                46m28s 120GB
Oct 05 15:27:16 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 05 15:52:18 Finished compiler/bootstrap/compilation/x64/64/proofs         25m00s  50GB
Oct 05 15:52:19 Starting compiler/bootstrap/compilation/x64/32
Oct 05 16:35:06 Finished compiler/bootstrap/compilation/x64/32                42m45s 106GB
Oct 05 16:35:07 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 05 16:39:54 Finished compiler/bootstrap/compilation/x64/32/proofs          4m46s  23GB
Oct 05 16:39:55 Starting compiler/bootstrap/compilation/arm8/64
Oct 05 17:40:01 Finished compiler/bootstrap/compilation/arm8/64             1h00m05s 141GB
Oct 05 17:40:02 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 05 17:45:49 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m46s  30GB
Oct 05 17:45:50 Starting compiler/bootstrap/compilation/ag32/32
Oct 05 18:28:21 Finished compiler/bootstrap/compilation/ag32/32               42m29s 110GB
Oct 05 18:28:22 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 05 18:34:18 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m55s  29GB
Oct 05 18:34:18 SUCCESS