Job 814

CakeML:1a2d3084bfdaae5268bd885fdc33519e46ad5612
  Extends loc_offset on ARM8 to 32bits [Apr 22 14:22:15]
#632 (extend_arm8)
Merging into:ccd4671556758a3ad5ce925a7688e8618e915248
  Merge pull request #630 from talsewell/compute-thmset [Apr 20 03:03:19]
HOL:d9d262ad8402d865a72735480268b9f2da63fcd9
  Change ThmSetData to store just theorem names in .dat files [Apr 21 04:26:27]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 23 09:28:54 Claimed job
Apr 23 09:28:57 Reusing HOL
Apr 23 09:29:02 Starting developers
Apr 23 09:29:03 Finished developers                                               0s  21MB
Apr 23 09:29:03 Starting developers/bin
Apr 23 09:29:36 Finished developers/bin                                          31s 205MB
Apr 23 09:29:36 Starting semantics/ffi
Apr 23 09:29:44 Finished semantics/ffi                                            7s 230MB
Apr 23 09:29:44 Starting semantics
Apr 23 09:31:02 Finished semantics                                             1m17s 958MB
Apr 23 09:31:03 Starting semantics/proofs
Apr 23 09:34:00 Finished semantics/proofs                                      2m56s   1GB
Apr 23 09:34:00 Starting basis/pure
Apr 23 09:34:45 Finished basis/pure                                              44s 593MB
Apr 23 09:34:46 Starting translator
Apr 23 09:36:25 Finished translator                                            1m38s   1GB
Apr 23 09:36:25 Starting compiler/parsing
Apr 23 09:37:23 Finished compiler/parsing                                        57s   2GB
Apr 23 09:37:24 Starting characteristic
Apr 23 09:42:36 Finished characteristic                                        5m12s   1GB
Apr 23 09:42:36 Starting translator/monadic
Apr 23 09:44:00 Finished translator/monadic                                    1m23s   1GB
Apr 23 09:44:01 Starting basis
Apr 23 10:00:34 Finished basis                                                16m32s   2GB
Apr 23 10:00:34 Starting compiler/inference
Apr 23 10:02:06 Finished compiler/inference                                    1m31s   1GB
Apr 23 10:02:07 Starting compiler/backend/reg_alloc
Apr 23 10:02:58 Finished compiler/backend/reg_alloc                              51s   1GB
Apr 23 10:02:58 Starting compiler/backend/gc
Apr 23 10:11:01 Finished compiler/backend/gc                                   8m02s   2GB
Apr 23 10:11:01 Starting compiler/backend
Apr 23 10:11:02 Finished compiler/backend                                         0s  42MB
Apr 23 10:11:03 Starting compiler/encoders/asm
Apr 23 10:11:03 Finished compiler/encoders/asm                                    0s  32MB
Apr 23 10:11:04 Starting compiler/encoders/x64
Apr 23 10:11:27 Finished compiler/encoders/x64                                   22s 648MB
Apr 23 10:11:27 Starting compiler/encoders/arm6
Apr 23 10:12:11 Finished compiler/encoders/arm6                                  43s 742MB
Apr 23 10:12:12 Starting compiler/encoders/arm8
Apr 23 10:12:24 Finished compiler/encoders/arm8                                  11s 883MB
Apr 23 10:12:24 Starting compiler/encoders/mips
Apr 23 10:12:40 Finished compiler/encoders/mips                                  15s   1GB
Apr 23 10:12:40 Starting compiler/encoders/riscv
Apr 23 10:12:54 Finished compiler/encoders/riscv                                 13s 955MB
Apr 23 10:12:54 Starting compiler/encoders/ag32
Apr 23 10:13:09 Finished compiler/encoders/ag32                                  14s 750MB
Apr 23 10:13:10 Starting compiler/backend/x64
Apr 23 10:13:26 Finished compiler/backend/x64                                    15s   1GB
Apr 23 10:13:26 Starting compiler/backend/arm6
Apr 23 10:13:44 Finished compiler/backend/arm6                                   17s   1GB
Apr 23 10:13:44 Starting compiler/backend/arm8
Apr 23 10:14:00 Finished compiler/backend/arm8                                   15s   1GB
Apr 23 10:14:01 Starting compiler/backend/mips
Apr 23 10:14:17 Finished compiler/backend/mips                                   16s   1GB
Apr 23 10:14:17 Starting compiler/backend/riscv
Apr 23 10:14:33 Finished compiler/backend/riscv                                  15s   1GB
Apr 23 10:14:33 Starting compiler/backend/ag32
Apr 23 10:15:40 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 23 10:15:40 Starting compiler/parsing/proofs
Apr 23 10:21:15 Finished compiler/parsing/proofs                               5m34s 800MB
Apr 23 10:21:16 Starting compiler/inference/proofs
Apr 23 10:23:55 Finished compiler/inference/proofs                             2m39s   1GB
Apr 23 10:23:56 Starting compiler/backend/semantics
Apr 23 10:31:04 Finished compiler/backend/semantics                            7m07s   1GB
Apr 23 10:31:04 Starting compiler/backend/reg_alloc/proofs
Apr 23 10:33:43 Finished compiler/backend/reg_alloc/proofs                     2m38s   1GB
Apr 23 10:33:44 Starting compiler/backend/proofs
Apr 23 11:12:33 Finished compiler/backend/proofs                              38m49s   3GB
Apr 23 11:12:34 Starting compiler/encoders/x64/proofs
Apr 23 11:21:50 Finished compiler/encoders/x64/proofs                          9m16s   4GB
Apr 23 11:21:51 Starting compiler/encoders/arm6/proofs
Apr 23 11:34:33 Finished compiler/encoders/arm6/proofs                        12m41s   3GB
Apr 23 11:34:33 Starting compiler/encoders/arm8/proofs
Apr 23 11:41:11 Finished compiler/encoders/arm8/proofs                         6m37s   1GB
Apr 23 11:41:11 Starting compiler/encoders/mips/proofs
Apr 23 11:50:43 Finished compiler/encoders/mips/proofs                         9m31s   3GB
Apr 23 11:50:44 Starting compiler/encoders/riscv/proofs
Apr 23 11:59:10 Finished compiler/encoders/riscv/proofs                        8m26s 996MB
Apr 23 11:59:10 Starting compiler/encoders/ag32/proofs
Apr 23 12:01:40 Finished compiler/encoders/ag32/proofs                         2m29s 678MB
Apr 23 12:01:40 Starting compiler/backend/x64/proofs
Apr 23 12:01:57 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 23 12:01:57 Starting compiler/backend/arm6/proofs
Apr 23 12:02:17 Finished compiler/backend/arm6/proofs                            19s   1GB
Apr 23 12:02:17 Starting compiler/backend/arm8/proofs
Apr 23 12:02:33 Finished compiler/backend/arm8/proofs                            15s 811MB
Apr 23 12:02:33 Starting compiler/backend/mips/proofs
Apr 23 12:02:50 Finished compiler/backend/mips/proofs                            16s   1GB
Apr 23 12:02:50 Starting compiler/backend/riscv/proofs
Apr 23 12:03:07 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 23 12:03:08 Starting compiler/backend/ag32/proofs
Apr 23 12:12:16 Finished compiler/backend/ag32/proofs                          9m08s   2GB
Apr 23 12:12:17 Starting compiler/proofs
Apr 23 12:13:41 Finished compiler/proofs                                       1m23s   2GB
Apr 23 12:13:41 Starting candle/set-theory
Apr 23 12:14:06 Finished candle/set-theory                                       24s 683MB
Apr 23 12:14:06 Starting candle/syntax-lib
Apr 23 12:14:16 Finished candle/syntax-lib                                        9s 633MB
Apr 23 12:14:16 Starting candle/standard/syntax
Apr 23 12:15:59 Finished candle/standard/syntax                                1m42s   1GB
Apr 23 12:16:00 Starting candle/standard/semantics
Apr 23 12:17:34 Finished candle/standard/semantics                             1m34s   1GB
Apr 23 12:17:35 Starting candle/standard/monadic
Apr 23 12:19:08 Finished candle/standard/monadic                               1m32s   1GB
Apr 23 12:19:08 Starting candle/standard/ml_kernel
Apr 23 12:22:54 Finished candle/standard/ml_kernel                             3m45s   6GB
Apr 23 12:22:55 Starting candle/standard/opentheory
Apr 23 12:31:18 Finished candle/standard/opentheory                            8m23s   3GB
Apr 23 12:31:19 Starting candle/standard/opentheory/compilation
Apr 23 13:01:25 Finished candle/standard/opentheory/compilation               30m06s  13GB
Apr 23 13:01:26 Starting candle/standard/opentheory/compilation/proofs
Apr 23 13:02:18 Finished candle/standard/opentheory/compilation/proofs           52s   2GB
Apr 23 13:02:19 Starting characteristic/examples
Apr 23 13:03:41 Finished characteristic/examples                               1m22s   1GB
Apr 23 13:03:42 Starting tutorial/solutions
Apr 23 13:16:58 Finished tutorial/solutions                                   13m15s   6GB
Apr 23 13:16:58 Starting translator/monadic/examples
Apr 23 13:19:28 Finished translator/monadic/examples                           2m27s   2GB
Apr 23 13:19:28 Starting examples
Apr 23 13:28:00 Finished examples                                              8m31s   4GB
Apr 23 13:28:01 Starting examples/compilation/x64
Apr 23 15:22:15 Finished examples/compilation/x64                           1h54m14s  13GB
Apr 23 15:22:16 Starting examples/compilation/x64/proofs
Apr 23 15:23:40 Finished examples/compilation/x64/proofs                       1m24s   2GB
Apr 23 15:23:41 Starting examples/compilation/ag32
Apr 23 15:52:36 Finished examples/compilation/ag32                            28m55s   5GB
Apr 23 15:52:36 Starting examples/compilation/ag32/proofs
Apr 23 15:53:31 Finished examples/compilation/ag32/proofs                        53s   2GB
Apr 23 15:53:31 Starting translator/okasaki-examples
Apr 23 15:57:43 Finished translator/okasaki-examples                           4m11s   1GB
Apr 23 15:57:43 Starting translator/other-examples
Apr 23 16:01:09 Finished translator/other-examples                             3m25s   1GB
Apr 23 16:01:09 Starting compiler/parsing/tests
Apr 23 16:01:34 Finished compiler/parsing/tests                                  24s 541MB
Apr 23 16:01:34 Starting compiler/inference/tests
Apr 23 16:05:48 Finished compiler/inference/tests                              4m13s   4GB
Apr 23 16:05:48 Starting compiler/bootstrap/translation
Apr 23 18:30:12 Finished compiler/bootstrap/translation                     2h24m23s  33GB
Apr 23 18:30:13 Starting unverified/sexpr-bootstrap/x64/64
Apr 23 18:37:29 Finished unverified/sexpr-bootstrap/x64/64                     7m15s   2GB
Apr 23 18:37:29 Starting unverified/sexpr-bootstrap/x64/32
Apr 23 18:41:58 Finished unverified/sexpr-bootstrap/x64/32                     4m28s   6GB
Apr 23 18:41:58 Starting compiler/benchmarks
Apr 23 19:20:11 Finished compiler/benchmarks                                  38m12s   1GB
Apr 23 19:20:11 Starting compiler/bootstrap/compilation/x64/64
Apr 24 05:56:11 Finished compiler/bootstrap/compilation/x64/64             10h35m57s  64GB
Apr 24 05:56:11 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 24 06:00:08 Finished compiler/bootstrap/compilation/x64/64/proofs          3m56s   4GB
Apr 24 06:00:08 Starting compiler/bootstrap/compilation/x64/32
Apr 24 16:07:43 Finished compiler/bootstrap/compilation/x64/32             10h07m34s  56GB
Apr 24 16:07:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 24 16:09:36 Finished compiler/bootstrap/compilation/x64/32/proofs          1m51s  10GB
Apr 24 16:09:36 Starting compiler/bootstrap/compilation/ag32/32
Apr 25 02:23:53 Finished compiler/bootstrap/compilation/ag32/32            10h14m16s  64GB
Apr 25 02:23:54 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 25 02:37:07 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m13s  12GB
Apr 25 02:37:08 SUCCESS