Job 1338

CakeML:85ff1d236459082c90c94fdde129f366318304e5
  riscv: Simplify/optimize FFI jumps [Sep 12 17:49:47]
#752 (rv_fixes)
Merging into:cbf24c13a47d5075fd44eed3a36178daaa7c0142
  Merge pull request #747 from CakeML/lpr_opt [Sep 13 12:05:55]
HOL:b7114ef478633386784cfe9274b99abcdde3c5d5
  fix proofs of WF_uR [Sep 14 01:07:44]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Sep 15 23:30:01 Claimed job
Sep 15 23:30:10 Building HOL
Sep 15 23:45:39 Starting developers
Sep 15 23:45:44 Finished developers                                               4s 117MB
Sep 15 23:45:44 Starting developers/bin
Sep 15 23:45:51 Finished developers/bin                                           7s   1GB
Sep 15 23:45:51 Starting semantics/ffi
Sep 15 23:46:03 Finished semantics/ffi                                           11s 238MB
Sep 15 23:46:03 Starting semantics
Sep 15 23:47:40 Finished semantics                                             1m36s 948MB
Sep 15 23:47:41 Starting semantics/proofs
Sep 15 23:51:15 Finished semantics/proofs                                      3m33s 922MB
Sep 15 23:51:15 Starting semantics/alt_semantics
Sep 15 23:51:24 Finished semantics/alt_semantics                                  9s 292MB
Sep 15 23:51:25 Starting semantics/alt_semantics/proofs
Sep 15 23:53:40 Finished semantics/alt_semantics/proofs                        2m15s 811MB
Sep 15 23:53:41 Starting basis/pure
Sep 15 23:56:48 Finished basis/pure                                            3m07s 870MB
Sep 15 23:56:48 Starting translator
Sep 15 23:59:36 Finished translator                                            2m47s   1GB
Sep 15 23:59:36 Starting compiler/parsing
Sep 16 00:00:49 Finished compiler/parsing                                      1m12s   2GB
Sep 16 00:00:50 Starting characteristic
Sep 16 00:07:04 Finished characteristic                                        6m14s   1GB
Sep 16 00:07:04 Starting translator/monadic
Sep 16 00:08:45 Finished translator/monadic                                    1m40s   1GB
Sep 16 00:08:46 Starting basis
Sep 16 00:44:52 Finished basis                                                36m06s  11GB
Sep 16 00:44:52 Starting compiler/inference
Sep 16 00:46:06 Finished compiler/inference                                    1m13s   1GB
Sep 16 00:46:08 Starting compiler/backend/reg_alloc
Sep 16 00:47:14 Finished compiler/backend/reg_alloc                            1m06s   1GB
Sep 16 00:47:14 Starting compiler/backend/gc
Sep 16 00:51:00 Finished compiler/backend/gc                                   3m45s   2GB
Sep 16 00:51:00 Starting compiler/backend
Sep 16 00:55:47 Finished compiler/backend                                      4m46s   3GB
Sep 16 00:55:47 Starting compiler/encoders/asm
Sep 16 00:56:11 Finished compiler/encoders/asm                                   23s 818MB
Sep 16 00:56:11 Starting compiler/encoders/x64
Sep 16 00:57:15 Finished compiler/encoders/x64                                 1m02s   1GB
Sep 16 00:57:15 Starting compiler/encoders/arm7
Sep 16 00:59:16 Finished compiler/encoders/arm7                                2m00s   1GB
Sep 16 00:59:16 Starting compiler/encoders/arm8
Sep 16 00:59:54 Finished compiler/encoders/arm8                                  38s 933MB
Sep 16 00:59:54 Starting compiler/encoders/mips
Sep 16 01:01:17 Finished compiler/encoders/mips                                1m22s 890MB
Sep 16 01:01:17 Starting compiler/encoders/riscv
Sep 16 01:02:57 Finished compiler/encoders/riscv                               1m39s   1GB
Sep 16 01:02:57 Starting compiler/encoders/ag32
Sep 16 01:03:16 Finished compiler/encoders/ag32                                  18s 750MB
Sep 16 01:03:16 Starting compiler/backend/x64
Sep 16 01:03:35 Finished compiler/backend/x64                                    19s   1GB
Sep 16 01:03:35 Starting compiler/backend/arm7
Sep 16 01:03:57 Finished compiler/backend/arm7                                   20s   1GB
Sep 16 01:03:57 Starting compiler/backend/arm8
Sep 16 01:04:16 Finished compiler/backend/arm8                                   19s   1GB
Sep 16 01:04:16 Starting compiler/backend/mips
Sep 16 01:04:37 Finished compiler/backend/mips                                   19s   1GB
Sep 16 01:04:37 Starting compiler/backend/riscv
Sep 16 01:04:57 Finished compiler/backend/riscv                                  19s   1GB
Sep 16 01:04:57 Starting compiler/backend/ag32
Sep 16 01:06:12 Finished compiler/backend/ag32                                 1m14s   1GB
Sep 16 01:06:12 Starting compiler/parsing/proofs
Sep 16 01:12:04 Finished compiler/parsing/proofs                               5m51s   1GB
Sep 16 01:12:04 Starting compiler/inference/proofs
Sep 16 01:14:44 Finished compiler/inference/proofs                             2m39s   1GB
Sep 16 01:14:44 Starting compiler/backend/semantics
Sep 16 01:45:54 Finished compiler/backend/semantics                           31m09s   2GB
Sep 16 01:45:54 Starting compiler/backend/reg_alloc/proofs
Sep 16 01:49:38 Finished compiler/backend/reg_alloc/proofs                     3m44s 998MB
Sep 16 01:49:38 Starting compiler/backend/proofs
Sep 16 02:47:14 Finished compiler/backend/proofs                              57m35s  16GB
Sep 16 02:47:14 Starting compiler/encoders/x64/proofs
Sep 16 02:57:37 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Sep 16 02:57:37 Starting compiler/encoders/arm7/proofs
Sep 16 03:11:33 Finished compiler/encoders/arm7/proofs                        13m55s   6GB
Sep 16 03:11:33 Starting compiler/encoders/arm8/proofs
Sep 16 03:18:31 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Sep 16 03:18:32 Starting compiler/encoders/mips/proofs
Sep 16 03:29:23 Finished compiler/encoders/mips/proofs                        10m51s   2GB
Sep 16 03:29:24 Starting compiler/encoders/riscv/proofs
Sep 16 03:38:53 Finished compiler/encoders/riscv/proofs                        9m29s   1GB
Sep 16 03:38:53 Starting compiler/encoders/ag32/proofs
Sep 16 03:41:39 Finished compiler/encoders/ag32/proofs                         2m46s   1GB
Sep 16 03:41:40 Starting compiler/backend/x64/proofs
Sep 16 03:42:00 Finished compiler/backend/x64/proofs                             20s   1GB
Sep 16 03:42:00 Starting compiler/backend/arm7/proofs
Sep 16 03:42:23 Finished compiler/backend/arm7/proofs                            22s   1GB
Sep 16 03:42:23 Starting compiler/backend/arm8/proofs
Sep 16 03:42:43 Finished compiler/backend/arm8/proofs                            19s   1GB
Sep 16 03:42:43 Starting compiler/backend/mips/proofs
Sep 16 03:43:05 Finished compiler/backend/mips/proofs                            21s   1GB
Sep 16 03:43:05 Starting compiler/backend/riscv/proofs
Sep 16 03:43:26 Finished compiler/backend/riscv/proofs                           21s   1GB
Sep 16 03:43:27 Starting compiler/backend/ag32/proofs
Sep 16 03:57:21 Finished compiler/backend/ag32/proofs                         13m53s   1GB
Sep 16 03:57:21 Starting compiler/proofs
Sep 16 03:59:14 Finished compiler/proofs                                       1m52s   4GB
Sep 16 03:59:14 Starting candle/set-theory
Sep 16 03:59:44 Finished candle/set-theory                                       29s 717MB
Sep 16 03:59:44 Starting candle/syntax-lib
Sep 16 03:59:55 Finished candle/syntax-lib                                       11s 696MB
Sep 16 03:59:55 Starting candle/standard/syntax
Sep 16 04:01:53 Finished candle/standard/syntax                                1m57s 920MB
Sep 16 04:01:53 Starting candle/standard/semantics
Sep 16 04:03:41 Finished candle/standard/semantics                             1m48s   1GB
Sep 16 04:03:42 Starting candle/standard/monadic
Sep 16 04:05:31 Finished candle/standard/monadic                               1m49s   1GB
Sep 16 04:05:31 Starting candle/standard/ml_kernel
Sep 16 04:11:20 Finished candle/standard/ml_kernel                             5m48s   4GB
Sep 16 04:11:20 Starting candle/overloading/syntax
Sep 16 04:14:39 Finished candle/overloading/syntax                             3m18s   1GB
Sep 16 04:14:39 Starting candle/overloading/semantics
Sep 16 04:27:48 Finished candle/overloading/semantics                         13m09s   4GB
Sep 16 04:27:48 Starting characteristic/examples
Sep 16 04:29:08 Finished characteristic/examples                               1m18s   2GB
Sep 16 04:29:08 Starting tutorial/solutions
Sep 16 04:43:55 Finished tutorial/solutions                                   14m46s   7GB
Sep 16 04:43:55 Starting translator/monadic/examples
Sep 16 04:47:13 Finished translator/monadic/examples                           3m18s   2GB
Sep 16 04:47:14 Starting examples
Sep 16 04:56:01 Finished examples                                              8m47s   3GB
Sep 16 04:56:01 Starting examples/compilation/x64
Sep 16 07:12:55 Finished examples/compilation/x64                           2h16m52s  17GB
Sep 16 07:12:55 Starting examples/compilation/x64/proofs
Sep 16 07:14:30 Finished examples/compilation/x64/proofs                       1m34s   2GB
Sep 16 07:14:30 Starting examples/compilation/ag32
Sep 16 07:46:23 Finished examples/compilation/ag32                            31m53s   5GB
Sep 16 07:46:23 Starting examples/compilation/ag32/proofs
Sep 16 07:47:07 Finished examples/compilation/ag32/proofs                        43s   2GB
Sep 16 07:47:07 Starting examples/cost
Sep 16 08:35:31 Finished examples/cost                                        48m23s   6GB
Sep 16 08:35:31 Starting examples/lpr_checker
Sep 16 08:39:29 Finished examples/lpr_checker                                  3m58s   3GB
Sep 16 08:39:29 Starting examples/lpr_checker/compilation
Sep 16 08:56:59 Finished examples/lpr_checker/compilation                     17m29s  13GB
Sep 16 08:56:59 Starting examples/lpr_checker/compilation/proofs
Sep 16 08:57:36 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Sep 16 08:57:36 Starting examples/lpr_checker/array Sep 16 08:57:36 1626s