Job 1048

CakeML:b8b20698feb965c78a1dc6dde4da81ce368ead3a
  Fix a proof broken by minor HOL change [Oct 05 13:27:47]
HOL:c80b32898bc7a3f692c1be84161e569112efdfa9
  Fix ARM_security_properties example for change in 44aabdd82 [Oct 02 12:15:29]
Machine:te1
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Oct 05 13:28:40 Claimed job
Oct 05 13:28:48 Building HOL
Oct 05 13:44:08 Starting developers
Oct 05 13:44:12 Finished developers                                               4s 104MB
Oct 05 13:44:12 Starting developers/bin
Oct 05 13:44:19 Finished developers/bin                                           6s 969MB
Oct 05 13:44:19 Starting semantics/ffi
Oct 05 13:45:17 Finished semantics/ffi                                           57s 584MB
Oct 05 13:45:17 Starting semantics
Oct 05 13:47:35 Finished semantics                                             2m18s   1GB
Oct 05 13:47:35 Starting semantics/proofs
Oct 05 13:52:03 Finished semantics/proofs                                      4m27s   1GB
Oct 05 13:52:03 Starting semantics/alt_semantics
Oct 05 13:52:14 Finished semantics/alt_semantics                                 11s 327MB
Oct 05 13:52:14 Starting semantics/alt_semantics/proofs
Oct 05 13:54:56 Finished semantics/alt_semantics/proofs                        2m42s   1GB
Oct 05 13:54:57 Starting basis/pure
Oct 05 14:00:25 Finished basis/pure                                            5m28s 878MB
Oct 05 14:00:25 Starting translator
Oct 05 14:02:59 Finished translator                                            2m34s   1GB
Oct 05 14:02:59 Starting compiler/parsing
Oct 05 14:04:20 Finished compiler/parsing                                      1m20s   1GB
Oct 05 14:04:20 Starting characteristic
Oct 05 14:12:01 Finished characteristic                                        7m41s   2GB
Oct 05 14:12:01 Starting translator/monadic
Oct 05 14:14:12 Finished translator/monadic                                    2m11s   1GB
Oct 05 14:14:12 Starting basis
Oct 05 14:41:36 Finished basis                                                27m23s   3GB
Oct 05 14:41:36 Starting compiler/inference
Oct 05 14:44:22 Finished compiler/inference                                    2m45s   1GB
Oct 05 14:44:22 Starting compiler/backend/reg_alloc
Oct 05 14:45:42 Finished compiler/backend/reg_alloc                            1m20s   1GB
Oct 05 14:45:42 Starting compiler/backend/gc
Oct 05 14:58:42 Finished compiler/backend/gc                                  13m00s   1GB
Oct 05 14:58:43 Starting compiler/backend
Oct 05 14:58:45 Finished compiler/backend                                         2s  33MB
Oct 05 14:58:45 Starting compiler/encoders/asm
Oct 05 14:58:46 Finished compiler/encoders/asm                                    1s  18MB
Oct 05 14:58:46 Starting compiler/encoders/x64
Oct 05 15:00:17 Finished compiler/encoders/x64                                 1m30s 725MB
Oct 05 15:00:17 Starting compiler/encoders/arm7
Oct 05 15:02:45 Finished compiler/encoders/arm7                                2m28s   1GB
Oct 05 15:02:45 Starting compiler/encoders/arm8
Oct 05 15:03:34 Finished compiler/encoders/arm8                                  48s 576MB
Oct 05 15:03:34 Starting compiler/encoders/mips
Oct 05 15:05:18 Finished compiler/encoders/mips                                1m43s 869MB
Oct 05 15:05:18 Starting compiler/encoders/riscv
Oct 05 15:07:14 Finished compiler/encoders/riscv                               1m56s   1GB
Oct 05 15:07:14 Starting compiler/encoders/ag32
Oct 05 15:07:39 Finished compiler/encoders/ag32                                  24s 800MB
Oct 05 15:07:39 Starting compiler/backend/x64
Oct 05 15:08:03 Finished compiler/backend/x64                                    24s 852MB
Oct 05 15:08:03 Starting compiler/backend/arm7
Oct 05 15:08:32 Finished compiler/backend/arm7                                   28s   1GB
Oct 05 15:08:32 Starting compiler/backend/arm8
Oct 05 15:09:00 Finished compiler/backend/arm8                                   27s   1GB
Oct 05 15:09:00 Starting compiler/backend/mips
Oct 05 15:09:26 Finished compiler/backend/mips                                   25s 941MB
Oct 05 15:09:26 Starting compiler/backend/riscv
Oct 05 15:09:53 Finished compiler/backend/riscv                                  27s   1GB
Oct 05 15:09:53 Starting compiler/backend/ag32
Oct 05 15:11:28 Finished compiler/backend/ag32                                 1m35s   1GB
Oct 05 15:11:28 Starting compiler/parsing/proofs
Oct 05 15:20:36 Finished compiler/parsing/proofs                               9m07s 947MB
Oct 05 15:20:36 Starting compiler/inference/proofs
Oct 05 15:24:46 Finished compiler/inference/proofs                             4m09s   1GB
Oct 05 15:24:46 Starting compiler/backend/semantics
Oct 05 15:32:49 Finished compiler/backend/semantics                            8m03s   2GB
Oct 05 15:32:49 Starting compiler/backend/reg_alloc/proofs
Oct 05 15:37:48 Finished compiler/backend/reg_alloc/proofs                     4m58s   1GB
Oct 05 15:37:48 Starting compiler/backend/proofs
Oct 05 16:32:52 Finished compiler/backend/proofs                              55m03s   5GB
Oct 05 16:32:53 Starting compiler/encoders/x64/proofs
Oct 05 16:46:58 Finished compiler/encoders/x64/proofs                         14m05s   4GB
Oct 05 16:46:58 Starting compiler/encoders/arm7/proofs
Oct 05 17:06:30 Finished compiler/encoders/arm7/proofs                        19m32s   3GB
Oct 05 17:06:30 Starting compiler/encoders/arm8/proofs
Oct 05 17:15:32 Finished compiler/encoders/arm8/proofs                         9m01s   1GB
Oct 05 17:15:32 Starting compiler/encoders/mips/proofs
Oct 05 17:29:25 Finished compiler/encoders/mips/proofs                        13m52s   2GB
Oct 05 17:29:25 Starting compiler/encoders/riscv/proofs
Oct 05 17:41:12 Finished compiler/encoders/riscv/proofs                       11m47s   1GB
Oct 05 17:41:12 Starting compiler/encoders/ag32/proofs
Oct 05 17:44:34 Finished compiler/encoders/ag32/proofs                         3m21s 917MB
Oct 05 17:44:34 Starting compiler/backend/x64/proofs
Oct 05 17:45:01 Finished compiler/backend/x64/proofs                             27s   1GB
Oct 05 17:45:01 Starting compiler/backend/arm7/proofs
Oct 05 17:45:30 Finished compiler/backend/arm7/proofs                            28s   1GB
Oct 05 17:45:30 Starting compiler/backend/arm8/proofs
Oct 05 17:46:01 Finished compiler/backend/arm8/proofs                            31s 750MB
Oct 05 17:46:01 Starting compiler/backend/mips/proofs
Oct 05 17:46:29 Finished compiler/backend/mips/proofs                            27s 967MB
Oct 05 17:46:29 Starting compiler/backend/riscv/proofs
Oct 05 17:46:56 Finished compiler/backend/riscv/proofs                           27s   1GB
Oct 05 17:46:56 Starting compiler/backend/ag32/proofs
Oct 05 17:59:46 Finished compiler/backend/ag32/proofs                         12m49s   2GB
Oct 05 17:59:46 Starting compiler/proofs
Oct 05 18:01:39 Finished compiler/proofs                                       1m52s   3GB
Oct 05 18:01:39 Starting candle/set-theory
Oct 05 18:02:16 Finished candle/set-theory                                       37s 857MB
Oct 05 18:02:16 Starting candle/syntax-lib
Oct 05 18:02:31 Finished candle/syntax-lib                                       14s 616MB
Oct 05 18:02:31 Starting candle/standard/syntax
Oct 05 18:04:59 Finished candle/standard/syntax                                2m27s   1GB
Oct 05 18:04:59 Starting candle/standard/semantics
Oct 05 18:07:24 Finished candle/standard/semantics                             2m24s   1GB
Oct 05 18:07:24 Starting candle/standard/monadic
Oct 05 18:09:40 Finished candle/standard/monadic                               2m16s   1GB
Oct 05 18:09:40 Starting candle/standard/ml_kernel
Oct 05 18:15:06 Finished candle/standard/ml_kernel                             5m25s   3GB
Oct 05 18:15:06 Starting candle/standard/opentheory
Oct 05 18:27:04 Finished candle/standard/opentheory                           11m58s   3GB
Oct 05 18:27:04 Starting candle/standard/opentheory/compilation
Oct 05 19:05:21 Finished candle/standard/opentheory/compilation               38m15s  17GB
Oct 05 19:05:21 Starting candle/standard/opentheory/compilation/proofs
Oct 05 19:06:13 Finished candle/standard/opentheory/compilation/proofs           52s   3GB
Oct 05 19:06:13 Starting characteristic/examples
Oct 05 19:08:27 Finished characteristic/examples                               2m13s   2GB
Oct 05 19:08:27 Starting tutorial/solutions
Oct 05 19:26:05 Finished tutorial/solutions                                   17m37s   8GB
Oct 05 19:26:05 Starting translator/monadic/examples
Oct 05 19:29:47 Finished translator/monadic/examples                           3m42s   3GB
Oct 05 19:29:47 Starting examples
Oct 05 19:40:31 Finished examples                                             10m43s   4GB
Oct 05 19:40:31 Starting examples/compilation/x64
Oct 05 22:29:39 Finished examples/compilation/x64                           2h49m07s  11GB
Oct 05 22:29:39 Starting examples/compilation/x64/proofs
Oct 05 22:31:44 Finished examples/compilation/x64/proofs                       2m05s   3GB
Oct 05 22:31:44 Starting examples/compilation/ag32
Oct 05 23:10:27 Finished examples/compilation/ag32                            38m43s   6GB
Oct 05 23:10:27 Starting examples/compilation/ag32/proofs
Oct 05 23:11:24 Finished examples/compilation/ag32/proofs                        56s   2GB
Oct 05 23:11:24 Starting translator/okasaki-examples
Oct 05 23:17:03 Finished translator/okasaki-examples                           5m39s   1GB
Oct 05 23:17:03 Starting translator/other-examples
Oct 05 23:22:16 Finished translator/other-examples                             5m12s   1GB
Oct 05 23:22:16 Starting compiler/parsing/tests
Oct 05 23:22:51 Finished compiler/parsing/tests                                  34s 567MB
Oct 05 23:22:51 Starting compiler/inference/tests
Oct 05 23:28:25 Finished compiler/inference/tests                              5m34s   3GB
Oct 05 23:28:25 Starting compiler/bootstrap/translation
Oct 06 02:54:38 Finished compiler/bootstrap/translation                     3h26m12s  40GB
Oct 06 02:54:38 Starting unverified/sexpr-bootstrap/x64/64
Oct 06 03:11:44 Finished unverified/sexpr-bootstrap/x64/64                    17m05s   2GB
Oct 06 03:11:44 Starting unverified/sexpr-bootstrap/x64/32
Oct 06 03:24:01 Finished unverified/sexpr-bootstrap/x64/32                    12m15s   5GB
Oct 06 03:24:01 Starting compiler/benchmarks
Oct 06 03:24:06 Finished compiler/benchmarks                                      5s  34MB
Oct 06 03:24:07 Starting compiler/bootstrap/compilation/x64/64
Oct 06 19:41:29 Finished compiler/bootstrap/compilation/x64/64             16h17m21s  60GB
Oct 06 19:41:29 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 06 19:46:14 Finished compiler/bootstrap/compilation/x64/64/proofs          4m45s   6GB
Oct 06 19:46:14 Starting compiler/bootstrap/compilation/x64/32
Oct 07 10:33:05 Finished compiler/bootstrap/compilation/x64/32             14h46m50s  60GB
Oct 07 10:33:05 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 07 10:37:28 Finished compiler/bootstrap/compilation/x64/32/proofs          4m23s   5GB
Oct 07 10:37:28 Starting compiler/bootstrap/compilation/ag32/32
Oct 08 02:13:34 Finished compiler/bootstrap/compilation/ag32/32            15h36m05s  59GB
Oct 08 02:13:34 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 08 02:52:25 Finished compiler/bootstrap/compilation/ag32/32/proofs        38m51s  28GB
Oct 08 02:52:25 SUCCESS