CakeML Regression Test

Job 508

CakeML:080a6785b6240f4b52bca428114fa7481c8ee9a8
  Improve err msg when ind proof fails in translator [Oct 02 09:20:57]
#532 (trans-msg)
Merging into:153ef4270fca8b5a3d6e9652f1f11edbad70406a
  Add reader compilation theories to build-sequence [Sep 26 17:48:15]
HOL:b42a4b729800b9a771bd1820e31e0ada14653ffb
  Document strange uninterruptibility of {PROVE,METIS}_TAC in comment [Oct 02 06:56:54]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Oct 02 09:25:05 Claimed job
Oct 02 09:26:46 Building HOL
Oct 02 09:34:31 Starting developers/bin
Oct 02 09:35:06 Finished developers/bin                                          34s 196MB
Oct 02 09:35:07 Starting semantics/ffi
Oct 02 09:35:42 Finished semantics/ffi                                           34s 395MB
Oct 02 09:35:43 Starting semantics
Oct 02 09:37:02 Finished semantics                                             1m18s 923MB
Oct 02 09:37:03 Starting semantics/proofs
Oct 02 09:39:44 Finished semantics/proofs                                      2m40s   1GB
Oct 02 09:39:45 Starting basis/pure
Oct 02 09:43:12 Finished basis/pure                                            3m26s 830MB
Oct 02 09:43:13 Starting translator
Oct 02 09:44:18 Finished translator                                            1m03s 922MB
Oct 02 09:44:18 Starting compiler/parsing
Oct 02 09:45:52 Finished compiler/parsing                                      1m32s   1GB
Oct 02 09:45:53 Starting characteristic
Oct 02 09:48:16 Finished characteristic                                        2m22s   1GB
Oct 02 09:48:17 Starting translator/monadic
Oct 02 09:49:41 Finished translator/monadic                                    1m22s   1GB
Oct 02 09:49:41 Starting basis
Oct 02 10:06:13 Finished basis                                                16m30s   3GB
Oct 02 10:06:13 Starting compiler/inference
Oct 02 10:07:51 Finished compiler/inference                                    1m36s   1GB
Oct 02 10:07:52 Starting compiler/backend/reg_alloc
Oct 02 10:08:39 Finished compiler/backend/reg_alloc                              45s 833MB
Oct 02 10:08:40 Starting compiler/backend/gc
Oct 02 10:17:24 Finished compiler/backend/gc                                   8m43s   3GB
Oct 02 10:17:25 Starting compiler/backend
Oct 02 10:17:28 Finished compiler/backend                                         2s  17MB
Oct 02 10:17:29 Starting compiler/encoders/asm
Oct 02 10:17:30 Finished compiler/encoders/asm                                    0s  13MB
Oct 02 10:17:31 Starting compiler/encoders/x64
Oct 02 10:18:20 Finished compiler/encoders/x64                                   47s 596MB
Oct 02 10:18:20 Starting compiler/encoders/arm6
Oct 02 10:20:03 Finished compiler/encoders/arm6                                1m41s   1GB
Oct 02 10:20:04 Starting compiler/encoders/arm8
Oct 02 10:20:28 Finished compiler/encoders/arm8                                  23s 420MB
Oct 02 10:20:28 Starting compiler/encoders/mips
Oct 02 10:21:24 Finished compiler/encoders/mips                                  54s 814MB
Oct 02 10:21:25 Starting compiler/encoders/riscv
Oct 02 10:22:25 Finished compiler/encoders/riscv                                 58s 643MB
Oct 02 10:22:26 Starting compiler/backend/x64
Oct 02 10:22:43 Finished compiler/backend/x64                                    16s 783MB
Oct 02 10:22:44 Starting compiler/backend/arm6
Oct 02 10:23:04 Finished compiler/backend/arm6                                   19s   1GB
Oct 02 10:23:05 Starting compiler/backend/arm8
Oct 02 10:23:23 Finished compiler/backend/arm8                                   17s   1GB
Oct 02 10:23:24 Starting compiler/backend/mips
Oct 02 10:23:43 Finished compiler/backend/mips                                   17s   1GB
Oct 02 10:23:44 Starting compiler/backend/riscv
Oct 02 10:24:03 Finished compiler/backend/riscv                                  18s   1GB
Oct 02 10:24:04 Starting compiler/parsing/proofs
Oct 02 10:30:08 Finished compiler/parsing/proofs                               6m03s 797MB
Oct 02 10:30:09 Starting compiler/inference/proofs
Oct 02 10:32:59 Finished compiler/inference/proofs                             2m49s   1GB
Oct 02 10:33:00 Starting compiler/backend/semantics
Oct 02 10:42:02 Finished compiler/backend/semantics                            9m01s   2GB
Oct 02 10:42:03 Starting compiler/backend/reg_alloc/proofs
Oct 02 10:49:18 Finished compiler/backend/reg_alloc/proofs                     7m14s 520MB
Oct 02 10:49:19 Starting compiler/backend/proofs
Oct 02 11:25:20 Finished compiler/backend/proofs                              35m59s   4GB
Oct 02 11:25:21 Starting compiler/encoders/x64/proofs
Oct 02 11:32:48 Finished compiler/encoders/x64/proofs                          7m26s   5GB
Oct 02 11:32:49 Starting compiler/encoders/arm6/proofs
Oct 02 11:40:20 Finished compiler/encoders/arm6/proofs                         7m30s   2GB
Oct 02 11:40:21 Starting compiler/encoders/arm8/proofs
Oct 02 11:45:46 Finished compiler/encoders/arm8/proofs                         5m24s   1GB
Oct 02 11:45:47 Starting compiler/encoders/mips/proofs
Oct 02 11:53:10 Finished compiler/encoders/mips/proofs                         7m22s   1GB
Oct 02 11:53:11 Starting compiler/encoders/riscv/proofs
Oct 02 12:01:09 Finished compiler/encoders/riscv/proofs                        7m57s 774MB
Oct 02 12:01:10 Starting compiler/backend/x64/proofs
Oct 02 12:01:30 Finished compiler/backend/x64/proofs                             19s   1GB
Oct 02 12:01:31 Starting compiler/backend/arm6/proofs
Oct 02 12:01:54 Finished compiler/backend/arm6/proofs                            22s   1GB
Oct 02 12:01:55 Starting compiler/backend/arm8/proofs
Oct 02 12:02:14 Finished compiler/backend/arm8/proofs                            18s 748MB
Oct 02 12:02:14 Starting compiler/backend/mips/proofs
Oct 02 12:02:35 Finished compiler/backend/mips/proofs                            19s 909MB
Oct 02 12:02:35 Starting compiler/backend/riscv/proofs
Oct 02 12:02:55 Finished compiler/backend/riscv/proofs                           19s   1GB
Oct 02 12:02:56 Starting compiler/proofs
Oct 02 12:04:14 Finished compiler/proofs                                       1m16s   2GB
Oct 02 12:04:14 Starting candle/set-theory
Oct 02 12:04:44 Finished candle/set-theory                                       28s 710MB
Oct 02 12:04:45 Starting candle/syntax-lib
Oct 02 12:04:55 Finished candle/syntax-lib                                        9s 624MB
Oct 02 12:04:56 Starting candle/standard/syntax
Oct 02 12:06:27 Finished candle/standard/syntax                                1m30s 578MB
Oct 02 12:06:28 Starting candle/standard/semantics
Oct 02 12:07:51 Finished candle/standard/semantics                             1m21s 907MB
Oct 02 12:07:52 Starting candle/standard/monadic
Oct 02 12:09:26 Finished candle/standard/monadic                               1m33s 789MB
Oct 02 12:09:27 Starting candle/standard/ml_kernel
Oct 02 12:25:40 Finished candle/standard/ml_kernel                            16m12s   3GB
Oct 02 12:25:41 Starting candle/standard/opentheory
Oct 02 12:34:24 Finished candle/standard/opentheory                            8m41s   6GB
Oct 02 12:34:24 Starting candle/standard/opentheory/compilation
Oct 02 13:09:52 Finished candle/standard/opentheory/compilation               35m26s  17GB
Oct 02 13:09:53 Starting characteristic/examples
Oct 02 13:11:29 Finished characteristic/examples                               1m36s   2GB
Oct 02 13:11:30 Starting tutorial/solutions
Oct 02 13:25:02 Finished tutorial/solutions                                   13m30s   7GB
Oct 02 13:25:03 Starting translator/monadic/examples
Oct 02 13:26:47 Finished translator/monadic/examples                           1m43s   2GB
Oct 02 13:26:48 Starting examples
Oct 02 13:32:31 Finished examples                                              5m42s   6GB
Oct 02 13:32:32 Starting examples/compilation
Oct 02 15:28:57 Finished examples/compilation                               1h56m24s  11GB
Oct 02 15:28:58 Starting examples/compilation/proofs
Oct 02 15:30:48 Finished examples/compilation/proofs                           1m49s   3GB
Oct 02 15:30:49 Starting compiler/benchmarks
Oct 02 15:30:50 Finished compiler/benchmarks                                      0s   4MB
Oct 02 15:30:51 Starting translator/okasaki-examples
Oct 02 15:34:19 Finished translator/okasaki-examples                           3m26s   2GB
Oct 02 15:34:20 Starting translator/other-examples
Oct 02 15:37:35 Finished translator/other-examples                             3m14s 900MB
Oct 02 15:37:36 Starting compiler/parsing/tests
Oct 02 15:38:01 Finished compiler/parsing/tests                                  24s 331MB
Oct 02 15:38:02 Starting compiler/inference/tests
Oct 02 15:42:06 Finished compiler/inference/tests                              4m03s   4GB
Oct 02 15:42:07 Starting compiler/bootstrap/translation
Oct 02 21:09:42 Finished compiler/bootstrap/translation                     5h27m34s  54GB
Oct 02 21:09:43 Starting unverified/sexpr-bootstrap/x64/64
Oct 02 21:17:18 Finished unverified/sexpr-bootstrap/x64/64                     7m33s  12GB
Oct 02 21:17:19 Starting unverified/sexpr-bootstrap/x64/32
Oct 02 21:22:20 Finished unverified/sexpr-bootstrap/x64/32                     5m00s  14GB
Oct 02 21:22:21 Starting compiler/bootstrap/compilation/x64/64
Oct 03 13:27:28 Finished compiler/bootstrap/compilation/x64/64             16h05m06s  64GB
Oct 03 13:27:29 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 03 13:30:41 Finished compiler/bootstrap/compilation/x64/64/proofs          3m11s  23GB
Oct 03 13:30:42 Starting compiler/bootstrap/compilation/x64/32
Oct 04 00:23:57 Finished compiler/bootstrap/compilation/x64/32             10h53m14s  58GB
Oct 04 00:23:58 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 04 00:25:46 Finished compiler/bootstrap/compilation/x64/32/proofs          1m47s  26GB
Oct 04 00:25:47 SUCCESS