Job 1216

CakeML:c258b1a13e66d1a4a064fbf7bee9ef20eb899d07
  Add diminish_srw_ss to build ARMv7 enc proofs [Mar 30 13:39:34]
HOL:6b4719d7d8f08e26a916ae574f5dda24c6fc4245
  Fix proofs broken by 508f79ea974 [Mar 25 05:16:14]
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

Mar 30 13:55:03 Claimed job
Mar 30 13:55:06 Reusing HOL
Mar 30 13:55:52 Starting developers
Mar 30 13:55:56 Finished developers                                               4s  94MB
Mar 30 13:55:56 Starting developers/bin
Mar 30 13:56:04 Finished developers/bin                                           7s   1GB
Mar 30 13:56:04 Starting semantics/ffi
Mar 30 13:56:15 Finished semantics/ffi                                           10s 213MB
Mar 30 13:56:15 Starting semantics
Mar 30 13:57:36 Finished semantics                                             1m21s   1GB
Mar 30 13:57:36 Starting semantics/proofs
Mar 30 14:01:04 Finished semantics/proofs                                      3m27s 831MB
Mar 30 14:01:04 Starting semantics/alt_semantics
Mar 30 14:01:13 Finished semantics/alt_semantics                                  8s 297MB
Mar 30 14:01:13 Starting semantics/alt_semantics/proofs
Mar 30 14:03:23 Finished semantics/alt_semantics/proofs                        2m09s 905MB
Mar 30 14:03:23 Starting basis/pure
Mar 30 14:04:14 Finished basis/pure                                              50s 671MB
Mar 30 14:04:14 Starting translator
Mar 30 14:06:54 Finished translator                                            2m39s   1GB
Mar 30 14:06:54 Starting compiler/parsing
Mar 30 14:08:05 Finished compiler/parsing                                      1m10s   2GB
Mar 30 14:08:05 Starting characteristic
Mar 30 14:14:06 Finished characteristic                                        6m01s   1GB
Mar 30 14:14:06 Starting translator/monadic
Mar 30 14:15:43 Finished translator/monadic                                    1m36s   1GB
Mar 30 14:15:43 Starting basis
Mar 30 14:49:14 Finished basis                                                33m30s  13GB
Mar 30 14:49:14 Starting compiler/inference
Mar 30 14:50:16 Finished compiler/inference                                    1m01s   1GB
Mar 30 14:50:16 Starting compiler/backend/reg_alloc
Mar 30 14:51:18 Finished compiler/backend/reg_alloc                            1m02s   1GB
Mar 30 14:51:18 Starting compiler/backend/gc
Mar 30 14:54:33 Finished compiler/backend/gc                                   3m14s   1GB
Mar 30 14:54:34 Starting compiler/backend
Mar 30 14:59:11 Finished compiler/backend                                      4m37s   3GB
Mar 30 14:59:11 Starting compiler/encoders/asm
Mar 30 14:59:33 Finished compiler/encoders/asm                                   21s 786MB
Mar 30 14:59:33 Starting compiler/encoders/x64
Mar 30 14:59:59 Finished compiler/encoders/x64                                   25s 954MB
Mar 30 14:59:59 Starting compiler/encoders/arm7
Mar 30 15:00:47 Finished compiler/encoders/arm7                                  48s 795MB
Mar 30 15:00:47 Starting compiler/encoders/arm8
Mar 30 15:01:01 Finished compiler/encoders/arm8                                  13s 817MB
Mar 30 15:01:01 Starting compiler/encoders/mips
Mar 30 15:01:18 Finished compiler/encoders/mips                                  16s   1GB
Mar 30 15:01:18 Starting compiler/encoders/riscv
Mar 30 15:01:33 Finished compiler/encoders/riscv                                 15s 775MB
Mar 30 15:01:34 Starting compiler/encoders/ag32
Mar 30 15:01:52 Finished compiler/encoders/ag32                                  17s 765MB
Mar 30 15:01:52 Starting compiler/backend/x64
Mar 30 15:02:11 Finished compiler/backend/x64                                    19s   1GB
Mar 30 15:02:11 Starting compiler/backend/arm7
Mar 30 15:02:31 Finished compiler/backend/arm7                                   20s   1GB
Mar 30 15:02:32 Starting compiler/backend/arm8
Mar 30 15:02:51 Finished compiler/backend/arm8                                   19s   1GB
Mar 30 15:02:51 Starting compiler/backend/mips
Mar 30 15:03:11 Finished compiler/backend/mips                                   19s   1GB
Mar 30 15:03:11 Starting compiler/backend/riscv
Mar 30 15:03:29 Finished compiler/backend/riscv                                  18s 925MB
Mar 30 15:03:30 Starting compiler/backend/ag32
Mar 30 15:04:40 Finished compiler/backend/ag32                                 1m09s   1GB
Mar 30 15:04:40 Starting compiler/parsing/proofs
Mar 30 15:10:24 Finished compiler/parsing/proofs                               5m44s   1GB
Mar 30 15:10:24 Starting compiler/inference/proofs
Mar 30 15:12:57 Finished compiler/inference/proofs                             2m32s   1GB
Mar 30 15:12:57 Starting compiler/backend/semantics
Mar 30 15:43:49 Finished compiler/backend/semantics                           30m50s   2GB
Mar 30 15:43:49 Starting compiler/backend/reg_alloc/proofs
Mar 30 15:47:33 Finished compiler/backend/reg_alloc/proofs                     3m43s 890MB
Mar 30 15:47:33 Starting compiler/backend/proofs
Mar 30 16:54:11 Finished compiler/backend/proofs                            1h06m37s  16GB
Mar 30 16:54:11 Starting compiler/encoders/x64/proofs
Mar 30 17:03:56 Finished compiler/encoders/x64/proofs                          9m44s   4GB
Mar 30 17:03:56 Starting compiler/encoders/arm7/proofs
Mar 30 17:17:11 Finished compiler/encoders/arm7/proofs                        13m15s   3GB
Mar 30 17:17:11 Starting compiler/encoders/arm8/proofs
Mar 30 17:23:50 Finished compiler/encoders/arm8/proofs                         6m38s   1GB
Mar 30 17:23:50 Starting compiler/encoders/mips/proofs
Mar 30 17:33:44 Finished compiler/encoders/mips/proofs                         9m54s   2GB
Mar 30 17:33:44 Starting compiler/encoders/riscv/proofs
Mar 30 17:42:30 Finished compiler/encoders/riscv/proofs                        8m45s   1GB
Mar 30 17:42:30 Starting compiler/encoders/ag32/proofs
Mar 30 17:45:09 Finished compiler/encoders/ag32/proofs                         2m38s 627MB
Mar 30 17:45:09 Starting compiler/backend/x64/proofs
Mar 30 17:45:30 Finished compiler/backend/x64/proofs                             20s   1GB
Mar 30 17:45:30 Starting compiler/backend/arm7/proofs
Mar 30 17:45:51 Finished compiler/backend/arm7/proofs                            20s   1GB
Mar 30 17:45:51 Starting compiler/backend/arm8/proofs
Mar 30 17:46:11 Finished compiler/backend/arm8/proofs                            19s   1GB
Mar 30 17:46:11 Starting compiler/backend/mips/proofs
Mar 30 17:46:33 Finished compiler/backend/mips/proofs                            21s   1GB
Mar 30 17:46:33 Starting compiler/backend/riscv/proofs
Mar 30 17:46:53 Finished compiler/backend/riscv/proofs                           20s   1GB
Mar 30 17:46:53 Starting compiler/backend/ag32/proofs
Mar 30 18:00:17 Finished compiler/backend/ag32/proofs                         13m22s   1GB
Mar 30 18:00:17 Starting compiler/proofs
Mar 30 18:02:04 Finished compiler/proofs                                       1m46s   3GB
Mar 30 18:02:04 Starting candle/set-theory
Mar 30 18:02:33 Finished candle/set-theory                                       28s 659MB
Mar 30 18:02:33 Starting candle/syntax-lib
Mar 30 18:02:44 Finished candle/syntax-lib                                       10s 671MB
Mar 30 18:02:44 Starting candle/standard/syntax
Mar 30 18:04:36 Finished candle/standard/syntax                                1m51s   1GB
Mar 30 18:04:36 Starting candle/standard/semantics
Mar 30 18:06:20 Finished candle/standard/semantics                             1m43s   1GB
Mar 30 18:06:20 Starting candle/standard/monadic
Mar 30 18:08:02 Finished candle/standard/monadic                               1m41s   1GB
Mar 30 18:08:02 Starting candle/standard/ml_kernel
Mar 30 18:13:33 Finished candle/standard/ml_kernel                             5m30s   3GB
Mar 30 18:13:33 Starting candle/standard/opentheory
Mar 30 18:23:00 Finished candle/standard/opentheory                            9m26s   4GB
Mar 30 18:23:01 Starting candle/standard/opentheory/compilation
Mar 30 18:55:05 Finished candle/standard/opentheory/compilation               32m04s  17GB
Mar 30 18:55:05 Starting candle/standard/opentheory/compilation/proofs
Mar 30 18:55:44 Finished candle/standard/opentheory/compilation/proofs           38s   3GB
Mar 30 18:55:44 Starting candle/overloading/syntax
Mar 30 18:58:51 Finished candle/overloading/syntax                             3m06s   1GB
Mar 30 18:58:51 Starting candle/overloading/semantics
Mar 30 19:06:03 Finished candle/overloading/semantics                          7m11s   2GB
Mar 30 19:06:03 Starting characteristic/examples
Mar 30 19:07:18 Finished characteristic/examples                               1m14s   3GB
Mar 30 19:07:18 Starting tutorial/solutions
Mar 30 19:21:46 Finished tutorial/solutions                                   14m27s   7GB
Mar 30 19:21:46 Starting translator/monadic/examples
Mar 30 19:24:50 Finished translator/monadic/examples                           3m04s   2GB
Mar 30 19:24:50 Starting examples
Mar 30 19:33:14 Finished examples                                              8m23s   4GB
Mar 30 19:33:14 Starting examples/compilation/x64
Mar 30 21:49:18 Finished examples/compilation/x64                           2h16m03s  13GB
Mar 30 21:49:18 Starting examples/compilation/x64/proofs
Mar 30 21:50:51 Finished examples/compilation/x64/proofs                       1m32s   3GB
Mar 30 21:50:51 Starting examples/compilation/ag32
Mar 30 22:21:32 Finished examples/compilation/ag32                            30m40s   7GB
Mar 30 22:21:32 Starting examples/compilation/ag32/proofs
Mar 30 22:22:14 Finished examples/compilation/ag32/proofs                        41s   2GB
Mar 30 22:22:14 Starting examples/cost
Mar 30 23:04:15 Finished examples/cost                                        42m00s   7GB
Mar 30 23:04:16 Starting examples/lpr_checker
Mar 30 23:07:57 Finished examples/lpr_checker                                  3m41s   2GB
Mar 30 23:07:57 Starting examples/lpr_checker/compilation
Mar 30 23:25:12 Finished examples/lpr_checker/compilation                     17m14s  10GB
Mar 30 23:25:12 Starting examples/lpr_checker/compilation/proofs
Mar 30 23:25:48 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Mar 30 23:25:48 Starting examples/lpr_checker/array
Mar 30 23:33:56 Finished examples/lpr_checker/array                            8m07s   2GB
Mar 30 23:33:57 Starting examples/lpr_checker/array/compilation
Mar 30 23:50:08 Finished examples/lpr_checker/array/compilation               16m11s   8GB
Mar 30 23:50:08 Starting examples/lpr_checker/array/compilation/proofs
Mar 30 23:50:53 Finished examples/lpr_checker/array/compilation/proofs           44s   3GB
Mar 30 23:50:53 Starting translator/okasaki-examples
Mar 30 23:55:16 Finished translator/okasaki-examples                           4m22s   1GB
Mar 30 23:55:17 Starting translator/other-examples
Mar 30 23:57:15 Finished translator/other-examples                             1m58s   1GB
Mar 30 23:57:15 Starting compiler/parsing/tests
Mar 30 23:57:41 Finished compiler/parsing/tests                                  25s 560MB
Mar 30 23:57:41 Starting compiler/inference/tests
Mar 31 00:02:15 Finished compiler/inference/tests                              4m33s   4GB
Mar 31 00:02:15 Starting compiler/bootstrap/translation
Mar 31 02:47:34 Finished compiler/bootstrap/translation                     2h45m18s  38GB
Mar 31 02:47:34 Starting unverified/sexpr-bootstrap/x64/64
Mar 31 03:01:29 Finished unverified/sexpr-bootstrap/x64/64                    13m54s   4GB
Mar 31 03:01:29 Starting unverified/sexpr-bootstrap/x64/32
Mar 31 03:11:29 Finished unverified/sexpr-bootstrap/x64/32                     9m58s   8GB
Mar 31 03:11:29 Starting compiler/benchmarks
Mar 31 03:11:33 Finished compiler/benchmarks                                      3s  26MB
Mar 31 03:11:33 Starting compiler/bootstrap/compilation/x64/64
Mar 31 17:38:41 Finished compiler/bootstrap/compilation/x64/64             14h27m07s  64GB
Mar 31 17:38:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 31 17:42:07 Finished compiler/bootstrap/compilation/x64/64/proofs          3m25s  14GB
Mar 31 17:42:07 Starting compiler/bootstrap/compilation/x64/32
Apr 01 06:30:18 Finished compiler/bootstrap/compilation/x64/32             12h48m10s  64GB
Apr 01 06:30:18 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 01 06:33:25 Finished compiler/bootstrap/compilation/x64/32/proofs          3m05s  13GB
Apr 01 06:33:25 Starting compiler/bootstrap/compilation/ag32/32
Apr 01 21:48:37 Finished compiler/bootstrap/compilation/ag32/32            15h15m11s  64GB
Apr 01 21:48:37 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 02 10:46:13 Resuming compiler/bootstrap/compilation/ag32/32/proofs
Apr 02 10:46:15 Finished compiler/bootstrap/compilation/ag32/32/proofs            1s  28MB
Apr 02 10:46:15 SUCCESS