Job 1241

CakeML:f93f027deacf28045d616637fa093fa94df726da
  Fix another proof [May 31 20:59:56]
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API [May 20 07:12:37]
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

Jun 01 01:30:02 Claimed job
Jun 01 01:30:04 Reusing HOL
Jun 01 01:30:50 Starting developers
Jun 01 01:30:54 Finished developers                                               4s 109MB
Jun 01 01:30:55 Starting developers/bin
Jun 01 01:31:02 Finished developers/bin                                           7s   1GB
Jun 01 01:31:03 Starting semantics/ffi
Jun 01 01:31:13 Finished semantics/ffi                                           10s 228MB
Jun 01 01:31:13 Starting semantics
Jun 01 01:32:37 Finished semantics                                             1m23s   1GB
Jun 01 01:32:37 Starting semantics/proofs
Jun 01 01:36:12 Finished semantics/proofs                                      3m34s   1GB
Jun 01 01:36:12 Starting semantics/alt_semantics
Jun 01 01:36:20 Finished semantics/alt_semantics                                  8s 305MB
Jun 01 01:36:21 Starting semantics/alt_semantics/proofs
Jun 01 01:38:32 Finished semantics/alt_semantics/proofs                        2m11s 926MB
Jun 01 01:38:33 Starting basis/pure
Jun 01 01:39:23 Finished basis/pure                                              50s 647MB
Jun 01 01:39:23 Starting translator
Jun 01 01:42:03 Finished translator                                            2m39s   1GB
Jun 01 01:42:03 Starting compiler/parsing
Jun 01 01:43:16 Finished compiler/parsing                                      1m12s   2GB
Jun 01 01:43:16 Starting characteristic
Jun 01 01:49:23 Finished characteristic                                        6m07s   1GB
Jun 01 01:49:24 Starting translator/monadic
Jun 01 01:50:59 Finished translator/monadic                                    1m35s   1GB
Jun 01 01:51:00 Starting basis
Jun 01 02:24:47 Finished basis                                                33m47s  13GB
Jun 01 02:24:47 Starting compiler/inference
Jun 01 02:25:49 Finished compiler/inference                                    1m01s   1GB
Jun 01 02:25:49 Starting compiler/backend/reg_alloc
Jun 01 02:26:52 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jun 01 02:26:53 Starting compiler/backend/gc
Jun 01 02:30:11 Finished compiler/backend/gc                                   3m18s   2GB
Jun 01 02:30:11 Starting compiler/backend
Jun 01 02:34:54 Finished compiler/backend                                      4m42s   4GB
Jun 01 02:34:55 Starting compiler/encoders/asm
Jun 01 02:35:17 Finished compiler/encoders/asm                                   22s 791MB
Jun 01 02:35:17 Starting compiler/encoders/x64
Jun 01 02:35:43 Finished compiler/encoders/x64                                   25s 837MB
Jun 01 02:35:43 Starting compiler/encoders/arm7
Jun 01 02:36:33 Finished compiler/encoders/arm7                                  50s 744MB
Jun 01 02:36:34 Starting compiler/encoders/arm8
Jun 01 02:36:47 Finished compiler/encoders/arm8                                  13s 829MB
Jun 01 02:36:47 Starting compiler/encoders/mips
Jun 01 02:37:05 Finished compiler/encoders/mips                                  17s   1GB
Jun 01 02:37:05 Starting compiler/encoders/riscv
Jun 01 02:37:20 Finished compiler/encoders/riscv                                 14s 763MB
Jun 01 02:37:20 Starting compiler/encoders/ag32
Jun 01 02:37:39 Finished compiler/encoders/ag32                                  18s 611MB
Jun 01 02:37:39 Starting compiler/backend/x64
Jun 01 02:37:58 Finished compiler/backend/x64                                    18s   1GB
Jun 01 02:37:58 Starting compiler/backend/arm7
Jun 01 02:38:19 Finished compiler/backend/arm7                                   20s   1GB
Jun 01 02:38:19 Starting compiler/backend/arm8
Jun 01 02:38:39 Finished compiler/backend/arm8                                   19s   1GB
Jun 01 02:38:39 Starting compiler/backend/mips
Jun 01 02:38:58 Finished compiler/backend/mips                                   19s   1GB
Jun 01 02:38:58 Starting compiler/backend/riscv
Jun 01 02:39:17 Finished compiler/backend/riscv                                  18s   1GB
Jun 01 02:39:17 Starting compiler/backend/ag32
Jun 01 02:40:30 Finished compiler/backend/ag32                                 1m13s   1GB
Jun 01 02:40:31 Starting compiler/parsing/proofs
Jun 01 02:46:22 Finished compiler/parsing/proofs                               5m51s 963MB
Jun 01 02:46:22 Starting compiler/inference/proofs
Jun 01 02:48:57 Finished compiler/inference/proofs                             2m35s   1GB
Jun 01 02:48:57 Starting compiler/backend/semantics
Jun 01 03:20:21 Finished compiler/backend/semantics                           31m22s   2GB
Jun 01 03:20:21 Starting compiler/backend/reg_alloc/proofs
Jun 01 03:24:08 Finished compiler/backend/reg_alloc/proofs                     3m46s 990MB
Jun 01 03:24:08 Starting compiler/backend/proofs
Jun 01 04:31:20 Finished compiler/backend/proofs                            1h07m11s  22GB
Jun 01 04:31:20 Starting compiler/encoders/x64/proofs
Jun 01 04:41:35 Finished compiler/encoders/x64/proofs                         10m14s   4GB
Jun 01 04:41:35 Starting compiler/encoders/arm7/proofs
Jun 01 04:55:01 Finished compiler/encoders/arm7/proofs                        13m26s   4GB
Jun 01 04:55:01 Starting compiler/encoders/arm8/proofs
Jun 01 05:01:51 Finished compiler/encoders/arm8/proofs                         6m49s   1GB
Jun 01 05:01:52 Starting compiler/encoders/mips/proofs
Jun 01 05:12:21 Finished compiler/encoders/mips/proofs                        10m29s   2GB
Jun 01 05:12:21 Starting compiler/encoders/riscv/proofs
Jun 01 05:21:30 Finished compiler/encoders/riscv/proofs                        9m08s   1GB
Jun 01 05:21:30 Starting compiler/encoders/ag32/proofs
Jun 01 05:24:13 Finished compiler/encoders/ag32/proofs                         2m43s 659MB
Jun 01 05:24:14 Starting compiler/backend/x64/proofs
Jun 01 05:24:34 Finished compiler/backend/x64/proofs                             20s   1GB
Jun 01 05:24:34 Starting compiler/backend/arm7/proofs
Jun 01 05:24:55 Finished compiler/backend/arm7/proofs                            21s   1GB
Jun 01 05:24:55 Starting compiler/backend/arm8/proofs
Jun 01 05:25:16 Finished compiler/backend/arm8/proofs                            20s   1GB
Jun 01 05:25:16 Starting compiler/backend/mips/proofs
Jun 01 05:25:37 Finished compiler/backend/mips/proofs                            21s   1GB
Jun 01 05:25:38 Starting compiler/backend/riscv/proofs
Jun 01 05:25:59 Finished compiler/backend/riscv/proofs                           21s   1GB
Jun 01 05:25:59 Starting compiler/backend/ag32/proofs
Jun 01 05:39:46 Finished compiler/backend/ag32/proofs                         13m46s   1GB
Jun 01 05:39:46 Starting compiler/proofs
Jun 01 05:41:17 Finished compiler/proofs                                       1m30s   3GB
Jun 01 05:41:17 Starting candle/set-theory
Jun 01 05:41:46 Finished candle/set-theory                                       28s 711MB
Jun 01 05:41:46 Starting candle/syntax-lib
Jun 01 05:41:57 Finished candle/syntax-lib                                       10s 620MB
Jun 01 05:41:57 Starting candle/standard/syntax
Jun 01 05:43:49 Finished candle/standard/syntax                                1m51s 939MB
Jun 01 05:43:50 Starting candle/standard/semantics
Jun 01 05:45:36 Finished candle/standard/semantics                             1m46s   1GB
Jun 01 05:45:36 Starting candle/standard/monadic
Jun 01 05:47:22 Finished candle/standard/monadic                               1m45s   1GB
Jun 01 05:47:22 Starting candle/standard/ml_kernel
Jun 01 05:53:07 Finished candle/standard/ml_kernel                             5m44s   2GB
Jun 01 05:53:07 Starting candle/standard/opentheory
Jun 01 06:02:45 Finished candle/standard/opentheory                            9m37s   3GB
Jun 01 06:02:45 Starting candle/standard/opentheory/compilation
Jun 01 06:33:52 Finished candle/standard/opentheory/compilation               31m06s  13GB
Jun 01 06:33:52 Starting candle/standard/opentheory/compilation/proofs
Jun 01 06:34:29 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Jun 01 06:34:29 Starting candle/overloading/syntax
Jun 01 06:37:42 Finished candle/overloading/syntax                             3m12s   1GB
Jun 01 06:37:42 Starting candle/overloading/semantics
Jun 01 06:44:59 Finished candle/overloading/semantics                          7m17s   2GB
Jun 01 06:44:59 Starting characteristic/examples
Jun 01 06:46:16 Finished characteristic/examples                               1m16s   2GB
Jun 01 06:46:16 Starting tutorial/solutions
Jun 01 07:00:58 Finished tutorial/solutions                                   14m41s   6GB
Jun 01 07:00:59 Starting translator/monadic/examples
Jun 01 07:04:05 Finished translator/monadic/examples                           3m05s   2GB
Jun 01 07:04:05 Starting examples
Jun 01 07:12:41 Finished examples                                              8m36s   3GB
Jun 01 07:12:41 Starting examples/compilation/x64
Jun 01 09:30:34 Finished examples/compilation/x64                           2h17m52s  15GB
Jun 01 09:30:34 Starting examples/compilation/x64/proofs
Jun 01 09:32:07 Finished examples/compilation/x64/proofs                       1m32s   2GB
Jun 01 09:32:07 Starting examples/compilation/ag32
Jun 01 10:03:33 Finished examples/compilation/ag32                            31m26s   5GB
Jun 01 10:03:34 Starting examples/compilation/ag32/proofs
Jun 01 10:04:17 Finished examples/compilation/ag32/proofs                        43s   2GB
Jun 01 10:04:18 Starting examples/cost
Jun 01 10:52:14 Finished examples/cost                                        47m56s   6GB
Jun 01 10:52:14 Starting examples/lpr_checker
Jun 01 10:56:06 Finished examples/lpr_checker                                  3m52s   2GB
Jun 01 10:56:06 Starting examples/lpr_checker/compilation
Jun 01 11:13:14 Finished examples/lpr_checker/compilation                     17m07s   8GB
Jun 01 11:13:14 Starting examples/lpr_checker/compilation/proofs
Jun 01 11:13:52 Finished examples/lpr_checker/compilation/proofs                 37s   2GB
Jun 01 11:13:52 Starting examples/lpr_checker/array
Jun 01 11:24:32 Finished examples/lpr_checker/array                           10m39s   2GB
Jun 01 11:24:32 Starting examples/lpr_checker/array/compilation
Jun 01 11:43:34 Finished examples/lpr_checker/array/compilation               19m01s  10GB
Jun 01 11:43:34 Starting examples/lpr_checker/array/compilation/proofs
Jun 01 11:44:23 Finished examples/lpr_checker/array/compilation/proofs           48s   3GB
Jun 01 11:44:23 Starting translator/okasaki-examples
Jun 01 11:48:46 Finished translator/okasaki-examples                           4m23s   1GB
Jun 01 11:48:47 Starting translator/other-examples
Jun 01 11:50:49 Finished translator/other-examples                             2m02s   1GB
Jun 01 11:50:49 Starting compiler/parsing/tests
Jun 01 11:51:15 Finished compiler/parsing/tests                                  26s 661MB
Jun 01 11:51:16 Starting compiler/inference/tests
Jun 01 11:55:50 Finished compiler/inference/tests                              4m34s   3GB
Jun 01 11:55:50 Starting compiler/bootstrap/translation
Jun 01 14:42:29 Finished compiler/bootstrap/translation                     2h46m38s  47GB
Jun 01 14:42:29 Starting unverified/sexpr-bootstrap/x64/64
Jun 01 14:56:30 Finished unverified/sexpr-bootstrap/x64/64                    14m00s   4GB
Jun 01 14:56:30 Starting unverified/sexpr-bootstrap/x64/32
Jun 01 15:06:35 Finished unverified/sexpr-bootstrap/x64/32                    10m04s   8GB
Jun 01 15:06:35 Starting compiler/benchmarks
Jun 01 15:06:37 Finished compiler/benchmarks                                      1s  25MB
Jun 01 15:06:38 Starting compiler/bootstrap/compilation/x64/64
Jun 02 05:46:24 Finished compiler/bootstrap/compilation/x64/64             14h39m45s  64GB
Jun 02 05:46:24 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 02 05:49:29 Finished compiler/bootstrap/compilation/x64/64/proofs          3m05s  13GB
Jun 02 05:49:29 Starting compiler/bootstrap/compilation/x64/32
Jun 02 18:39:30 Finished compiler/bootstrap/compilation/x64/32             12h49m59s  64GB
Jun 02 18:39:30 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 02 18:42:36 Finished compiler/bootstrap/compilation/x64/32/proofs          3m05s  13GB
Jun 02 18:42:36 Starting compiler/bootstrap/compilation/ag32/32
Jun 03 09:37:36 Finished compiler/bootstrap/compilation/ag32/32            14h54m59s  64GB
Jun 03 09:37:36 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 03 10:03:19 Finished compiler/bootstrap/compilation/ag32/32/proofs        25m43s  25GB
Jun 03 10:03:20 SUCCESS