Job 1698

CakeML:2295e66c17f21e28d1fa7e6b96eca17bde61a0d7
  Merge pull request #850 from CakeML/eval [Dec 21 12:12:01]
HOL:9d2d0e89bd165c1ea71279ed6f2ed14ed6c15d27
  Add comment to explain function of a somewhat mysterious file [Dec 20 05:01:21]
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

Dec 21 12:30:13 Claimed job
Dec 21 12:30:23 Building HOL
Dec 21 12:40:24 Starting developers
Dec 21 12:40:28 Finished developers                                               4s  99MB
Dec 21 12:40:29 Starting developers/bin
Dec 21 12:40:34 Finished developers/bin                                           5s 670MB
Dec 21 12:40:34 Starting semantics/ffi
Dec 21 12:40:43 Finished semantics/ffi                                            8s 225MB
Dec 21 12:40:43 Starting semantics
Dec 21 12:42:20 Finished semantics                                             1m36s   1GB
Dec 21 12:42:20 Starting semantics/proofs
Dec 21 12:46:10 Finished semantics/proofs                                      3m49s   1GB
Dec 21 12:46:10 Starting semantics/alt_semantics
Dec 21 12:46:22 Finished semantics/alt_semantics                                 11s 358MB
Dec 21 12:46:22 Starting semantics/alt_semantics/proofs
Dec 21 12:48:58 Finished semantics/alt_semantics/proofs                        2m36s 784MB
Dec 21 12:48:59 Starting basis/pure
Dec 21 12:52:00 Finished basis/pure                                            3m01s 693MB
Dec 21 12:52:00 Starting translator
Dec 21 12:55:00 Finished translator                                            2m58s   1GB
Dec 21 12:55:00 Starting compiler/parsing
Dec 21 12:56:20 Finished compiler/parsing                                      1m19s   2GB
Dec 21 12:56:20 Starting characteristic
Dec 21 13:02:17 Finished characteristic                                        5m56s   1GB
Dec 21 13:02:17 Starting translator/monadic
Dec 21 13:04:00 Finished translator/monadic                                    1m42s   1GB
Dec 21 13:04:00 Starting basis
Dec 21 13:52:38 Finished basis                                                48m37s  10GB
Dec 21 13:52:38 Starting compiler/inference
Dec 21 13:53:57 Finished compiler/inference                                    1m18s   1GB
Dec 21 13:53:57 Starting compiler/backend/reg_alloc
Dec 21 13:55:05 Finished compiler/backend/reg_alloc                            1m07s   1GB
Dec 21 13:55:05 Starting compiler/backend/gc
Dec 21 13:58:51 Finished compiler/backend/gc                                   3m45s   1GB
Dec 21 13:58:51 Starting compiler/backend
Dec 21 14:03:40 Finished compiler/backend                                      4m48s   2GB
Dec 21 14:03:40 Starting compiler/encoders/asm
Dec 21 14:04:04 Finished compiler/encoders/asm                                   23s 690MB
Dec 21 14:04:04 Starting compiler/encoders/x64
Dec 21 14:05:09 Finished compiler/encoders/x64                                 1m04s   1GB
Dec 21 14:05:10 Starting compiler/encoders/arm7
Dec 21 14:07:18 Finished compiler/encoders/arm7                                2m08s   1GB
Dec 21 14:07:19 Starting compiler/encoders/arm8
Dec 21 14:07:58 Finished compiler/encoders/arm8                                  39s 658MB
Dec 21 14:07:58 Starting compiler/encoders/mips
Dec 21 14:09:35 Finished compiler/encoders/mips                                1m36s   1GB
Dec 21 14:09:35 Starting compiler/encoders/riscv
Dec 21 14:11:29 Finished compiler/encoders/riscv                               1m53s   1GB
Dec 21 14:11:29 Starting compiler/encoders/ag32
Dec 21 14:11:48 Finished compiler/encoders/ag32                                  18s 857MB
Dec 21 14:11:48 Starting compiler/backend/x64
Dec 21 14:12:08 Finished compiler/backend/x64                                    19s   1GB
Dec 21 14:12:08 Starting compiler/backend/arm7
Dec 21 14:12:30 Finished compiler/backend/arm7                                   21s   1GB
Dec 21 14:12:31 Starting compiler/backend/arm8
Dec 21 14:12:51 Finished compiler/backend/arm8                                   20s   1GB
Dec 21 14:12:51 Starting compiler/backend/mips
Dec 21 14:13:12 Finished compiler/backend/mips                                   20s   1GB
Dec 21 14:13:12 Starting compiler/backend/riscv
Dec 21 14:13:34 Finished compiler/backend/riscv                                  21s   1GB
Dec 21 14:13:34 Starting compiler/backend/ag32
Dec 21 14:14:45 Finished compiler/backend/ag32                                 1m10s   1GB
Dec 21 14:14:45 Starting compiler/parsing/proofs
Dec 21 14:18:48 Finished compiler/parsing/proofs                               4m02s   1GB
Dec 21 14:18:49 Starting compiler/inference/proofs
Dec 21 14:21:22 Finished compiler/inference/proofs                             2m32s 894MB
Dec 21 14:21:22 Starting compiler/backend/semantics
Dec 21 14:54:03 Finished compiler/backend/semantics                           32m39s   2GB
Dec 21 14:54:03 Starting compiler/backend/reg_alloc/proofs
Dec 21 14:57:50 Finished compiler/backend/reg_alloc/proofs                     3m47s   1GB
Dec 21 14:57:51 Starting compiler/backend/proofs
Dec 21 15:56:17 Finished compiler/backend/proofs                              58m24s  16GB
Dec 21 15:56:17 Starting compiler/backend/serialiser
Dec 21 15:57:33 Finished compiler/backend/serialiser                           1m15s   1GB
Dec 21 15:57:33 Starting compiler/encoders/x64/proofs
Dec 21 16:07:53 Finished compiler/encoders/x64/proofs                         10m19s   4GB
Dec 21 16:07:53 Starting compiler/encoders/arm7/proofs
Dec 21 16:21:58 Finished compiler/encoders/arm7/proofs                        14m04s   5GB
Dec 21 16:21:58 Starting compiler/encoders/arm8/proofs
Dec 21 16:29:22 Finished compiler/encoders/arm8/proofs                         7m23s   1GB
Dec 21 16:29:22 Starting compiler/encoders/mips/proofs
Dec 21 16:40:06 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Dec 21 16:40:06 Starting compiler/encoders/riscv/proofs
Dec 21 16:49:21 Finished compiler/encoders/riscv/proofs                        9m14s   1GB
Dec 21 16:49:22 Starting compiler/encoders/ag32/proofs
Dec 21 16:52:11 Finished compiler/encoders/ag32/proofs                         2m48s 599MB
Dec 21 16:52:11 Starting compiler/backend/x64/proofs
Dec 21 16:52:35 Finished compiler/backend/x64/proofs                             23s   1GB
Dec 21 16:52:35 Starting compiler/backend/arm7/proofs
Dec 21 16:52:59 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 21 16:52:59 Starting compiler/backend/arm8/proofs
Dec 21 16:53:23 Finished compiler/backend/arm8/proofs                            23s   1GB
Dec 21 16:53:23 Starting compiler/backend/mips/proofs
Dec 21 16:53:48 Finished compiler/backend/mips/proofs                            24s   1GB
Dec 21 16:53:48 Starting compiler/backend/riscv/proofs
Dec 21 16:54:12 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 21 16:54:13 Starting compiler/backend/ag32/proofs
Dec 21 17:08:04 Finished compiler/backend/ag32/proofs                         13m50s   2GB
Dec 21 17:08:04 Starting compiler/proofs
Dec 21 17:10:07 Finished compiler/proofs                                       2m02s   3GB
Dec 21 17:10:07 Starting candle/set-theory
Dec 21 17:10:36 Finished candle/set-theory                                       28s 705MB
Dec 21 17:10:36 Starting candle/syntax-lib
Dec 21 17:10:47 Finished candle/syntax-lib                                       10s 671MB
Dec 21 17:10:47 Starting candle/standard/syntax
Dec 21 17:12:42 Finished candle/standard/syntax                                1m53s 926MB
Dec 21 17:12:42 Starting candle/standard/semantics
Dec 21 17:14:26 Finished candle/standard/semantics                             1m44s 950MB
Dec 21 17:14:27 Starting candle/standard/monadic
Dec 21 17:16:16 Finished candle/standard/monadic                               1m48s   1GB
Dec 21 17:16:16 Starting candle/standard/ml_kernel
Dec 21 17:22:15 Finished candle/standard/ml_kernel                             5m58s   3GB
Dec 21 17:22:15 Starting candle/overloading/syntax
Dec 21 17:25:31 Finished candle/overloading/syntax                             3m16s   1GB
Dec 21 17:25:32 Starting candle/overloading/semantics
Dec 21 17:37:59 Finished candle/overloading/semantics                         12m27s   2GB
Dec 21 17:37:59 Starting pancake
Dec 21 17:39:55 Finished pancake                                               1m55s   3GB
Dec 21 17:39:55 Starting pancake/ffi
Dec 21 17:39:56 Finished pancake/ffi                                              0s   4MB
Dec 21 17:39:56 Starting pancake/semantics
Dec 21 17:42:24 Finished pancake/semantics                                     2m27s   1GB
Dec 21 17:42:24 Starting pancake/proofs
Dec 21 17:55:10 Finished pancake/proofs                                       12m46s   6GB
Dec 21 17:55:11 Starting characteristic/examples
Dec 21 17:56:36 Finished characteristic/examples                               1m25s   3GB
Dec 21 17:56:37 Starting tutorial/solutions
Dec 21 18:13:29 Finished tutorial/solutions                                   16m51s   9GB
Dec 21 18:13:29 Starting translator/monadic/examples
Dec 21 18:16:55 Finished translator/monadic/examples                           3m25s   2GB
Dec 21 18:16:55 Starting examples
Dec 21 18:27:06 Finished examples                                             10m11s   3GB
Dec 21 18:27:07 Starting examples/compilation/x64
Dec 21 20:59:55 Finished examples/compilation/x64                           2h32m47s  18GB
Dec 21 20:59:55 Starting examples/compilation/x64/proofs
Dec 21 21:02:00 Finished examples/compilation/x64/proofs                       2m05s   3GB
Dec 21 21:02:01 Starting examples/compilation/ag32
Dec 21 21:37:14 Finished examples/compilation/ag32                            35m13s  10GB
Dec 21 21:37:14 Starting examples/compilation/ag32/proofs
Dec 21 21:38:02 Finished examples/compilation/ag32/proofs                        47s   2GB
Dec 21 21:38:03 Starting examples/cost
Dec 21 22:38:47 Finished examples/cost                                      1h00m44s   8GB
Dec 21 22:38:48 Starting examples/lpr_checker
Dec 21 22:39:37 Finished examples/lpr_checker                                    48s   1GB
Dec 21 22:39:37 Starting examples/lpr_checker/array
Dec 21 23:11:08 Finished examples/lpr_checker/array                           31m30s   5GB
Dec 21 23:11:08 Starting examples/lpr_checker/array/compilation
Dec 22 00:39:01 Finished examples/lpr_checker/array/compilation             1h27m52s  26GB
Dec 22 00:39:01 Starting examples/lpr_checker/array/compilation/proofs
Dec 22 00:40:19 Finished examples/lpr_checker/array/compilation/proofs         1m17s   6GB
Dec 22 00:40:19 Starting examples/opentheory
Dec 22 00:50:23 Finished examples/opentheory                                  10m03s   5GB
Dec 22 00:50:23 Starting examples/opentheory
Dec 22 00:50:24 Finished examples/opentheory                                      1s  23MB
Dec 22 00:50:25 Starting examples/opentheory/compilation
Dec 22 01:28:25 Finished examples/opentheory/compilation                      37m59s  23GB
Dec 22 01:28:25 Starting examples/opentheory/compilation/proofs
Dec 22 01:29:22 Finished examples/opentheory/compilation/proofs                  56s   2GB
Dec 22 01:29:22 Starting examples/opentheory/compilation/ag32
Dec 22 02:09:01 Finished examples/opentheory/compilation/ag32                 39m36s  24GB
Dec 22 02:09:01 Starting examples/opentheory/compilation/ag32/proofs
Dec 22 02:10:42 Finished examples/opentheory/compilation/ag32/proofs           1m41s   6GB
Dec 22 02:10:43 Starting examples/sat_encodings
Dec 22 02:12:32 Finished examples/sat_encodings                                1m49s 881MB
Dec 22 02:12:32 Starting examples/sat_encodings/case_studies
Dec 22 02:14:15 Finished examples/sat_encodings/case_studies                   1m42s 660MB
Dec 22 02:14:15 Starting examples/sat_encodings/translation
Dec 22 02:20:05 Finished examples/sat_encodings/translation                    5m50s   5GB
Dec 22 02:20:05 Starting examples/sat_encodings/translation/compilation
Dec 22 03:14:12 Finished examples/sat_encodings/translation/compilation       54m06s  20GB
Dec 22 03:14:12 Starting translator/okasaki-examples
Dec 22 03:19:01 Finished translator/okasaki-examples                           4m48s   1GB
Dec 22 03:19:01 Starting translator/other-examples
Dec 22 03:21:01 Finished translator/other-examples                             1m59s   1GB
Dec 22 03:21:01 Starting compiler/parsing/tests
Dec 22 03:21:32 Finished compiler/parsing/tests                                  30s 563MB
Dec 22 03:21:32 Starting compiler/inference/tests
Dec 22 03:30:00 Finished compiler/inference/tests                              8m28s   4GB
Dec 22 03:30:01 Starting compiler/bootstrap/translation
Dec 22 06:19:39 Finished compiler/bootstrap/translation                     2h49m36s  38GB
Dec 22 06:19:39 Starting unverified/sexpr-bootstrap/x64/64
Dec 22 06:29:05 Finished unverified/sexpr-bootstrap/x64/64                     9m22s   9GB
Dec 22 06:29:05 Starting unverified/sexpr-bootstrap/x64/32
Dec 22 06:37:08 Finished unverified/sexpr-bootstrap/x64/32                     7m59s   8GB
Dec 22 06:37:08 Starting compiler/benchmarks
Dec 22 06:37:14 Finished compiler/benchmarks                                      5s  34MB
Dec 22 06:37:14 Starting compiler/bootstrap/compilation/x64/64
Dec 22 20:34:43 Finished compiler/bootstrap/compilation/x64/64             13h57m24s  64GB
Dec 22 20:34:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 22 20:37:16 Finished compiler/bootstrap/compilation/x64/64/proofs          2m32s  14GB
Dec 22 20:37:16 Starting compiler/bootstrap/compilation/x64/32
Dec 23 08:17:38 Finished compiler/bootstrap/compilation/x64/32             11h40m18s  64GB
Dec 23 08:17:38 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 23 08:20:33 Finished compiler/bootstrap/compilation/x64/32/proofs          2m54s  11GB
Dec 23 08:20:33 Starting compiler/bootstrap/compilation/ag32/32
Dec 23 20:09:51 Finished compiler/bootstrap/compilation/ag32/32            11h49m17s  64GB
Dec 23 20:09:52 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 23 20:32:35 Finished compiler/bootstrap/compilation/ag32/32/proofs        22m43s  23GB
Dec 23 20:32:35 SUCCESS