Job 1826

CakeML:94ac4b68ba71917ede94f5bb752deb85333acb21
  Fix a build error caused by HOL-Theorem-Prover/HOL@60adf92493ffff [Mar 17 04:55:12]
HOL:2889e3eb7587e74c7f267d8a2382549dbdfbe44a
  Some testing of various definition 'styles' for DefnBase [Mar 16 23:15:21]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Mar 17 10:38:43 Claimed job
Mar 17 10:38:49 Building HOL
Mar 17 10:48:23 Starting developers
Mar 17 10:48:27 Finished developers                                               4s 128MB
Mar 17 10:48:27 Starting developers/bin
Mar 17 10:48:48 Finished developers/bin                                          21s   1GB
Mar 17 10:48:49 Starting semantics/ffi
Mar 17 10:48:58 Finished semantics/ffi                                            9s 249MB
Mar 17 10:48:58 Starting semantics
Mar 17 10:51:07 Finished semantics                                             2m08s   1GB
Mar 17 10:51:07 Starting semantics/proofs
Mar 17 10:55:17 Finished semantics/proofs                                      4m09s   2GB
Mar 17 10:55:17 Starting semantics/alt_semantics
Mar 17 10:55:35 Finished semantics/alt_semantics                                 17s 489MB
Mar 17 10:55:35 Starting semantics/alt_semantics/proofs
Mar 17 10:57:56 Finished semantics/alt_semantics/proofs                        2m21s 896MB
Mar 17 10:57:57 Starting basis/pure
Mar 17 11:01:06 Finished basis/pure                                            3m09s 894MB
Mar 17 11:01:07 Starting translator
Mar 17 11:04:07 Finished translator                                            3m00s   1GB
Mar 17 11:04:07 Starting compiler/parsing
Mar 17 11:05:22 Finished compiler/parsing                                      1m15s   2GB
Mar 17 11:05:22 Starting characteristic
Mar 17 11:11:47 Finished characteristic                                        6m25s   1GB
Mar 17 11:11:48 Starting translator/monadic
Mar 17 11:13:45 Finished translator/monadic                                    1m57s   1GB
Mar 17 11:13:45 Starting basis
Mar 17 12:01:09 Finished basis                                                47m23s  14GB
Mar 17 12:01:10 Starting compiler/inference
Mar 17 12:02:38 Finished compiler/inference                                    1m28s   1GB
Mar 17 12:02:38 Starting compiler/backend/reg_alloc
Mar 17 12:04:22 Finished compiler/backend/reg_alloc                            1m44s   1GB
Mar 17 12:04:22 Starting compiler/backend/gc
Mar 17 12:08:44 Finished compiler/backend/gc                                   4m21s   1GB
Mar 17 12:08:44 Starting compiler/backend
Mar 17 12:14:26 Finished compiler/backend                                      5m41s   2GB
Mar 17 12:14:26 Starting compiler/encoders/asm
Mar 17 12:14:56 Finished compiler/encoders/asm                                   29s 767MB
Mar 17 12:14:56 Starting compiler/encoders/x64
Mar 17 12:16:04 Finished compiler/encoders/x64                                 1m07s 874MB
Mar 17 12:16:04 Starting compiler/encoders/arm7
Mar 17 12:18:08 Finished compiler/encoders/arm7                                2m03s   1GB
Mar 17 12:18:08 Starting compiler/encoders/arm8
Mar 17 12:18:51 Finished compiler/encoders/arm8                                  42s 844MB
Mar 17 12:18:51 Starting compiler/encoders/arm8_asl
Mar 17 14:29:47 Finished compiler/encoders/arm8_asl                         2h10m55s  32GB
Mar 17 14:29:47 Starting compiler/encoders/mips
Mar 17 14:31:19 Finished compiler/encoders/mips                                1m31s 900MB
Mar 17 14:31:20 Starting compiler/encoders/riscv
Mar 17 14:33:08 Finished compiler/encoders/riscv                               1m48s 857MB
Mar 17 14:33:08 Starting compiler/encoders/ag32
Mar 17 14:33:30 Finished compiler/encoders/ag32                                  21s 716MB
Mar 17 14:33:30 Starting compiler/backend/x64
Mar 17 14:33:52 Finished compiler/backend/x64                                    21s   1GB
Mar 17 14:33:52 Starting compiler/backend/arm7
Mar 17 14:34:16 Finished compiler/backend/arm7                                   23s   1GB
Mar 17 14:34:16 Starting compiler/backend/arm8
Mar 17 14:34:39 Finished compiler/backend/arm8                                   22s   1GB
Mar 17 14:34:39 Starting compiler/backend/mips
Mar 17 14:35:02 Finished compiler/backend/mips                                   22s   1GB
Mar 17 14:35:02 Starting compiler/backend/riscv
Mar 17 14:35:24 Finished compiler/backend/riscv                                  22s   1GB
Mar 17 14:35:25 Starting compiler/backend/ag32
Mar 17 14:36:51 Finished compiler/backend/ag32                                 1m26s   1GB
Mar 17 14:36:51 Starting compiler/parsing/proofs
Mar 17 14:40:37 Finished compiler/parsing/proofs                               3m46s   1GB
Mar 17 14:40:37 Starting compiler/inference/proofs
Mar 17 14:43:10 Finished compiler/inference/proofs                             2m32s 888MB
Mar 17 14:43:10 Starting compiler/backend/semantics
Mar 17 15:11:15 Finished compiler/backend/semantics                           28m04s   2GB
Mar 17 15:11:15 Starting compiler/backend/reg_alloc/proofs
Mar 17 15:14:47 Finished compiler/backend/reg_alloc/proofs                     3m31s 811MB
Mar 17 15:14:47 Starting compiler/backend/proofs
Mar 17 16:04:48 Finished compiler/backend/proofs                              49m59s  16GB
Mar 17 16:04:48 Starting compiler/backend/serialiser
Mar 17 16:06:24 Finished compiler/backend/serialiser                           1m36s   1GB
Mar 17 16:06:24 Starting compiler/encoders/x64/proofs
Mar 17 16:15:54 Finished compiler/encoders/x64/proofs                          9m29s   5GB
Mar 17 16:15:54 Starting compiler/encoders/arm7/proofs
Mar 17 16:28:58 Finished compiler/encoders/arm7/proofs                        13m03s   6GB
Mar 17 16:28:58 Starting compiler/encoders/arm8/proofs
Mar 17 16:35:45 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
Mar 17 16:35:45 Starting compiler/encoders/arm8_asl/proofs
Mar 17 17:26:24 Finished compiler/encoders/arm8_asl/proofs                    50m38s   6GB
Mar 17 17:26:25 Starting compiler/encoders/mips/proofs
Mar 17 17:36:24 Finished compiler/encoders/mips/proofs                         9m59s   2GB
Mar 17 17:36:25 Starting compiler/encoders/riscv/proofs
Mar 17 17:45:11 Finished compiler/encoders/riscv/proofs                        8m46s   1GB
Mar 17 17:45:11 Starting compiler/encoders/ag32/proofs
Mar 17 17:47:46 Finished compiler/encoders/ag32/proofs                         2m34s 904MB
Mar 17 17:47:46 Starting compiler/backend/x64/proofs
Mar 17 17:48:13 Finished compiler/backend/x64/proofs                             26s   1GB
Mar 17 17:48:13 Starting compiler/backend/arm7/proofs
Mar 17 17:48:42 Finished compiler/backend/arm7/proofs                            28s   1GB
Mar 17 17:48:42 Starting compiler/backend/arm8/proofs
Mar 17 17:49:10 Finished compiler/backend/arm8/proofs                            28s   1GB
Mar 17 17:49:10 Starting compiler/backend/arm8_asl
Mar 17 17:49:34 Finished compiler/backend/arm8_asl                               23s   1GB
Mar 17 17:49:34 Starting compiler/backend/mips/proofs
Mar 17 17:50:02 Finished compiler/backend/mips/proofs                            27s   1GB
Mar 17 17:50:02 Starting compiler/backend/riscv/proofs
Mar 17 17:50:30 Finished compiler/backend/riscv/proofs                           28s   1GB
Mar 17 17:50:30 Starting compiler/backend/ag32/proofs
Mar 17 18:03:09 Finished compiler/backend/ag32/proofs                         12m39s   3GB
Mar 17 18:03:09 Starting compiler/proofs
Mar 17 18:05:32 Finished compiler/proofs                                       2m22s   3GB
Mar 17 18:05:32 Starting candle/set-theory
Mar 17 18:06:06 Finished candle/set-theory                                       34s 920MB
Mar 17 18:06:06 Starting candle/syntax-lib
Mar 17 18:06:19 Finished candle/syntax-lib                                       13s 712MB
Mar 17 18:06:19 Starting candle/standard/syntax
Mar 17 18:08:27 Finished candle/standard/syntax                                2m08s   1GB
Mar 17 18:08:28 Starting candle/standard/semantics
Mar 17 18:10:18 Finished candle/standard/semantics                             1m50s   1GB
Mar 17 18:10:18 Starting candle/standard/monadic
Mar 17 18:12:12 Finished candle/standard/monadic                               1m54s   1GB
Mar 17 18:12:12 Starting candle/standard/ml_kernel
Mar 17 18:18:24 Finished candle/standard/ml_kernel                             6m11s   3GB
Mar 17 18:18:24 Starting candle/overloading/syntax
Mar 17 18:21:32 Finished candle/overloading/syntax                             3m07s   1GB
Mar 17 18:21:33 Starting candle/overloading/semantics
Mar 17 18:33:07 Finished candle/overloading/semantics                         11m31s   2GB
Mar 17 18:33:08 Starting candle/overloading/monadic
Mar 17 18:35:41 Finished candle/overloading/monadic                            2m33s   1GB
Mar 17 18:35:41 Starting candle/overloading/ml_kernel
Mar 17 18:42:48 Finished candle/overloading/ml_kernel                          7m06s   3GB
Mar 17 18:42:48 Starting candle/overloading/ml_checker
Mar 17 18:45:11 Finished candle/overloading/ml_checker                         2m23s   3GB
Mar 17 18:45:12 Starting candle/prover
Mar 17 18:53:18 Finished candle/prover                                         8m06s   2GB
Mar 17 18:53:18 Starting pancake
Mar 17 18:57:01 Finished pancake                                               3m42s   4GB
Mar 17 18:57:01 Starting pancake/ffi
Mar 17 18:57:01 Finished pancake/ffi                                              0s  35MB
Mar 17 18:57:01 Starting pancake/semantics
Mar 17 18:59:29 Finished pancake/semantics                                     2m28s 997MB
Mar 17 18:59:29 Starting pancake/proofs
Mar 17 19:11:25 Finished pancake/proofs                                       11m55s   6GB
Mar 17 19:11:25 Starting characteristic/examples
Mar 17 19:12:46 Finished characteristic/examples                               1m20s   3GB
Mar 17 19:12:46 Starting tutorial/solutions
Mar 17 19:29:21 Finished tutorial/solutions                                   16m34s  11GB
Mar 17 19:29:21 Starting translator/monadic/examples
Mar 17 19:33:11 Finished translator/monadic/examples                           3m49s   2GB
Mar 17 19:33:11 Starting examples
Mar 17 19:42:44 Finished examples                                              9m32s   4GB
Mar 17 19:42:44 Starting examples/compilation/x64
Mar 17 22:14:34 Finished examples/compilation/x64                           2h31m49s  35GB
Mar 17 22:14:34 Starting examples/compilation/x64/proofs
Mar 17 22:17:09 Finished examples/compilation/x64/proofs                       2m34s   3GB
Mar 17 22:17:09 Starting examples/compilation/ag32
Mar 17 22:51:46 Finished examples/compilation/ag32                            34m36s   9GB
Mar 17 22:51:46 Starting examples/compilation/ag32/proofs
Mar 17 22:52:40 Finished examples/compilation/ag32/proofs                        54s   2GB
Mar 17 22:52:40 Starting examples/cost
Mar 17 23:48:44 Finished examples/cost                                        56m02s   9GB
Mar 17 23:48:44 Starting examples/lpr_checker
Mar 17 23:49:46 Finished examples/lpr_checker                                  1m02s   1GB
Mar 17 23:49:46 Starting examples/lpr_checker/array
Mar 18 00:18:10 Finished examples/lpr_checker/array                           28m23s   8GB
Mar 18 00:18:10 Starting examples/lpr_checker/array/compilation
Mar 18 01:39:37 Finished examples/lpr_checker/array/compilation             1h21m25s  33GB
Mar 18 01:39:38 Starting examples/lpr_checker/array/compilation/proofs
Mar 18 01:41:25 Finished examples/lpr_checker/array/compilation/proofs         1m46s   6GB
Mar 18 01:41:25 Starting examples/opentheory
Mar 18 01:51:13 Finished examples/opentheory                                   9m47s   6GB
Mar 18 01:51:13 Starting examples/opentheory
Mar 18 01:51:14 Finished examples/opentheory                                      1s 130MB
Mar 18 01:51:14 Starting examples/opentheory/compilation
Mar 18 02:31:38 Finished examples/opentheory/compilation                      40m23s  30GB
Mar 18 02:31:38 Starting examples/opentheory/compilation/proofs
Mar 18 02:32:57 Finished examples/opentheory/compilation/proofs                1m18s   3GB
Mar 18 02:32:57 Starting examples/opentheory/compilation/ag32
Mar 18 03:10:44 Finished examples/opentheory/compilation/ag32                 37m45s  28GB
Mar 18 03:10:44 Starting examples/opentheory/compilation/ag32/proofs
Mar 18 03:12:30 Finished examples/opentheory/compilation/ag32/proofs           1m46s   6GB
Mar 18 03:12:30 Starting examples/sat_encodings
Mar 18 03:14:31 Finished examples/sat_encodings                                2m00s 781MB
Mar 18 03:14:31 Starting examples/sat_encodings/case_studies
Mar 18 03:16:15 Finished examples/sat_encodings/case_studies                   1m43s 807MB
Mar 18 03:16:15 Starting examples/sat_encodings/translation
Mar 18 03:22:02 Finished examples/sat_encodings/translation                    5m46s   3GB
Mar 18 03:22:02 Starting examples/sat_encodings/translation/compilation
Mar 18 04:11:13 Finished examples/sat_encodings/translation/compilation       49m08s  22GB
Mar 18 04:11:13 Starting translator/okasaki-examples
Mar 18 04:16:02 Finished translator/okasaki-examples                           4m49s   2GB
Mar 18 04:16:02 Starting translator/other-examples
Mar 18 04:17:57 Finished translator/other-examples                             1m54s   1GB
Mar 18 04:17:57 Starting compiler/parsing/tests
Mar 18 04:18:27 Finished compiler/parsing/tests                                  29s 612MB
Mar 18 04:18:27 Starting compiler/inference/tests
Mar 18 04:26:24 Finished compiler/inference/tests                              7m56s   3GB
Mar 18 04:26:25 Starting compiler/printing/test
Mar 18 04:30:01 Finished compiler/printing/test                                3m36s   3GB
Mar 18 04:30:01 Starting compiler/repl
Mar 18 04:42:27 Finished compiler/repl                                        12m25s   5GB
Mar 18 04:42:28 Starting compiler/bootstrap/translation
Mar 18 08:35:08 Finished compiler/bootstrap/translation                     3h52m37s  46GB
Mar 18 08:35:08 Starting unverified/sexpr-bootstrap/x64/64
Mar 18 08:47:23 Finished unverified/sexpr-bootstrap/x64/64                    12m13s   8GB
Mar 18 08:47:23 Starting unverified/sexpr-bootstrap/x64/32
Mar 18 08:56:45 Finished unverified/sexpr-bootstrap/x64/32                     9m21s  10GB
Mar 18 08:56:45 Starting compiler/benchmarks
Mar 18 08:57:41 Finished compiler/benchmarks                                     55s 673MB
Mar 18 08:57:41 Starting compiler/bootstrap/compilation/x64/64
Mar 19 03:30:47 Finished compiler/bootstrap/compilation/x64/64             18h33m00s  64GB
Mar 19 03:30:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 19 03:48:05 Finished compiler/bootstrap/compilation/x64/64/proofs         17m18s  35GB
Mar 19 03:48:05 Starting compiler/bootstrap/compilation/x64/32
Mar 19 16:43:02 Finished compiler/bootstrap/compilation/x64/32             12h54m52s  64GB
Mar 19 16:43:03 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 19 16:47:29 Finished compiler/bootstrap/compilation/x64/32/proofs          4m26s  15GB
Mar 19 16:47:29 Starting compiler/bootstrap/compilation/ag32/32
Mar 20 05:37:51 Finished compiler/bootstrap/compilation/ag32/32            12h50m19s  64GB
Mar 20 05:37:51 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 20 06:05:31 Finished compiler/bootstrap/compilation/ag32/32/proofs        27m39s  25GB
Mar 20 06:05:31 SUCCESS