Job 1477

CakeML:dd7aa9e3110787b7b7265a7cfb50ad016e79de4b
  remove another obsolete lemma [Feb 17 08:53:32]
#816 (cyclicity-check)
Merging into:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:3f7004dd05c08c5551cb3ab2dbfe6eccdb876a19
  Fix some problems in generation of REFERENCE manual [Feb 15 02:29:05]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 18 05:43:50 Claimed job
Feb 18 05:43:52 Reusing HOL
Feb 18 05:43:58 Starting developers
Feb 18 05:43:59 Finished developers                                               0s  36MB
Feb 18 05:43:59 Starting developers/bin
Feb 18 05:44:05 Finished developers/bin                                           5s   1GB
Feb 18 05:44:05 Starting semantics/ffi
Feb 18 05:44:15 Finished semantics/ffi                                            9s 285MB
Feb 18 05:44:15 Starting semantics
Feb 18 05:45:38 Finished semantics                                             1m22s   1GB
Feb 18 05:45:38 Starting semantics/proofs
Feb 18 05:48:55 Finished semantics/proofs                                      3m16s   1GB
Feb 18 05:48:56 Starting semantics/alt_semantics
Feb 18 05:49:04 Finished semantics/alt_semantics                                  8s 390MB
Feb 18 05:49:04 Starting semantics/alt_semantics/proofs
Feb 18 05:51:12 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Feb 18 05:51:12 Starting basis/pure
Feb 18 05:52:05 Finished basis/pure                                              52s   1GB
Feb 18 05:52:05 Starting translator
Feb 18 05:54:38 Finished translator                                            2m32s   2GB
Feb 18 05:54:38 Starting compiler/parsing
Feb 18 05:55:44 Finished compiler/parsing                                      1m05s   3GB
Feb 18 05:55:44 Starting characteristic
Feb 18 06:01:40 Finished characteristic                                        5m55s   4GB
Feb 18 06:01:40 Starting translator/monadic
Feb 18 06:03:26 Finished translator/monadic                                    1m45s   2GB
Feb 18 06:03:26 Starting basis
Feb 18 06:46:39 Finished basis                                                43m12s  30GB
Feb 18 06:46:39 Starting compiler/inference
Feb 18 06:47:43 Finished compiler/inference                                    1m03s   2GB
Feb 18 06:47:43 Starting compiler/backend/reg_alloc
Feb 18 06:48:47 Finished compiler/backend/reg_alloc                            1m03s   1GB
Feb 18 06:48:47 Starting compiler/backend/gc
Feb 18 06:52:09 Finished compiler/backend/gc                                   3m21s   3GB
Feb 18 06:52:09 Starting compiler/backend
Feb 18 06:57:14 Finished compiler/backend                                      5m04s   4GB
Feb 18 06:57:14 Starting compiler/encoders/asm
Feb 18 06:57:36 Finished compiler/encoders/asm                                   21s   1GB
Feb 18 06:57:36 Starting compiler/encoders/x64
Feb 18 06:58:03 Finished compiler/encoders/x64                                   26s   1GB
Feb 18 06:58:03 Starting compiler/encoders/arm7
Feb 18 06:58:54 Finished compiler/encoders/arm7                                  50s   1GB
Feb 18 06:58:54 Starting compiler/encoders/arm8
Feb 18 06:59:08 Finished compiler/encoders/arm8                                  13s   1GB
Feb 18 06:59:08 Starting compiler/encoders/mips
Feb 18 06:59:26 Finished compiler/encoders/mips                                  17s   1GB
Feb 18 06:59:26 Starting compiler/encoders/riscv
Feb 18 06:59:42 Finished compiler/encoders/riscv                                 16s   1GB
Feb 18 06:59:42 Starting compiler/encoders/ag32
Feb 18 07:00:01 Finished compiler/encoders/ag32                                  18s 956MB
Feb 18 07:00:01 Starting compiler/backend/x64
Feb 18 07:00:21 Finished compiler/backend/x64                                    19s   1GB
Feb 18 07:00:21 Starting compiler/backend/arm7
Feb 18 07:00:42 Finished compiler/backend/arm7                                   20s   1GB
Feb 18 07:00:42 Starting compiler/backend/arm8
Feb 18 07:01:02 Finished compiler/backend/arm8                                   20s   1GB
Feb 18 07:01:03 Starting compiler/backend/mips
Feb 18 07:01:23 Finished compiler/backend/mips                                   20s   1GB
Feb 18 07:01:23 Starting compiler/backend/riscv
Feb 18 07:01:44 Finished compiler/backend/riscv                                  20s   1GB
Feb 18 07:01:44 Starting compiler/backend/ag32
Feb 18 07:02:54 Finished compiler/backend/ag32                                 1m09s   2GB
Feb 18 07:02:54 Starting compiler/parsing/proofs
Feb 18 07:08:22 Finished compiler/parsing/proofs                               5m27s   2GB
Feb 18 07:08:22 Starting compiler/inference/proofs
Feb 18 07:10:53 Finished compiler/inference/proofs                             2m31s   2GB
Feb 18 07:10:54 Starting compiler/backend/semantics
Feb 18 07:37:40 Finished compiler/backend/semantics                           26m46s   3GB
Feb 18 07:37:40 Starting compiler/backend/reg_alloc/proofs
Feb 18 07:40:55 Finished compiler/backend/reg_alloc/proofs                     3m15s   2GB
Feb 18 07:40:55 Starting compiler/backend/proofs
Feb 18 08:34:25 Finished compiler/backend/proofs                              53m29s  14GB
Feb 18 08:34:26 Starting compiler/encoders/x64/proofs
Feb 18 08:43:51 Finished compiler/encoders/x64/proofs                          9m25s   6GB
Feb 18 08:43:51 Starting compiler/encoders/arm7/proofs
Feb 18 08:56:38 Finished compiler/encoders/arm7/proofs                        12m47s   7GB
Feb 18 08:56:39 Starting compiler/encoders/arm8/proofs
Feb 18 09:02:56 Finished compiler/encoders/arm8/proofs                         6m17s   3GB
Feb 18 09:02:56 Starting compiler/encoders/mips/proofs
Feb 18 09:12:49 Finished compiler/encoders/mips/proofs                         9m52s   7GB
Feb 18 09:12:49 Starting compiler/encoders/riscv/proofs
Feb 18 09:21:08 Finished compiler/encoders/riscv/proofs                        8m18s   3GB
Feb 18 09:21:08 Starting compiler/encoders/ag32/proofs
Feb 18 09:23:28 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Feb 18 09:23:28 Starting compiler/backend/x64/proofs
Feb 18 09:23:50 Finished compiler/backend/x64/proofs                             21s   2GB
Feb 18 09:23:50 Starting compiler/backend/arm7/proofs
Feb 18 09:24:14 Finished compiler/backend/arm7/proofs                            23s   1GB
Feb 18 09:24:14 Starting compiler/backend/arm8/proofs
Feb 18 09:24:34 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 18 09:24:34 Starting compiler/backend/mips/proofs
Feb 18 09:24:56 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 18 09:24:56 Starting compiler/backend/riscv/proofs
Feb 18 09:25:19 Finished compiler/backend/riscv/proofs                           22s   2GB
Feb 18 09:25:20 Starting compiler/backend/ag32/proofs
Feb 18 09:37:19 Finished compiler/backend/ag32/proofs                         11m58s   4GB
Feb 18 09:37:19 Starting compiler/proofs
Feb 18 09:38:59 Finished compiler/proofs                                       1m39s   6GB
Feb 18 09:38:59 Starting candle/set-theory
Feb 18 09:39:28 Finished candle/set-theory                                       28s 958MB
Feb 18 09:39:28 Starting candle/syntax-lib
Feb 18 09:39:40 Finished candle/syntax-lib                                       11s 793MB
Feb 18 09:39:40 Starting candle/standard/syntax
Feb 18 09:41:29 Finished candle/standard/syntax                                1m48s   1GB
Feb 18 09:41:29 Starting candle/standard/semantics
Feb 18 09:43:15 Finished candle/standard/semantics                             1m46s   2GB
Feb 18 09:43:15 Starting candle/standard/monadic
Feb 18 09:44:56 Finished candle/standard/monadic                               1m40s   1GB
Feb 18 09:44:56 Starting candle/standard/ml_kernel
Feb 18 09:50:12 Finished candle/standard/ml_kernel                             5m15s   5GB
Feb 18 09:50:12 Starting candle/overloading/syntax
Feb 18 09:53:21 Finished candle/overloading/syntax                             3m09s   1GB
Feb 18 09:53:21 Starting candle/overloading/semantics
Feb 18 10:05:31 Finished candle/overloading/semantics                         12m09s   8GB
Feb 18 10:05:31 Starting characteristic/examples
Feb 18 10:06:50 Finished characteristic/examples                               1m18s   4GB
Feb 18 10:06:50 Starting tutorial/solutions
Feb 18 10:21:49 Finished tutorial/solutions                                   14m59s  17GB
Feb 18 10:21:49 Starting translator/monadic/examples
Feb 18 10:25:09 Finished translator/monadic/examples                           3m19s   4GB
Feb 18 10:25:10 Starting examples
Feb 18 10:33:51 Finished examples                                              8m41s   8GB
Feb 18 10:33:51 Starting examples/compilation/x64
Feb 18 12:54:19 Finished examples/compilation/x64                           2h20m27s  22GB
Feb 18 12:54:19 Starting examples/compilation/x64/proofs
Feb 18 12:56:15 Finished examples/compilation/x64/proofs                       1m56s   3GB
Feb 18 12:56:15 Starting examples/compilation/ag32
Feb 18 13:29:33 Finished examples/compilation/ag32                            33m17s  12GB
Feb 18 13:29:33 Starting examples/compilation/ag32/proofs
Feb 18 13:30:22 Finished examples/compilation/ag32/proofs                        48s   4GB
Feb 18 13:30:22 Starting examples/cost
Feb 18 14:23:45 Finished examples/cost                                        53m22s  10GB
Feb 18 14:23:45 Starting examples/lpr_checker
Feb 18 14:27:33 Finished examples/lpr_checker                                  3m47s   5GB
Feb 18 14:27:33 Starting examples/lpr_checker/compilation
Feb 18 14:46:04 Finished examples/lpr_checker/compilation                     18m31s  14GB
Feb 18 14:46:05 Starting examples/lpr_checker/compilation/proofs
Feb 18 14:46:47 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Feb 18 14:46:47 Starting examples/lpr_checker/array
Feb 18 15:00:24 Finished examples/lpr_checker/array                           13m36s   4GB
Feb 18 15:00:24 Starting examples/lpr_checker/array/compilation
Feb 18 15:19:49 Finished examples/lpr_checker/array/compilation               19m24s  15GB
Feb 18 15:19:49 Starting examples/lpr_checker/array/compilation/proofs
Feb 18 15:20:36 Finished examples/lpr_checker/array/compilation/proofs           47s   4GB
Feb 18 15:20:37 Starting examples/opentheory
Feb 18 15:29:49 Finished examples/opentheory                                   9m12s   7GB
Feb 18 15:29:50 Starting examples/opentheory
Feb 18 15:29:50 Finished examples/opentheory                                      0s 100MB
Feb 18 15:29:51 Starting examples/opentheory/compilation
Feb 18 16:02:24 Finished examples/opentheory/compilation                      32m33s  33GB
Feb 18 16:02:24 Starting examples/opentheory/compilation/proofs
Feb 18 16:03:07 Finished examples/opentheory/compilation/proofs                  42s   3GB
Feb 18 16:03:07 Starting examples/opentheory/compilation/ag32
Feb 18 16:35:27 Finished examples/opentheory/compilation/ag32                 32m19s  22GB
Feb 18 16:35:27 Starting examples/opentheory/compilation/ag32/proofs
Feb 18 16:36:59 Finished examples/opentheory/compilation/ag32/proofs           1m31s   6GB
Feb 18 16:36:59 Starting translator/okasaki-examples
Feb 18 16:41:10 Finished translator/okasaki-examples                           4m10s   3GB
Feb 18 16:41:10 Starting translator/other-examples
Feb 18 16:43:16 Finished translator/other-examples                             2m05s   1GB
Feb 18 16:43:16 Starting compiler/parsing/tests
Feb 18 16:43:40 Finished compiler/parsing/tests                                  23s 702MB
Feb 18 16:43:40 Starting compiler/inference/tests
Feb 18 16:50:50 Finished compiler/inference/tests                              7m09s   5GB
Feb 18 16:50:50 Starting compiler/bootstrap/translation
Feb 18 19:26:44 Finished compiler/bootstrap/translation                     2h35m52s  47GB
Feb 18 19:26:44 Starting unverified/sexpr-bootstrap/x64/64
Feb 18 19:38:55 Finished unverified/sexpr-bootstrap/x64/64                    12m10s   8GB
Feb 18 19:38:55 Starting unverified/sexpr-bootstrap/x64/32
Feb 18 19:49:20 Finished unverified/sexpr-bootstrap/x64/32                    10m25s   8GB
Feb 18 19:49:20 Starting compiler/benchmarks
Feb 18 20:27:05 Finished compiler/benchmarks                                  37m44s   2GB
Feb 18 20:27:05 Starting compiler/bootstrap/compilation/x64/64
Feb 19 13:09:30 Finished compiler/bootstrap/compilation/x64/64             16h42m23s  64GB
Feb 19 13:09:30 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 19 13:11:46 Finished compiler/bootstrap/compilation/x64/64/proofs          2m16s  15GB
Feb 19 13:11:46 Starting compiler/bootstrap/compilation/x64/32
Feb 20 03:08:13 Finished compiler/bootstrap/compilation/x64/32             13h56m25s  64GB
Feb 20 03:08:13 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 20 03:10:36 Finished compiler/bootstrap/compilation/x64/32/proofs          2m23s  13GB
Feb 20 03:10:37 Starting compiler/bootstrap/compilation/ag32/32
Feb 20 19:31:27 Finished compiler/bootstrap/compilation/ag32/32            16h20m48s  64GB
Feb 20 19:31:27 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 20 19:40:39 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m12s  56GB
Feb 20 19:40:39 SUCCESS