Job 45

CakeML:33fd129284ed4a2524d4797dfb2af322073dd45f
  Fix another proof [Nov 26 00:08:04]
HOL:5a30cd803ef0c285a4edf698778113ac21ce5509
  Prove more about RATN & RATD; define RAT_SGN; prove results about it [Nov 24 04:53:00]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux
Artefacts:cake-riscv.tar.gz
cake-x64.tar.gz

Nov 26 00:33:28 Claimed job
Nov 26 00:33:35 Building HOL
Nov 26 00:33:47 Starting semantics/ffi
Nov 26 00:34:08 Finished semantics/ffi                                           19s 256MB
Nov 26 00:34:10 Starting semantics
Nov 26 00:36:25 Finished semantics                                             2m13s   1GB
Nov 26 00:36:27 Starting semantics/proofs
Nov 26 00:39:55 Finished semantics/proofs                                      3m26s   1GB
Nov 26 00:39:57 Starting basis/pure
Nov 26 00:41:06 Finished basis/pure                                            1m06s 668MB
Nov 26 00:41:08 Starting translator
Nov 26 00:48:22 Finished translator                                            7m11s 960MB
Nov 26 00:48:24 Starting compiler/parsing
Nov 26 00:50:48 Finished compiler/parsing                                      2m22s   1GB
Nov 26 00:50:50 Starting characteristic
Nov 26 00:55:32 Finished characteristic                                        4m40s   1GB
Nov 26 00:55:34 Starting basis
Nov 26 01:23:00 Finished basis                                                27m23s   2GB
Nov 26 01:23:02 Starting translator/monadic
Nov 26 01:26:40 Finished translator/monadic                                    3m36s   1GB
Nov 26 01:26:42 Starting compiler/inference
Nov 26 01:29:01 Finished compiler/inference                                    2m16s   1GB
Nov 26 01:29:03 Starting compiler/backend/reg_alloc
Nov 26 01:29:53 Finished compiler/backend/reg_alloc                              48s 829MB
Nov 26 01:29:55 Starting compiler/backend/gc
Nov 26 01:44:14 Finished compiler/backend/gc                                  14m17s   2GB
Nov 26 01:44:16 Starting compiler/backend
Nov 26 01:44:19 Finished compiler/backend                                         1s  18MB
Nov 26 01:44:21 Starting compiler/encoders/asm
Nov 26 01:44:24 Finished compiler/encoders/asm                                    0s  11MB
Nov 26 01:44:26 Starting compiler/encoders/x64
Nov 26 01:44:54 Finished compiler/encoders/x64                                   26s 416MB
Nov 26 01:44:56 Starting compiler/encoders/arm6
Nov 26 01:46:21 Finished compiler/encoders/arm6                                1m23s 464MB
Nov 26 01:46:23 Starting compiler/encoders/arm8
Nov 26 01:46:39 Finished compiler/encoders/arm8                                  14s 435MB
Nov 26 01:46:41 Starting compiler/encoders/mips
Nov 26 01:47:03 Finished compiler/encoders/mips                                  19s 561MB
Nov 26 01:47:05 Starting compiler/encoders/riscv
Nov 26 01:47:23 Finished compiler/encoders/riscv                                 15s 422MB
Nov 26 01:47:25 Starting compiler/backend/x64
Nov 26 01:48:09 Finished compiler/backend/x64                                    42s   1GB
Nov 26 01:48:11 Starting compiler/backend/arm6
Nov 26 01:48:57 Finished compiler/backend/arm6                                   44s   1GB
Nov 26 01:48:59 Starting compiler/backend/arm8
Nov 26 01:49:43 Finished compiler/backend/arm8                                   41s   1GB
Nov 26 01:49:45 Starting compiler/backend/mips
Nov 26 01:50:30 Finished compiler/backend/mips                                   43s   1GB
Nov 26 01:50:32 Starting compiler/backend/riscv
Nov 26 01:51:18 Finished compiler/backend/riscv                                  43s   1GB
Nov 26 01:51:20 Starting compiler/parsing/proofs
Nov 26 01:56:11 Finished compiler/parsing/proofs                               4m49s 793MB
Nov 26 01:56:13 Starting compiler/inference/proofs
Nov 26 02:00:37 Finished compiler/inference/proofs                             4m21s   1GB
Nov 26 02:00:39 Starting compiler/backend/semantics
Nov 26 02:19:55 Finished compiler/backend/semantics                           19m14s   4GB
Nov 26 02:19:57 Starting compiler/backend/reg_alloc/proofs
Nov 26 02:21:09 Finished compiler/backend/reg_alloc/proofs                     1m09s 404MB
Nov 26 02:21:11 Starting compiler/backend/proofs
Nov 26 03:33:41 Finished compiler/backend/proofs                            1h12m27s   4GB
Nov 26 03:33:43 Starting compiler/encoders/x64/proofs
Nov 26 03:43:37 Finished compiler/encoders/x64/proofs                          9m51s 989MB
Nov 26 03:43:39 Starting compiler/encoders/arm6/proofs
Nov 26 03:54:40 Finished compiler/encoders/arm6/proofs                        10m59s   1GB
Nov 26 03:54:42 Starting compiler/encoders/arm8/proofs
Nov 26 04:03:34 Finished compiler/encoders/arm8/proofs                         8m49s   1GB
Nov 26 04:03:36 Starting compiler/encoders/mips/proofs
Nov 26 04:15:56 Finished compiler/encoders/mips/proofs                        12m18s   1GB
Nov 26 04:15:58 Starting compiler/encoders/riscv/proofs
Nov 26 04:29:39 Finished compiler/encoders/riscv/proofs                       13m38s 927MB
Nov 26 04:29:41 Starting compiler/backend/x64/proofs
Nov 26 04:30:32 Finished compiler/backend/x64/proofs                             49s   1GB
Nov 26 04:30:34 Starting compiler/backend/arm6/proofs
Nov 26 04:31:34 Finished compiler/backend/arm6/proofs                            57s   1GB
Nov 26 04:31:36 Starting compiler/backend/arm8/proofs
Nov 26 04:32:28 Finished compiler/backend/arm8/proofs                            50s   1GB
Nov 26 04:32:30 Starting compiler/backend/mips/proofs
Nov 26 04:33:26 Finished compiler/backend/mips/proofs                            54s   1GB
Nov 26 04:33:28 Starting compiler/backend/riscv/proofs
Nov 26 04:34:20 Finished compiler/backend/riscv/proofs                           50s   1GB
Nov 26 04:34:22 Starting compiler/proofs
Nov 26 04:36:09 Finished compiler/proofs                                       1m44s   1GB
Nov 26 04:36:11 Starting candle/set-theory
Nov 26 04:37:00 Finished candle/set-theory                                       47s 615MB
Nov 26 04:37:02 Starting candle/syntax-lib
Nov 26 04:37:24 Finished candle/syntax-lib                                       19s 551MB
Nov 26 04:37:26 Starting candle/standard/syntax
Nov 26 04:40:29 Finished candle/standard/syntax                                3m01s 746MB
Nov 26 04:40:31 Starting candle/standard/semantics
Nov 26 04:43:01 Finished candle/standard/semantics                             2m28s 695MB
Nov 26 04:43:03 Starting candle/standard/monadic
Nov 26 04:45:48 Finished candle/standard/monadic                               2m42s 959MB
Nov 26 04:45:50 Starting candle/standard/ml_kernel
Nov 26 04:57:13 Finished candle/standard/ml_kernel                            11m21s   2GB
Nov 26 04:57:15 Starting candle/standard/opentheory
Nov 26 04:57:47 Finished candle/standard/opentheory                              30s 664MB
Nov 26 04:57:49 Starting characteristic/examples
Nov 26 04:59:57 Finished characteristic/examples                               2m05s   1GB
Nov 26 04:59:58 Starting tutorial/solutions
Nov 26 05:31:43 Finished tutorial/solutions                                   31m43s   8GB
Nov 26 05:31:45 Starting examples
Nov 26 05:39:34 Finished examples                                              7m46s   2GB
Nov 26 05:39:36 Starting examples/compilation
Nov 26 10:21:55 Finished examples/compilation                               4h42m16s  14GB
Nov 26 10:21:57 Starting examples/compilation/proofs
Nov 26 10:27:26 Finished examples/compilation/proofs                           5m26s   4GB
Nov 26 10:27:28 Starting compiler/benchmarks
Nov 26 12:13:11 Finished compiler/benchmarks                                1h45m40s  12GB
Nov 26 12:13:13 Starting translator/okasaki-examples
Nov 26 12:20:46 Finished translator/okasaki-examples                           7m31s   1GB
Nov 26 12:20:48 Starting translator/other-examples
Nov 26 12:21:53 Finished translator/other-examples                             1m02s 995MB
Nov 26 12:21:55 Starting compiler/parsing/tests
Nov 26 12:22:35 Finished compiler/parsing/tests                                  38s 401MB
Nov 26 12:22:37 Starting compiler/bootstrap/translation
Nov 26 19:56:40 Finished compiler/bootstrap/translation                     7h34m00s  34GB
Nov 26 19:56:42 Starting compiler/bootstrap/translation/x64
Nov 26 20:15:30 Finished compiler/bootstrap/translation/x64                   18m46s  29GB
Nov 26 20:16:24 Starting compiler/bootstrap/compilation/x64
Nov 27 15:21:32 Finished compiler/bootstrap/compilation/x64                19h05m05s  91GB
Nov 27 15:21:34 Starting compiler/bootstrap/compilation/x64/proofs
Nov 27 15:24:30 Finished compiler/bootstrap/compilation/x64/proofs             2m54s  20GB
Nov 27 15:24:32 Starting compiler/bootstrap/translation/riscv
Nov 27 15:45:33 Finished compiler/bootstrap/translation/riscv                 20m59s  39GB
Nov 27 15:45:35 Starting compiler/bootstrap/compilation/riscv
Nov 28 14:55:59 Finished compiler/bootstrap/compilation/riscv              23h10m21s  92GB
Nov 28 14:56:01 SUCCESS