Job 582

CakeML:5716e686a48f8ae55f4a4512ff05993964d64379
  Fix proofs [Nov 23 10:49:24]
#562 (issue548)
Merging into:9198606c60fba7a58aaad203a4814adb5383d2f7
  Merge pull request #554 from CakeML/tiny [Nov 24 22:25:55]
HOL:1601ee10ec6c927e058311a9fb12a220d44b4a7c
  Make holpathdb bindings available in base Holmake variable environment [Nov 23 11:14:13]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 25 10:30:49 Claimed job
Nov 25 10:30:58 Building HOL
Nov 25 10:38:47 Starting developers/bin
Nov 25 10:39:18 Finished developers/bin                                          29s 201MB
Nov 25 10:39:19 Starting semantics/ffi
Nov 25 10:39:55 Finished semantics/ffi                                           35s 403MB
Nov 25 10:39:55 Starting semantics
Nov 25 10:41:22 Finished semantics                                             1m25s   1GB
Nov 25 10:41:23 Starting semantics/proofs
Nov 25 10:44:17 Finished semantics/proofs                                      2m53s   1GB
Nov 25 10:44:18 Starting basis/pure
Nov 25 10:47:53 Finished basis/pure                                            3m34s 649MB
Nov 25 10:47:54 Starting translator
Nov 25 10:50:58 Finished translator                                            3m03s 945MB
Nov 25 10:50:59 Starting compiler/parsing
Nov 25 10:52:15 Finished compiler/parsing                                      1m15s   1GB
Nov 25 10:52:15 Starting characteristic
Nov 25 10:54:42 Finished characteristic                                        2m26s   1GB
Nov 25 10:54:43 Starting translator/monadic
Nov 25 10:56:06 Finished translator/monadic                                    1m22s   1GB
Nov 25 10:56:07 Starting basis
Nov 25 11:12:20 Finished basis                                                16m11s   2GB
Nov 25 11:12:21 Starting compiler/inference
Nov 25 11:14:00 Finished compiler/inference                                    1m37s   1GB
Nov 25 11:14:01 Starting compiler/backend/reg_alloc
Nov 25 11:14:47 Finished compiler/backend/reg_alloc                              45s   1GB
Nov 25 11:14:47 Starting compiler/backend/gc
Nov 25 11:22:08 Finished compiler/backend/gc                                   7m19s   1GB
Nov 25 11:22:09 Starting compiler/backend
Nov 25 11:22:11 Finished compiler/backend                                         1s  15MB
Nov 25 11:22:12 Starting compiler/encoders/asm
Nov 25 11:22:14 Finished compiler/encoders/asm                                    0s  12MB
Nov 25 11:22:15 Starting compiler/encoders/x64
Nov 25 11:23:04 Finished compiler/encoders/x64                                   48s 659MB
Nov 25 11:23:05 Starting compiler/encoders/arm6
Nov 25 11:24:48 Finished compiler/encoders/arm6                                1m42s   1GB
Nov 25 11:24:49 Starting compiler/encoders/arm8
Nov 25 11:25:14 Finished compiler/encoders/arm8                                  24s 450MB
Nov 25 11:25:15 Starting compiler/encoders/mips
Nov 25 11:26:12 Finished compiler/encoders/mips                                  56s 886MB
Nov 25 11:26:12 Starting compiler/encoders/riscv
Nov 25 11:27:12 Finished compiler/encoders/riscv                                 58s 906MB
Nov 25 11:27:13 Starting compiler/encoders/ag32
Nov 25 11:27:30 Finished compiler/encoders/ag32                                  15s 477MB
Nov 25 11:27:30 Starting compiler/backend/x64
Nov 25 11:27:47 Finished compiler/backend/x64                                    16s 791MB
Nov 25 11:27:48 Starting compiler/backend/arm6
Nov 25 11:28:08 Finished compiler/backend/arm6                                   19s   1GB
Nov 25 11:28:09 Starting compiler/backend/arm8
Nov 25 11:28:27 Finished compiler/backend/arm8                                   17s   1GB
Nov 25 11:28:28 Starting compiler/backend/mips
Nov 25 11:28:46 Finished compiler/backend/mips                                   16s 972MB
Nov 25 11:28:46 Starting compiler/backend/riscv
Nov 25 11:29:04 Finished compiler/backend/riscv                                  17s   1GB
Nov 25 11:29:05 Starting compiler/backend/ag32
Nov 25 11:30:21 Finished compiler/backend/ag32                                 1m14s   1GB
Nov 25 11:30:21 Starting compiler/parsing/proofs
Nov 25 11:36:24 Finished compiler/parsing/proofs                               6m02s 825MB
Nov 25 11:36:25 Starting compiler/inference/proofs
Nov 25 11:39:17 Finished compiler/inference/proofs                             2m51s   1GB
Nov 25 11:39:18 Starting compiler/backend/semantics
Nov 25 11:48:21 Finished compiler/backend/semantics                            9m02s   2GB
Nov 25 11:48:22 Starting compiler/backend/reg_alloc/proofs
Nov 25 11:51:03 Finished compiler/backend/reg_alloc/proofs                     2m40s 526MB
Nov 25 11:51:04 Starting compiler/backend/proofs
Nov 25 12:36:55 Finished compiler/backend/proofs                              45m50s   3GB
Nov 25 12:36:56 Starting compiler/encoders/x64/proofs
Nov 25 12:47:25 Finished compiler/encoders/x64/proofs                         10m28s   5GB
Nov 25 12:47:26 Starting compiler/encoders/arm6/proofs
Nov 25 13:02:26 Finished compiler/encoders/arm6/proofs                        14m59s   3GB
Nov 25 13:02:27 Starting compiler/encoders/arm8/proofs
Nov 25 13:08:31 Finished compiler/encoders/arm8/proofs                         6m02s   1GB
Nov 25 13:08:31 Starting compiler/encoders/mips/proofs
Nov 25 13:19:02 Finished compiler/encoders/mips/proofs                        10m29s   2GB
Nov 25 13:19:02 Starting compiler/encoders/riscv/proofs
Nov 25 13:27:03 Finished compiler/encoders/riscv/proofs                        8m00s 844MB
Nov 25 13:27:04 Starting compiler/encoders/ag32/proofs
Nov 25 13:29:49 Finished compiler/encoders/ag32/proofs                         2m43s 679MB
Nov 25 13:29:49 Starting compiler/backend/x64/proofs
Nov 25 13:30:09 Finished compiler/backend/x64/proofs                             19s   1GB
Nov 25 13:30:10 Starting compiler/backend/arm6/proofs
Nov 25 13:30:33 Finished compiler/backend/arm6/proofs                            21s   1GB
Nov 25 13:30:34 Starting compiler/backend/arm8/proofs
Nov 25 13:30:54 Finished compiler/backend/arm8/proofs                            19s   1GB
Nov 25 13:30:54 Starting compiler/backend/mips/proofs
Nov 25 13:31:16 Finished compiler/backend/mips/proofs                            21s   1GB
Nov 25 13:31:17 Starting compiler/backend/riscv/proofs
Nov 25 13:31:38 Finished compiler/backend/riscv/proofs                           19s   1GB
Nov 25 13:31:38 Starting compiler/backend/ag32/proofs
Nov 25 13:41:38 Finished compiler/backend/ag32/proofs                          9m59s   3GB
Nov 25 13:41:39 Starting compiler/proofs
Nov 25 13:42:59 Finished compiler/proofs                                       1m18s   1GB
Nov 25 13:42:59 Starting candle/set-theory
Nov 25 13:43:29 Finished candle/set-theory                                       29s 611MB
Nov 25 13:43:30 Starting candle/syntax-lib
Nov 25 13:43:40 Finished candle/syntax-lib                                        9s 529MB
Nov 25 13:43:41 Starting candle/standard/syntax
Nov 25 13:45:14 Finished candle/standard/syntax                                1m31s   1GB
Nov 25 13:45:14 Starting candle/standard/semantics
Nov 25 13:46:34 Finished candle/standard/semantics                             1m19s 756MB
Nov 25 13:46:35 Starting candle/standard/monadic
Nov 25 13:48:09 Finished candle/standard/monadic                               1m33s   1GB
Nov 25 13:48:10 Starting candle/standard/ml_kernel
Nov 25 14:03:30 Finished candle/standard/ml_kernel                            15m19s   3GB
Nov 25 14:03:30 Starting candle/standard/opentheory
Nov 25 14:11:21 Finished candle/standard/opentheory                            7m49s   2GB
Nov 25 14:11:22 Starting candle/standard/opentheory/compilation
Nov 25 14:41:31 Finished candle/standard/opentheory/compilation               30m08s  16GB
Nov 25 14:41:32 Starting candle/standard/opentheory/compilation/proofs
Nov 25 14:42:09 Finished candle/standard/opentheory/compilation/proofs           36s   4GB
Nov 25 14:42:10 Starting characteristic/examples
Nov 25 14:43:39 Finished characteristic/examples                               1m28s   2GB
Nov 25 14:43:40 Starting tutorial/solutions
Nov 25 14:57:05 Finished tutorial/solutions                                   13m23s   7GB
Nov 25 14:57:05 Starting translator/monadic/examples
Nov 25 14:58:51 Finished translator/monadic/examples                           1m44s   2GB
Nov 25 14:58:51 Starting examples
Nov 25 15:05:21 Finished examples                                              6m29s   2GB
Nov 25 15:05:22 Starting examples/compilation/x64
Nov 25 17:00:52 Finished examples/compilation/x64                           1h55m28s  10GB
Nov 25 17:00:53 Starting examples/compilation/x64/proofs
Nov 25 17:02:43 Finished examples/compilation/x64/proofs                       1m49s   3GB
Nov 25 17:02:44 Starting examples/compilation/ag32
Nov 25 17:29:16 Finished examples/compilation/ag32                            26m30s   5GB
Nov 25 17:29:17 Starting examples/compilation/ag32/proofs
Nov 25 17:29:43 Finished examples/compilation/ag32/proofs                        25s   2GB
Nov 25 17:29:44 Starting compiler/benchmarks
Nov 25 17:29:45 Finished compiler/benchmarks                                      0s   4MB
Nov 25 17:29:46 Starting translator/okasaki-examples
Nov 25 17:33:19 Finished translator/okasaki-examples                           3m32s   2GB
Nov 25 17:33:20 Starting translator/other-examples
Nov 25 17:36:45 Finished translator/other-examples                             3m24s   1GB
Nov 25 17:36:46 Starting compiler/parsing/tests
Nov 25 17:37:11 Finished compiler/parsing/tests                                  24s 320MB
Nov 25 17:37:12 Starting compiler/inference/tests
Nov 25 17:41:12 Finished compiler/inference/tests                              3m58s   4GB
Nov 25 17:41:12 Starting compiler/bootstrap/translation
Nov 25 20:56:01 Finished compiler/bootstrap/translation                     3h14m46s  40GB
Nov 25 20:56:01 Starting unverified/sexpr-bootstrap/x64/64
Nov 25 21:04:12 Finished unverified/sexpr-bootstrap/x64/64                     8m10s  13GB
Nov 25 21:04:13 Starting unverified/sexpr-bootstrap/x64/32
Nov 25 21:09:53 Finished unverified/sexpr-bootstrap/x64/32                     5m39s  20GB
Nov 25 21:09:54 Starting compiler/bootstrap/compilation/x64/64
Nov 26 08:54:43 Finished compiler/bootstrap/compilation/x64/64             11h44m48s  64GB
Nov 26 08:54:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 26 08:58:08 Finished compiler/bootstrap/compilation/x64/64/proofs          3m23s  24GB
Nov 26 08:58:09 Starting compiler/bootstrap/compilation/x64/32
Nov 26 20:45:52 Finished compiler/bootstrap/compilation/x64/32             11h47m41s  63GB
Nov 26 20:45:52 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 26 20:49:21 Finished compiler/bootstrap/compilation/x64/32/proofs          3m28s  22GB
Nov 26 20:49:22 SUCCESS