Job 379

CakeML:5039f563acf2301d3c2c1ce53e28d84d9e9aa77d
  Prove a correctness result for a cmlPtreeConversion function [Jul 25 01:26:38]
HOL:b152d73a25322bb37746c431e3cdc16f0fd96e23
  Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL [Jul 24 17:40:58]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jul 25 03:30:01 Claimed job
Jul 25 03:30:11 Building HOL
Jul 25 03:42:44 Starting developers/bin
Jul 25 03:42:54 Finished developers/bin                                           8s 224MB
Jul 25 03:42:56 Starting semantics/ffi
Jul 25 03:43:59 Finished semantics/ffi                                         1m01s 406MB
Jul 25 03:44:01 Starting semantics
Jul 25 03:46:26 Finished semantics                                             2m22s   1GB
Jul 25 03:46:28 Starting semantics/proofs
Jul 25 03:49:45 Finished semantics/proofs                                      3m14s   1GB
Jul 25 03:49:47 Starting basis/pure
Jul 25 03:55:34 Finished basis/pure                                            5m45s 849MB
Jul 25 03:55:36 Starting translator
Jul 25 04:02:12 Finished translator                                            6m34s   1GB
Jul 25 04:02:14 Starting compiler/parsing
Jul 25 04:04:22 Finished compiler/parsing                                      2m06s   2GB
Jul 25 04:04:24 Starting characteristic
Jul 25 04:08:50 Finished characteristic                                        4m23s   1GB
Jul 25 04:08:52 Starting basis
Jul 25 04:37:38 Finished basis                                                28m44s   2GB
Jul 25 04:37:40 Starting translator/monadic
Jul 25 04:37:45 Finished translator/monadic                                       2s  13MB
Jul 25 04:37:46 Starting compiler/inference
Jul 25 04:40:27 Finished compiler/inference                                    2m39s   1GB
Jul 25 04:40:29 Starting compiler/backend/reg_alloc
Jul 25 04:41:27 Finished compiler/backend/reg_alloc                              55s   1GB
Jul 25 04:41:29 Starting compiler/backend/gc
Jul 25 04:56:16 Finished compiler/backend/gc                                  14m45s   3GB
Jul 25 04:56:18 Starting compiler/backend
Jul 25 04:56:23 Finished compiler/backend                                         3s  32MB
Jul 25 04:56:25 Starting compiler/encoders/asm
Jul 25 04:56:28 Finished compiler/encoders/asm                                    0s  11MB
Jul 25 04:56:30 Starting compiler/encoders/x64
Jul 25 04:57:58 Finished compiler/encoders/x64                                 1m25s 507MB
Jul 25 04:58:00 Starting compiler/encoders/arm6
Jul 25 05:00:57 Finished compiler/encoders/arm6                                2m55s   1GB
Jul 25 05:00:59 Starting compiler/encoders/arm8
Jul 25 05:01:45 Finished compiler/encoders/arm8                                  43s 400MB
Jul 25 05:01:47 Starting compiler/encoders/mips
Jul 25 05:03:26 Finished compiler/encoders/mips                                1m37s   1GB
Jul 25 05:03:28 Starting compiler/encoders/riscv
Jul 25 05:05:04 Finished compiler/encoders/riscv                               1m33s 647MB
Jul 25 05:05:06 Starting compiler/backend/x64
Jul 25 05:05:37 Finished compiler/backend/x64                                    29s 839MB
Jul 25 05:05:39 Starting compiler/backend/arm6
Jul 25 05:06:16 Finished compiler/backend/arm6                                   35s   1GB
Jul 25 05:06:18 Starting compiler/backend/arm8
Jul 25 05:06:53 Finished compiler/backend/arm8                                   32s   1GB
Jul 25 05:06:55 Starting compiler/backend/mips
Jul 25 05:07:27 Finished compiler/backend/mips                                   30s 842MB
Jul 25 05:07:29 Starting compiler/backend/riscv
Jul 25 05:08:04 Finished compiler/backend/riscv                                  32s   1GB
Jul 25 05:08:06 Starting compiler/parsing/proofs
Jul 25 05:12:04 Finished compiler/parsing/proofs                               3m56s 769MB
Jul 25 05:12:06 Starting compiler/inference/proofs
Jul 25 05:16:05 Finished compiler/inference/proofs                             3m56s   1GB
Jul 25 05:16:07 Starting compiler/backend/semantics
Jul 25 05:30:13 Finished compiler/backend/semantics                           14m04s   2GB
Jul 25 05:30:15 Starting compiler/backend/reg_alloc/proofs
Jul 25 05:31:39 Finished compiler/backend/reg_alloc/proofs                     1m21s 536MB
Jul 25 05:31:41 Starting compiler/backend/proofs
Jul 25 06:27:09 Finished compiler/backend/proofs                              55m26s   4GB
Jul 25 06:27:11 Starting compiler/encoders/x64/proofs
Jul 25 06:38:50 Finished compiler/encoders/x64/proofs                         11m36s   1GB
Jul 25 06:38:53 Starting compiler/encoders/arm6/proofs
Jul 25 06:51:05 Finished compiler/encoders/arm6/proofs                        12m10s   2GB
Jul 25 06:51:07 Starting compiler/encoders/arm8/proofs
Jul 25 06:59:29 Finished compiler/encoders/arm8/proofs                         8m20s   1GB
Jul 25 06:59:31 Starting compiler/encoders/mips/proofs
Jul 25 07:11:16 Finished compiler/encoders/mips/proofs                        11m42s   1GB
Jul 25 07:11:18 Starting compiler/encoders/riscv/proofs
Jul 25 07:23:55 Finished compiler/encoders/riscv/proofs                       12m34s   1GB
Jul 25 07:23:57 Starting compiler/backend/x64/proofs
Jul 25 07:24:35 Finished compiler/backend/x64/proofs                             35s   1GB
Jul 25 07:24:37 Starting compiler/backend/arm6/proofs
Jul 25 07:25:18 Finished compiler/backend/arm6/proofs                            38s   1GB
Jul 25 07:25:20 Starting compiler/backend/arm8/proofs
Jul 25 07:25:56 Finished compiler/backend/arm8/proofs                            34s   1GB
Jul 25 07:25:58 Starting compiler/backend/mips/proofs
Jul 25 07:26:37 Finished compiler/backend/mips/proofs                            36s   1GB
Jul 25 07:26:39 Starting compiler/backend/riscv/proofs
Jul 25 07:27:16 Finished compiler/backend/riscv/proofs                           35s   1GB
Jul 25 07:27:18 Starting compiler/proofs
Jul 25 07:29:41 Finished compiler/proofs                                       2m20s   2GB
Jul 25 07:29:43 Starting candle/set-theory
Jul 25 07:30:41 Finished candle/set-theory                                       56s 577MB
Jul 25 07:30:43 Starting candle/syntax-lib
Jul 25 07:31:01 Finished candle/syntax-lib                                       16s 451MB
Jul 25 07:31:03 Starting candle/standard/syntax
Jul 25 07:33:47 Finished candle/standard/syntax                                2m41s 725MB
Jul 25 07:33:49 Starting candle/standard/semantics
Jul 25 07:36:05 Finished candle/standard/semantics                             2m13s 933MB
Jul 25 07:36:07 Starting candle/standard/monadic
Jul 25 07:38:32 Finished candle/standard/monadic                               2m23s   1GB
Jul 25 07:38:34 Starting candle/standard/ml_kernel
Jul 25 07:48:44 Finished candle/standard/ml_kernel                            10m08s   2GB
Jul 25 07:48:46 Starting candle/standard/opentheory
Jul 25 07:49:12 Finished candle/standard/opentheory                              23s 623MB
Jul 25 07:49:14 Starting characteristic/examples
Jul 25 07:51:39 Finished characteristic/examples                               2m23s   1GB
Jul 25 07:51:41 Starting tutorial/solutions
Jul 25 08:26:23 Finished tutorial/solutions                                   34m39s  14GB
Jul 25 08:26:24 Starting translator/monadic/examples
Jul 25 08:29:23 Finished translator/monadic/examples                           2m56s   2GB
Jul 25 08:29:25 Starting examples
Jul 25 08:37:32 Finished examples                                              8m05s   2GB
Jul 25 08:37:34 Starting examples/compilation
Jul 25 14:19:54 Finished examples/compilation                               5h42m17s  17GB
Jul 25 14:19:56 Starting examples/compilation/proofs
Jul 25 14:25:15 Finished examples/compilation/proofs                           5m17s   4GB
Jul 25 14:25:17 Starting compiler/benchmarks
Jul 25 14:25:19 Finished compiler/benchmarks                                      0s   4MB
Jul 25 14:25:21 Starting translator/okasaki-examples
Jul 25 14:31:55 Finished translator/okasaki-examples                           6m31s   1GB
Jul 25 14:31:57 Starting translator/other-examples
Jul 25 14:38:44 Finished translator/other-examples                             6m45s 878MB
Jul 25 14:38:46 Starting compiler/parsing/tests
Jul 25 14:39:28 Finished compiler/parsing/tests                                  39s 388MB
Jul 25 14:39:30 Starting compiler/bootstrap/translation
Jul 25 22:46:27 Finished compiler/bootstrap/translation                     8h06m54s  49GB
Jul 25 22:46:29 Starting unverified/sexpr-bootstrap/x64/64
Jul 25 22:57:35 Finished unverified/sexpr-bootstrap/x64/64                    10m58s  15GB
Jul 25 22:57:37 Starting unverified/sexpr-bootstrap/x64/32
Jul 25 23:06:38 Finished unverified/sexpr-bootstrap/x64/32                     8m54s  12GB
Jul 25 23:06:40 Starting compiler/bootstrap/compilation/x64/64
Jul 27 02:35:12 Finished compiler/bootstrap/compilation/x64/64             27h28m25s  94GB
Jul 27 02:35:14 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 27 02:41:35 Finished compiler/bootstrap/compilation/x64/64/proofs          6m18s  26GB
Jul 27 02:41:37 Starting compiler/bootstrap/compilation/x64/32
Jul 28 03:47:00 Finished compiler/bootstrap/compilation/x64/32             25h05m15s  89GB
Jul 28 03:47:02 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 28 03:50:50 Finished compiler/bootstrap/compilation/x64/32/proofs          3m45s  28GB
Jul 28 03:50:52 SUCCESS