Job 858

CakeML:c3401d437bf9ee17407b3c33d54cf9b8eb77d3c6
  Fix some variable names after switch to HOL's spt theorems [May 10 16:43:09]
#643 (cleanup)
Merging into:53fd12a2f3ee14927097506986b55a5d2bcf1b97
  Merge pull request #641 from CakeML/issue465 [May 10 05:54:52]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 10 18:48:01 Claimed job
May 10 18:48:06 Reusing HOL
May 10 18:48:10 Starting developers
May 10 18:48:11 Finished developers                                               0s  21MB
May 10 18:48:11 Starting developers/bin
May 10 18:48:14 Finished developers/bin                                           3s 144MB
May 10 18:48:15 Starting semantics/ffi
May 10 18:48:23 Finished semantics/ffi                                            7s 218MB
May 10 18:48:23 Starting semantics
May 10 18:49:39 Finished semantics                                             1m15s 977MB
May 10 18:49:39 Starting semantics/proofs
May 10 18:52:35 Finished semantics/proofs                                      2m55s   1GB
May 10 18:52:35 Starting basis/pure
May 10 18:53:20 Finished basis/pure                                              43s 875MB
May 10 18:53:20 Starting translator
May 10 18:54:56 Finished translator                                            1m35s   1GB
May 10 18:54:56 Starting compiler/parsing
May 10 18:55:53 Finished compiler/parsing                                        56s   1GB
May 10 18:55:53 Starting characteristic
May 10 19:00:58 Finished characteristic                                        5m04s   1GB
May 10 19:00:59 Starting translator/monadic
May 10 19:02:25 Finished translator/monadic                                    1m26s   1GB
May 10 19:02:25 Starting basis
May 10 19:19:07 Finished basis                                                16m40s   2GB
May 10 19:19:07 Starting compiler/inference
May 10 19:20:36 Finished compiler/inference                                    1m28s   2GB
May 10 19:20:37 Starting compiler/backend/reg_alloc
May 10 19:21:33 Finished compiler/backend/reg_alloc                              56s   1GB
May 10 19:21:34 Starting compiler/backend/gc
May 10 19:29:22 Finished compiler/backend/gc                                   7m48s   2GB
May 10 19:29:23 Starting compiler/backend
May 10 19:29:24 Finished compiler/backend                                         0s  42MB
May 10 19:29:24 Starting compiler/encoders/asm
May 10 19:29:25 Finished compiler/encoders/asm                                    0s  32MB
May 10 19:29:25 Starting compiler/encoders/x64
May 10 19:29:47 Finished compiler/encoders/x64                                   22s 948MB
May 10 19:29:48 Starting compiler/encoders/arm6
May 10 19:30:31 Finished compiler/encoders/arm6                                  43s 757MB
May 10 19:30:31 Starting compiler/encoders/arm8
May 10 19:30:43 Finished compiler/encoders/arm8                                  10s 541MB
May 10 19:30:43 Starting compiler/encoders/mips
May 10 19:30:59 Finished compiler/encoders/mips                                  16s 966MB
May 10 19:31:00 Starting compiler/encoders/riscv
May 10 19:31:13 Finished compiler/encoders/riscv                                 12s 784MB
May 10 19:31:13 Starting compiler/encoders/ag32
May 10 19:31:28 Finished compiler/encoders/ag32                                  14s 613MB
May 10 19:31:28 Starting compiler/backend/x64
May 10 19:31:44 Finished compiler/backend/x64                                    15s   1GB
May 10 19:31:44 Starting compiler/backend/arm6
May 10 19:32:02 Finished compiler/backend/arm6                                   17s   1GB
May 10 19:32:02 Starting compiler/backend/arm8
May 10 19:32:19 Finished compiler/backend/arm8                                   16s   1GB
May 10 19:32:19 Starting compiler/backend/mips
May 10 19:32:36 Finished compiler/backend/mips                                   16s   1GB
May 10 19:32:37 Starting compiler/backend/riscv
May 10 19:32:53 Finished compiler/backend/riscv                                  15s   1GB
May 10 19:32:53 Starting compiler/backend/ag32
May 10 19:34:01 Finished compiler/backend/ag32                                 1m07s   1GB
May 10 19:34:01 Starting compiler/parsing/proofs
May 10 19:39:30 Finished compiler/parsing/proofs                               5m28s 820MB
May 10 19:39:30 Starting compiler/inference/proofs
May 10 19:42:08 Finished compiler/inference/proofs                             2m37s 854MB
May 10 19:42:08 Starting compiler/backend/semantics
May 10 19:49:00 Finished compiler/backend/semantics                            6m51s   1GB
May 10 19:49:00 Starting compiler/backend/reg_alloc/proofs
May 10 19:52:19 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
May 10 19:52:19 Starting compiler/backend/proofs
May 10 20:29:32 Finished compiler/backend/proofs                              37m12s   5GB
May 10 20:29:33 Starting compiler/encoders/x64/proofs
May 10 20:38:32 Finished compiler/encoders/x64/proofs                          8m59s   5GB
May 10 20:38:32 Starting compiler/encoders/arm6/proofs
May 10 20:50:51 Finished compiler/encoders/arm6/proofs                        12m17s   3GB
May 10 20:50:51 Starting compiler/encoders/arm8/proofs
May 10 20:57:30 Finished compiler/encoders/arm8/proofs                         6m39s   1GB
May 10 20:57:31 Starting compiler/encoders/mips/proofs
May 10 21:07:33 Finished compiler/encoders/mips/proofs                        10m01s   1GB
May 10 21:07:33 Starting compiler/encoders/riscv/proofs
May 10 21:15:53 Finished compiler/encoders/riscv/proofs                        8m19s   1GB
May 10 21:15:53 Starting compiler/encoders/ag32/proofs
May 10 21:18:20 Finished compiler/encoders/ag32/proofs                         2m26s 798MB
May 10 21:18:20 Starting compiler/backend/x64/proofs
May 10 21:18:37 Finished compiler/backend/x64/proofs                             16s   1GB
May 10 21:18:37 Starting compiler/backend/arm6/proofs
May 10 21:18:55 Finished compiler/backend/arm6/proofs                            17s   1GB
May 10 21:18:55 Starting compiler/backend/arm8/proofs
May 10 21:19:11 Finished compiler/backend/arm8/proofs                            15s 918MB
May 10 21:19:11 Starting compiler/backend/mips/proofs
May 10 21:19:28 Finished compiler/backend/mips/proofs                            17s   1GB
May 10 21:19:29 Starting compiler/backend/riscv/proofs
May 10 21:19:45 Finished compiler/backend/riscv/proofs                           16s   1GB
May 10 21:19:46 Starting compiler/backend/ag32/proofs
May 10 21:28:40 Finished compiler/backend/ag32/proofs                          8m53s   2GB
May 10 21:28:40 Starting compiler/proofs
May 10 21:29:52 Finished compiler/proofs                                       1m11s   2GB
May 10 21:29:52 Starting candle/set-theory
May 10 21:30:17 Finished candle/set-theory                                       24s 682MB
May 10 21:30:17 Starting candle/syntax-lib
May 10 21:30:27 Finished candle/syntax-lib                                        8s 626MB
May 10 21:30:27 Starting candle/standard/syntax
May 10 21:32:07 Finished candle/standard/syntax                                1m40s   1GB
May 10 21:32:08 Starting candle/standard/semantics
May 10 21:33:41 Finished candle/standard/semantics                             1m33s   1GB
May 10 21:33:42 Starting candle/standard/monadic
May 10 21:35:14 Finished candle/standard/monadic                               1m32s   1GB
May 10 21:35:15 Starting candle/standard/ml_kernel
May 10 21:39:04 Finished candle/standard/ml_kernel                             3m49s   3GB
May 10 21:39:04 Starting candle/standard/opentheory
May 10 21:47:22 Finished candle/standard/opentheory                            8m17s   3GB
May 10 21:47:23 Starting candle/standard/opentheory/compilation
May 10 22:16:41 Finished candle/standard/opentheory/compilation               29m17s  13GB
May 10 22:16:41 Starting candle/standard/opentheory/compilation/proofs
May 10 22:17:19 Finished candle/standard/opentheory/compilation/proofs           38s   2GB
May 10 22:17:20 Starting characteristic/examples
May 10 22:18:42 Finished characteristic/examples                               1m21s   2GB
May 10 22:18:42 Starting tutorial/solutions
May 10 22:31:26 Finished tutorial/solutions                                   12m43s   6GB
May 10 22:31:26 Starting translator/monadic/examples
May 10 22:34:17 Finished translator/monadic/examples                           2m50s   2GB
May 10 22:34:18 Starting examples
May 10 22:42:54 Finished examples                                              8m36s   3GB
May 10 22:42:54 Starting examples/compilation/x64
May 11 00:43:02 Finished examples/compilation/x64                           2h00m07s  15GB
May 11 00:43:02 Starting examples/compilation/x64/proofs
May 11 00:44:28 Finished examples/compilation/x64/proofs                       1m25s   2GB
May 11 00:44:28 Starting examples/compilation/ag32
May 11 01:11:49 Finished examples/compilation/ag32                            27m20s   6GB
May 11 01:11:50 Starting examples/compilation/ag32/proofs
May 11 01:12:36 Finished examples/compilation/ag32/proofs                        46s   2GB
May 11 01:12:37 Starting translator/okasaki-examples
May 11 01:16:42 Finished translator/okasaki-examples                           4m04s   1GB
May 11 01:16:42 Starting translator/other-examples
May 11 01:20:03 Finished translator/other-examples                             3m20s   1GB
May 11 01:20:03 Starting compiler/parsing/tests
May 11 01:20:27 Finished compiler/parsing/tests                                  23s 550MB
May 11 01:20:27 Starting compiler/inference/tests
May 11 01:24:35 Finished compiler/inference/tests                              4m07s   4GB
May 11 01:24:35 Starting compiler/bootstrap/translation
May 11 03:50:11 Finished compiler/bootstrap/translation                     2h25m35s  33GB
May 11 03:50:11 Starting unverified/sexpr-bootstrap/x64/64
May 11 03:57:14 Finished unverified/sexpr-bootstrap/x64/64                     7m03s   3GB
May 11 03:57:15 Starting unverified/sexpr-bootstrap/x64/32
May 11 04:01:46 Finished unverified/sexpr-bootstrap/x64/32                     4m31s   6GB
May 11 04:01:46 Starting compiler/benchmarks
May 11 04:39:44 Finished compiler/benchmarks                                  37m57s   2GB
May 11 04:39:44 Starting compiler/bootstrap/compilation/x64/64
May 11 14:46:09 Finished compiler/bootstrap/compilation/x64/64             10h06m23s  63GB
May 11 14:46:09 Starting compiler/bootstrap/compilation/x64/64/proofs
May 11 14:49:22 Finished compiler/bootstrap/compilation/x64/64/proofs          3m12s   5GB
May 11 14:49:23 Starting compiler/bootstrap/compilation/x64/32
May 12 00:01:52 Finished compiler/bootstrap/compilation/x64/32              9h12m28s  64GB
May 12 00:01:53 Starting compiler/bootstrap/compilation/x64/32/proofs
May 12 00:04:54 Finished compiler/bootstrap/compilation/x64/32/proofs          3m00s   4GB
May 12 00:04:54 Starting compiler/bootstrap/compilation/ag32/32
May 12 09:54:54 Finished compiler/bootstrap/compilation/ag32/32             9h49m59s  63GB
May 12 09:54:55 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 12 10:25:56 Finished compiler/bootstrap/compilation/ag32/32/proofs        31m01s  16GB
May 12 10:25:56 SUCCESS