Job 1459

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:e66e816f5730e26e7f1d1d5ec10b2cd2030ef4c7
  Fix an infinite loop in the simplifier + REALMULCANON [Jan 26 09:24:11]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 29 19:21:22 Claimed job
Jan 29 19:21:28 Building HOL
Jan 29 19:37:12 Starting developers
Jan 29 19:37:17 Finished developers                                               4s 116MB
Jan 29 19:37:17 Starting developers/bin
Jan 29 19:37:24 Finished developers/bin                                           6s   1GB
Jan 29 19:37:24 Starting semantics/ffi
Jan 29 19:37:36 Finished semantics/ffi                                           11s 239MB
Jan 29 19:37:36 Starting semantics
Jan 29 19:39:12 Finished semantics                                             1m35s   1GB
Jan 29 19:39:12 Starting semantics/proofs
Jan 29 19:42:46 Finished semantics/proofs                                      3m33s 971MB
Jan 29 19:42:46 Starting semantics/alt_semantics
Jan 29 19:42:55 Finished semantics/alt_semantics                                  9s 271MB
Jan 29 19:42:55 Starting semantics/alt_semantics/proofs
Jan 29 19:45:13 Finished semantics/alt_semantics/proofs                        2m17s 730MB
Jan 29 19:45:13 Starting basis/pure
Jan 29 19:48:21 Finished basis/pure                                            3m08s 869MB
Jan 29 19:48:21 Starting translator
Jan 29 19:51:07 Finished translator                                            2m45s   1GB
Jan 29 19:51:07 Starting compiler/parsing
Jan 29 19:52:21 Finished compiler/parsing                                      1m13s   3GB
Jan 29 19:52:22 Starting characteristic
Jan 29 19:58:35 Finished characteristic                                        6m12s   1GB
Jan 29 19:58:35 Starting translator/monadic
Jan 29 20:00:16 Finished translator/monadic                                    1m40s   1GB
Jan 29 20:00:16 Starting basis
Jan 29 20:47:06 Finished basis                                                46m48s  14GB
Jan 29 20:47:06 Starting compiler/inference
Jan 29 20:48:19 Finished compiler/inference                                    1m12s   1GB
Jan 29 20:48:19 Starting compiler/backend/reg_alloc
Jan 29 20:49:26 Finished compiler/backend/reg_alloc                            1m07s   1GB
Jan 29 20:49:26 Starting compiler/backend/gc
Jan 29 20:53:14 Finished compiler/backend/gc                                   3m47s   2GB
Jan 29 20:53:14 Starting compiler/backend
Jan 29 20:58:15 Finished compiler/backend                                      5m00s   3GB
Jan 29 20:58:15 Starting compiler/encoders/asm
Jan 29 20:58:38 Finished compiler/encoders/asm                                   23s 841MB
Jan 29 20:58:39 Starting compiler/encoders/x64
Jan 29 20:59:43 Finished compiler/encoders/x64                                 1m04s 923MB
Jan 29 20:59:43 Starting compiler/encoders/arm7
Jan 29 21:01:56 Finished compiler/encoders/arm7                                2m12s   1GB
Jan 29 21:01:56 Starting compiler/encoders/arm8
Jan 29 21:02:35 Finished compiler/encoders/arm8                                  39s 577MB
Jan 29 21:02:35 Starting compiler/encoders/mips
Jan 29 21:04:12 Finished compiler/encoders/mips                                1m36s   1GB
Jan 29 21:04:12 Starting compiler/encoders/riscv
Jan 29 21:06:01 Finished compiler/encoders/riscv                               1m48s 964MB
Jan 29 21:06:01 Starting compiler/encoders/ag32
Jan 29 21:06:20 Finished compiler/encoders/ag32                                  18s 851MB
Jan 29 21:06:20 Starting compiler/backend/x64
Jan 29 21:06:39 Finished compiler/backend/x64                                    19s   1GB
Jan 29 21:06:39 Starting compiler/backend/arm7
Jan 29 21:07:01 Finished compiler/backend/arm7                                   21s   1GB
Jan 29 21:07:01 Starting compiler/backend/arm8
Jan 29 21:07:21 Finished compiler/backend/arm8                                   19s   1GB
Jan 29 21:07:21 Starting compiler/backend/mips
Jan 29 21:07:41 Finished compiler/backend/mips                                   19s   1GB
Jan 29 21:07:41 Starting compiler/backend/riscv
Jan 29 21:08:02 Finished compiler/backend/riscv                                  20s   1GB
Jan 29 21:08:02 Starting compiler/backend/ag32
Jan 29 21:09:15 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 29 21:09:15 Starting compiler/parsing/proofs
Jan 29 21:15:03 Finished compiler/parsing/proofs                               5m47s   1GB
Jan 29 21:15:03 Starting compiler/inference/proofs
Jan 29 21:17:42 Finished compiler/inference/proofs                             2m38s   1GB
Jan 29 21:17:42 Starting compiler/backend/semantics
Jan 29 21:50:50 Finished compiler/backend/semantics                           33m07s   3GB
Jan 29 21:50:50 Starting compiler/backend/reg_alloc/proofs
Jan 29 21:54:37 Finished compiler/backend/reg_alloc/proofs                     3m45s 899MB
Jan 29 21:54:37 Starting compiler/backend/proofs
Jan 29 22:53:53 Finished compiler/backend/proofs                              59m15s  16GB
Jan 29 22:53:53 Starting compiler/encoders/x64/proofs
Jan 29 23:04:17 Finished compiler/encoders/x64/proofs                         10m23s   4GB
Jan 29 23:04:17 Starting compiler/encoders/arm7/proofs
Jan 29 23:18:21 Finished compiler/encoders/arm7/proofs                        14m04s   3GB
Jan 29 23:18:21 Starting compiler/encoders/arm8/proofs
Jan 29 23:25:19 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Jan 29 23:25:20 Starting compiler/encoders/mips/proofs
Jan 29 23:36:02 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Jan 29 23:36:02 Starting compiler/encoders/riscv/proofs
Jan 29 23:45:32 Finished compiler/encoders/riscv/proofs                        9m29s   1GB
Jan 29 23:45:32 Starting compiler/encoders/ag32/proofs
Jan 29 23:48:21 Finished compiler/encoders/ag32/proofs                         2m49s 768MB
Jan 29 23:48:22 Starting compiler/backend/x64/proofs
Jan 29 23:48:44 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 29 23:48:44 Starting compiler/backend/arm7/proofs
Jan 29 23:49:08 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 29 23:49:08 Starting compiler/backend/arm8/proofs
Jan 29 23:49:30 Finished compiler/backend/arm8/proofs                            21s   1GB
Jan 29 23:49:30 Starting compiler/backend/mips/proofs
Jan 29 23:49:51 Finished compiler/backend/mips/proofs                            21s   1GB
Jan 29 23:49:51 Starting compiler/backend/riscv/proofs
Jan 29 23:50:13 Finished compiler/backend/riscv/proofs                           21s   1GB
Jan 29 23:50:14 Starting compiler/backend/ag32/proofs
Jan 30 00:04:02 Finished compiler/backend/ag32/proofs                         13m48s   2GB
Jan 30 00:04:02 Starting compiler/proofs
Jan 30 00:06:01 Finished compiler/proofs                                       1m58s   4GB
Jan 30 00:06:02 Starting candle/set-theory
Jan 30 00:06:31 Finished candle/set-theory                                       29s 938MB
Jan 30 00:06:31 Starting candle/syntax-lib
Jan 30 00:06:42 Finished candle/syntax-lib                                       10s 707MB
Jan 30 00:06:42 Starting candle/standard/syntax
Jan 30 00:08:37 Finished candle/standard/syntax                                1m55s   1GB
Jan 30 00:08:38 Starting candle/standard/semantics
Jan 30 00:10:26 Finished candle/standard/semantics                             1m48s   1GB
Jan 30 00:10:26 Starting candle/standard/monadic
Jan 30 00:12:13 Finished candle/standard/monadic                               1m46s   1GB
Jan 30 00:12:13 Starting candle/standard/ml_kernel
Jan 30 00:18:10 Finished candle/standard/ml_kernel                             5m56s   5GB
Jan 30 00:18:10 Starting candle/overloading/syntax
Jan 30 00:21:29 Finished candle/overloading/syntax                             3m19s 998MB
Jan 30 00:21:30 Starting candle/overloading/semantics
Jan 30 00:34:27 Finished candle/overloading/semantics                         12m56s   4GB
Jan 30 00:34:27 Starting characteristic/examples
Jan 30 00:35:47 Finished characteristic/examples                               1m19s   2GB
Jan 30 00:35:47 Starting tutorial/solutions
Jan 30 00:51:46 Finished tutorial/solutions                                   15m59s   8GB
Jan 30 00:51:47 Starting translator/monadic/examples
Jan 30 00:55:02 Finished translator/monadic/examples                           3m15s   2GB
Jan 30 00:55:03 Starting examples
Jan 30 01:03:55 Finished examples                                              8m51s   5GB
Jan 30 01:03:55 Starting examples/compilation/x64
Jan 30 03:31:09 Finished examples/compilation/x64                           2h27m13s  19GB
Jan 30 03:31:09 Starting examples/compilation/x64/proofs
Jan 30 03:32:54 Finished examples/compilation/x64/proofs                       1m44s   3GB
Jan 30 03:32:54 Starting examples/compilation/ag32
Jan 30 04:07:19 Finished examples/compilation/ag32                            34m24s   7GB
Jan 30 04:07:20 Starting examples/compilation/ag32/proofs
Jan 30 04:08:05 Finished examples/compilation/ag32/proofs                        45s   2GB
Jan 30 04:08:06 Starting examples/cost
Jan 30 05:05:59 Finished examples/cost                                        57m53s   6GB
Jan 30 05:05:59 Starting examples/lpr_checker
Jan 30 05:10:15 Finished examples/lpr_checker                                  4m15s   4GB
Jan 30 05:10:16 Starting examples/lpr_checker/compilation
Jan 30 05:29:05 Finished examples/lpr_checker/compilation                     18m48s   9GB
Jan 30 05:29:05 Starting examples/lpr_checker/compilation/proofs
Jan 30 05:29:48 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Jan 30 05:29:48 Starting examples/lpr_checker/array
Jan 30 05:45:06 Finished examples/lpr_checker/array                           15m17s   3GB
Jan 30 05:45:06 Starting examples/lpr_checker/array/compilation
Jan 30 06:05:11 Finished examples/lpr_checker/array/compilation               20m04s  12GB
Jan 30 06:05:12 Starting examples/lpr_checker/array/compilation/proofs
Jan 30 06:06:21 Finished examples/lpr_checker/array/compilation/proofs         1m09s   3GB
Jan 30 06:06:21 Starting examples/opentheory
Jan 30 06:16:33 Finished examples/opentheory                                  10m11s   5GB
Jan 30 06:16:33 Starting examples/opentheory
Jan 30 06:16:34 Finished examples/opentheory                                      1s  22MB
Jan 30 06:16:34 Starting examples/opentheory/compilation
Jan 30 06:50:54 Finished examples/opentheory/compilation                      34m19s  19GB
Jan 30 06:50:54 Starting examples/opentheory/compilation/proofs
Jan 30 06:51:37 Finished examples/opentheory/compilation/proofs                  42s   3GB
Jan 30 06:51:37 Starting examples/opentheory/compilation/ag32
Jan 30 07:26:49 Finished examples/opentheory/compilation/ag32                 35m11s  18GB
Jan 30 07:26:49 Starting examples/opentheory/compilation/ag32/proofs
Jan 30 07:28:34 Finished examples/opentheory/compilation/ag32/proofs           1m44s   6GB
Jan 30 07:28:34 Starting translator/okasaki-examples
Jan 30 07:33:03 Finished translator/okasaki-examples                           4m28s   1GB
Jan 30 07:33:03 Starting translator/other-examples
Jan 30 07:35:03 Finished translator/other-examples                             2m00s   1GB
Jan 30 07:35:03 Starting compiler/parsing/tests
Jan 30 07:35:31 Finished compiler/parsing/tests                                  26s 534MB
Jan 30 07:35:31 Starting compiler/inference/tests
Jan 30 07:43:19 Finished compiler/inference/tests                              7m47s   4GB
Jan 30 07:43:19 Starting compiler/bootstrap/translation
Jan 30 10:33:56 Finished compiler/bootstrap/translation                     2h50m37s  42GB
Jan 30 10:33:57 Starting unverified/sexpr-bootstrap/x64/64
Jan 30 10:46:02 Finished unverified/sexpr-bootstrap/x64/64                    12m05s   8GB
Jan 30 10:46:03 Starting unverified/sexpr-bootstrap/x64/32
Jan 30 10:55:57 Finished unverified/sexpr-bootstrap/x64/32                     9m54s   9GB
Jan 30 10:55:57 Starting compiler/benchmarks
Jan 30 10:55:59 Finished compiler/benchmarks                                      1s  26MB
Jan 30 10:55:59 Starting compiler/bootstrap/compilation/x64/64
Jan 31 00:28:58 Finished compiler/bootstrap/compilation/x64/64             13h32m58s  64GB
Jan 31 00:28:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 31 00:32:02 Finished compiler/bootstrap/compilation/x64/64/proofs          3m03s  13GB
Jan 31 00:32:03 Starting compiler/bootstrap/compilation/x64/32
Jan 31 11:52:50 Finished compiler/bootstrap/compilation/x64/32             11h20m47s  64GB
Jan 31 11:52:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 31 11:55:48 Finished compiler/bootstrap/compilation/x64/32/proofs          2m56s  12GB
Jan 31 11:55:48 Starting compiler/bootstrap/compilation/ag32/32
Jan 31 23:34:19 Finished compiler/bootstrap/compilation/ag32/32            11h38m30s  64GB
Jan 31 23:34:19 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 31 23:46:40 Finished compiler/bootstrap/compilation/ag32/32/proofs        12m21s  25GB
Jan 31 23:46:40 SUCCESS