Job 1821

CakeML:ae75ff1c7037decacc9961931bf6a0490a3fe5f2
  Merge pull request #864 from CakeML/tidy-up [Mar 13 10:12:35]
HOL:9ef02c741e59da2e5b90512fc92aa8194c043623
  Fix Holmakefiles for Tamarack example; further modernise port-full [Mar 07 23:09:46]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 13 10:25:07 Claimed job
Mar 13 10:25:11 Reusing HOL
Mar 13 10:25:50 Starting developers
Mar 13 10:25:55 Finished developers                                               4s  96MB
Mar 13 10:25:55 Starting developers/bin
Mar 13 10:26:03 Finished developers/bin                                           7s   1GB
Mar 13 10:26:03 Starting semantics/ffi
Mar 13 10:26:18 Finished semantics/ffi                                           14s 215MB
Mar 13 10:26:18 Starting semantics
Mar 13 10:28:39 Finished semantics                                             2m20s 998MB
Mar 13 10:28:39 Starting semantics/proofs
Mar 13 10:32:57 Finished semantics/proofs                                      4m17s   1GB
Mar 13 10:32:57 Starting semantics/alt_semantics
Mar 13 10:33:16 Finished semantics/alt_semantics                                 18s 480MB
Mar 13 10:33:16 Starting semantics/alt_semantics/proofs
Mar 13 10:36:14 Finished semantics/alt_semantics/proofs                        2m57s   1GB
Mar 13 10:36:15 Starting basis/pure
Mar 13 10:37:30 Finished basis/pure                                            1m15s   1GB
Mar 13 10:37:30 Starting translator
Mar 13 10:41:10 Finished translator                                            3m39s   1GB
Mar 13 10:41:10 Starting compiler/parsing
Mar 13 10:42:52 Finished compiler/parsing                                      1m41s   1GB
Mar 13 10:42:52 Starting characteristic
Mar 13 10:50:15 Finished characteristic                                        7m21s   2GB
Mar 13 10:50:15 Starting translator/monadic
Mar 13 10:52:34 Finished translator/monadic                                    2m18s   1GB
Mar 13 10:52:35 Starting basis
Mar 13 11:47:17 Finished basis                                                54m42s   5GB
Mar 13 11:47:18 Starting compiler/inference
Mar 13 11:48:47 Finished compiler/inference                                    1m29s   1GB
Mar 13 11:48:48 Starting compiler/backend/reg_alloc
Mar 13 11:50:57 Finished compiler/backend/reg_alloc                            2m08s   1GB
Mar 13 11:50:57 Starting compiler/backend/gc
Mar 13 11:57:07 Finished compiler/backend/gc                                   6m09s 835MB
Mar 13 11:57:07 Starting compiler/backend
Mar 13 12:05:03 Finished compiler/backend                                      7m55s   1GB
Mar 13 12:05:03 Starting compiler/encoders/asm
Mar 13 12:05:36 Finished compiler/encoders/asm                                   32s 831MB
Mar 13 12:05:36 Starting compiler/encoders/x64
Mar 13 12:06:10 Finished compiler/encoders/x64                                   33s 770MB
Mar 13 12:06:10 Starting compiler/encoders/arm7
Mar 13 12:07:19 Finished compiler/encoders/arm7                                1m08s 695MB
Mar 13 12:07:19 Starting compiler/encoders/arm8
Mar 13 12:07:40 Finished compiler/encoders/arm8                                  20s 423MB
Mar 13 12:07:40 Starting compiler/encoders/arm8_asl
Mar 13 12:11:06 Finished compiler/encoders/arm8_asl                            3m25s 542MB
Mar 13 12:11:06 Starting compiler/encoders/mips
Mar 13 12:11:34 Finished compiler/encoders/mips                                  27s   1GB
Mar 13 12:11:34 Starting compiler/encoders/riscv
Mar 13 12:11:56 Finished compiler/encoders/riscv                                 21s 817MB
Mar 13 12:11:56 Starting compiler/encoders/ag32
Mar 13 12:12:20 Finished compiler/encoders/ag32                                  23s 700MB
Mar 13 12:12:21 Starting compiler/backend/x64
Mar 13 12:12:46 Finished compiler/backend/x64                                    25s   1GB
Mar 13 12:12:46 Starting compiler/backend/arm7
Mar 13 12:13:13 Finished compiler/backend/arm7                                   26s   1GB
Mar 13 12:13:14 Starting compiler/backend/arm8
Mar 13 12:13:50 Finished compiler/backend/arm8                                   36s 686MB
Mar 13 12:13:50 Starting compiler/backend/mips
Mar 13 12:14:16 Finished compiler/backend/mips                                   25s   1GB
Mar 13 12:14:16 Starting compiler/backend/riscv
Mar 13 12:14:40 Finished compiler/backend/riscv                                  23s   1GB
Mar 13 12:14:40 Starting compiler/backend/ag32
Mar 13 12:16:19 Finished compiler/backend/ag32                                 1m39s   1GB
Mar 13 12:16:19 Starting compiler/parsing/proofs
Mar 13 12:20:37 Finished compiler/parsing/proofs                               4m17s   1GB
Mar 13 12:20:37 Starting compiler/inference/proofs
Mar 13 12:23:29 Finished compiler/inference/proofs                             2m52s   1GB
Mar 13 12:23:30 Starting compiler/backend/semantics
Mar 13 13:00:31 Finished compiler/backend/semantics                           36m59s   1GB
Mar 13 13:00:31 Starting compiler/backend/reg_alloc/proofs
Mar 13 13:04:48 Finished compiler/backend/reg_alloc/proofs                     4m16s 893MB
Mar 13 13:04:48 Starting compiler/backend/proofs
Mar 13 14:17:59 Finished compiler/backend/proofs                            1h13m10s   5GB
Mar 13 14:17:59 Starting compiler/backend/serialiser
Mar 13 14:19:53 Finished compiler/backend/serialiser                           1m53s   2GB
Mar 13 14:19:53 Starting compiler/encoders/x64/proofs
Mar 13 14:31:03 Finished compiler/encoders/x64/proofs                         11m08s   5GB
Mar 13 14:31:03 Starting compiler/encoders/arm7/proofs
Mar 13 14:46:54 Finished compiler/encoders/arm7/proofs                        15m50s   1GB
Mar 13 14:46:54 Starting compiler/encoders/arm8/proofs
Mar 13 14:54:24 Finished compiler/encoders/arm8/proofs                         7m30s   1GB
Mar 13 14:54:25 Starting compiler/encoders/arm8_asl/proofs
Mar 13 15:11:35 Finished compiler/encoders/arm8_asl/proofs                    17m09s   2GB
Mar 13 15:11:35 Starting compiler/encoders/mips/proofs
Mar 13 15:23:10 Finished compiler/encoders/mips/proofs                        11m34s   2GB
Mar 13 15:23:10 Starting compiler/encoders/riscv/proofs
Mar 13 15:34:10 Finished compiler/encoders/riscv/proofs                       10m59s 604MB
Mar 13 15:34:10 Starting compiler/encoders/ag32/proofs
Mar 13 15:37:11 Finished compiler/encoders/ag32/proofs                         3m01s 780MB
Mar 13 15:37:11 Starting compiler/backend/x64/proofs
Mar 13 15:37:48 Finished compiler/backend/x64/proofs                             35s   1GB
Mar 13 15:37:48 Starting compiler/backend/arm7/proofs
Mar 13 15:38:31 Finished compiler/backend/arm7/proofs                            43s   1GB
Mar 13 15:38:31 Starting compiler/backend/arm8/proofs
Mar 13 15:39:03 Finished compiler/backend/arm8/proofs                            31s   1GB
Mar 13 15:39:04 Starting compiler/backend/arm8_asl
Mar 13 15:39:48 Finished compiler/backend/arm8_asl                               44s 817MB
Mar 13 15:39:48 Starting compiler/backend/mips/proofs
Mar 13 15:40:31 Finished compiler/backend/mips/proofs                            42s 877MB
Mar 13 15:40:31 Starting compiler/backend/riscv/proofs
Mar 13 15:41:05 Finished compiler/backend/riscv/proofs                           33s   1GB
Mar 13 15:41:05 Starting compiler/backend/ag32/proofs
Mar 13 15:56:48 Finished compiler/backend/ag32/proofs                         15m42s   2GB
Mar 13 15:56:48 Starting compiler/proofs
Mar 13 15:59:07 Finished compiler/proofs                                       2m18s   2GB
Mar 13 15:59:07 Starting candle/set-theory
Mar 13 15:59:44 Finished candle/set-theory                                       36s   1GB
Mar 13 15:59:44 Starting candle/syntax-lib
Mar 13 15:59:59 Finished candle/syntax-lib                                       14s 693MB
Mar 13 15:59:59 Starting candle/standard/syntax
Mar 13 16:02:14 Finished candle/standard/syntax                                2m14s   1GB
Mar 13 16:02:14 Starting candle/standard/semantics
Mar 13 16:04:14 Finished candle/standard/semantics                             1m59s   2GB
Mar 13 16:04:14 Starting candle/standard/monadic
Mar 13 16:06:20 Finished candle/standard/monadic                               2m05s   1GB
Mar 13 16:06:20 Starting candle/standard/ml_kernel
Mar 13 16:14:07 Finished candle/standard/ml_kernel                             7m46s   2GB
Mar 13 16:14:07 Starting candle/overloading/syntax
Mar 13 16:17:42 Finished candle/overloading/syntax                             3m34s   1GB
Mar 13 16:17:42 Starting candle/overloading/semantics
Mar 13 16:30:40 Finished candle/overloading/semantics                         12m58s   3GB
Mar 13 16:30:41 Starting candle/overloading/monadic
Mar 13 16:33:55 Finished candle/overloading/monadic                            3m14s 895MB
Mar 13 16:33:55 Starting candle/overloading/ml_kernel
Mar 13 16:43:18 Finished candle/overloading/ml_kernel                          9m23s   1GB
Mar 13 16:43:18 Starting candle/overloading/ml_checker
Mar 13 16:46:06 Finished candle/overloading/ml_checker                         2m47s   2GB
Mar 13 16:46:06 Starting candle/prover
Mar 13 16:55:35 Finished candle/prover                                         9m27s   1GB
Mar 13 16:55:35 Starting pancake
Mar 13 16:59:53 Finished pancake                                               4m17s   2GB
Mar 13 16:59:53 Starting pancake/ffi
Mar 13 16:59:54 Finished pancake/ffi                                              0s  13MB
Mar 13 16:59:54 Starting pancake/semantics
Mar 13 17:02:53 Finished pancake/semantics                                     2m59s   1GB
Mar 13 17:02:53 Starting pancake/proofs
Mar 13 17:17:28 Finished pancake/proofs                                       14m34s   2GB
Mar 13 17:17:29 Starting characteristic/examples
Mar 13 17:19:03 Finished characteristic/examples                               1m33s   2GB
Mar 13 17:19:03 Starting tutorial/solutions
Mar 13 17:39:29 Finished tutorial/solutions                                   20m25s   3GB
Mar 13 17:39:30 Starting translator/monadic/examples
Mar 13 17:44:33 Finished translator/monadic/examples                           5m03s   2GB
Mar 13 17:44:33 Starting examples
Mar 13 17:58:42 Finished examples                                             14m08s   3GB
Mar 13 17:58:43 Starting examples/compilation/x64
Mar 13 21:09:49 Finished examples/compilation/x64                           3h11m03s   5GB
Mar 13 21:09:49 Starting examples/compilation/x64/proofs
Mar 13 21:13:38 Finished examples/compilation/x64/proofs                       3m48s   2GB
Mar 13 21:13:39 Starting examples/compilation/ag32
Mar 13 21:58:23 Finished examples/compilation/ag32                            44m43s   4GB
Mar 13 21:58:23 Starting examples/compilation/ag32/proofs
Mar 13 22:00:05 Finished examples/compilation/ag32/proofs                      1m41s   1GB
Mar 13 22:00:05 Starting examples/cost
Mar 13 23:18:05 Finished examples/cost                                      1h18m00s   3GB
Mar 13 23:18:06 Starting examples/lpr_checker
Mar 13 23:19:22 Finished examples/lpr_checker                                  1m16s 982MB
Mar 13 23:19:22 Starting examples/lpr_checker/array
Mar 13 23:55:42 Finished examples/lpr_checker/array                           36m18s   1GB
Mar 13 23:55:42 Starting examples/lpr_checker/array/compilation
Mar 14 01:53:27 Finished examples/lpr_checker/array/compilation             1h57m45s   9GB
Mar 14 01:53:27 Starting examples/lpr_checker/array/compilation/proofs
Mar 14 01:56:43 Finished examples/lpr_checker/array/compilation/proofs         3m15s   3GB
Mar 14 01:56:43 Starting examples/opentheory
Mar 14 02:09:43 Finished examples/opentheory                                  12m59s   2GB
Mar 14 02:09:43 Starting examples/opentheory
Mar 14 02:09:45 Finished examples/opentheory                                      1s  19MB
Mar 14 02:09:45 Starting examples/opentheory/compilation
Mar 14 03:08:36 Finished examples/opentheory/compilation                      58m49s   4GB
Mar 14 03:08:36 Starting examples/opentheory/compilation/proofs
Mar 14 03:10:05 Finished examples/opentheory/compilation/proofs                1m28s   2GB
Mar 14 03:10:05 Starting examples/opentheory/compilation/ag32
Mar 14 04:03:18 Finished examples/opentheory/compilation/ag32                 53m11s   5GB
Mar 14 04:03:18 Starting examples/opentheory/compilation/ag32/proofs
Mar 14 04:05:48 Finished examples/opentheory/compilation/ag32/proofs           2m29s   3GB
Mar 14 04:05:48 Starting examples/sat_encodings
Mar 14 04:08:00 Finished examples/sat_encodings                                2m11s 868MB
Mar 14 04:08:00 Starting examples/sat_encodings/case_studies
Mar 14 04:09:58 Finished examples/sat_encodings/case_studies                   1m57s 794MB
Mar 14 04:09:58 Starting examples/sat_encodings/translation
Mar 14 04:17:11 Finished examples/sat_encodings/translation                    7m12s   2GB
Mar 14 04:17:11 Starting examples/sat_encodings/translation/compilation
Mar 14 05:25:20 Finished examples/sat_encodings/translation/compilation     1h08m08s   7GB
Mar 14 05:25:21 Starting translator/okasaki-examples
Mar 14 05:31:08 Finished translator/okasaki-examples                           5m47s   1GB
Mar 14 05:31:08 Starting translator/other-examples
Mar 14 05:32:20 Finished translator/other-examples                             1m11s   1GB
Mar 14 05:32:20 Starting compiler/parsing/tests
Mar 14 05:32:55 Finished compiler/parsing/tests                                  34s 495MB
Mar 14 05:32:55 Starting compiler/inference/tests
Mar 14 05:41:51 Finished compiler/inference/tests                              8m55s   4GB
Mar 14 05:41:51 Starting compiler/printing/test
Mar 14 05:46:11 Finished compiler/printing/test                                4m19s   1GB
Mar 14 05:46:11 Starting compiler/repl
Mar 14 06:01:59 Finished compiler/repl                                        15m47s   3GB
Mar 14 06:01:59 Starting compiler/bootstrap/translation Mar 14 06:01:59 19507s