Job 1376

CakeML:bc1d24030a96270694c72cff1c37f656c1e85a9f
  Disambiguate some terms [Oct 16 13:02:29]
HOL:d4432472eed4748a30cac85026440e3a4fa77c0a
  Give finite maps their size function without an adjoin_to_theory call [Oct 17 10:04:49]
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

Oct 17 13:30:12 Claimed job
Oct 17 13:30:21 Building HOL
Oct 17 13:45:43 Starting developers
Oct 17 13:45:47 Finished developers                                               4s 102MB
Oct 17 13:45:48 Starting developers/bin
Oct 17 13:45:54 Finished developers/bin                                           6s   1GB
Oct 17 13:45:55 Starting semantics/ffi
Oct 17 13:46:06 Finished semantics/ffi                                           11s 241MB
Oct 17 13:46:06 Starting semantics
Oct 17 13:47:41 Finished semantics                                             1m34s 914MB
Oct 17 13:47:41 Starting semantics/proofs
Oct 17 13:51:17 Finished semantics/proofs                                      3m35s 844MB
Oct 17 13:51:17 Starting semantics/alt_semantics
Oct 17 13:51:26 Finished semantics/alt_semantics                                  9s 277MB
Oct 17 13:51:26 Starting semantics/alt_semantics/proofs
Oct 17 13:53:44 Finished semantics/alt_semantics/proofs                        2m17s 829MB
Oct 17 13:53:44 Starting basis/pure
Oct 17 13:56:46 Finished basis/pure                                            3m02s 899MB
Oct 17 13:56:47 Starting translator
Oct 17 13:59:33 Finished translator                                            2m45s   1GB
Oct 17 13:59:33 Starting compiler/parsing
Oct 17 14:00:47 Finished compiler/parsing                                      1m14s   3GB
Oct 17 14:00:47 Starting characteristic
Oct 17 14:06:59 Finished characteristic                                        6m11s   1GB
Oct 17 14:06:59 Starting translator/monadic
Oct 17 14:08:40 Finished translator/monadic                                    1m40s   1GB
Oct 17 14:08:41 Starting basis
Oct 17 14:44:52 Finished basis                                                36m10s  11GB
Oct 17 14:44:52 Starting compiler/inference
Oct 17 14:46:03 Finished compiler/inference                                    1m11s 938MB
Oct 17 14:46:03 Starting compiler/backend/reg_alloc
Oct 17 14:47:09 Finished compiler/backend/reg_alloc                            1m05s   1GB
Oct 17 14:47:09 Starting compiler/backend/gc
Oct 17 14:50:50 Finished compiler/backend/gc                                   3m40s   2GB
Oct 17 14:50:51 Starting compiler/backend
Oct 17 14:55:32 Finished compiler/backend                                      4m40s   4GB
Oct 17 14:55:32 Starting compiler/encoders/asm
Oct 17 14:55:55 Finished compiler/encoders/asm                                   22s 623MB
Oct 17 14:55:55 Starting compiler/encoders/x64
Oct 17 14:56:59 Finished compiler/encoders/x64                                 1m03s 722MB
Oct 17 14:56:59 Starting compiler/encoders/arm7
Oct 17 14:58:58 Finished compiler/encoders/arm7                                1m58s   1GB
Oct 17 14:58:58 Starting compiler/encoders/arm8
Oct 17 14:59:36 Finished compiler/encoders/arm8                                  37s 626MB
Oct 17 14:59:36 Starting compiler/encoders/mips
Oct 17 15:00:59 Finished compiler/encoders/mips                                1m22s   1GB
Oct 17 15:00:59 Starting compiler/encoders/riscv
Oct 17 15:02:38 Finished compiler/encoders/riscv                               1m38s   1GB
Oct 17 15:02:38 Starting compiler/encoders/ag32
Oct 17 15:02:56 Finished compiler/encoders/ag32                                  17s 710MB
Oct 17 15:02:56 Starting compiler/backend/x64
Oct 17 15:03:15 Finished compiler/backend/x64                                    18s   1GB
Oct 17 15:03:16 Starting compiler/backend/arm7
Oct 17 15:03:36 Finished compiler/backend/arm7                                   19s   1GB
Oct 17 15:03:36 Starting compiler/backend/arm8
Oct 17 15:03:54 Finished compiler/backend/arm8                                   18s   1GB
Oct 17 15:03:55 Starting compiler/backend/mips
Oct 17 15:04:14 Finished compiler/backend/mips                                   19s   1GB
Oct 17 15:04:14 Starting compiler/backend/riscv
Oct 17 15:04:34 Finished compiler/backend/riscv                                  19s   1GB
Oct 17 15:04:34 Starting compiler/backend/ag32
Oct 17 15:05:47 Finished compiler/backend/ag32                                 1m12s 973MB
Oct 17 15:05:47 Starting compiler/parsing/proofs
Oct 17 15:11:32 Finished compiler/parsing/proofs                               5m45s   1GB
Oct 17 15:11:32 Starting compiler/inference/proofs
Oct 17 15:14:10 Finished compiler/inference/proofs                             2m37s   1GB
Oct 17 15:14:10 Starting compiler/backend/semantics
Oct 17 15:45:39 Finished compiler/backend/semantics                           31m27s   2GB
Oct 17 15:45:39 Starting compiler/backend/reg_alloc/proofs
Oct 17 15:49:24 Finished compiler/backend/reg_alloc/proofs                     3m44s 944MB
Oct 17 15:49:24 Starting compiler/backend/proofs
Oct 17 16:47:04 Finished compiler/backend/proofs                              57m39s  16GB
Oct 17 16:47:04 Starting compiler/encoders/x64/proofs
Oct 17 16:57:31 Finished compiler/encoders/x64/proofs                         10m26s   5GB
Oct 17 16:57:31 Starting compiler/encoders/arm7/proofs
Oct 17 17:11:23 Finished compiler/encoders/arm7/proofs                        13m51s   6GB
Oct 17 17:11:23 Starting compiler/encoders/arm8/proofs
Oct 17 17:18:26 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Oct 17 17:18:27 Starting compiler/encoders/mips/proofs
Oct 17 17:29:10 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Oct 17 17:29:10 Starting compiler/encoders/riscv/proofs
Oct 17 17:38:48 Finished compiler/encoders/riscv/proofs                        9m37s   1GB
Oct 17 17:38:48 Starting compiler/encoders/ag32/proofs
Oct 17 17:41:37 Finished compiler/encoders/ag32/proofs                         2m48s 660MB
Oct 17 17:41:37 Starting compiler/backend/x64/proofs
Oct 17 17:41:58 Finished compiler/backend/x64/proofs                             20s   1GB
Oct 17 17:41:58 Starting compiler/backend/arm7/proofs
Oct 17 17:42:19 Finished compiler/backend/arm7/proofs                            21s   1GB
Oct 17 17:42:20 Starting compiler/backend/arm8/proofs
Oct 17 17:42:40 Finished compiler/backend/arm8/proofs                            19s   1GB
Oct 17 17:42:40 Starting compiler/backend/mips/proofs
Oct 17 17:43:00 Finished compiler/backend/mips/proofs                            20s   1GB
Oct 17 17:43:01 Starting compiler/backend/riscv/proofs
Oct 17 17:43:22 Finished compiler/backend/riscv/proofs                           21s   1GB
Oct 17 17:43:22 Starting compiler/backend/ag32/proofs
Oct 17 17:57:11 Finished compiler/backend/ag32/proofs                         13m49s   1GB
Oct 17 17:57:12 Starting compiler/proofs
Oct 17 17:59:01 Finished compiler/proofs                                       1m49s   2GB
Oct 17 17:59:01 Starting candle/set-theory
Oct 17 17:59:31 Finished candle/set-theory                                       28s 781MB
Oct 17 17:59:31 Starting candle/syntax-lib
Oct 17 17:59:42 Finished candle/syntax-lib                                       11s 673MB
Oct 17 17:59:42 Starting candle/standard/syntax
Oct 17 18:01:37 Finished candle/standard/syntax                                1m54s 946MB
Oct 17 18:01:37 Starting candle/standard/semantics
Oct 17 18:03:26 Finished candle/standard/semantics                             1m48s   1GB
Oct 17 18:03:26 Starting candle/standard/monadic
Oct 17 18:05:15 Finished candle/standard/monadic                               1m48s   1GB
Oct 17 18:05:15 Starting candle/standard/ml_kernel
Oct 17 18:11:08 Finished candle/standard/ml_kernel                             5m52s   2GB
Oct 17 18:11:08 Starting candle/overloading/syntax
Oct 17 18:14:28 Finished candle/overloading/syntax                             3m19s   1GB
Oct 17 18:14:29 Starting candle/overloading/semantics
Oct 17 18:27:17 Finished candle/overloading/semantics                         12m48s   5GB
Oct 17 18:27:17 Starting characteristic/examples
Oct 17 18:28:37 Finished characteristic/examples                               1m19s   1GB
Oct 17 18:28:37 Starting tutorial/solutions
Oct 17 18:44:04 Finished tutorial/solutions                                   15m26s   8GB
Oct 17 18:44:04 Starting translator/monadic/examples
Oct 17 18:47:19 Finished translator/monadic/examples                           3m15s   2GB
Oct 17 18:47:19 Starting examples
Oct 17 18:56:07 Finished examples                                              8m46s   3GB
Oct 17 18:56:07 Starting examples/compilation/x64
Oct 17 21:17:09 Finished examples/compilation/x64                           2h21m01s  14GB
Oct 17 21:17:09 Starting examples/compilation/x64/proofs
Oct 17 21:18:42 Finished examples/compilation/x64/proofs                       1m32s   3GB
Oct 17 21:18:42 Starting examples/compilation/ag32
Oct 17 21:50:50 Finished examples/compilation/ag32                            32m07s   7GB
Oct 17 21:50:50 Starting examples/compilation/ag32/proofs
Oct 17 21:51:35 Finished examples/compilation/ag32/proofs                        44s   3GB
Oct 17 21:51:35 Starting examples/cost
Oct 17 22:40:39 Finished examples/cost                                        49m03s   7GB
Oct 17 22:40:39 Starting examples/lpr_checker
Oct 17 22:44:38 Finished examples/lpr_checker                                  3m59s   2GB
Oct 17 22:44:38 Starting examples/lpr_checker/compilation
Oct 17 23:02:42 Finished examples/lpr_checker/compilation                     18m02s   9GB
Oct 17 23:02:42 Starting examples/lpr_checker/compilation/proofs
Oct 17 23:03:19 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Oct 17 23:03:19 Starting examples/lpr_checker/array
Oct 17 23:18:31 Finished examples/lpr_checker/array                           15m12s   4GB
Oct 17 23:18:32 Starting examples/lpr_checker/array/compilation
Oct 17 23:38:16 Finished examples/lpr_checker/array/compilation               19m44s  11GB
Oct 17 23:38:16 Starting examples/lpr_checker/array/compilation/proofs
Oct 17 23:39:03 Finished examples/lpr_checker/array/compilation/proofs           46s   3GB
Oct 17 23:39:03 Starting examples/opentheory
Oct 17 23:49:02 Finished examples/opentheory                                   9m58s   4GB
Oct 17 23:49:02 Starting examples/opentheory
Oct 17 23:49:03 Finished examples/opentheory                                      1s  19MB
Oct 17 23:49:03 Starting examples/opentheory/compilation
Oct 18 00:23:31 Finished examples/opentheory/compilation                      34m27s  18GB
Oct 18 00:23:31 Starting examples/opentheory/compilation/proofs
Oct 18 00:24:11 Finished examples/opentheory/compilation/proofs                  39s   3GB
Oct 18 00:24:11 Starting examples/opentheory/compilation/ag32
Oct 18 01:00:04 Finished examples/opentheory/compilation/ag32                 35m53s  19GB
Oct 18 01:00:05 Starting examples/opentheory/compilation/ag32/proofs
Oct 18 01:01:48 Finished examples/opentheory/compilation/ag32/proofs           1m43s   5GB
Oct 18 01:01:48 Starting translator/okasaki-examples
Oct 18 01:06:17 Finished translator/okasaki-examples                           4m28s   1GB
Oct 18 01:06:17 Starting translator/other-examples
Oct 18 01:08:24 Finished translator/other-examples                             2m06s   1GB
Oct 18 01:08:24 Starting compiler/parsing/tests
Oct 18 01:08:51 Finished compiler/parsing/tests                                  26s 603MB
Oct 18 01:08:51 Starting compiler/inference/tests
Oct 18 01:13:36 Finished compiler/inference/tests                              4m44s   2GB
Oct 18 01:13:36 Starting compiler/bootstrap/translation
Oct 18 04:08:20 Finished compiler/bootstrap/translation                     2h54m43s  52GB
Oct 18 04:08:20 Starting unverified/sexpr-bootstrap/x64/64
Oct 18 04:17:57 Finished unverified/sexpr-bootstrap/x64/64                     9m27s   8GB
Oct 18 04:17:57 Starting unverified/sexpr-bootstrap/x64/32
Oct 18 04:25:33 Finished unverified/sexpr-bootstrap/x64/32                     7m25s   8GB
Oct 18 04:25:33 Starting compiler/benchmarks
Oct 18 04:25:35 Finished compiler/benchmarks                                      1s  23MB
Oct 18 04:25:35 Starting compiler/bootstrap/compilation/x64/64
Oct 18 17:01:44 Finished compiler/bootstrap/compilation/x64/64             12h36m03s  64GB
Oct 18 17:01:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 18 17:04:52 Finished compiler/bootstrap/compilation/x64/64/proofs          3m07s  13GB
Oct 18 17:04:52 Starting compiler/bootstrap/compilation/x64/32
Oct 19 04:08:48 Finished compiler/bootstrap/compilation/x64/32             11h03m53s  64GB
Oct 19 04:08:48 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 19 04:11:45 Finished compiler/bootstrap/compilation/x64/32/proofs          2m56s  12GB
Oct 19 04:11:45 Starting compiler/bootstrap/compilation/ag32/32
Oct 19 15:41:57 Finished compiler/bootstrap/compilation/ag32/32            11h30m11s  64GB
Oct 19 15:41:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 19 16:00:32 Finished compiler/bootstrap/compilation/ag32/32/proofs        18m34s  24GB
Oct 19 16:00:32 SUCCESS