Job 1481

CakeML:773a7927a5af89e94a1c3bda992bdd7afb8fbb02
  Merge pull request #815 from hrutvik/master [Feb 23 15:27:11]
HOL:466ca124556d0d92defbe6ca514c428ca12727c9
  Prove theorems for Euler phi function, and a simple Chinese Remainder [Feb 17 00:14:31]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Feb 23 18:05:57 Claimed job
Feb 23 18:06:00 Reusing HOL
Feb 23 18:06:06 Starting developers
Feb 23 18:06:08 Finished developers                                               2s 111MB
Feb 23 18:06:08 Starting developers/bin
Feb 23 18:06:14 Finished developers/bin                                           5s   1GB
Feb 23 18:06:14 Starting semantics/ffi
Feb 23 18:06:24 Finished semantics/ffi                                           10s 316MB
Feb 23 18:06:25 Starting semantics
Feb 23 18:07:46 Finished semantics                                             1m21s   1GB
Feb 23 18:07:46 Starting semantics/proofs
Feb 23 18:11:03 Finished semantics/proofs                                      3m16s   1GB
Feb 23 18:11:03 Starting semantics/alt_semantics
Feb 23 18:11:11 Finished semantics/alt_semantics                                  7s 440MB
Feb 23 18:11:11 Starting semantics/alt_semantics/proofs
Feb 23 18:13:18 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Feb 23 18:13:18 Starting basis/pure
Feb 23 18:14:10 Finished basis/pure                                              50s   1GB
Feb 23 18:14:10 Starting translator
Feb 23 18:16:45 Finished translator                                            2m35s   2GB
Feb 23 18:16:45 Starting compiler/parsing
Feb 23 18:17:52 Finished compiler/parsing                                      1m06s   2GB
Feb 23 18:17:52 Starting characteristic
Feb 23 18:23:50 Finished characteristic                                        5m58s   3GB
Feb 23 18:23:50 Starting translator/monadic
Feb 23 18:25:36 Finished translator/monadic                                    1m45s   3GB
Feb 23 18:25:36 Starting basis
Feb 23 19:08:27 Finished basis                                                42m50s  25GB
Feb 23 19:08:27 Starting compiler/inference
Feb 23 19:09:31 Finished compiler/inference                                    1m03s   2GB
Feb 23 19:09:31 Starting compiler/backend/reg_alloc
Feb 23 19:10:35 Finished compiler/backend/reg_alloc                            1m03s   1GB
Feb 23 19:10:35 Starting compiler/backend/gc
Feb 23 19:13:54 Finished compiler/backend/gc                                   3m19s   2GB
Feb 23 19:13:54 Starting compiler/backend
Feb 23 19:18:57 Finished compiler/backend                                      5m00s   5GB
Feb 23 19:18:57 Starting compiler/encoders/asm
Feb 23 19:19:19 Finished compiler/encoders/asm                                   21s   1GB
Feb 23 19:19:19 Starting compiler/encoders/x64
Feb 23 19:19:45 Finished compiler/encoders/x64                                   26s   1GB
Feb 23 19:19:46 Starting compiler/encoders/arm7
Feb 23 19:20:36 Finished compiler/encoders/arm7                                  50s   1GB
Feb 23 19:20:36 Starting compiler/encoders/arm8
Feb 23 19:20:49 Finished compiler/encoders/arm8                                  13s   1GB
Feb 23 19:20:50 Starting compiler/encoders/mips
Feb 23 19:21:08 Finished compiler/encoders/mips                                  17s   1GB
Feb 23 19:21:08 Starting compiler/encoders/riscv
Feb 23 19:21:25 Finished compiler/encoders/riscv                                 16s   1GB
Feb 23 19:21:25 Starting compiler/encoders/ag32
Feb 23 19:21:43 Finished compiler/encoders/ag32                                  18s 908MB
Feb 23 19:21:43 Starting compiler/backend/x64
Feb 23 19:22:01 Finished compiler/backend/x64                                    17s   1GB
Feb 23 19:22:01 Starting compiler/backend/arm7
Feb 23 19:22:24 Finished compiler/backend/arm7                                   22s   1GB
Feb 23 19:22:24 Starting compiler/backend/arm8
Feb 23 19:22:44 Finished compiler/backend/arm8                                   20s   1GB
Feb 23 19:22:44 Starting compiler/backend/mips
Feb 23 19:23:05 Finished compiler/backend/mips                                   20s   1GB
Feb 23 19:23:05 Starting compiler/backend/riscv
Feb 23 19:23:26 Finished compiler/backend/riscv                                  20s   1GB
Feb 23 19:23:26 Starting compiler/backend/ag32
Feb 23 19:24:36 Finished compiler/backend/ag32                                 1m10s   2GB
Feb 23 19:24:37 Starting compiler/parsing/proofs
Feb 23 19:29:59 Finished compiler/parsing/proofs                               5m22s   2GB
Feb 23 19:30:00 Starting compiler/inference/proofs
Feb 23 19:32:29 Finished compiler/inference/proofs                             2m29s   2GB
Feb 23 19:32:29 Starting compiler/backend/semantics
Feb 23 19:59:36 Finished compiler/backend/semantics                           27m06s   3GB
Feb 23 19:59:36 Starting compiler/backend/reg_alloc/proofs
Feb 23 20:02:53 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Feb 23 20:02:53 Starting compiler/backend/proofs
Feb 23 20:56:22 Finished compiler/backend/proofs                              53m28s  17GB
Feb 23 20:56:22 Starting compiler/encoders/x64/proofs
Feb 23 21:05:46 Finished compiler/encoders/x64/proofs                          9m23s   6GB
Feb 23 21:05:46 Starting compiler/encoders/arm7/proofs
Feb 23 21:18:25 Finished compiler/encoders/arm7/proofs                        12m39s   6GB
Feb 23 21:18:26 Starting compiler/encoders/arm8/proofs
Feb 23 21:24:35 Finished compiler/encoders/arm8/proofs                         6m09s   3GB
Feb 23 21:24:35 Starting compiler/encoders/mips/proofs
Feb 23 21:34:20 Finished compiler/encoders/mips/proofs                         9m44s   7GB
Feb 23 21:34:20 Starting compiler/encoders/riscv/proofs
Feb 23 21:42:33 Finished compiler/encoders/riscv/proofs                        8m13s   3GB
Feb 23 21:42:34 Starting compiler/encoders/ag32/proofs
Feb 23 21:44:53 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Feb 23 21:44:53 Starting compiler/backend/x64/proofs
Feb 23 21:45:15 Finished compiler/backend/x64/proofs                             20s   1GB
Feb 23 21:45:15 Starting compiler/backend/arm7/proofs
Feb 23 21:45:37 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 23 21:45:37 Starting compiler/backend/arm8/proofs
Feb 23 21:45:58 Finished compiler/backend/arm8/proofs                            21s   1GB
Feb 23 21:45:58 Starting compiler/backend/mips/proofs
Feb 23 21:46:20 Finished compiler/backend/mips/proofs                            21s   1GB
Feb 23 21:46:20 Starting compiler/backend/riscv/proofs
Feb 23 21:46:43 Finished compiler/backend/riscv/proofs                           22s   2GB
Feb 23 21:46:43 Starting compiler/backend/ag32/proofs
Feb 23 21:58:43 Finished compiler/backend/ag32/proofs                         11m59s   4GB
Feb 23 21:58:43 Starting compiler/proofs
Feb 23 22:00:22 Finished compiler/proofs                                       1m39s   6GB
Feb 23 22:00:22 Starting candle/set-theory
Feb 23 22:00:52 Finished candle/set-theory                                       28s 887MB
Feb 23 22:00:52 Starting candle/syntax-lib
Feb 23 22:01:03 Finished candle/syntax-lib                                       11s 796MB
Feb 23 22:01:03 Starting candle/standard/syntax
Feb 23 22:02:51 Finished candle/standard/syntax                                1m47s   1GB
Feb 23 22:02:51 Starting candle/standard/semantics
Feb 23 22:04:36 Finished candle/standard/semantics                             1m44s   2GB
Feb 23 22:04:36 Starting candle/standard/monadic
Feb 23 22:06:15 Finished candle/standard/monadic                               1m38s   1GB
Feb 23 22:06:15 Starting candle/standard/ml_kernel
Feb 23 22:11:33 Finished candle/standard/ml_kernel                             5m17s   6GB
Feb 23 22:11:33 Starting candle/overloading/syntax
Feb 23 22:14:42 Finished candle/overloading/syntax                             3m09s   1GB
Feb 23 22:14:43 Starting candle/overloading/semantics
Feb 23 22:26:42 Finished candle/overloading/semantics                         11m59s   9GB
Feb 23 22:26:42 Starting characteristic/examples
Feb 23 22:28:00 Finished characteristic/examples                               1m17s   4GB
Feb 23 22:28:00 Starting tutorial/solutions
Feb 23 22:42:56 Finished tutorial/solutions                                   14m56s  14GB
Feb 23 22:42:57 Starting translator/monadic/examples
Feb 23 22:46:18 Finished translator/monadic/examples                           3m21s   4GB
Feb 23 22:46:18 Starting examples
Feb 23 22:54:51 Finished examples                                              8m32s   6GB
Feb 23 22:54:51 Starting examples/compilation/x64
Feb 24 01:14:41 Finished examples/compilation/x64                           2h19m50s  30GB
Feb 24 01:14:41 Starting examples/compilation/x64/proofs
Feb 24 01:16:36 Finished examples/compilation/x64/proofs                       1m54s   3GB
Feb 24 01:16:36 Starting examples/compilation/ag32
Feb 24 01:49:25 Finished examples/compilation/ag32                            32m49s  11GB
Feb 24 01:49:26 Starting examples/compilation/ag32/proofs
Feb 24 01:50:19 Finished examples/compilation/ag32/proofs                        52s   4GB
Feb 24 01:50:19 Starting examples/cost
Feb 24 02:43:43 Finished examples/cost                                        53m23s  13GB
Feb 24 02:43:43 Starting examples/lpr_checker
Feb 24 02:47:28 Finished examples/lpr_checker                                  3m45s   5GB
Feb 24 02:47:28 Starting examples/lpr_checker/compilation
Feb 24 03:05:21 Finished examples/lpr_checker/compilation                     17m52s  11GB
Feb 24 03:05:21 Starting examples/lpr_checker/compilation/proofs
Feb 24 03:06:05 Finished examples/lpr_checker/compilation/proofs                 43s   3GB
Feb 24 03:06:05 Starting examples/lpr_checker/array
Feb 24 03:19:41 Finished examples/lpr_checker/array                           13m35s   6GB
Feb 24 03:19:41 Starting examples/lpr_checker/array/compilation
Feb 24 03:38:52 Finished examples/lpr_checker/array/compilation               19m10s  12GB
Feb 24 03:38:52 Starting examples/lpr_checker/array/compilation/proofs
Feb 24 03:39:41 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Feb 24 03:39:41 Starting examples/opentheory
Feb 24 03:48:51 Finished examples/opentheory                                   9m09s   6GB
Feb 24 03:48:51 Starting examples/opentheory
Feb 24 03:48:52 Finished examples/opentheory                                      0s 100MB
Feb 24 03:48:52 Starting examples/opentheory/compilation
Feb 24 04:19:09 Finished examples/opentheory/compilation                      30m17s  25GB
Feb 24 04:19:10 Starting examples/opentheory/compilation/proofs
Feb 24 04:19:52 Finished examples/opentheory/compilation/proofs                  42s   4GB
Feb 24 04:19:53 Starting examples/opentheory/compilation/ag32
Feb 24 04:52:01 Finished examples/opentheory/compilation/ag32                 32m08s  25GB
Feb 24 04:52:01 Starting examples/opentheory/compilation/ag32/proofs
Feb 24 04:53:37 Finished examples/opentheory/compilation/ag32/proofs           1m35s   9GB
Feb 24 04:53:37 Starting translator/okasaki-examples
Feb 24 04:57:42 Finished translator/okasaki-examples                           4m04s   2GB
Feb 24 04:57:42 Starting translator/other-examples
Feb 24 04:59:47 Finished translator/other-examples                             2m04s   2GB
Feb 24 04:59:47 Starting compiler/parsing/tests
Feb 24 05:00:11 Finished compiler/parsing/tests                                  23s 719MB
Feb 24 05:00:11 Starting compiler/inference/tests
Feb 24 05:07:18 Finished compiler/inference/tests                              7m06s   6GB
Feb 24 05:07:18 Starting compiler/bootstrap/translation
Feb 24 07:48:25 Finished compiler/bootstrap/translation                     2h41m06s  51GB
Feb 24 07:48:26 Starting unverified/sexpr-bootstrap/x64/64
Feb 24 08:01:04 Finished unverified/sexpr-bootstrap/x64/64                    12m12s   8GB
Feb 24 08:01:04 Starting unverified/sexpr-bootstrap/x64/32
Feb 24 08:12:01 Finished unverified/sexpr-bootstrap/x64/32                    10m30s   8GB
Feb 24 08:12:01 Starting compiler/benchmarks
Feb 24 08:49:52 Finished compiler/benchmarks                                  37m50s   2GB
Feb 24 08:49:52 Starting compiler/bootstrap/compilation/x64/64
Feb 25 00:19:01 Finished compiler/bootstrap/compilation/x64/64             15h28m51s  64GB
Feb 25 00:19:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 25 00:21:24 Finished compiler/bootstrap/compilation/x64/64/proofs          2m22s  20GB
Feb 25 00:21:25 Starting compiler/bootstrap/compilation/x64/32
Feb 25 14:46:57 Finished compiler/bootstrap/compilation/x64/32             14h25m19s  64GB
Feb 25 14:46:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 25 14:49:13 Finished compiler/bootstrap/compilation/x64/32/proofs          2m15s  18GB
Feb 25 14:49:13 Starting compiler/bootstrap/compilation/ag32/32
Feb 26 05:52:47 Finished compiler/bootstrap/compilation/ag32/32            15h03m33s  64GB
Feb 26 05:52:47 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 26 06:02:12 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m24s  56GB
Feb 26 06:02:12 SUCCESS