Job 892

CakeML:cfefc5ef488c0a47e68c80c41a37349892bbaff6
  Fix a broken ag32 proof [May 22 00:01:08]
#635 (thm)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to [May 17 12:31:32]
HOL:15a1e85b5308eeb3ca329cafe2c409f1fd21edfd
  Fix Holmake regressions arising from b03aecf7b [May 20 00:34:31]
Machine:brain12 4.14.89.1.amd64-smp x86_64 GNU/Linux

May 22 01:22:53 Claimed job
May 22 01:22:56 Reusing HOL
May 22 01:24:02 Starting developers
May 22 01:24:05 Finished developers                                               2s  32MB
May 22 01:24:05 Starting developers/bin
May 22 01:24:15 Finished developers/bin                                           9s 930MB
May 22 01:24:15 Starting semantics/ffi
May 22 01:24:34 Finished semantics/ffi                                           18s 244MB
May 22 01:24:34 Starting semantics
May 22 01:27:05 Finished semantics                                             2m30s 992MB
May 22 01:27:05 Starting semantics/proofs
May 22 01:32:53 Finished semantics/proofs                                      5m47s   1GB
May 22 01:32:53 Starting basis/pure
May 22 01:39:37 Finished basis/pure                                            6m44s 759MB
May 22 01:39:37 Starting translator
May 22 01:42:50 Finished translator                                            3m12s   1GB
May 22 01:42:50 Starting compiler/parsing
May 22 01:44:39 Finished compiler/parsing                                      1m48s   1GB
May 22 01:44:39 Starting characteristic
May 22 01:54:57 Finished characteristic                                       10m17s   2GB
May 22 01:54:57 Starting translator/monadic
May 22 01:57:49 Finished translator/monadic                                    2m51s   1GB
May 22 01:57:49 Starting basis
May 22 02:30:04 Finished basis                                                32m13s   2GB
May 22 02:30:04 Starting compiler/inference
May 22 02:33:43 Finished compiler/inference                                    3m39s   1GB
May 22 02:33:43 Starting compiler/backend/reg_alloc
May 22 02:35:25 Finished compiler/backend/reg_alloc                            1m41s   1GB
May 22 02:35:25 Starting compiler/backend/gc
May 22 02:52:06 Finished compiler/backend/gc                                  16m41s   1GB
May 22 02:52:06 Starting compiler/backend
May 22 02:52:16 Finished compiler/backend                                         9s 269MB
May 22 02:52:16 Starting compiler/encoders/asm
May 22 02:52:17 Finished compiler/encoders/asm                                    1s  27MB
May 22 02:52:17 Starting compiler/encoders/x64
May 22 02:54:21 Finished compiler/encoders/x64                                 2m03s 725MB
May 22 02:54:22 Starting compiler/encoders/arm6
May 22 02:57:36 Finished compiler/encoders/arm6                                3m14s   1GB
May 22 02:57:36 Starting compiler/encoders/arm8
May 22 02:58:35 Finished compiler/encoders/arm8                                  58s 651MB
May 22 02:58:35 Starting compiler/encoders/mips
May 22 03:00:50 Finished compiler/encoders/mips                                2m14s 945MB
May 22 03:00:50 Starting compiler/encoders/riscv
May 22 03:03:31 Finished compiler/encoders/riscv                               2m40s 871MB
May 22 03:03:31 Starting compiler/encoders/ag32
May 22 03:04:04 Finished compiler/encoders/ag32                                  32s 669MB
May 22 03:04:04 Starting compiler/backend/x64
May 22 03:04:45 Finished compiler/backend/x64                                    41s   1GB
May 22 03:04:45 Starting compiler/backend/arm6
May 22 03:05:30 Finished compiler/backend/arm6                                   44s   1GB
May 22 03:05:30 Starting compiler/backend/arm8
May 22 03:06:13 Finished compiler/backend/arm8                                   42s   1GB
May 22 03:06:13 Starting compiler/backend/mips
May 22 03:06:56 Finished compiler/backend/mips                                   42s   1GB
May 22 03:06:56 Starting compiler/backend/riscv
May 22 03:07:39 Finished compiler/backend/riscv                                  43s   1GB
May 22 03:07:39 Starting compiler/backend/ag32
May 22 03:09:48 Finished compiler/backend/ag32                                 2m08s   1GB
May 22 03:09:48 Starting compiler/parsing/proofs
May 22 03:20:09 Finished compiler/parsing/proofs                              10m20s 910MB
May 22 03:20:09 Starting compiler/inference/proofs
May 22 03:25:32 Finished compiler/inference/proofs                             5m22s   1GB
May 22 03:25:32 Starting compiler/backend/semantics
May 22 03:38:11 Finished compiler/backend/semantics                           12m38s   1GB
May 22 03:38:11 Starting compiler/backend/reg_alloc/proofs
May 22 03:44:43 Finished compiler/backend/reg_alloc/proofs                     6m31s   1GB
May 22 03:44:43 Starting compiler/backend/proofs
May 22 04:49:49 Finished compiler/backend/proofs                            1h05m05s   4GB
May 22 04:49:49 Starting compiler/encoders/x64/proofs
May 22 05:09:24 Finished compiler/encoders/x64/proofs                         19m35s   5GB
May 22 05:09:25 Starting compiler/encoders/arm6/proofs
May 22 05:35:58 Finished compiler/encoders/arm6/proofs                        26m32s   3GB
May 22 05:35:58 Starting compiler/encoders/arm8/proofs
May 22 05:49:18 Finished compiler/encoders/arm8/proofs                        13m19s   1GB
May 22 05:49:18 Starting compiler/encoders/mips/proofs
May 22 06:08:09 Finished compiler/encoders/mips/proofs                        18m50s   3GB
May 22 06:08:09 Starting compiler/encoders/riscv/proofs
May 22 06:24:15 Finished compiler/encoders/riscv/proofs                       16m06s   1GB
May 22 06:24:16 Starting compiler/encoders/ag32/proofs
May 22 06:28:54 Finished compiler/encoders/ag32/proofs                         4m38s 875MB
May 22 06:28:54 Starting compiler/backend/x64/proofs
May 22 06:29:34 Finished compiler/backend/x64/proofs                             39s 863MB
May 22 06:29:34 Starting compiler/backend/arm6/proofs
May 22 06:30:24 Finished compiler/backend/arm6/proofs                            49s 860MB
May 22 06:30:24 Starting compiler/backend/arm8/proofs
May 22 06:31:03 Finished compiler/backend/arm8/proofs                            38s 878MB
May 22 06:31:03 Starting compiler/backend/mips/proofs
May 22 06:31:49 Finished compiler/backend/mips/proofs                            45s   1GB
May 22 06:31:49 Starting compiler/backend/riscv/proofs
May 22 06:32:31 Finished compiler/backend/riscv/proofs                           41s   1GB
May 22 06:32:31 Starting compiler/backend/ag32/proofs
May 22 06:49:31 Finished compiler/backend/ag32/proofs                         16m59s   1GB
May 22 06:49:31 Starting compiler/proofs
May 22 06:52:04 Finished compiler/proofs                                       2m32s   2GB
May 22 06:52:04 Starting candle/set-theory
May 22 06:52:51 Finished candle/set-theory                                       46s 958MB
May 22 06:52:52 Starting candle/syntax-lib
May 22 06:53:16 Finished candle/syntax-lib                                       24s 681MB
May 22 06:53:17 Starting candle/standard/syntax
May 22 06:56:43 Finished candle/standard/syntax                                3m26s 857MB
May 22 06:56:43 Starting candle/standard/semantics
May 22 07:00:07 Finished candle/standard/semantics                             3m23s   1GB
May 22 07:00:07 Starting candle/standard/monadic
May 22 07:03:18 Finished candle/standard/monadic                               3m10s   1GB
May 22 07:03:18 Starting candle/standard/ml_kernel
May 22 07:10:34 Finished candle/standard/ml_kernel                             7m15s   7GB
May 22 07:10:34 Starting candle/standard/opentheory
May 22 07:26:45 Finished candle/standard/opentheory                           16m11s   5GB
May 22 07:26:45 Starting candle/standard/opentheory/compilation
May 22 08:18:58 Finished candle/standard/opentheory/compilation               52m12s  12GB
May 22 08:18:58 Starting candle/standard/opentheory/compilation/proofs
May 22 08:20:20 Finished candle/standard/opentheory/compilation/proofs         1m22s   2GB
May 22 08:20:21 Starting characteristic/examples
May 22 08:23:06 Finished characteristic/examples                               2m45s   2GB
May 22 08:23:06 Starting tutorial/solutions
May 22 08:47:42 Finished tutorial/solutions                                   24m35s   6GB
May 22 08:47:42 Starting translator/monadic/examples
May 22 08:52:20 Finished translator/monadic/examples                           4m37s   2GB
May 22 08:52:20 Starting examples
May 22 09:05:12 Finished examples                                             12m51s   3GB
May 22 09:05:12 Starting examples/compilation/x64
May 22 12:50:06 Finished examples/compilation/x64                           3h44m53s  16GB
May 22 12:50:06 Starting examples/compilation/x64/proofs
May 22 12:52:52 Finished examples/compilation/x64/proofs                       2m46s   2GB
May 22 12:52:52 Starting examples/compilation/ag32
May 22 13:44:01 Finished examples/compilation/ag32                            51m08s   5GB
May 22 13:44:01 Starting examples/compilation/ag32/proofs
May 22 13:45:35 Finished examples/compilation/ag32/proofs                      1m33s   3GB
May 22 13:45:35 Starting translator/okasaki-examples
May 22 13:52:56 Finished translator/okasaki-examples                           7m21s   1GB
May 22 13:52:57 Starting translator/other-examples
May 22 13:59:44 Finished translator/other-examples                             6m47s   1GB
May 22 13:59:44 Starting compiler/parsing/tests
May 22 14:00:30 Finished compiler/parsing/tests                                  45s 564MB
May 22 14:00:30 Starting compiler/inference/tests
May 22 14:07:51 Finished compiler/inference/tests                              7m20s   7GB
May 22 14:07:51 Starting compiler/bootstrap/translation
May 22 18:44:03 Finished compiler/bootstrap/translation                     4h36m11s  84GB
May 22 18:44:03 Starting unverified/sexpr-bootstrap/x64/64
May 22 18:55:28 Finished unverified/sexpr-bootstrap/x64/64                    11m24s   6GB
May 22 18:55:28 Starting unverified/sexpr-bootstrap/x64/32
May 22 19:03:47 Finished unverified/sexpr-bootstrap/x64/32                     8m18s   5GB
May 22 19:03:47 Starting compiler/benchmarks
May 22 19:27:46 Finished compiler/benchmarks                                  23m58s   2GB
May 22 19:27:46 Starting compiler/bootstrap/compilation/x64/64
May 23 19:56:20 Finished compiler/bootstrap/compilation/x64/64             24h28m33s 306GB
May 23 19:56:20 Starting compiler/bootstrap/compilation/x64/64/proofs
May 23 20:00:53 Finished compiler/bootstrap/compilation/x64/64/proofs          4m33s  12GB
May 23 20:00:54 Starting compiler/bootstrap/compilation/x64/32
May 24 16:40:22 Finished compiler/bootstrap/compilation/x64/32             20h39m28s 264GB
May 24 16:40:23 Starting compiler/bootstrap/compilation/x64/32/proofs
May 24 16:44:20 Finished compiler/bootstrap/compilation/x64/32/proofs          3m57s  11GB
May 24 16:44:21 Starting compiler/bootstrap/compilation/ag32/32
May 25 13:30:05 Finished compiler/bootstrap/compilation/ag32/32            20h45m43s 206GB
May 25 13:30:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 25 13:46:43 Finished compiler/bootstrap/compilation/ag32/32/proofs        16m38s  30GB
May 25 13:46:44 SUCCESS