Job 1841

CakeML:8eb9e723e9f4cc989c97a68a0a5adbf6e5bec1e3
  Merge pull request #869 from CakeML/ffi-changes [Mar 31 15:20:09]
HOL:e423188b196a54551b2b4fddb00dc960d0ee96c4
  Minkowski's inequality and its applications in Probability (#1009) [Mar 25 02:18:56]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 31 15:30:02 Claimed job
Mar 31 15:30:04 Reusing HOL
Mar 31 15:30:43 Starting developers
Mar 31 15:30:48 Finished developers                                               4s 125MB
Mar 31 15:30:49 Starting developers/bin
Mar 31 15:31:00 Finished developers/bin                                          10s   1GB
Mar 31 15:31:00 Starting semantics/ffi
Mar 31 15:31:15 Finished semantics/ffi                                           14s 211MB
Mar 31 15:31:15 Starting semantics
Mar 31 15:33:48 Finished semantics                                             2m33s   1GB
Mar 31 15:33:49 Starting semantics/proofs
Mar 31 15:39:22 Finished semantics/proofs                                      5m32s   1GB
Mar 31 15:39:22 Starting semantics/alt_semantics
Mar 31 15:39:43 Finished semantics/alt_semantics                                 20s 275MB
Mar 31 15:39:43 Starting semantics/alt_semantics/proofs
Mar 31 15:42:25 Finished semantics/alt_semantics/proofs                        2m41s 885MB
Mar 31 15:42:25 Starting basis/pure
Mar 31 15:46:04 Finished basis/pure                                            3m38s 830MB
Mar 31 15:46:04 Starting translator
Mar 31 15:49:56 Finished translator                                            3m51s   1GB
Mar 31 15:49:57 Starting compiler/parsing
Mar 31 15:51:32 Finished compiler/parsing                                      1m35s   1GB
Mar 31 15:51:32 Starting characteristic
Mar 31 15:59:05 Finished characteristic                                        7m31s   1GB
Mar 31 15:59:05 Starting translator/monadic
Mar 31 16:01:23 Finished translator/monadic                                    2m17s   1GB
Mar 31 16:01:23 Starting basis
Mar 31 16:59:57 Finished basis                                                58m33s   2GB
Mar 31 16:59:57 Starting compiler/inference
Mar 31 17:01:34 Finished compiler/inference                                    1m36s   1GB
Mar 31 17:01:34 Starting compiler/backend/reg_alloc
Mar 31 17:03:33 Finished compiler/backend/reg_alloc                            1m58s   1GB
Mar 31 17:03:33 Starting compiler/backend/gc
Mar 31 17:09:28 Finished compiler/backend/gc                                   5m54s   1GB
Mar 31 17:09:28 Starting compiler/backend
Mar 31 17:17:18 Finished compiler/backend                                      7m49s   2GB
Mar 31 17:17:18 Starting compiler/encoders/asm
Mar 31 17:17:53 Finished compiler/encoders/asm                                   35s 682MB
Mar 31 17:17:53 Starting compiler/encoders/x64
Mar 31 17:19:11 Finished compiler/encoders/x64                                 1m17s 865MB
Mar 31 17:19:11 Starting compiler/encoders/arm7
Mar 31 17:21:45 Finished compiler/encoders/arm7                                2m33s   1GB
Mar 31 17:21:45 Starting compiler/encoders/arm8
Mar 31 17:22:37 Finished compiler/encoders/arm8                                  51s 776MB
Mar 31 17:22:37 Starting compiler/encoders/arm8_asl
Mar 31 20:14:53 Finished compiler/encoders/arm8_asl                         2h52m15s   6GB
Mar 31 20:14:53 Starting compiler/encoders/mips
Mar 31 20:17:40 Finished compiler/encoders/mips                                2m46s 759MB
Mar 31 20:17:40 Starting compiler/encoders/riscv
Mar 31 20:20:15 Finished compiler/encoders/riscv                               2m35s 402MB
Mar 31 20:20:16 Starting compiler/encoders/ag32
Mar 31 20:20:52 Finished compiler/encoders/ag32                                  35s 278MB
Mar 31 20:20:52 Starting compiler/backend/x64
Mar 31 20:21:32 Finished compiler/backend/x64                                    40s 625MB
Mar 31 20:21:32 Starting compiler/backend/arm7
Mar 31 20:22:11 Finished compiler/backend/arm7                                   38s 776MB
Mar 31 20:22:11 Starting compiler/backend/arm8
Mar 31 20:22:44 Finished compiler/backend/arm8                                   32s 715MB
Mar 31 20:22:44 Starting compiler/backend/mips
Mar 31 20:23:10 Finished compiler/backend/mips                                   25s   1GB
Mar 31 20:23:11 Starting compiler/backend/riscv
Mar 31 20:23:37 Finished compiler/backend/riscv                                  26s   1GB
Mar 31 20:23:37 Starting compiler/backend/ag32
Mar 31 20:25:54 Finished compiler/backend/ag32                                 2m16s 610MB
Mar 31 20:25:54 Starting compiler/parsing/proofs
Mar 31 20:31:06 Finished compiler/parsing/proofs                               5m11s 742MB
Mar 31 20:31:07 Starting compiler/inference/proofs
Mar 31 20:34:21 Finished compiler/inference/proofs                             3m13s 968MB
Mar 31 20:34:21 Starting compiler/backend/semantics
Mar 31 21:13:58 Finished compiler/backend/semantics                           39m36s   1GB
Mar 31 21:13:58 Starting compiler/backend/reg_alloc/proofs
Mar 31 21:18:07 Finished compiler/backend/reg_alloc/proofs                     4m08s 728MB
Mar 31 21:18:07 Starting compiler/backend/proofs
Mar 31 22:30:02 Finished compiler/backend/proofs                            1h11m53s   5GB
Mar 31 22:30:03 Starting compiler/backend/serialiser
Mar 31 22:31:59 Finished compiler/backend/serialiser                           1m56s   2GB
Mar 31 22:32:00 Starting compiler/encoders/x64/proofs
Mar 31 22:44:44 Finished compiler/encoders/x64/proofs                         12m43s   1GB
Mar 31 22:44:44 Starting compiler/encoders/arm7/proofs
Mar 31 23:01:34 Finished compiler/encoders/arm7/proofs                        16m50s   1GB
Mar 31 23:01:35 Starting compiler/encoders/arm8/proofs
Mar 31 23:09:50 Finished compiler/encoders/arm8/proofs                         8m14s 848MB
Mar 31 23:09:50 Starting compiler/encoders/arm8_asl/proofs
Apr 01 00:12:32 Finished compiler/encoders/arm8_asl/proofs                  1h02m41s   3GB
Apr 01 00:12:32 Starting compiler/encoders/mips/proofs
Apr 01 00:24:40 Finished compiler/encoders/mips/proofs                        12m07s   1GB
Apr 01 00:24:40 Starting compiler/encoders/riscv/proofs
Apr 01 00:35:29 Finished compiler/encoders/riscv/proofs                       10m48s 639MB
Apr 01 00:35:30 Starting compiler/encoders/ag32/proofs
Apr 01 00:38:39 Finished compiler/encoders/ag32/proofs                         3m09s 497MB
Apr 01 00:38:39 Starting compiler/backend/x64/proofs
Apr 01 00:39:21 Finished compiler/backend/x64/proofs                             41s 877MB
Apr 01 00:39:21 Starting compiler/backend/arm7/proofs
Apr 01 00:40:06 Finished compiler/backend/arm7/proofs                            44s 999MB
Apr 01 00:40:06 Starting compiler/backend/arm8/proofs
Apr 01 00:40:54 Finished compiler/backend/arm8/proofs                            48s 594MB
Apr 01 00:40:55 Starting compiler/backend/arm8_asl
Apr 01 00:41:32 Finished compiler/backend/arm8_asl                               37s 807MB
Apr 01 00:41:33 Starting compiler/backend/mips/proofs
Apr 01 00:42:16 Finished compiler/backend/mips/proofs                            43s 709MB
Apr 01 00:42:17 Starting compiler/backend/riscv/proofs
Apr 01 00:42:49 Finished compiler/backend/riscv/proofs                           32s   1GB
Apr 01 00:42:49 Starting compiler/backend/ag32/proofs
Apr 01 00:59:22 Finished compiler/backend/ag32/proofs                         16m32s   1GB
Apr 01 00:59:22 Starting compiler/proofs
Apr 01 01:03:05 Finished compiler/proofs                                       3m42s   1GB
Apr 01 01:03:05 Starting candle/set-theory
Apr 01 01:03:48 Finished candle/set-theory                                       42s 696MB
Apr 01 01:03:48 Starting candle/syntax-lib
Apr 01 01:04:04 Finished candle/syntax-lib                                       15s 701MB
Apr 01 01:04:04 Starting candle/standard/syntax
Apr 01 01:06:23 Finished candle/standard/syntax                                2m18s   1GB
Apr 01 01:06:23 Starting candle/standard/semantics
Apr 01 01:08:28 Finished candle/standard/semantics                             2m04s   1GB
Apr 01 01:08:28 Starting candle/standard/monadic
Apr 01 01:10:44 Finished candle/standard/monadic                               2m15s   1GB
Apr 01 01:10:44 Starting candle/standard/ml_kernel
Apr 01 01:19:02 Finished candle/standard/ml_kernel                             8m15s   1GB
Apr 01 01:19:02 Starting candle/overloading/syntax
Apr 01 01:23:18 Finished candle/overloading/syntax                             4m15s 306MB
Apr 01 01:23:18 Starting candle/overloading/semantics
Apr 01 01:38:13 Finished candle/overloading/semantics                         14m54s   1GB
Apr 01 01:38:13 Starting candle/overloading/monadic
Apr 01 01:41:17 Finished candle/overloading/monadic                            3m03s 824MB
Apr 01 01:41:17 Starting candle/overloading/ml_kernel
Apr 01 01:50:52 Finished candle/overloading/ml_kernel                          9m34s   1GB
Apr 01 01:50:52 Starting candle/overloading/ml_checker
Apr 01 01:53:51 Finished candle/overloading/ml_checker                         2m58s   1GB
Apr 01 01:53:51 Starting candle/prover
Apr 01 02:03:58 Finished candle/prover                                        10m07s   3GB
Apr 01 02:03:58 Starting pancake
Apr 01 02:08:48 Finished pancake                                               4m49s   1GB
Apr 01 02:08:48 Starting pancake/ffi
Apr 01 02:08:49 Finished pancake/ffi                                              0s  11MB
Apr 01 02:08:49 Starting pancake/semantics
Apr 01 02:11:53 Finished pancake/semantics                                     3m03s   1GB
Apr 01 02:11:53 Starting pancake/proofs
Apr 01 02:28:17 Finished pancake/proofs                                       16m22s   2GB
Apr 01 02:28:17 Starting characteristic/examples
Apr 01 02:30:33 Finished characteristic/examples                               2m15s 972MB
Apr 01 02:30:33 Starting tutorial/solutions
Apr 01 02:53:30 Finished tutorial/solutions                                   22m56s   2GB
Apr 01 02:53:30 Starting translator/monadic/examples
Apr 01 02:58:48 Finished translator/monadic/examples                           5m17s   2GB
Apr 01 02:58:48 Starting examples
Apr 01 03:13:38 Finished examples                                             14m49s   2GB
Apr 01 03:13:39 Starting examples/compilation/x64
Apr 01 06:33:17 Finished examples/compilation/x64                           3h19m37s   3GB
Apr 01 06:33:17 Starting examples/compilation/x64/proofs
Apr 01 06:37:36 Finished examples/compilation/x64/proofs                       4m16s   2GB
Apr 01 06:37:36 Starting examples/compilation/ag32
Apr 01 07:23:30 Finished examples/compilation/ag32                            45m53s   3GB
Apr 01 07:23:30 Starting examples/compilation/ag32/proofs
Apr 01 07:25:30 Finished examples/compilation/ag32/proofs                      1m59s   1GB
Apr 01 07:25:30 Starting examples/cost
Apr 01 08:47:02 Finished examples/cost                                      1h21m31s   2GB
Apr 01 08:47:02 Starting examples/lpr_checker
Apr 01 08:48:35 Finished examples/lpr_checker                                  1m32s 243MB
Apr 01 08:48:35 Starting examples/lpr_checker/array Apr 01 08:48:35 1748s