Job 1199

CakeML:cc300b057d3c4870d8abe70a8129375fa3ac9e55
  Merge pull request #732 from CakeML/fix_lem_top [Mar 03 14:11:14]
HOL:72f6abae3df1a87d5c1b26e309f5d2a379929e63
  Fix off-by-one error in RISC-V DecodeRVC [Mar 01 19:20:54]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Mar 03 14:30:35 Claimed job
Mar 03 14:30:42 Building HOL
Mar 03 14:43:15 Starting developers
Mar 03 14:43:19 Finished developers                                               4s 106MB
Mar 03 14:43:19 Starting developers/bin
Mar 03 14:43:27 Finished developers/bin                                           7s   1GB
Mar 03 14:43:27 Starting semantics/ffi
Mar 03 14:43:37 Finished semantics/ffi                                           10s 225MB
Mar 03 14:43:38 Starting semantics
Mar 03 14:45:09 Finished semantics                                             1m31s   1GB
Mar 03 14:45:09 Starting semantics/proofs
Mar 03 14:48:36 Finished semantics/proofs                                      3m26s 986MB
Mar 03 14:48:36 Starting semantics/alt_semantics
Mar 03 14:48:44 Finished semantics/alt_semantics                                  8s 286MB
Mar 03 14:48:45 Starting semantics/alt_semantics/proofs
Mar 03 14:50:52 Finished semantics/alt_semantics/proofs                        2m07s 781MB
Mar 03 14:50:53 Starting basis/pure
Mar 03 14:53:55 Finished basis/pure                                            3m02s 777MB
Mar 03 14:53:55 Starting translator
Mar 03 14:56:32 Finished translator                                            2m36s   1GB
Mar 03 14:56:32 Starting compiler/parsing
Mar 03 14:57:42 Finished compiler/parsing                                      1m09s   2GB
Mar 03 14:57:42 Starting characteristic
Mar 03 15:03:39 Finished characteristic                                        5m56s   1GB
Mar 03 15:03:39 Starting translator/monadic
Mar 03 15:05:16 Finished translator/monadic                                    1m36s   1GB
Mar 03 15:05:16 Starting basis
Mar 03 15:38:40 Finished basis                                                33m23s  12GB
Mar 03 15:38:40 Starting compiler/inference
Mar 03 15:39:49 Finished compiler/inference                                    1m09s   1GB
Mar 03 15:39:50 Starting compiler/backend/reg_alloc
Mar 03 15:40:52 Finished compiler/backend/reg_alloc                            1m02s   1GB
Mar 03 15:40:52 Starting compiler/backend/gc
Mar 03 15:44:21 Finished compiler/backend/gc                                   3m28s   2GB
Mar 03 15:44:21 Starting compiler/backend
Mar 03 15:48:55 Finished compiler/backend                                      4m34s   3GB
Mar 03 15:48:55 Starting compiler/encoders/asm
Mar 03 15:49:18 Finished compiler/encoders/asm                                   21s 686MB
Mar 03 15:49:18 Starting compiler/encoders/x64
Mar 03 15:50:16 Finished compiler/encoders/x64                                   57s 991MB
Mar 03 15:50:16 Starting compiler/encoders/arm7
Mar 03 15:52:10 Finished compiler/encoders/arm7                                1m54s   1GB
Mar 03 15:52:10 Starting compiler/encoders/arm8
Mar 03 15:52:45 Finished compiler/encoders/arm8                                  34s 596MB
Mar 03 15:52:45 Starting compiler/encoders/mips
Mar 03 15:53:56 Finished compiler/encoders/mips                                1m10s   1GB
Mar 03 15:53:56 Starting compiler/encoders/riscv
Mar 03 15:55:23 Finished compiler/encoders/riscv                               1m26s   1GB
Mar 03 15:55:23 Starting compiler/encoders/ag32
Mar 03 15:55:42 Finished compiler/encoders/ag32                                  18s 706MB
Mar 03 15:55:42 Starting compiler/backend/x64
Mar 03 15:56:01 Finished compiler/backend/x64                                    18s   1GB
Mar 03 15:56:01 Starting compiler/backend/arm7
Mar 03 15:56:21 Finished compiler/backend/arm7                                   20s   1GB
Mar 03 15:56:21 Starting compiler/backend/arm8
Mar 03 15:56:41 Finished compiler/backend/arm8                                   18s   1GB
Mar 03 15:56:41 Starting compiler/backend/mips
Mar 03 15:56:58 Finished compiler/backend/mips                                   17s 867MB
Mar 03 15:56:58 Starting compiler/backend/riscv
Mar 03 15:57:17 Finished compiler/backend/riscv                                  19s   1GB
Mar 03 15:57:18 Starting compiler/backend/ag32
Mar 03 15:58:28 Finished compiler/backend/ag32                                 1m10s   1GB
Mar 03 15:58:28 Starting compiler/parsing/proofs
Mar 03 16:04:19 Finished compiler/parsing/proofs                               5m50s   1GB
Mar 03 16:04:19 Starting compiler/inference/proofs
Mar 03 16:06:52 Finished compiler/inference/proofs                             2m31s   1GB
Mar 03 16:06:52 Starting compiler/backend/semantics
Mar 03 16:37:22 Finished compiler/backend/semantics                           30m30s   2GB
Mar 03 16:37:22 Starting compiler/backend/reg_alloc/proofs
Mar 03 16:41:03 Finished compiler/backend/reg_alloc/proofs                     3m39s 966MB
Mar 03 16:41:04 Starting compiler/backend/proofs
Mar 03 17:47:54 Finished compiler/backend/proofs                            1h06m49s  15GB
Mar 03 17:47:54 Starting compiler/encoders/x64/proofs
Mar 03 17:57:37 Finished compiler/encoders/x64/proofs                          9m42s   4GB
Mar 03 17:57:37 Starting compiler/encoders/arm7/proofs
Mar 03 18:10:44 Finished compiler/encoders/arm7/proofs                        13m06s   4GB
Mar 03 18:10:45 Starting compiler/encoders/arm8/proofs
Mar 03 18:17:26 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Mar 03 18:17:26 Starting compiler/encoders/mips/proofs
Mar 03 18:27:32 Finished compiler/encoders/mips/proofs                        10m05s   2GB
Mar 03 18:27:32 Starting compiler/encoders/riscv/proofs
Mar 03 18:36:26 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Mar 03 18:36:26 Starting compiler/encoders/ag32/proofs
Mar 03 18:39:06 Finished compiler/encoders/ag32/proofs                         2m40s 733MB
Mar 03 18:39:07 Starting compiler/backend/x64/proofs
Mar 03 18:39:27 Finished compiler/backend/x64/proofs                             20s   1GB
Mar 03 18:39:27 Starting compiler/backend/arm7/proofs
Mar 03 18:39:48 Finished compiler/backend/arm7/proofs                            20s   1GB
Mar 03 18:39:49 Starting compiler/backend/arm8/proofs
Mar 03 18:40:08 Finished compiler/backend/arm8/proofs                            19s 833MB
Mar 03 18:40:08 Starting compiler/backend/mips/proofs
Mar 03 18:40:29 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 03 18:40:29 Starting compiler/backend/riscv/proofs
Mar 03 18:40:50 Finished compiler/backend/riscv/proofs                           20s   1GB
Mar 03 18:40:50 Starting compiler/backend/ag32/proofs
Mar 03 18:53:58 Finished compiler/backend/ag32/proofs                         13m07s   2GB
Mar 03 18:53:58 Starting compiler/proofs
Mar 03 18:55:44 Finished compiler/proofs                                       1m45s   3GB
Mar 03 18:55:44 Starting candle/set-theory
Mar 03 18:56:12 Finished candle/set-theory                                       27s 661MB
Mar 03 18:56:12 Starting candle/syntax-lib
Mar 03 18:56:23 Finished candle/syntax-lib                                       10s 648MB
Mar 03 18:56:23 Starting candle/standard/syntax
Mar 03 18:58:13 Finished candle/standard/syntax                                1m49s   1GB
Mar 03 18:58:13 Starting candle/standard/semantics
Mar 03 18:59:57 Finished candle/standard/semantics                             1m44s   1GB
Mar 03 18:59:58 Starting candle/standard/monadic
Mar 03 19:01:40 Finished candle/standard/monadic                               1m42s   1GB
Mar 03 19:01:41 Starting candle/standard/ml_kernel
Mar 03 19:07:14 Finished candle/standard/ml_kernel                             5m33s   4GB
Mar 03 19:07:15 Starting candle/standard/opentheory
Mar 03 19:16:40 Finished candle/standard/opentheory                            9m25s   4GB
Mar 03 19:16:40 Starting candle/standard/opentheory/compilation
Mar 03 19:48:10 Finished candle/standard/opentheory/compilation               31m29s  20GB
Mar 03 19:48:10 Starting candle/standard/opentheory/compilation/proofs
Mar 03 19:48:47 Finished candle/standard/opentheory/compilation/proofs           36s   2GB
Mar 03 19:48:47 Starting candle/overloading/syntax
Mar 03 19:51:53 Finished candle/overloading/syntax                             3m06s   1GB
Mar 03 19:51:54 Starting candle/overloading/semantics
Mar 03 19:58:59 Finished candle/overloading/semantics                          7m04s   2GB
Mar 03 19:58:59 Starting characteristic/examples
Mar 03 20:00:17 Finished characteristic/examples                               1m17s   2GB
Mar 03 20:00:17 Starting tutorial/solutions
Mar 03 20:14:38 Finished tutorial/solutions                                   14m20s  10GB
Mar 03 20:14:38 Starting translator/monadic/examples
Mar 03 20:17:39 Finished translator/monadic/examples                           3m00s   3GB
Mar 03 20:17:39 Starting examples
Mar 03 20:26:03 Finished examples                                              8m23s   3GB
Mar 03 20:26:03 Starting examples/compilation/x64
Mar 03 22:42:47 Finished examples/compilation/x64                           2h16m43s  11GB
Mar 03 22:42:47 Starting examples/compilation/x64/proofs
Mar 03 22:44:21 Finished examples/compilation/x64/proofs                       1m34s   2GB
Mar 03 22:44:22 Starting examples/compilation/ag32
Mar 03 23:15:16 Finished examples/compilation/ag32                            30m53s   6GB
Mar 03 23:15:16 Starting examples/compilation/ag32/proofs
Mar 03 23:15:58 Finished examples/compilation/ag32/proofs                        42s   2GB
Mar 03 23:15:58 Starting examples/cost
Mar 03 23:59:28 Finished examples/cost                                        43m28s   5GB
Mar 03 23:59:28 Starting examples/lpr_checker
Mar 04 00:03:07 Finished examples/lpr_checker                                  3m38s   3GB
Mar 04 00:03:07 Starting examples/lpr_checker/compilation
Mar 04 00:20:01 Finished examples/lpr_checker/compilation                     16m53s  13GB
Mar 04 00:20:01 Starting examples/lpr_checker/compilation/proofs
Mar 04 00:20:37 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Mar 04 00:20:38 Starting examples/lpr_checker/array
Mar 04 00:28:43 Finished examples/lpr_checker/array                            8m05s   3GB
Mar 04 00:28:43 Starting examples/lpr_checker/array/compilation
Mar 04 00:44:19 Finished examples/lpr_checker/array/compilation               15m35s   7GB
Mar 04 00:44:19 Starting examples/lpr_checker/array/compilation/proofs
Mar 04 00:45:04 Finished examples/lpr_checker/array/compilation/proofs           43s   3GB
Mar 04 00:45:04 Starting translator/okasaki-examples
Mar 04 00:49:28 Finished translator/okasaki-examples                           4m24s   1GB
Mar 04 00:49:28 Starting translator/other-examples
Mar 04 00:51:29 Finished translator/other-examples                             2m00s   1GB
Mar 04 00:51:29 Starting compiler/parsing/tests
Mar 04 00:51:55 Finished compiler/parsing/tests                                  26s 545MB
Mar 04 00:51:55 Starting compiler/inference/tests
Mar 04 00:56:30 Finished compiler/inference/tests                              4m34s   5GB
Mar 04 00:56:30 Starting compiler/bootstrap/translation
Mar 04 03:40:54 Finished compiler/bootstrap/translation                     2h44m23s  38GB
Mar 04 03:40:54 Starting unverified/sexpr-bootstrap/x64/64
Mar 04 03:54:46 Finished unverified/sexpr-bootstrap/x64/64                    13m50s   5GB
Mar 04 03:54:46 Starting unverified/sexpr-bootstrap/x64/32
Mar 04 04:04:40 Finished unverified/sexpr-bootstrap/x64/32                     9m52s   7GB
Mar 04 04:04:40 Starting compiler/benchmarks
Mar 04 04:04:42 Finished compiler/benchmarks                                      1s  27MB
Mar 04 04:04:42 Starting compiler/bootstrap/compilation/x64/64
Mar 04 19:01:31 Finished compiler/bootstrap/compilation/x64/64             14h56m47s  64GB
Mar 04 19:01:31 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 04 19:04:48 Finished compiler/bootstrap/compilation/x64/64/proofs          3m16s  13GB
Mar 04 19:04:48 Starting compiler/bootstrap/compilation/x64/32
Mar 05 08:37:47 Finished compiler/bootstrap/compilation/x64/32             13h32m57s  64GB
Mar 05 08:37:47 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 05 08:40:52 Finished compiler/bootstrap/compilation/x64/32/proofs          3m04s  13GB
Mar 05 08:40:52 Starting compiler/bootstrap/compilation/ag32/32
Mar 05 23:33:17 Finished compiler/bootstrap/compilation/ag32/32            14h52m24s  64GB
Mar 05 23:33:17 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 05 23:59:26 Finished compiler/bootstrap/compilation/ag32/32/proofs        26m09s  29GB
Mar 05 23:59:26 SUCCESS