Job 1957

CakeML:939c98b120105252f0e1ee40b7fe9d6d0d028e12
  Fix proof broken by recent HOL change [Jul 06 08:39:40]
HOL:8b0248d705162f895cc7228fd638fe1c7d74b600
  Fix Unicode violation from 5184a58dae1 [Jul 04 06:34:10]
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

Jul 07 00:00:02 Claimed job
Jul 07 00:00:05 Reusing HOL
Jul 07 00:00:45 Starting developers
Jul 07 00:00:50 Finished developers                                               5s  83MB
Jul 07 00:00:50 Starting developers/bin
Jul 07 00:02:28 Finished developers/bin                                        1m37s   1GB
Jul 07 00:02:28 Starting semantics/ffi
Jul 07 00:02:39 Finished semantics/ffi                                           10s 195MB
Jul 07 00:02:39 Starting semantics
Jul 07 00:05:22 Finished semantics                                             2m43s   1GB
Jul 07 00:05:23 Starting semantics/proofs
Jul 07 00:13:06 Finished semantics/proofs                                      7m43s   1GB
Jul 07 00:13:07 Starting semantics/alt_semantics
Jul 07 00:13:37 Finished semantics/alt_semantics                                 29s 516MB
Jul 07 00:13:37 Starting semantics/alt_semantics/proofs
Jul 07 00:26:21 Finished semantics/alt_semantics/proofs                       12m43s   1GB
Jul 07 00:26:21 Starting basis/pure
Jul 07 00:27:34 Finished basis/pure                                            1m10s 805MB
Jul 07 00:27:34 Starting translator
Jul 07 00:31:36 Finished translator                                            4m02s   1GB
Jul 07 00:31:36 Starting compiler/parsing
Jul 07 00:33:09 Finished compiler/parsing                                      1m32s   5GB
Jul 07 00:33:09 Starting characteristic
Jul 07 00:40:35 Finished characteristic                                        7m25s   1GB
Jul 07 00:40:35 Starting translator/monadic
Jul 07 00:42:45 Finished translator/monadic                                    2m09s   1GB
Jul 07 00:42:45 Starting basis
Jul 07 01:39:43 Finished basis                                                56m57s  20GB
Jul 07 01:39:44 Starting compiler/inference
Jul 07 01:41:21 Finished compiler/inference                                    1m36s   1GB
Jul 07 01:41:21 Starting compiler/backend/reg_alloc
Jul 07 01:43:09 Finished compiler/backend/reg_alloc                            1m48s   1GB
Jul 07 01:43:09 Starting compiler/backend/gc
Jul 07 01:48:03 Finished compiler/backend/gc                                   4m53s   2GB
Jul 07 01:48:04 Starting compiler/backend
Jul 07 01:54:51 Finished compiler/backend                                      6m47s   2GB
Jul 07 01:54:52 Starting compiler/encoders/asm
Jul 07 01:55:25 Finished compiler/encoders/asm                                   32s 731MB
Jul 07 01:55:25 Starting compiler/encoders/x64
Jul 07 01:55:57 Finished compiler/encoders/x64                                   31s   1GB
Jul 07 01:55:57 Starting compiler/encoders/arm7
Jul 07 01:57:01 Finished compiler/encoders/arm7                                1m03s   1GB
Jul 07 01:57:01 Starting compiler/encoders/arm8
Jul 07 01:57:19 Finished compiler/encoders/arm8                                  18s 993MB
Jul 07 01:57:20 Starting compiler/encoders/arm8_asl
Jul 07 02:00:20 Finished compiler/encoders/arm8_asl                            2m59s   1GB
Jul 07 02:00:20 Starting compiler/encoders/mips
Jul 07 02:00:43 Finished compiler/encoders/mips                                  22s   1GB
Jul 07 02:00:43 Starting compiler/encoders/riscv
Jul 07 02:01:04 Finished compiler/encoders/riscv                                 21s 921MB
Jul 07 02:01:05 Starting compiler/encoders/ag32
Jul 07 02:01:29 Finished compiler/encoders/ag32                                  23s 627MB
Jul 07 02:01:29 Starting compiler/backend/x64
Jul 07 02:01:53 Finished compiler/backend/x64                                    24s   1GB
Jul 07 02:01:54 Starting compiler/backend/arm7
Jul 07 02:02:19 Finished compiler/backend/arm7                                   25s   1GB
Jul 07 02:02:19 Starting compiler/backend/arm8
Jul 07 02:02:44 Finished compiler/backend/arm8                                   24s   1GB
Jul 07 02:02:44 Starting compiler/backend/mips
Jul 07 02:03:08 Finished compiler/backend/mips                                   24s   1GB
Jul 07 02:03:09 Starting compiler/backend/riscv
Jul 07 02:03:33 Finished compiler/backend/riscv                                  24s   1GB
Jul 07 02:03:33 Starting compiler/backend/ag32
Jul 07 02:05:07 Finished compiler/backend/ag32                                 1m33s   1GB
Jul 07 02:05:07 Starting compiler/parsing/proofs
Jul 07 02:09:15 Finished compiler/parsing/proofs                               4m07s   1GB
Jul 07 02:09:16 Starting compiler/inference/proofs
Jul 07 02:12:16 Finished compiler/inference/proofs                             3m00s   1GB
Jul 07 02:12:16 Starting compiler/backend/semantics
Jul 07 02:42:54 Finished compiler/backend/semantics                           30m36s   2GB
Jul 07 02:42:54 Starting compiler/backend/reg_alloc/proofs
Jul 07 02:46:59 Finished compiler/backend/reg_alloc/proofs                     4m04s   1GB
Jul 07 02:46:59 Starting compiler/backend/proofs
Jul 07 03:50:14 Finished compiler/backend/proofs                            1h03m12s  12GB
Jul 07 03:50:14 Starting compiler/backend/serialiser
Jul 07 03:52:02 Finished compiler/backend/serialiser                           1m48s   2GB
Jul 07 03:52:03 Starting compiler/encoders/x64/proofs
Jul 07 04:02:43 Finished compiler/encoders/x64/proofs                         10m40s   4GB
Jul 07 04:02:43 Starting compiler/encoders/arm7/proofs
Jul 07 04:17:24 Finished compiler/encoders/arm7/proofs                        14m40s   2GB
Jul 07 04:17:24 Starting compiler/encoders/arm8/proofs
Jul 07 04:24:52 Finished compiler/encoders/arm8/proofs                         7m26s   1GB
Jul 07 04:24:52 Starting compiler/encoders/arm8_asl/proofs
Jul 07 04:41:27 Finished compiler/encoders/arm8_asl/proofs                    16m34s   2GB
Jul 07 04:41:27 Starting compiler/encoders/mips/proofs
Jul 07 04:52:53 Finished compiler/encoders/mips/proofs                        11m24s   1GB
Jul 07 04:52:53 Starting compiler/encoders/riscv/proofs
Jul 07 05:02:26 Finished compiler/encoders/riscv/proofs                        9m32s   1GB
Jul 07 05:02:26 Starting compiler/encoders/ag32/proofs
Jul 07 05:05:20 Finished compiler/encoders/ag32/proofs                         2m53s 801MB
Jul 07 05:05:21 Starting compiler/backend/x64/proofs
Jul 07 05:05:51 Finished compiler/backend/x64/proofs                             30s   1GB
Jul 07 05:05:51 Starting compiler/backend/arm7/proofs
Jul 07 05:06:23 Finished compiler/backend/arm7/proofs                            31s   1GB
Jul 07 05:06:23 Starting compiler/backend/arm8/proofs
Jul 07 05:06:54 Finished compiler/backend/arm8/proofs                            30s   1GB
Jul 07 05:06:54 Starting compiler/backend/arm8_asl
Jul 07 05:07:28 Finished compiler/backend/arm8_asl                               34s   1GB
Jul 07 05:07:28 Starting compiler/backend/mips/proofs
Jul 07 05:07:59 Finished compiler/backend/mips/proofs                            30s   1GB
Jul 07 05:07:59 Starting compiler/backend/riscv/proofs
Jul 07 05:08:29 Finished compiler/backend/riscv/proofs                           30s   1GB
Jul 07 05:08:30 Starting compiler/backend/ag32/proofs
Jul 07 05:23:10 Finished compiler/backend/ag32/proofs                         14m39s   2GB
Jul 07 05:23:10 Starting compiler/proofs
Jul 07 05:25:30 Finished compiler/proofs                                       2m20s   3GB
Jul 07 05:25:31 Starting candle/set-theory
Jul 07 05:26:07 Finished candle/set-theory                                       36s   1GB
Jul 07 05:26:08 Starting candle/syntax-lib
Jul 07 05:26:22 Finished candle/syntax-lib                                       13s 767MB
Jul 07 05:26:22 Starting candle/standard/syntax
Jul 07 05:28:33 Finished candle/standard/syntax                                2m10s   1GB
Jul 07 05:28:33 Starting candle/standard/semantics
Jul 07 05:30:30 Finished candle/standard/semantics                             1m56s   1GB
Jul 07 05:30:30 Starting candle/standard/monadic
Jul 07 05:32:35 Finished candle/standard/monadic                               2m04s   1GB
Jul 07 05:32:35 Starting candle/standard/ml_kernel
Jul 07 05:39:39 Finished candle/standard/ml_kernel                             7m03s   3GB
Jul 07 05:39:40 Starting candle/overloading/syntax
Jul 07 05:43:08 Finished candle/overloading/syntax                             3m27s   1GB
Jul 07 05:43:08 Starting candle/overloading/semantics
Jul 07 05:55:54 Finished candle/overloading/semantics                         12m44s   2GB
Jul 07 05:55:55 Starting candle/overloading/monadic
Jul 07 05:58:44 Finished candle/overloading/monadic                            2m48s   1GB
Jul 07 05:58:44 Starting candle/overloading/ml_kernel
Jul 07 06:06:51 Finished candle/overloading/ml_kernel                          8m06s   3GB
Jul 07 06:06:51 Starting candle/overloading/ml_checker
Jul 07 06:09:20 Finished candle/overloading/ml_checker                         2m29s   3GB
Jul 07 06:09:21 Starting candle/prover
Jul 07 06:21:03 Finished candle/prover                                        11m42s   2GB
Jul 07 06:21:04 Starting pancake
Jul 07 06:25:10 Finished pancake                                               4m05s   3GB
Jul 07 06:25:10 Starting pancake/ffi
Jul 07 06:25:11 Finished pancake/ffi                                              0s  20MB
Jul 07 06:25:11 Starting pancake/semantics
Jul 07 06:28:01 Finished pancake/semantics                                     2m50s   1GB
Jul 07 06:28:02 Starting pancake/proofs
Jul 07 06:41:32 Finished pancake/proofs                                       13m29s   5GB
Jul 07 06:41:32 Starting characteristic/examples
Jul 07 06:43:02 Finished characteristic/examples                               1m29s   3GB
Jul 07 06:43:02 Starting tutorial/solutions
Jul 07 06:59:56 Finished tutorial/solutions                                   16m52s   9GB
Jul 07 06:59:57 Starting translator/monadic/examples
Jul 07 07:04:08 Finished translator/monadic/examples                           4m10s   2GB
Jul 07 07:04:08 Starting examples
Jul 07 07:15:16 Finished examples                                             11m07s   3GB
Jul 07 07:15:16 Starting examples/compilation/x64
Jul 07 09:25:14 Finished examples/compilation/x64                           2h09m57s  12GB
Jul 07 09:25:14 Starting examples/compilation/x64/proofs
Jul 07 09:27:55 Finished examples/compilation/x64/proofs                       2m40s   3GB
Jul 07 09:27:55 Starting examples/compilation/ag32
Jul 07 10:02:38 Finished examples/compilation/ag32                            34m42s   8GB
Jul 07 10:02:38 Starting examples/compilation/ag32/proofs
Jul 07 10:03:37 Finished examples/compilation/ag32/proofs                        59s   3GB
Jul 07 10:03:38 Starting examples/lpr_checker
Jul 07 10:04:43 Finished examples/lpr_checker                                  1m04s   1GB
Jul 07 10:04:43 Starting examples/lpr_checker/array
Jul 07 10:42:07 Finished examples/lpr_checker/array                           37m21s   6GB
Jul 07 10:42:07 Starting examples/lpr_checker/array/compilation
Jul 07 11:24:26 Finished examples/lpr_checker/array/compilation               42m19s  26GB
Jul 07 11:24:27 Starting examples/lpr_checker/array/compilation/proofs
Jul 07 11:25:54 Finished examples/lpr_checker/array/compilation/proofs         1m27s   5GB
Jul 07 11:25:54 Starting examples/opentheory
Jul 07 11:37:22 Finished examples/opentheory                                  11m26s   5GB
Jul 07 11:37:22 Starting examples/opentheory
Jul 07 11:37:24 Finished examples/opentheory                                      1s  22MB
Jul 07 11:37:24 Starting examples/opentheory/compilation
Jul 07 12:16:43 Finished examples/opentheory/compilation                      39m18s  26GB
Jul 07 12:16:43 Starting examples/opentheory/compilation/proofs
Jul 07 12:17:41 Finished examples/opentheory/compilation/proofs                  58s   3GB
Jul 07 12:17:42 Starting examples/opentheory/compilation/ag32
Jul 07 12:53:43 Finished examples/opentheory/compilation/ag32                 36m00s  21GB
Jul 07 12:53:43 Starting examples/opentheory/compilation/ag32/proofs
Jul 07 12:55:37 Finished examples/opentheory/compilation/ag32/proofs           1m53s   5GB
Jul 07 12:55:37 Starting examples/sat_encodings
Jul 07 12:57:44 Finished examples/sat_encodings                                2m06s 738MB
Jul 07 12:57:44 Starting examples/sat_encodings/case_studies
Jul 07 12:59:37 Finished examples/sat_encodings/case_studies                   1m52s 890MB
Jul 07 12:59:37 Starting examples/sat_encodings/translation
Jul 07 13:05:51 Finished examples/sat_encodings/translation                    6m14s   5GB
Jul 07 13:05:52 Starting examples/sat_encodings/translation/compilation
Jul 07 13:58:12 Finished examples/sat_encodings/translation/compilation       52m18s  22GB
Jul 07 13:58:12 Starting examples/deflate
Jul 07 13:59:14 Finished examples/deflate                                      1m01s 877MB
Jul 07 13:59:14 Starting examples/deflate/translation
Jul 07 14:00:57 Finished examples/deflate/translation                          1m42s   3GB
Jul 07 14:00:58 Starting examples/deflate/translation/compilation
Jul 07 14:24:31 Finished examples/deflate/translation/compilation             23m33s  15GB
Jul 07 14:24:31 Starting translator/okasaki-examples
Jul 07 14:29:59 Finished translator/okasaki-examples                           5m25s   1GB
Jul 07 14:29:59 Starting translator/other-examples
Jul 07 14:30:54 Finished translator/other-examples                               55s   1GB
Jul 07 14:30:55 Starting compiler/parsing/tests
Jul 07 14:31:26 Finished compiler/parsing/tests                                  31s 517MB
Jul 07 14:31:27 Starting compiler/inference/tests
Jul 07 14:40:09 Finished compiler/inference/tests                              8m41s   5GB
Jul 07 14:40:09 Starting compiler/printing/test
Jul 07 14:43:59 Finished compiler/printing/test                                3m49s   3GB
Jul 07 14:43:59 Starting icing/flover
Jul 07 15:36:19 Finished icing/flover                                         52m19s   1GB
Jul 07 15:36:20 Starting icing/
Jul 07 16:54:38 Finished icing/                                             1h18m18s   5GB
Jul 07 16:54:38 Starting icing/examples
Jul 07 16:56:19 Finished icing/examples                                        1m40s   3GB
Jul 07 16:56:19 Starting compiler/repl
Jul 07 17:10:14 Finished compiler/repl                                        13m54s   4GB
Jul 07 17:10:14 Starting compiler/bootstrap/translation
Jul 07 21:50:40 Finished compiler/bootstrap/translation                     4h40m25s  44GB
Jul 07 21:50:40 Starting unverified/sexpr-bootstrap/x64/64
Jul 07 22:01:53 Finished unverified/sexpr-bootstrap/x64/64                    11m10s   8GB
Jul 07 22:01:53 Starting unverified/sexpr-bootstrap/x64/32
Jul 07 22:10:45 Finished unverified/sexpr-bootstrap/x64/32                     8m49s  10GB
Jul 07 22:10:45 Starting compiler/benchmarks
Jul 07 22:10:48 Finished compiler/benchmarks                                      2s  35MB
Jul 07 22:10:48 Starting compiler/bootstrap/compilation/x64/64
Jul 08 09:57:54 Finished compiler/bootstrap/compilation/x64/64             11h47m04s  64GB
Jul 08 09:57:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 08 10:17:06 Finished compiler/bootstrap/compilation/x64/64/proofs         19m12s  30GB
Jul 08 10:17:07 Starting compiler/bootstrap/compilation/x64/32
Jul 08 16:50:37 Finished compiler/bootstrap/compilation/x64/32              6h33m28s  57GB
Jul 08 16:50:37 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 08 16:53:06 Finished compiler/bootstrap/compilation/x64/32/proofs          2m28s  16GB
Jul 08 16:53:06 Starting compiler/bootstrap/compilation/ag32/32
Jul 08 23:43:21 Finished compiler/bootstrap/compilation/ag32/32             6h50m15s  64GB
Jul 08 23:43:22 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 08 23:52:56 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m34s  14GB
Jul 08 23:52:57 SUCCESS