Job 1460

CakeML:bc023195dc4c8301551290b1c2d86ec57b683dac
  add a .type to exporters [Jan 29 15:03:53]
#814 (export_type)
Merging into:6aec50bac4a52b18c8752ed3f7c7e086652c0edc
  Get some examples working again [Jan 27 11:10:52]
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

Feb 01 06:00:05 Claimed job
Feb 01 06:00:09 Building HOL
Feb 01 06:15:56 Starting developers
Feb 01 06:16:01 Finished developers                                               4s 123MB
Feb 01 06:16:01 Starting developers/bin
Feb 01 06:16:08 Finished developers/bin                                           6s   1GB
Feb 01 06:16:08 Starting semantics/ffi
Feb 01 06:16:19 Finished semantics/ffi                                           11s 234MB
Feb 01 06:16:19 Starting semantics
Feb 01 06:17:55 Finished semantics                                             1m35s   1GB
Feb 01 06:17:56 Starting semantics/proofs
Feb 01 06:21:27 Finished semantics/proofs                                      3m31s   1GB
Feb 01 06:21:27 Starting semantics/alt_semantics
Feb 01 06:21:37 Finished semantics/alt_semantics                                  8s 285MB
Feb 01 06:21:37 Starting semantics/alt_semantics/proofs
Feb 01 06:23:54 Finished semantics/alt_semantics/proofs                        2m16s 737MB
Feb 01 06:23:54 Starting basis/pure
Feb 01 06:27:01 Finished basis/pure                                            3m06s 875MB
Feb 01 06:27:01 Starting translator
Feb 01 06:29:49 Finished translator                                            2m47s   1GB
Feb 01 06:29:49 Starting compiler/parsing
Feb 01 06:31:02 Finished compiler/parsing                                      1m12s   3GB
Feb 01 06:31:02 Starting characteristic
Feb 01 06:37:13 Finished characteristic                                        6m10s   2GB
Feb 01 06:37:14 Starting translator/monadic
Feb 01 06:38:57 Finished translator/monadic                                    1m43s   1GB
Feb 01 06:38:57 Starting basis
Feb 01 07:25:21 Finished basis                                                46m23s  16GB
Feb 01 07:25:21 Starting compiler/inference
Feb 01 07:26:34 Finished compiler/inference                                    1m13s   1GB
Feb 01 07:26:35 Starting compiler/backend/reg_alloc
Feb 01 07:27:42 Finished compiler/backend/reg_alloc                            1m06s   1GB
Feb 01 07:27:42 Starting compiler/backend/gc
Feb 01 07:31:30 Finished compiler/backend/gc                                   3m48s   2GB
Feb 01 07:31:30 Starting compiler/backend
Feb 01 07:36:31 Finished compiler/backend                                      5m00s   3GB
Feb 01 07:36:31 Starting compiler/encoders/asm
Feb 01 07:36:54 Finished compiler/encoders/asm                                   22s 730MB
Feb 01 07:36:54 Starting compiler/encoders/x64
Feb 01 07:38:01 Finished compiler/encoders/x64                                 1m06s   1GB
Feb 01 07:38:01 Starting compiler/encoders/arm7
Feb 01 07:40:13 Finished compiler/encoders/arm7                                2m11s   1GB
Feb 01 07:40:13 Starting compiler/encoders/arm8
Feb 01 07:40:53 Finished compiler/encoders/arm8                                  40s 573MB
Feb 01 07:40:53 Starting compiler/encoders/mips
Feb 01 07:42:30 Finished compiler/encoders/mips                                1m36s 845MB
Feb 01 07:42:30 Starting compiler/encoders/riscv
Feb 01 07:44:19 Finished compiler/encoders/riscv                               1m48s 951MB
Feb 01 07:44:19 Starting compiler/encoders/ag32
Feb 01 07:44:38 Finished compiler/encoders/ag32                                  18s 674MB
Feb 01 07:44:38 Starting compiler/backend/x64
Feb 01 07:44:57 Finished compiler/backend/x64                                    19s   1GB
Feb 01 07:44:57 Starting compiler/backend/arm7
Feb 01 07:45:19 Finished compiler/backend/arm7                                   21s   1GB
Feb 01 07:45:19 Starting compiler/backend/arm8
Feb 01 07:45:39 Finished compiler/backend/arm8                                   19s   1GB
Feb 01 07:45:39 Starting compiler/backend/mips
Feb 01 07:45:59 Finished compiler/backend/mips                                   19s   1GB
Feb 01 07:45:59 Starting compiler/backend/riscv
Feb 01 07:46:19 Finished compiler/backend/riscv                                  19s   1GB
Feb 01 07:46:19 Starting compiler/backend/ag32
Feb 01 07:47:31 Finished compiler/backend/ag32                                 1m12s   1GB
Feb 01 07:47:32 Starting compiler/parsing/proofs
Feb 01 07:53:18 Finished compiler/parsing/proofs                               5m45s   1GB
Feb 01 07:53:18 Starting compiler/inference/proofs
Feb 01 07:55:54 Finished compiler/inference/proofs                             2m36s 997MB
Feb 01 07:55:55 Starting compiler/backend/semantics
Feb 01 08:29:31 Finished compiler/backend/semantics                           33m36s   2GB
Feb 01 08:29:32 Starting compiler/backend/reg_alloc/proofs
Feb 01 08:33:19 Finished compiler/backend/reg_alloc/proofs                     3m46s   1GB
Feb 01 08:33:19 Starting compiler/backend/proofs
Feb 01 09:31:56 Finished compiler/backend/proofs                              58m36s  18GB
Feb 01 09:31:56 Starting compiler/encoders/x64/proofs
Feb 01 09:42:17 Finished compiler/encoders/x64/proofs                         10m20s   4GB
Feb 01 09:42:17 Starting compiler/encoders/arm7/proofs
Feb 01 09:56:27 Finished compiler/encoders/arm7/proofs                        14m09s   6GB
Feb 01 09:56:27 Starting compiler/encoders/arm8/proofs
Feb 01 10:03:37 Finished compiler/encoders/arm8/proofs                         7m08s   1GB
Feb 01 10:03:37 Starting compiler/encoders/mips/proofs
Feb 01 10:14:26 Finished compiler/encoders/mips/proofs                        10m49s   1GB
Feb 01 10:14:26 Starting compiler/encoders/riscv/proofs
Feb 01 10:23:52 Finished compiler/encoders/riscv/proofs                        9m25s   1GB
Feb 01 10:23:53 Starting compiler/encoders/ag32/proofs
Feb 01 10:26:40 Finished compiler/encoders/ag32/proofs                         2m47s 768MB
Feb 01 10:26:40 Starting compiler/backend/x64/proofs
Feb 01 10:27:01 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 01 10:27:02 Starting compiler/backend/arm7/proofs
Feb 01 10:27:26 Finished compiler/backend/arm7/proofs                            23s   1GB
Feb 01 10:27:26 Starting compiler/backend/arm8/proofs
Feb 01 10:27:48 Finished compiler/backend/arm8/proofs                            21s   1GB
Feb 01 10:27:48 Starting compiler/backend/mips/proofs
Feb 01 10:28:09 Finished compiler/backend/mips/proofs                            21s   1GB
Feb 01 10:28:10 Starting compiler/backend/riscv/proofs
Feb 01 10:28:31 Finished compiler/backend/riscv/proofs                           21s   1GB
Feb 01 10:28:31 Starting compiler/backend/ag32/proofs
Feb 01 10:42:16 Finished compiler/backend/ag32/proofs                         13m44s   2GB
Feb 01 10:42:17 Starting compiler/proofs
Feb 01 10:44:12 Finished compiler/proofs                                       1m55s   2GB
Feb 01 10:44:12 Starting candle/set-theory
Feb 01 10:44:41 Finished candle/set-theory                                       28s 697MB
Feb 01 10:44:41 Starting candle/syntax-lib
Feb 01 10:44:52 Finished candle/syntax-lib                                       10s 613MB
Feb 01 10:44:53 Starting candle/standard/syntax
Feb 01 10:46:48 Finished candle/standard/syntax                                1m55s   1GB
Feb 01 10:46:48 Starting candle/standard/semantics
Feb 01 10:48:37 Finished candle/standard/semantics                             1m49s   1GB
Feb 01 10:48:38 Starting candle/standard/monadic
Feb 01 10:50:26 Finished candle/standard/monadic                               1m48s   1GB
Feb 01 10:50:26 Starting candle/standard/ml_kernel
Feb 01 10:56:33 Finished candle/standard/ml_kernel                             6m06s   3GB
Feb 01 10:56:33 Starting candle/overloading/syntax
Feb 01 10:59:52 Finished candle/overloading/syntax                             3m17s   1GB
Feb 01 10:59:52 Starting candle/overloading/semantics
Feb 01 11:12:43 Finished candle/overloading/semantics                         12m51s   4GB
Feb 01 11:12:43 Starting characteristic/examples
Feb 01 11:14:03 Finished characteristic/examples                               1m19s   3GB
Feb 01 11:14:03 Starting tutorial/solutions
Feb 01 11:30:09 Finished tutorial/solutions                                   16m05s   8GB
Feb 01 11:30:10 Starting translator/monadic/examples
Feb 01 11:33:30 Finished translator/monadic/examples                           3m19s   2GB
Feb 01 11:33:30 Starting examples
Feb 01 11:42:31 Finished examples                                              9m00s   4GB
Feb 01 11:42:31 Starting examples/compilation/x64
Feb 01 14:08:28 Finished examples/compilation/x64                           2h25m57s  20GB
Feb 01 14:08:29 Starting examples/compilation/x64/proofs
Feb 01 14:10:35 Finished examples/compilation/x64/proofs                       2m06s   3GB
Feb 01 14:10:35 Starting examples/compilation/ag32
Feb 01 14:44:44 Finished examples/compilation/ag32                            34m08s   8GB
Feb 01 14:44:44 Starting examples/compilation/ag32/proofs
Feb 01 14:45:30 Finished examples/compilation/ag32/proofs                        45s   2GB
Feb 01 14:45:30 Starting examples/cost
Feb 01 15:43:20 Finished examples/cost                                        57m49s   7GB
Feb 01 15:43:20 Starting examples/lpr_checker
Feb 01 15:47:35 Finished examples/lpr_checker                                  4m14s   2GB
Feb 01 15:47:35 Starting examples/lpr_checker/compilation
Feb 01 16:06:19 Finished examples/lpr_checker/compilation                     18m43s   9GB
Feb 01 16:06:19 Starting examples/lpr_checker/compilation/proofs
Feb 01 16:07:00 Finished examples/lpr_checker/compilation/proofs                 41s   3GB
Feb 01 16:07:01 Starting examples/lpr_checker/array
Feb 01 16:22:37 Finished examples/lpr_checker/array                           15m35s   3GB
Feb 01 16:22:37 Starting examples/lpr_checker/array/compilation
Feb 01 16:42:18 Finished examples/lpr_checker/array/compilation               19m40s  14GB
Feb 01 16:42:18 Starting examples/lpr_checker/array/compilation/proofs
Feb 01 16:43:27 Finished examples/lpr_checker/array/compilation/proofs         1m08s   3GB
Feb 01 16:43:27 Starting examples/opentheory
Feb 01 16:53:33 Finished examples/opentheory                                  10m04s   5GB
Feb 01 16:53:33 Starting examples/opentheory
Feb 01 16:53:34 Finished examples/opentheory                                      1s  17MB
Feb 01 16:53:34 Starting examples/opentheory/compilation
Feb 01 17:27:57 Finished examples/opentheory/compilation                      34m22s  17GB
Feb 01 17:27:57 Starting examples/opentheory/compilation/proofs
Feb 01 17:28:39 Finished examples/opentheory/compilation/proofs                  41s   4GB
Feb 01 17:28:39 Starting examples/opentheory/compilation/ag32
Feb 01 18:04:24 Finished examples/opentheory/compilation/ag32                 35m44s  19GB
Feb 01 18:04:24 Starting examples/opentheory/compilation/ag32/proofs
Feb 01 18:06:02 Finished examples/opentheory/compilation/ag32/proofs           1m37s   5GB
Feb 01 18:06:02 Starting translator/okasaki-examples
Feb 01 18:10:32 Finished translator/okasaki-examples                           4m29s   1GB
Feb 01 18:10:32 Starting translator/other-examples
Feb 01 18:12:41 Finished translator/other-examples                             2m08s   1GB
Feb 01 18:12:41 Starting compiler/parsing/tests
Feb 01 18:13:08 Finished compiler/parsing/tests                                  26s 438MB
Feb 01 18:13:08 Starting compiler/inference/tests
Feb 01 18:21:04 Finished compiler/inference/tests                              7m55s   4GB
Feb 01 18:21:04 Starting compiler/bootstrap/translation
Feb 01 21:11:39 Finished compiler/bootstrap/translation                     2h50m35s  43GB
Feb 01 21:11:40 Starting unverified/sexpr-bootstrap/x64/64
Feb 01 21:23:38 Finished unverified/sexpr-bootstrap/x64/64                    11m58s   8GB
Feb 01 21:23:39 Starting unverified/sexpr-bootstrap/x64/32
Feb 01 21:33:39 Finished unverified/sexpr-bootstrap/x64/32                     9m59s   9GB
Feb 01 21:33:39 Starting compiler/benchmarks
Feb 01 21:33:41 Finished compiler/benchmarks                                      1s  24MB
Feb 01 21:33:41 Starting compiler/bootstrap/compilation/x64/64
Feb 02 09:59:47 Finished compiler/bootstrap/compilation/x64/64             12h26m03s  64GB
Feb 02 09:59:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 02 10:02:50 Finished compiler/bootstrap/compilation/x64/64/proofs          3m03s  12GB
Feb 02 10:02:51 Starting compiler/bootstrap/compilation/x64/32
Feb 02 21:18:43 Finished compiler/bootstrap/compilation/x64/32             11h15m52s  64GB
Feb 02 21:18:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 02 21:21:39 Finished compiler/bootstrap/compilation/x64/32/proofs          2m55s  11GB
Feb 02 21:21:39 Starting compiler/bootstrap/compilation/ag32/32
Feb 03 09:04:31 Finished compiler/bootstrap/compilation/ag32/32            11h42m50s  64GB
Feb 03 09:04:31 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 03 09:25:53 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m22s  25GB
Feb 03 09:25:53 SUCCESS