Job 1218

CakeML:c258b1a13e66d1a4a064fbf7bee9ef20eb899d07
  Add diminish_srw_ss to build ARMv7 enc proofs [Mar 30 13:39:34]
HOL:ef343a121219c92126d7a1031bf089448507844c
  Implement, document and regression-test some "term tactics" [Apr 14 07:28:57]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Apr 15 09:11:57 Claimed job
Apr 15 09:12:05 Building HOL
Apr 15 09:24:59 Starting developers
Apr 15 09:25:03 Finished developers                                               4s  98MB
Apr 15 09:25:03 Starting developers/bin
Apr 15 09:25:11 Finished developers/bin                                           7s   1GB
Apr 15 09:25:11 Starting semantics/ffi
Apr 15 09:25:22 Finished semantics/ffi                                           10s 228MB
Apr 15 09:25:22 Starting semantics
Apr 15 09:26:54 Finished semantics                                             1m31s 843MB
Apr 15 09:26:54 Starting semantics/proofs
Apr 15 09:30:25 Finished semantics/proofs                                      3m30s   1GB
Apr 15 09:30:25 Starting semantics/alt_semantics
Apr 15 09:30:34 Finished semantics/alt_semantics                                  8s 285MB
Apr 15 09:30:34 Starting semantics/alt_semantics/proofs
Apr 15 09:32:42 Finished semantics/alt_semantics/proofs                        2m08s 834MB
Apr 15 09:32:43 Starting basis/pure
Apr 15 09:35:45 Finished basis/pure                                            3m01s 761MB
Apr 15 09:35:45 Starting translator
Apr 15 09:38:23 Finished translator                                            2m37s   1GB
Apr 15 09:38:23 Starting compiler/parsing
Apr 15 09:39:35 Finished compiler/parsing                                      1m11s   1GB
Apr 15 09:39:35 Starting characteristic
Apr 15 09:45:34 Finished characteristic                                        5m59s   1GB
Apr 15 09:45:35 Starting translator/monadic
Apr 15 09:47:13 Finished translator/monadic                                    1m38s   1GB
Apr 15 09:47:13 Starting basis
Apr 15 10:20:33 Finished basis                                                33m19s  14GB
Apr 15 10:20:33 Starting compiler/inference
Apr 15 10:21:43 Finished compiler/inference                                    1m09s   1GB
Apr 15 10:21:43 Starting compiler/backend/reg_alloc
Apr 15 10:22:47 Finished compiler/backend/reg_alloc                            1m03s   1GB
Apr 15 10:22:47 Starting compiler/backend/gc
Apr 15 10:26:18 Finished compiler/backend/gc                                   3m30s   2GB
Apr 15 10:26:18 Starting compiler/backend
Apr 15 10:30:59 Finished compiler/backend                                      4m40s   3GB
Apr 15 10:30:59 Starting compiler/encoders/asm
Apr 15 10:31:21 Finished compiler/encoders/asm                                   22s 707MB
Apr 15 10:31:21 Starting compiler/encoders/x64
Apr 15 10:32:20 Finished compiler/encoders/x64                                   58s 928MB
Apr 15 10:32:20 Starting compiler/encoders/arm7
Apr 15 10:34:07 Finished compiler/encoders/arm7                                1m46s   1GB
Apr 15 10:34:07 Starting compiler/encoders/arm8
Apr 15 10:34:41 Finished compiler/encoders/arm8                                  33s 812MB
Apr 15 10:34:41 Starting compiler/encoders/mips
Apr 15 10:35:52 Finished compiler/encoders/mips                                1m11s   1GB
Apr 15 10:35:52 Starting compiler/encoders/riscv
Apr 15 10:37:18 Finished compiler/encoders/riscv                               1m25s 758MB
Apr 15 10:37:19 Starting compiler/encoders/ag32
Apr 15 10:37:37 Finished compiler/encoders/ag32                                  17s 731MB
Apr 15 10:37:37 Starting compiler/backend/x64
Apr 15 10:37:55 Finished compiler/backend/x64                                    18s   1GB
Apr 15 10:37:55 Starting compiler/backend/arm7
Apr 15 10:38:15 Finished compiler/backend/arm7                                   19s   1GB
Apr 15 10:38:15 Starting compiler/backend/arm8
Apr 15 10:38:35 Finished compiler/backend/arm8                                   19s   1GB
Apr 15 10:38:35 Starting compiler/backend/mips
Apr 15 10:38:54 Finished compiler/backend/mips                                   19s   1GB
Apr 15 10:38:54 Starting compiler/backend/riscv
Apr 15 10:39:14 Finished compiler/backend/riscv                                  20s   1GB
Apr 15 10:39:15 Starting compiler/backend/ag32
Apr 15 10:40:25 Finished compiler/backend/ag32                                 1m10s   1GB
Apr 15 10:40:25 Starting compiler/parsing/proofs
Apr 15 10:46:10 Finished compiler/parsing/proofs                               5m44s   1GB
Apr 15 10:46:10 Starting compiler/inference/proofs
Apr 15 10:48:42 Finished compiler/inference/proofs                             2m32s   1GB
Apr 15 10:48:43 Starting compiler/backend/semantics
Apr 15 11:18:54 Finished compiler/backend/semantics                           30m11s   2GB
Apr 15 11:18:55 Starting compiler/backend/reg_alloc/proofs
Apr 15 11:22:38 Finished compiler/backend/reg_alloc/proofs                     3m42s 737MB
Apr 15 11:22:38 Starting compiler/backend/proofs
Apr 15 12:29:19 Finished compiler/backend/proofs                            1h06m41s  24GB
Apr 15 12:29:20 Starting compiler/encoders/x64/proofs
Apr 15 12:39:05 Finished compiler/encoders/x64/proofs                          9m44s   4GB
Apr 15 12:39:05 Starting compiler/encoders/arm7/proofs
Apr 15 12:52:14 Finished compiler/encoders/arm7/proofs                        13m08s   5GB
Apr 15 12:52:14 Starting compiler/encoders/arm8/proofs
Apr 15 12:58:50 Finished compiler/encoders/arm8/proofs                         6m36s   1GB
Apr 15 12:58:50 Starting compiler/encoders/mips/proofs
Apr 15 13:08:53 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Apr 15 13:08:54 Starting compiler/encoders/riscv/proofs
Apr 15 13:17:51 Finished compiler/encoders/riscv/proofs                        8m57s   1GB
Apr 15 13:17:52 Starting compiler/encoders/ag32/proofs
Apr 15 13:20:30 Finished compiler/encoders/ag32/proofs                         2m38s 790MB
Apr 15 13:20:30 Starting compiler/backend/x64/proofs
Apr 15 13:20:51 Finished compiler/backend/x64/proofs                             20s   1GB
Apr 15 13:20:51 Starting compiler/backend/arm7/proofs
Apr 15 13:21:13 Finished compiler/backend/arm7/proofs                            20s 863MB
Apr 15 13:21:13 Starting compiler/backend/arm8/proofs
Apr 15 13:21:32 Finished compiler/backend/arm8/proofs                            19s   1GB
Apr 15 13:21:32 Starting compiler/backend/mips/proofs
Apr 15 13:21:53 Finished compiler/backend/mips/proofs                            19s   1GB
Apr 15 13:21:53 Starting compiler/backend/riscv/proofs
Apr 15 13:22:14 Finished compiler/backend/riscv/proofs                           21s   1GB
Apr 15 13:22:14 Starting compiler/backend/ag32/proofs
Apr 15 13:35:38 Finished compiler/backend/ag32/proofs                         13m22s   1GB
Apr 15 13:35:38 Starting compiler/proofs
Apr 15 13:37:24 Finished compiler/proofs                                       1m46s   2GB
Apr 15 13:37:25 Starting candle/set-theory
Apr 15 13:37:53 Finished candle/set-theory                                       28s 759MB
Apr 15 13:37:53 Starting candle/syntax-lib
Apr 15 13:38:05 Finished candle/syntax-lib                                       10s 689MB
Apr 15 13:38:05 Starting candle/standard/syntax
Apr 15 13:39:56 Finished candle/standard/syntax                                1m50s   1GB
Apr 15 13:39:56 Starting candle/standard/semantics
Apr 15 13:41:40 Finished candle/standard/semantics                             1m44s 989MB
Apr 15 13:41:40 Starting candle/standard/monadic
Apr 15 13:43:22 Finished candle/standard/monadic                               1m41s   1GB
Apr 15 13:43:23 Starting candle/standard/ml_kernel
Apr 15 13:48:57 Finished candle/standard/ml_kernel                             5m34s   4GB
Apr 15 13:48:57 Starting candle/standard/opentheory
Apr 15 13:58:21 Finished candle/standard/opentheory                            9m23s   4GB
Apr 15 13:58:21 Starting candle/standard/opentheory/compilation
Apr 15 14:29:57 Finished candle/standard/opentheory/compilation               31m35s  16GB
Apr 15 14:29:57 Starting candle/standard/opentheory/compilation/proofs
Apr 15 14:30:34 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Apr 15 14:30:34 Starting candle/overloading/syntax
Apr 15 14:33:45 Finished candle/overloading/syntax                             3m10s   1GB
Apr 15 14:33:45 Starting candle/overloading/semantics
Apr 15 14:40:56 Finished candle/overloading/semantics                          7m10s   2GB
Apr 15 14:40:56 Starting characteristic/examples
Apr 15 14:42:12 Finished characteristic/examples                               1m15s   2GB
Apr 15 14:42:12 Starting tutorial/solutions
Apr 15 14:56:46 Finished tutorial/solutions                                   14m33s   6GB
Apr 15 14:56:46 Starting translator/monadic/examples
Apr 15 14:59:53 Finished translator/monadic/examples                           3m06s   2GB
Apr 15 14:59:53 Starting examples
Apr 15 15:08:15 Finished examples                                              8m21s   3GB
Apr 15 15:08:15 Starting examples/compilation/x64
Apr 15 17:25:14 Finished examples/compilation/x64                           2h16m57s  12GB
Apr 15 17:25:14 Starting examples/compilation/x64/proofs
Apr 15 17:26:49 Finished examples/compilation/x64/proofs                       1m35s   2GB
Apr 15 17:26:50 Starting examples/compilation/ag32
Apr 15 17:58:13 Finished examples/compilation/ag32                            31m23s   7GB
Apr 15 17:58:14 Starting examples/compilation/ag32/proofs
Apr 15 17:58:56 Finished examples/compilation/ag32/proofs                        41s   2GB
Apr 15 17:58:56 Starting examples/cost
Apr 15 18:40:49 Finished examples/cost                                        41m52s   5GB
Apr 15 18:40:49 Starting examples/lpr_checker
Apr 15 18:44:35 Finished examples/lpr_checker                                  3m45s   2GB
Apr 15 18:44:35 Starting examples/lpr_checker/compilation
Apr 15 19:01:30 Finished examples/lpr_checker/compilation                     16m54s  13GB
Apr 15 19:01:30 Starting examples/lpr_checker/compilation/proofs
Apr 15 19:02:07 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Apr 15 19:02:07 Starting examples/lpr_checker/array
Apr 15 19:10:18 Finished examples/lpr_checker/array                            8m11s   2GB
Apr 15 19:10:19 Starting examples/lpr_checker/array/compilation
Apr 15 19:26:34 Finished examples/lpr_checker/array/compilation               16m14s   8GB
Apr 15 19:26:34 Starting examples/lpr_checker/array/compilation/proofs
Apr 15 19:27:16 Finished examples/lpr_checker/array/compilation/proofs           42s   3GB
Apr 15 19:27:17 Starting translator/okasaki-examples
Apr 15 19:31:38 Finished translator/okasaki-examples                           4m21s   1GB
Apr 15 19:31:38 Starting translator/other-examples
Apr 15 19:33:35 Finished translator/other-examples                             1m56s   1GB
Apr 15 19:33:35 Starting compiler/parsing/tests
Apr 15 19:34:02 Finished compiler/parsing/tests                                  25s 618MB
Apr 15 19:34:02 Starting compiler/inference/tests
Apr 15 19:38:37 Finished compiler/inference/tests                              4m35s   3GB
Apr 15 19:38:37 Starting compiler/bootstrap/translation
Apr 15 22:23:15 Finished compiler/bootstrap/translation                     2h44m37s  39GB
Apr 15 22:23:15 Starting unverified/sexpr-bootstrap/x64/64
Apr 15 22:37:14 Finished unverified/sexpr-bootstrap/x64/64                    13m58s   4GB
Apr 15 22:37:14 Starting unverified/sexpr-bootstrap/x64/32
Apr 15 22:47:12 Finished unverified/sexpr-bootstrap/x64/32                     9m56s   6GB
Apr 15 22:47:12 Starting compiler/benchmarks
Apr 15 22:47:14 Finished compiler/benchmarks                                      1s  31MB
Apr 15 22:47:14 Starting compiler/bootstrap/compilation/x64/64
Apr 16 14:06:42 Finished compiler/bootstrap/compilation/x64/64             15h19m26s  64GB
Apr 16 14:06:42 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 16 14:09:50 Finished compiler/bootstrap/compilation/x64/64/proofs          3m08s  13GB
Apr 16 14:09:50 Starting compiler/bootstrap/compilation/x64/32
Apr 17 03:07:10 Finished compiler/bootstrap/compilation/x64/32             12h57m18s  64GB
Apr 17 03:07:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 17 03:10:22 Finished compiler/bootstrap/compilation/x64/32/proofs          3m11s  13GB
Apr 17 03:10:22 Starting compiler/bootstrap/compilation/ag32/32
Apr 17 18:06:52 Finished compiler/bootstrap/compilation/ag32/32            14h56m29s  64GB
Apr 17 18:06:52 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 17 18:34:00 Finished compiler/bootstrap/compilation/ag32/32/proofs        27m08s  30GB
Apr 17 18:34:01 SUCCESS