Job 1462

CakeML:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:c0a9cb83695e6a160a6ea2014d3b32ab4543ca2f
  emacs-mode: handle colons better (different in HOL and SML contexts) [Jan 29 05:20:22]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Feb 03 09:30:02 Claimed job
Feb 03 09:30:07 Reusing HOL
Feb 03 09:30:57 Starting developers
Feb 03 09:31:02 Finished developers                                               4s 103MB
Feb 03 09:31:02 Starting developers/bin
Feb 03 09:31:09 Finished developers/bin                                           6s   1GB
Feb 03 09:31:09 Starting semantics/ffi
Feb 03 09:31:21 Finished semantics/ffi                                           11s 239MB
Feb 03 09:31:21 Starting semantics
Feb 03 09:32:47 Finished semantics                                             1m26s   1GB
Feb 03 09:32:47 Starting semantics/proofs
Feb 03 09:36:20 Finished semantics/proofs                                      3m32s 880MB
Feb 03 09:36:21 Starting semantics/alt_semantics
Feb 03 09:36:30 Finished semantics/alt_semantics                                  9s 304MB
Feb 03 09:36:30 Starting semantics/alt_semantics/proofs
Feb 03 09:38:45 Finished semantics/alt_semantics/proofs                        2m14s 792MB
Feb 03 09:38:45 Starting basis/pure
Feb 03 09:39:38 Finished basis/pure                                              52s 673MB
Feb 03 09:39:38 Starting translator
Feb 03 09:42:26 Finished translator                                            2m47s   1GB
Feb 03 09:42:26 Starting compiler/parsing
Feb 03 09:43:39 Finished compiler/parsing                                      1m12s   2GB
Feb 03 09:43:40 Starting characteristic
Feb 03 09:49:54 Finished characteristic                                        6m13s   1GB
Feb 03 09:49:54 Starting translator/monadic
Feb 03 09:51:35 Finished translator/monadic                                    1m40s   1GB
Feb 03 09:51:35 Starting basis
Feb 03 10:37:48 Finished basis                                                46m13s  15GB
Feb 03 10:37:50 Starting compiler/inference
Feb 03 10:38:54 Finished compiler/inference                                    1m04s   1GB
Feb 03 10:38:54 Starting compiler/backend/reg_alloc
Feb 03 10:40:01 Finished compiler/backend/reg_alloc                            1m06s   1GB
Feb 03 10:40:01 Starting compiler/backend/gc
Feb 03 10:43:35 Finished compiler/backend/gc                                   3m33s   2GB
Feb 03 10:43:35 Starting compiler/backend
Feb 03 10:48:40 Finished compiler/backend                                      5m04s   3GB
Feb 03 10:48:40 Starting compiler/encoders/asm
Feb 03 10:49:03 Finished compiler/encoders/asm                                   23s 675MB
Feb 03 10:49:04 Starting compiler/encoders/x64
Feb 03 10:49:30 Finished compiler/encoders/x64                                   25s   1GB
Feb 03 10:49:30 Starting compiler/encoders/arm7
Feb 03 10:50:23 Finished compiler/encoders/arm7                                  53s 738MB
Feb 03 10:50:24 Starting compiler/encoders/arm8
Feb 03 10:50:37 Finished compiler/encoders/arm8                                  13s 928MB
Feb 03 10:50:38 Starting compiler/encoders/mips
Feb 03 10:50:56 Finished compiler/encoders/mips                                  17s   1GB
Feb 03 10:50:56 Starting compiler/encoders/riscv
Feb 03 10:51:11 Finished compiler/encoders/riscv                                 14s 807MB
Feb 03 10:51:11 Starting compiler/encoders/ag32
Feb 03 10:51:30 Finished compiler/encoders/ag32                                  18s 674MB
Feb 03 10:51:30 Starting compiler/backend/x64
Feb 03 10:51:49 Finished compiler/backend/x64                                    19s   1GB
Feb 03 10:51:49 Starting compiler/backend/arm7
Feb 03 10:52:11 Finished compiler/backend/arm7                                   21s   1GB
Feb 03 10:52:11 Starting compiler/backend/arm8
Feb 03 10:52:31 Finished compiler/backend/arm8                                   20s   1GB
Feb 03 10:52:31 Starting compiler/backend/mips
Feb 03 10:52:51 Finished compiler/backend/mips                                   19s   1GB
Feb 03 10:52:52 Starting compiler/backend/riscv
Feb 03 10:53:12 Finished compiler/backend/riscv                                  19s   1GB
Feb 03 10:53:12 Starting compiler/backend/ag32
Feb 03 10:54:25 Finished compiler/backend/ag32                                 1m12s   1GB
Feb 03 10:54:25 Starting compiler/parsing/proofs
Feb 03 11:00:14 Finished compiler/parsing/proofs                               5m49s   1GB
Feb 03 11:00:15 Starting compiler/inference/proofs
Feb 03 11:02:55 Finished compiler/inference/proofs                             2m40s   1GB
Feb 03 11:02:55 Starting compiler/backend/semantics
Feb 03 11:35:29 Finished compiler/backend/semantics                           32m34s   2GB
Feb 03 11:35:30 Starting compiler/backend/reg_alloc/proofs
Feb 03 11:39:14 Finished compiler/backend/reg_alloc/proofs                     3m44s 857MB
Feb 03 11:39:14 Starting compiler/backend/proofs
Feb 03 12:37:33 Finished compiler/backend/proofs                              58m18s  24GB
Feb 03 12:37:33 Starting compiler/encoders/x64/proofs
Feb 03 12:47:50 Finished compiler/encoders/x64/proofs                         10m16s   5GB
Feb 03 12:47:50 Starting compiler/encoders/arm7/proofs
Feb 03 13:01:48 Finished compiler/encoders/arm7/proofs                        13m57s   6GB
Feb 03 13:01:48 Starting compiler/encoders/arm8/proofs
Feb 03 13:08:57 Finished compiler/encoders/arm8/proofs                         7m08s   1GB
Feb 03 13:08:57 Starting compiler/encoders/mips/proofs
Feb 03 13:19:51 Finished compiler/encoders/mips/proofs                        10m53s   2GB
Feb 03 13:19:51 Starting compiler/encoders/riscv/proofs
Feb 03 13:29:31 Finished compiler/encoders/riscv/proofs                        9m39s   1GB
Feb 03 13:29:31 Starting compiler/encoders/ag32/proofs
Feb 03 13:32:20 Finished compiler/encoders/ag32/proofs                         2m48s 665MB
Feb 03 13:32:20 Starting compiler/backend/x64/proofs
Feb 03 13:32:42 Finished compiler/backend/x64/proofs                             22s   1GB
Feb 03 13:32:42 Starting compiler/backend/arm7/proofs
Feb 03 13:33:05 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 03 13:33:06 Starting compiler/backend/arm8/proofs
Feb 03 13:33:27 Finished compiler/backend/arm8/proofs                            21s   1GB
Feb 03 13:33:27 Starting compiler/backend/mips/proofs
Feb 03 13:33:50 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 03 13:33:50 Starting compiler/backend/riscv/proofs
Feb 03 13:34:12 Finished compiler/backend/riscv/proofs                           21s   1GB
Feb 03 13:34:12 Starting compiler/backend/ag32/proofs
Feb 03 13:47:51 Finished compiler/backend/ag32/proofs                         13m38s   3GB
Feb 03 13:47:51 Starting compiler/proofs
Feb 03 13:49:29 Finished compiler/proofs                                       1m37s   4GB
Feb 03 13:49:29 Starting candle/set-theory
Feb 03 13:49:58 Finished candle/set-theory                                       29s 688MB
Feb 03 13:49:59 Starting candle/syntax-lib
Feb 03 13:50:09 Finished candle/syntax-lib                                       10s 706MB
Feb 03 13:50:10 Starting candle/standard/syntax
Feb 03 13:52:06 Finished candle/standard/syntax                                1m56s   1GB
Feb 03 13:52:07 Starting candle/standard/semantics
Feb 03 13:53:55 Finished candle/standard/semantics                             1m48s   1GB
Feb 03 13:53:55 Starting candle/standard/monadic
Feb 03 13:55:43 Finished candle/standard/monadic                               1m48s   1GB
Feb 03 13:55:44 Starting candle/standard/ml_kernel
Feb 03 14:01:54 Finished candle/standard/ml_kernel                             6m09s   3GB
Feb 03 14:01:54 Starting candle/overloading/syntax
Feb 03 14:05:11 Finished candle/overloading/syntax                             3m17s   1GB
Feb 03 14:05:12 Starting candle/overloading/semantics
Feb 03 14:18:13 Finished candle/overloading/semantics                         13m01s   2GB
Feb 03 14:18:14 Starting characteristic/examples
Feb 03 14:19:34 Finished characteristic/examples                               1m20s   3GB
Feb 03 14:19:34 Starting tutorial/solutions
Feb 03 14:35:29 Finished tutorial/solutions                                   15m54s   7GB
Feb 03 14:35:29 Starting translator/monadic/examples
Feb 03 14:38:45 Finished translator/monadic/examples                           3m15s   2GB
Feb 03 14:38:45 Starting examples
Feb 03 14:47:37 Finished examples                                              8m52s   3GB
Feb 03 14:47:38 Starting examples/compilation/x64
Feb 03 17:14:40 Finished examples/compilation/x64                           2h27m01s  16GB
Feb 03 17:14:40 Starting examples/compilation/x64/proofs
Feb 03 17:16:44 Finished examples/compilation/x64/proofs                       2m03s   3GB
Feb 03 17:16:45 Starting examples/compilation/ag32
Feb 03 17:50:36 Finished examples/compilation/ag32                            33m51s   8GB
Feb 03 17:50:36 Starting examples/compilation/ag32/proofs
Feb 03 17:51:23 Finished examples/compilation/ag32/proofs                        46s   3GB
Feb 03 17:51:23 Starting examples/cost
Feb 03 18:49:40 Finished examples/cost                                        58m15s   7GB
Feb 03 18:49:41 Starting examples/lpr_checker
Feb 03 18:53:51 Finished examples/lpr_checker                                  4m10s   4GB
Feb 03 18:53:52 Starting examples/lpr_checker/compilation
Feb 03 19:12:53 Finished examples/lpr_checker/compilation                     19m01s  10GB
Feb 03 19:12:54 Starting examples/lpr_checker/compilation/proofs
Feb 03 19:13:33 Finished examples/lpr_checker/compilation/proofs                 39s   2GB
Feb 03 19:13:34 Starting examples/lpr_checker/array
Feb 03 19:29:47 Finished examples/lpr_checker/array                           16m13s   5GB
Feb 03 19:29:47 Starting examples/lpr_checker/array/compilation
Feb 03 19:50:08 Finished examples/lpr_checker/array/compilation               20m19s  13GB
Feb 03 19:50:08 Starting examples/lpr_checker/array/compilation/proofs
Feb 03 19:50:57 Finished examples/lpr_checker/array/compilation/proofs           48s   4GB
Feb 03 19:50:57 Starting examples/opentheory
Feb 03 20:01:07 Finished examples/opentheory                                  10m09s   5GB
Feb 03 20:01:07 Starting examples/opentheory
Feb 03 20:01:09 Finished examples/opentheory                                      1s  19MB
Feb 03 20:01:09 Starting examples/opentheory/compilation
Feb 03 20:35:49 Finished examples/opentheory/compilation                      34m39s  17GB
Feb 03 20:35:49 Starting examples/opentheory/compilation/proofs
Feb 03 20:36:31 Finished examples/opentheory/compilation/proofs                  42s   3GB
Feb 03 20:36:32 Starting examples/opentheory/compilation/ag32
Feb 03 21:12:00 Finished examples/opentheory/compilation/ag32                 35m28s  25GB
Feb 03 21:12:01 Starting examples/opentheory/compilation/ag32/proofs
Feb 03 21:13:37 Finished examples/opentheory/compilation/ag32/proofs           1m36s   5GB
Feb 03 21:13:38 Starting translator/okasaki-examples
Feb 03 21:18:05 Finished translator/okasaki-examples                           4m27s   1GB
Feb 03 21:18:05 Starting translator/other-examples
Feb 03 21:18:50 Finished translator/other-examples                               44s   1GB
Feb 03 21:18:50 Starting compiler/parsing/tests
Feb 03 21:19:17 Finished compiler/parsing/tests                                  26s 595MB
Feb 03 21:19:17 Starting compiler/inference/tests
Feb 03 21:27:11 Finished compiler/inference/tests                              7m53s   5GB
Feb 03 21:27:11 Starting compiler/bootstrap/translation
Feb 04 00:23:40 Finished compiler/bootstrap/translation                     2h56m28s  39GB
Feb 04 00:23:40 Starting unverified/sexpr-bootstrap/x64/64
Feb 04 00:36:17 Finished unverified/sexpr-bootstrap/x64/64                    11m53s   8GB
Feb 04 00:36:18 Starting unverified/sexpr-bootstrap/x64/32
Feb 04 00:46:59 Finished unverified/sexpr-bootstrap/x64/32                     9m59s   8GB
Feb 04 00:46:59 Starting compiler/benchmarks
Feb 04 00:47:01 Finished compiler/benchmarks                                      1s  23MB
Feb 04 00:47:02 Starting compiler/bootstrap/compilation/x64/64
Feb 04 13:14:03 Finished compiler/bootstrap/compilation/x64/64             12h26m33s  64GB
Feb 04 13:14:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 04 13:17:10 Finished compiler/bootstrap/compilation/x64/64/proofs          3m06s  13GB
Feb 04 13:17:11 Starting compiler/bootstrap/compilation/x64/32
Feb 05 01:13:45 Finished compiler/bootstrap/compilation/x64/32             11h56m08s  64GB
Feb 05 01:13:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 05 01:16:45 Finished compiler/bootstrap/compilation/x64/32/proofs          3m00s  13GB
Feb 05 01:16:45 Starting compiler/bootstrap/compilation/ag32/32
Feb 05 12:55:51 Finished compiler/bootstrap/compilation/ag32/32            11h39m05s  64GB
Feb 05 12:55:51 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 05 13:15:55 Finished compiler/bootstrap/compilation/ag32/32/proofs        20m03s  24GB
Feb 05 13:15:55 SUCCESS