Job 1461

CakeML: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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 01 06:00:34 Claimed job
Feb 01 06:00:43 Building HOL
Feb 01 06:14:54 Starting developers
Feb 01 06:14:55 Finished developers                                               0s  35MB
Feb 01 06:14:55 Starting developers/bin
Feb 01 06:15:01 Finished developers/bin                                           5s   1GB
Feb 01 06:15:01 Starting semantics/ffi
Feb 01 06:15:11 Finished semantics/ffi                                            9s 290MB
Feb 01 06:15:11 Starting semantics
Feb 01 06:16:44 Finished semantics                                             1m32s   1GB
Feb 01 06:16:44 Starting semantics/proofs
Feb 01 06:20:03 Finished semantics/proofs                                      3m18s   1GB
Feb 01 06:20:03 Starting semantics/alt_semantics
Feb 01 06:20:11 Finished semantics/alt_semantics                                  7s 415MB
Feb 01 06:20:11 Starting semantics/alt_semantics/proofs
Feb 01 06:22:18 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Feb 01 06:22:18 Starting basis/pure
Feb 01 06:24:59 Finished basis/pure                                            2m40s   1GB
Feb 01 06:24:59 Starting translator
Feb 01 06:27:35 Finished translator                                            2m35s   2GB
Feb 01 06:27:35 Starting compiler/parsing
Feb 01 06:28:41 Finished compiler/parsing                                      1m06s   4GB
Feb 01 06:28:41 Starting characteristic
Feb 01 06:34:39 Finished characteristic                                        5m57s   3GB
Feb 01 06:34:39 Starting translator/monadic
Feb 01 06:36:24 Finished translator/monadic                                    1m44s   3GB
Feb 01 06:36:24 Starting basis
Feb 01 07:19:44 Finished basis                                                43m19s  40GB
Feb 01 07:19:44 Starting compiler/inference
Feb 01 07:20:51 Finished compiler/inference                                    1m06s   1GB
Feb 01 07:20:51 Starting compiler/backend/reg_alloc
Feb 01 07:21:56 Finished compiler/backend/reg_alloc                            1m04s   1GB
Feb 01 07:21:56 Starting compiler/backend/gc
Feb 01 07:25:30 Finished compiler/backend/gc                                   3m34s   3GB
Feb 01 07:25:30 Starting compiler/backend
Feb 01 07:30:31 Finished compiler/backend                                      5m00s   5GB
Feb 01 07:30:31 Starting compiler/encoders/asm
Feb 01 07:30:53 Finished compiler/encoders/asm                                   21s   1GB
Feb 01 07:30:53 Starting compiler/encoders/x64
Feb 01 07:31:55 Finished compiler/encoders/x64                                 1m02s   1GB
Feb 01 07:31:55 Starting compiler/encoders/arm7
Feb 01 07:33:58 Finished compiler/encoders/arm7                                2m02s   1GB
Feb 01 07:33:58 Starting compiler/encoders/arm8
Feb 01 07:34:37 Finished compiler/encoders/arm8                                  38s 968MB
Feb 01 07:34:37 Starting compiler/encoders/mips
Feb 01 07:36:02 Finished compiler/encoders/mips                                1m25s   1GB
Feb 01 07:36:02 Starting compiler/encoders/riscv
Feb 01 07:37:40 Finished compiler/encoders/riscv                               1m37s   1GB
Feb 01 07:37:40 Starting compiler/encoders/ag32
Feb 01 07:37:58 Finished compiler/encoders/ag32                                  17s 954MB
Feb 01 07:37:58 Starting compiler/backend/x64
Feb 01 07:38:15 Finished compiler/backend/x64                                    17s   1GB
Feb 01 07:38:16 Starting compiler/backend/arm7
Feb 01 07:38:37 Finished compiler/backend/arm7                                   21s   1GB
Feb 01 07:38:37 Starting compiler/backend/arm8
Feb 01 07:38:57 Finished compiler/backend/arm8                                   19s   1GB
Feb 01 07:38:57 Starting compiler/backend/mips
Feb 01 07:39:18 Finished compiler/backend/mips                                   20s   1GB
Feb 01 07:39:18 Starting compiler/backend/riscv
Feb 01 07:39:40 Finished compiler/backend/riscv                                  21s   1GB
Feb 01 07:39:40 Starting compiler/backend/ag32
Feb 01 07:40:49 Finished compiler/backend/ag32                                 1m08s   1GB
Feb 01 07:40:49 Starting compiler/parsing/proofs
Feb 01 07:46:20 Finished compiler/parsing/proofs                               5m31s   2GB
Feb 01 07:46:20 Starting compiler/inference/proofs
Feb 01 07:48:52 Finished compiler/inference/proofs                             2m31s   2GB
Feb 01 07:48:52 Starting compiler/backend/semantics
Feb 01 08:16:01 Finished compiler/backend/semantics                           27m08s   5GB
Feb 01 08:16:01 Starting compiler/backend/reg_alloc/proofs
Feb 01 08:19:18 Finished compiler/backend/reg_alloc/proofs                     3m17s   1GB
Feb 01 08:19:18 Starting compiler/backend/proofs
Feb 01 09:12:55 Finished compiler/backend/proofs                              53m36s  25GB
Feb 01 09:12:56 Starting compiler/encoders/x64/proofs
Feb 01 09:22:10 Finished compiler/encoders/x64/proofs                          9m14s   7GB
Feb 01 09:22:10 Starting compiler/encoders/arm7/proofs
Feb 01 09:34:40 Finished compiler/encoders/arm7/proofs                        12m29s   4GB
Feb 01 09:34:40 Starting compiler/encoders/arm8/proofs
Feb 01 09:41:10 Finished compiler/encoders/arm8/proofs                         6m29s   3GB
Feb 01 09:41:10 Starting compiler/encoders/mips/proofs
Feb 01 09:50:58 Finished compiler/encoders/mips/proofs                         9m48s   6GB
Feb 01 09:50:58 Starting compiler/encoders/riscv/proofs
Feb 01 09:59:14 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Feb 01 09:59:14 Starting compiler/encoders/ag32/proofs
Feb 01 10:01:36 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Feb 01 10:01:36 Starting compiler/backend/x64/proofs
Feb 01 10:01:57 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 01 10:01:57 Starting compiler/backend/arm7/proofs
Feb 01 10:02:20 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 01 10:02:20 Starting compiler/backend/arm8/proofs
Feb 01 10:02:40 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 01 10:02:41 Starting compiler/backend/mips/proofs
Feb 01 10:03:02 Finished compiler/backend/mips/proofs                            21s   1GB
Feb 01 10:03:02 Starting compiler/backend/riscv/proofs
Feb 01 10:03:24 Finished compiler/backend/riscv/proofs                           21s   2GB
Feb 01 10:03:24 Starting compiler/backend/ag32/proofs
Feb 01 10:15:31 Finished compiler/backend/ag32/proofs                         12m06s   5GB
Feb 01 10:15:31 Starting compiler/proofs
Feb 01 10:17:25 Finished compiler/proofs                                       1m54s   6GB
Feb 01 10:17:25 Starting candle/set-theory
Feb 01 10:17:56 Finished candle/set-theory                                       30s   1GB
Feb 01 10:17:56 Starting candle/syntax-lib
Feb 01 10:18:07 Finished candle/syntax-lib                                       10s 851MB
Feb 01 10:18:07 Starting candle/standard/syntax
Feb 01 10:19:54 Finished candle/standard/syntax                                1m47s   1GB
Feb 01 10:19:54 Starting candle/standard/semantics
Feb 01 10:21:42 Finished candle/standard/semantics                             1m46s   2GB
Feb 01 10:21:42 Starting candle/standard/monadic
Feb 01 10:23:22 Finished candle/standard/monadic                               1m40s   1GB
Feb 01 10:23:22 Starting candle/standard/ml_kernel
Feb 01 10:28:40 Finished candle/standard/ml_kernel                             5m17s   6GB
Feb 01 10:28:40 Starting candle/overloading/syntax
Feb 01 10:31:50 Finished candle/overloading/syntax                             3m09s   1GB
Feb 01 10:31:51 Starting candle/overloading/semantics
Feb 01 10:44:01 Finished candle/overloading/semantics                         12m10s   8GB
Feb 01 10:44:01 Starting characteristic/examples
Feb 01 10:45:19 Finished characteristic/examples                               1m17s   4GB
Feb 01 10:45:19 Starting tutorial/solutions
Feb 01 11:00:03 Finished tutorial/solutions                                   14m44s  11GB
Feb 01 11:00:03 Starting translator/monadic/examples
Feb 01 11:03:22 Finished translator/monadic/examples                           3m18s   4GB
Feb 01 11:03:22 Starting examples
Feb 01 11:11:59 Finished examples                                              8m36s   7GB
Feb 01 11:11:59 Starting examples/compilation/x64
Feb 01 13:31:27 Finished examples/compilation/x64                           2h19m27s  20GB
Feb 01 13:31:27 Starting examples/compilation/x64/proofs
Feb 01 13:33:20 Finished examples/compilation/x64/proofs                       1m52s   3GB
Feb 01 13:33:20 Starting examples/compilation/ag32
Feb 01 14:06:04 Finished examples/compilation/ag32                            32m43s  12GB
Feb 01 14:06:04 Starting examples/compilation/ag32/proofs
Feb 01 14:06:58 Finished examples/compilation/ag32/proofs                        53s   4GB
Feb 01 14:06:58 Starting examples/cost
Feb 01 15:00:02 Finished examples/cost                                        53m04s  15GB
Feb 01 15:00:02 Starting examples/lpr_checker
Feb 01 15:03:54 Finished examples/lpr_checker                                  3m50s   5GB
Feb 01 15:03:54 Starting examples/lpr_checker/compilation
Feb 01 15:22:17 Finished examples/lpr_checker/compilation                     18m22s  18GB
Feb 01 15:22:17 Starting examples/lpr_checker/compilation/proofs
Feb 01 15:23:02 Finished examples/lpr_checker/compilation/proofs                 44s   3GB
Feb 01 15:23:02 Starting examples/lpr_checker/array
Feb 01 15:36:42 Finished examples/lpr_checker/array                           13m39s   5GB
Feb 01 15:36:42 Starting examples/lpr_checker/array/compilation
Feb 01 15:55:58 Finished examples/lpr_checker/array/compilation               19m15s  15GB
Feb 01 15:55:59 Starting examples/lpr_checker/array/compilation/proofs
Feb 01 15:56:47 Finished examples/lpr_checker/array/compilation/proofs           48s   5GB
Feb 01 15:56:47 Starting examples/opentheory
Feb 01 16:05:59 Finished examples/opentheory                                   9m11s   8GB
Feb 01 16:05:59 Starting examples/opentheory
Feb 01 16:06:00 Finished examples/opentheory                                      0s 100MB
Feb 01 16:06:00 Starting examples/opentheory/compilation
Feb 01 16:37:01 Finished examples/opentheory/compilation                      31m01s  53GB
Feb 01 16:37:01 Starting examples/opentheory/compilation/proofs
Feb 01 16:37:44 Finished examples/opentheory/compilation/proofs                  42s   4GB
Feb 01 16:37:45 Starting examples/opentheory/compilation/ag32
Feb 01 17:10:13 Finished examples/opentheory/compilation/ag32                 32m28s  17GB
Feb 01 17:10:13 Starting examples/opentheory/compilation/ag32/proofs
Feb 01 17:11:44 Finished examples/opentheory/compilation/ag32/proofs           1m30s   6GB
Feb 01 17:11:44 Starting translator/okasaki-examples
Feb 01 17:15:54 Finished translator/okasaki-examples                           4m10s   2GB
Feb 01 17:15:54 Starting translator/other-examples
Feb 01 17:17:58 Finished translator/other-examples                             2m03s   1GB
Feb 01 17:17:58 Starting compiler/parsing/tests
Feb 01 17:18:22 Finished compiler/parsing/tests                                  23s 650MB
Feb 01 17:18:22 Starting compiler/inference/tests
Feb 01 17:25:27 Finished compiler/inference/tests                              7m05s   6GB
Feb 01 17:25:28 Starting compiler/bootstrap/translation
Feb 01 20:01:39 Finished compiler/bootstrap/translation                     2h36m11s  46GB
Feb 01 20:01:40 Starting unverified/sexpr-bootstrap/x64/64
Feb 01 20:14:42 Finished unverified/sexpr-bootstrap/x64/64                    12m16s   8GB
Feb 01 20:14:43 Starting unverified/sexpr-bootstrap/x64/32
Feb 01 20:25:39 Finished unverified/sexpr-bootstrap/x64/32                    10m25s   8GB
Feb 01 20:25:39 Starting compiler/benchmarks
Feb 01 21:03:39 Finished compiler/benchmarks                                  37m58s   2GB
Feb 01 21:03:39 Starting compiler/bootstrap/compilation/x64/64
Feb 02 14:26:34 Finished compiler/bootstrap/compilation/x64/64             17h22m30s  64GB
Feb 02 14:26:34 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 02 14:28:50 Finished compiler/bootstrap/compilation/x64/64/proofs          2m16s  15GB
Feb 02 14:28:50 Starting compiler/bootstrap/compilation/x64/32
Feb 03 04:56:49 Finished compiler/bootstrap/compilation/x64/32             14h27m31s  64GB
Feb 03 04:56:50 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 03 04:58:57 Finished compiler/bootstrap/compilation/x64/32/proofs          2m07s  19GB
Feb 03 04:58:58 Starting compiler/bootstrap/compilation/ag32/32
Feb 03 23:04:23 Finished compiler/bootstrap/compilation/ag32/32            18h05m24s  63GB
Feb 03 23:04:23 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 03 23:14:30 Finished compiler/bootstrap/compilation/ag32/32/proofs        10m07s  56GB
Feb 03 23:14:31 SUCCESS