Job 1206

CakeML:af4fe7db1744fab35b0c5111130b3a0789d96e94
  Merge remote-tracking branch 'origin/master' into trans-pure-seq [Mar 13 08:53:18]
#733 (trans-pure-seq)
Merging into:45617dff3e8e8a2fb75036081dfa74919b8e6390
  Apply fix that Konrad recommends [Mar 13 08:52:50]
HOL:ba25c5756203bd0ef0d73e04022916ccb291e1e5
  Write some comment-documentation [Mar 10 00:09:00]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 13 08:53:50 Claimed job
Mar 13 08:53:55 Reusing HOL
Mar 13 08:54:06 Starting developers
Mar 13 08:54:08 Finished developers                                               2s  98MB
Mar 13 08:54:09 Starting developers/bin
Mar 13 08:54:15 Finished developers/bin                                           6s   1GB
Mar 13 08:54:15 Starting semantics/ffi
Mar 13 08:54:24 Finished semantics/ffi                                            8s 248MB
Mar 13 08:54:24 Starting semantics
Mar 13 08:55:42 Finished semantics                                             1m17s   1GB
Mar 13 08:55:42 Starting semantics/proofs
Mar 13 08:58:51 Finished semantics/proofs                                      3m09s   1GB
Mar 13 08:58:52 Starting semantics/alt_semantics
Mar 13 08:58:59 Finished semantics/alt_semantics                                  6s 332MB
Mar 13 08:58:59 Starting semantics/alt_semantics/proofs
Mar 13 09:00:59 Finished semantics/alt_semantics/proofs                        1m59s 865MB
Mar 13 09:00:59 Starting basis/pure
Mar 13 09:01:46 Finished basis/pure                                              47s 699MB
Mar 13 09:01:47 Starting translator
Mar 13 09:04:16 Finished translator                                            2m29s   1GB
Mar 13 09:04:16 Starting compiler/parsing
Mar 13 09:05:24 Finished compiler/parsing                                      1m07s   1GB
Mar 13 09:05:24 Starting characteristic
Mar 13 09:11:04 Finished characteristic                                        5m39s   2GB
Mar 13 09:11:04 Starting translator/monadic
Mar 13 09:12:36 Finished translator/monadic                                    1m31s   1GB
Mar 13 09:12:36 Starting basis
Mar 13 09:42:51 Finished basis                                                30m14s  24GB
Mar 13 09:42:51 Starting compiler/inference
Mar 13 09:43:50 Finished compiler/inference                                      58s   1GB
Mar 13 09:43:50 Starting compiler/backend/reg_alloc
Mar 13 09:44:53 Finished compiler/backend/reg_alloc                            1m02s   1GB
Mar 13 09:44:53 Starting compiler/backend/gc
Mar 13 09:48:06 Finished compiler/backend/gc                                   3m13s   2GB
Mar 13 09:48:07 Starting compiler/backend
Mar 13 09:52:38 Finished compiler/backend                                      4m30s   3GB
Mar 13 09:52:38 Starting compiler/encoders/asm
Mar 13 09:52:59 Finished compiler/encoders/asm                                   21s 837MB
Mar 13 09:52:59 Starting compiler/encoders/x64
Mar 13 09:53:24 Finished compiler/encoders/x64                                   24s 986MB
Mar 13 09:53:24 Starting compiler/encoders/arm7
Mar 13 09:54:17 Finished compiler/encoders/arm7                                  52s 853MB
Mar 13 09:54:17 Starting compiler/encoders/arm8
Mar 13 09:54:29 Finished compiler/encoders/arm8                                  11s 890MB
Mar 13 09:54:29 Starting compiler/encoders/mips
Mar 13 09:54:45 Finished compiler/encoders/mips                                  16s   1GB
Mar 13 09:54:46 Starting compiler/encoders/riscv
Mar 13 09:54:59 Finished compiler/encoders/riscv                                 13s 771MB
Mar 13 09:54:59 Starting compiler/encoders/ag32
Mar 13 09:55:16 Finished compiler/encoders/ag32                                  16s 793MB
Mar 13 09:55:16 Starting compiler/backend/x64
Mar 13 09:55:34 Finished compiler/backend/x64                                    17s   1GB
Mar 13 09:55:34 Starting compiler/backend/arm7
Mar 13 09:55:53 Finished compiler/backend/arm7                                   19s   1GB
Mar 13 09:55:53 Starting compiler/backend/arm8
Mar 13 09:56:12 Finished compiler/backend/arm8                                   18s   1GB
Mar 13 09:56:12 Starting compiler/backend/mips
Mar 13 09:56:30 Finished compiler/backend/mips                                   18s   1GB
Mar 13 09:56:31 Starting compiler/backend/riscv
Mar 13 09:56:49 Finished compiler/backend/riscv                                  18s   1GB
Mar 13 09:56:50 Starting compiler/backend/ag32
Mar 13 09:57:57 Finished compiler/backend/ag32                                 1m07s   1GB
Mar 13 09:57:57 Starting compiler/parsing/proofs
Mar 13 10:03:40 Finished compiler/parsing/proofs                               5m42s   1GB
Mar 13 10:03:40 Starting compiler/inference/proofs
Mar 13 10:06:01 Finished compiler/inference/proofs                             2m20s   1GB
Mar 13 10:06:01 Starting compiler/backend/semantics
Mar 13 10:34:34 Finished compiler/backend/semantics                           28m32s   2GB
Mar 13 10:34:34 Starting compiler/backend/reg_alloc/proofs
Mar 13 10:38:19 Finished compiler/backend/reg_alloc/proofs                     3m44s 970MB
Mar 13 10:38:19 Starting compiler/backend/proofs
Mar 13 11:44:39 Finished compiler/backend/proofs                            1h06m19s  18GB
Mar 13 11:44:39 Starting compiler/encoders/x64/proofs
Mar 13 11:53:52 Finished compiler/encoders/x64/proofs                          9m12s   4GB
Mar 13 11:53:52 Starting compiler/encoders/arm7/proofs
Mar 13 12:06:14 Finished compiler/encoders/arm7/proofs                        12m22s   4GB
Mar 13 12:06:14 Starting compiler/encoders/arm8/proofs
Mar 13 12:12:27 Finished compiler/encoders/arm8/proofs                         6m12s   1GB
Mar 13 12:12:27 Starting compiler/encoders/mips/proofs
Mar 13 12:21:41 Finished compiler/encoders/mips/proofs                         9m13s   3GB
Mar 13 12:21:41 Starting compiler/encoders/riscv/proofs
Mar 13 12:30:08 Finished compiler/encoders/riscv/proofs                        8m26s   1GB
Mar 13 12:30:08 Starting compiler/encoders/ag32/proofs
Mar 13 12:32:35 Finished compiler/encoders/ag32/proofs                         2m26s 715MB
Mar 13 12:32:35 Starting compiler/backend/x64/proofs
Mar 13 12:32:54 Finished compiler/backend/x64/proofs                             19s   1GB
Mar 13 12:32:54 Starting compiler/backend/arm7/proofs
Mar 13 12:33:14 Finished compiler/backend/arm7/proofs                            19s   1GB
Mar 13 12:33:14 Starting compiler/backend/arm8/proofs
Mar 13 12:33:33 Finished compiler/backend/arm8/proofs                            18s 845MB
Mar 13 12:33:33 Starting compiler/backend/mips/proofs
Mar 13 12:33:54 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 13 12:33:54 Starting compiler/backend/riscv/proofs
Mar 13 12:34:13 Finished compiler/backend/riscv/proofs                           18s   1GB
Mar 13 12:34:13 Starting compiler/backend/ag32/proofs
Mar 13 12:46:35 Finished compiler/backend/ag32/proofs                         12m21s   2GB
Mar 13 12:46:35 Starting compiler/proofs
Mar 13 12:48:02 Finished compiler/proofs                                       1m26s   2GB
Mar 13 12:48:02 Starting candle/set-theory
Mar 13 12:48:29 Finished candle/set-theory                                       26s 791MB
Mar 13 12:48:29 Starting candle/syntax-lib
Mar 13 12:48:39 Finished candle/syntax-lib                                        9s 649MB
Mar 13 12:48:39 Starting candle/standard/syntax
Mar 13 12:50:23 Finished candle/standard/syntax                                1m43s   1GB
Mar 13 12:50:23 Starting candle/standard/semantics
Mar 13 12:52:03 Finished candle/standard/semantics                             1m39s   1GB
Mar 13 12:52:03 Starting candle/standard/monadic
Mar 13 12:53:38 Finished candle/standard/monadic                               1m35s   1GB
Mar 13 12:53:38 Starting candle/standard/ml_kernel
Mar 13 12:58:39 Finished candle/standard/ml_kernel                             5m00s   4GB
Mar 13 12:58:39 Starting candle/standard/opentheory
Mar 13 14:37:50 Resuming candle/standard/opentheory
Mar 13 14:37:51 Finished candle/standard/opentheory                               0s 101MB
Mar 13 14:37:51 Starting candle/standard/opentheory/compilation
Mar 13 15:10:37 Finished candle/standard/opentheory/compilation               32m45s  17GB
Mar 13 15:10:37 Starting candle/standard/opentheory/compilation/proofs
Mar 13 15:11:14 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Mar 13 15:11:15 Starting candle/overloading/syntax
Mar 13 15:14:10 Finished candle/overloading/syntax                             2m55s   1GB
Mar 13 15:14:10 Starting candle/overloading/semantics
Mar 13 15:20:51 Finished candle/overloading/semantics                          6m40s   2GB
Mar 13 15:20:51 Starting characteristic/examples
Mar 13 15:22:04 Finished characteristic/examples                               1m12s   2GB
Mar 13 15:22:04 Starting tutorial/solutions
Mar 13 15:36:19 Finished tutorial/solutions                                   14m15s   7GB
Mar 13 15:36:20 Starting translator/monadic/examples
Mar 13 15:39:21 Finished translator/monadic/examples                           3m01s   2GB
Mar 13 15:39:21 Starting examples
Mar 13 15:47:26 Finished examples                                              8m04s   3GB
Mar 13 15:47:27 Starting examples/compilation/x64
Mar 13 18:01:30 Finished examples/compilation/x64                           2h14m03s  12GB
Mar 13 18:01:30 Starting examples/compilation/x64/proofs
Mar 13 18:03:03 Finished examples/compilation/x64/proofs                       1m32s   3GB
Mar 13 18:03:03 Starting examples/compilation/ag32
Mar 13 18:33:20 Finished examples/compilation/ag32                            30m16s   7GB
Mar 13 18:33:20 Starting examples/compilation/ag32/proofs
Mar 13 18:34:04 Finished examples/compilation/ag32/proofs                        43s   3GB
Mar 13 18:34:04 Starting examples/cost
Mar 13 19:14:30 Finished examples/cost                                        40m26s   6GB
Mar 13 19:14:30 Starting examples/lpr_checker
Mar 13 19:17:55 Finished examples/lpr_checker                                  3m24s   2GB
Mar 13 19:17:55 Starting examples/lpr_checker/compilation
Mar 13 19:34:49 Finished examples/lpr_checker/compilation                     16m53s  12GB
Mar 13 19:34:49 Starting examples/lpr_checker/compilation/proofs
Mar 13 19:35:28 Finished examples/lpr_checker/compilation/proofs                 38s   3GB
Mar 13 19:35:28 Starting examples/lpr_checker/array
Mar 13 19:42:59 Finished examples/lpr_checker/array                            7m31s   3GB
Mar 13 19:42:59 Starting examples/lpr_checker/array/compilation
Mar 13 19:58:29 Finished examples/lpr_checker/array/compilation               15m29s   6GB
Mar 13 19:58:30 Starting examples/lpr_checker/array/compilation/proofs
Mar 13 19:59:12 Finished examples/lpr_checker/array/compilation/proofs           42s   2GB
Mar 13 19:59:12 Starting translator/okasaki-examples
Mar 13 20:03:24 Finished translator/okasaki-examples                           4m11s   1GB
Mar 13 20:03:24 Starting translator/other-examples
Mar 13 20:05:14 Finished translator/other-examples                             1m50s   1GB
Mar 13 20:05:15 Starting compiler/parsing/tests
Mar 13 20:05:39 Finished compiler/parsing/tests                                  24s 560MB
Mar 13 20:05:39 Starting compiler/inference/tests
Mar 13 20:10:07 Finished compiler/inference/tests                              4m27s   5GB
Mar 13 20:10:07 Starting compiler/bootstrap/translation
Mar 13 22:41:41 Finished compiler/bootstrap/translation                     2h31m33s  42GB
Mar 13 22:41:41 Starting unverified/sexpr-bootstrap/x64/64
Mar 13 22:56:31 Finished unverified/sexpr-bootstrap/x64/64                    14m49s   5GB
Mar 13 22:56:32 Starting unverified/sexpr-bootstrap/x64/32
Mar 13 23:07:14 Finished unverified/sexpr-bootstrap/x64/32                    10m42s   6GB
Mar 13 23:07:14 Starting compiler/benchmarks
Mar 13 23:46:15 Finished compiler/benchmarks                                  38m59s   2GB
Mar 13 23:46:15 Starting compiler/bootstrap/compilation/x64/64
Mar 14 14:51:23 Finished compiler/bootstrap/compilation/x64/64             15h05m06s  64GB
Mar 14 14:51:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 14 14:54:55 Finished compiler/bootstrap/compilation/x64/64/proofs          3m31s  15GB
Mar 14 14:54:55 Starting compiler/bootstrap/compilation/x64/32
Mar 15 04:11:39 Finished compiler/bootstrap/compilation/x64/32             13h16m43s  64GB
Mar 15 04:11:39 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 15 04:14:44 Finished compiler/bootstrap/compilation/x64/32/proofs          3m05s  12GB
Mar 15 04:14:44 Starting compiler/bootstrap/compilation/ag32/32
Mar 15 19:18:09 Finished compiler/bootstrap/compilation/ag32/32            15h03m24s  64GB
Mar 15 19:18:09 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 15 19:47:38 Finished compiler/bootstrap/compilation/ag32/32/proofs        29m28s  29GB
Mar 15 19:47:38 SUCCESS