Job 2014

CakeML:195acbd7ebcbd184f5caf4344eb2572eb3913266
  pancake: move parser files to a separate dir [Oct 12 00:26:22]
#912 (pan_cleanup)
Merging into:59e14a942bb54a58350e86539c1953c541eff3f4
  Merge pull request #909 from mktnk3/word_to_word_Pancake [Oct 01 15:44:31]
HOL:52406bd0bb1d700af123bb9b3fe55c38be50c11c
  Use Zorn's Lemma to show all strong orders can extend to linear ones [Oct 10 05:46:28]
Machine:oven3

Oct 12 15:31:24 Claimed job
Oct 12 15:31:27 Reusing HOL
Oct 12 15:32:21 Starting developers
Oct 12 15:32:30 Finished developers                                               9s 142MB
Oct 12 15:32:30 Starting developers/bin
Oct 12 15:32:43 Finished developers/bin                                          12s   1GB
Oct 12 15:32:43 Starting compiler/proofs
Oct 12 18:54:56 Finished compiler/proofs                                    3h22m12s  15GB
Oct 12 18:54:56 Starting compiler/bootstrap/translation
Oct 13 05:20:36 Finished compiler/bootstrap/translation                    10h25m39s  39GB
Oct 13 05:20:36 Starting semantics/ffi
Oct 13 05:20:44 Finished semantics/ffi                                            7s 217MB
Oct 13 05:20:45 Starting semantics
Oct 13 05:20:47 Finished semantics                                                2s  16MB
Oct 13 05:20:47 Starting semantics/proofs
Oct 13 05:22:03 Finished semantics/proofs                                      1m15s 942MB
Oct 13 05:22:03 Starting semantics/alt_semantics
Oct 13 05:22:57 Finished semantics/alt_semantics                                 53s 566MB
Oct 13 05:22:57 Starting semantics/alt_semantics/proofs
Oct 13 05:48:51 Finished semantics/alt_semantics/proofs                       25m54s   1GB
Oct 13 05:48:52 Starting basis/pure
Oct 13 05:48:54 Finished basis/pure                                               2s  33MB
Oct 13 05:48:54 Starting translator
Oct 13 05:52:40 Finished translator                                            3m45s   1GB
Oct 13 05:52:40 Starting compiler/parsing
Oct 13 05:52:43 Finished compiler/parsing                                         2s  16MB
Oct 13 05:52:43 Starting characteristic
Oct 13 05:52:46 Finished characteristic                                           3s  22MB
Oct 13 05:52:47 Starting translator/monadic
Oct 13 05:52:50 Finished translator/monadic                                       2s  28MB
Oct 13 05:52:50 Starting basis
Oct 13 06:00:23 Finished basis                                                 7m32s   2GB
Oct 13 06:00:23 Starting compiler/inference
Oct 13 06:00:26 Finished compiler/inference                                       2s  33MB
Oct 13 06:00:26 Starting compiler/backend/reg_alloc
Oct 13 06:00:28 Finished compiler/backend/reg_alloc                               2s  16MB
Oct 13 06:00:29 Starting compiler/backend/gc
Oct 13 06:00:32 Finished compiler/backend/gc                                      3s  35MB
Oct 13 06:00:33 Starting compiler/backend
Oct 13 06:00:55 Finished compiler/backend                                        21s 520MB
Oct 13 06:00:55 Starting compiler/encoders/asm
Oct 13 06:00:58 Finished compiler/encoders/asm                                    2s  25MB
Oct 13 06:00:58 Starting compiler/encoders/x64
Oct 13 06:01:01 Finished compiler/encoders/x64                                    2s  29MB
Oct 13 06:01:01 Starting compiler/encoders/arm7
Oct 13 06:01:04 Finished compiler/encoders/arm7                                   2s  33MB
Oct 13 06:01:04 Starting compiler/encoders/arm8
Oct 13 06:01:07 Finished compiler/encoders/arm8                                   2s  29MB
Oct 13 06:01:07 Starting compiler/encoders/arm8_asl
Oct 13 10:23:52 Finished compiler/encoders/arm8_asl                         4h22m44s  45GB
Oct 13 10:23:52 Starting compiler/encoders/mips
Oct 13 10:23:55 Finished compiler/encoders/mips                                   2s  32MB
Oct 13 10:23:55 Starting compiler/encoders/riscv
Oct 13 10:23:58 Finished compiler/encoders/riscv                                  2s  32MB
Oct 13 10:23:58 Starting compiler/encoders/ag32
Oct 13 10:24:01 Finished compiler/encoders/ag32                                   2s  29MB
Oct 13 10:24:01 Starting compiler/backend/x64
Oct 13 10:24:05 Finished compiler/backend/x64                                     3s  32MB
Oct 13 10:24:05 Starting compiler/backend/arm7
Oct 13 10:24:09 Finished compiler/backend/arm7                                    3s  35MB
Oct 13 10:24:09 Starting compiler/backend/arm8
Oct 13 10:24:13 Finished compiler/backend/arm8                                    3s  34MB
Oct 13 10:24:13 Starting compiler/backend/mips
Oct 13 10:24:17 Finished compiler/backend/mips                                    3s  34MB
Oct 13 10:24:17 Starting compiler/backend/riscv
Oct 13 10:24:21 Finished compiler/backend/riscv                                   3s  34MB
Oct 13 10:24:21 Starting compiler/backend/ag32
Oct 13 10:27:15 Finished compiler/backend/ag32                                 2m53s   1GB
Oct 13 10:27:15 Starting compiler/parsing/proofs
Oct 13 10:27:18 Finished compiler/parsing/proofs                                  2s  27MB
Oct 13 10:27:18 Starting compiler/inference/proofs
Oct 13 10:27:21 Finished compiler/inference/proofs                                2s  32MB
Oct 13 10:27:22 Starting compiler/backend/semantics
Oct 13 10:29:49 Finished compiler/backend/semantics                            2m27s   1GB
Oct 13 10:29:49 Starting compiler/backend/reg_alloc/proofs
Oct 13 10:29:53 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Oct 13 10:29:53 Starting compiler/backend/proofs
Oct 13 10:31:45 Finished compiler/backend/proofs                               1m52s   2GB
Oct 13 10:31:46 Starting compiler/backend/serialiser
Oct 13 10:31:51 Finished compiler/backend/serialiser                              5s  50MB
Oct 13 10:31:51 Starting compiler/encoders/x64/proofs
Oct 13 10:54:16 Finished compiler/encoders/x64/proofs                         22m24s   4GB
Oct 13 10:54:16 Starting compiler/encoders/arm7/proofs
Oct 13 11:25:18 Finished compiler/encoders/arm7/proofs                        31m01s   6GB
Oct 13 11:25:18 Starting compiler/encoders/arm8/proofs
Oct 13 11:41:20 Finished compiler/encoders/arm8/proofs                        16m02s   1GB
Oct 13 11:41:21 Starting compiler/encoders/arm8_asl/proofs
Oct 13 13:37:44 Finished compiler/encoders/arm8_asl/proofs                  1h56m23s   5GB
Oct 13 13:37:45 Starting compiler/encoders/mips/proofs
Oct 13 14:01:17 Finished compiler/encoders/mips/proofs                        23m31s   2GB
Oct 13 14:01:17 Starting compiler/encoders/riscv/proofs
Oct 13 14:21:47 Finished compiler/encoders/riscv/proofs                       20m30s   1GB
Oct 13 14:21:48 Starting compiler/encoders/ag32/proofs
Oct 13 14:27:43 Finished compiler/encoders/ag32/proofs                         5m55s   1GB
Oct 13 14:27:44 Starting compiler/backend/x64/proofs
Oct 13 14:28:38 Finished compiler/backend/x64/proofs                             54s   1GB
Oct 13 14:28:38 Starting compiler/backend/arm7/proofs
Oct 13 14:29:35 Finished compiler/backend/arm7/proofs                            56s   1GB
Oct 13 14:29:35 Starting compiler/backend/arm8/proofs
Oct 13 14:30:31 Finished compiler/backend/arm8/proofs                            55s   1GB
Oct 13 14:30:31 Starting compiler/backend/arm8_asl
Oct 13 14:31:16 Finished compiler/backend/arm8_asl                               45s   1GB
Oct 13 14:31:17 Starting compiler/backend/mips/proofs
Oct 13 14:32:12 Finished compiler/backend/mips/proofs                            55s   1GB
Oct 13 14:32:13 Starting compiler/backend/riscv/proofs
Oct 13 14:33:08 Finished compiler/backend/riscv/proofs                           54s   1GB
Oct 13 14:33:08 Starting compiler/backend/ag32/proofs
Oct 13 15:03:21 Finished compiler/backend/ag32/proofs                         30m12s   2GB
Oct 13 15:03:21 Starting candle/set-theory
Oct 13 15:04:29 Finished candle/set-theory                                     1m07s 964MB
Oct 13 15:04:29 Starting candle/syntax-lib
Oct 13 15:04:32 Finished candle/syntax-lib                                        2s  35MB
Oct 13 15:04:32 Starting candle/standard/syntax
Oct 13 15:04:51 Finished candle/standard/syntax                                  18s 486MB
Oct 13 15:04:51 Starting candle/standard/semantics
Oct 13 15:08:44 Finished candle/standard/semantics                             3m52s   1GB
Oct 13 15:08:44 Starting candle/standard/monadic
Oct 13 15:08:47 Finished candle/standard/monadic                                  3s  34MB
Oct 13 15:08:47 Starting candle/standard/ml_kernel
Oct 13 15:11:50 Finished candle/standard/ml_kernel                             3m02s   2GB
Oct 13 15:11:50 Starting candle/overloading/syntax
Oct 13 15:18:39 Finished candle/overloading/syntax                             6m48s   1GB
Oct 13 15:18:40 Starting candle/overloading/semantics
Oct 13 15:44:53 Finished candle/overloading/semantics                         26m13s   2GB
Oct 13 15:44:54 Starting candle/overloading/monadic
Oct 13 15:50:31 Finished candle/overloading/monadic                            5m37s   1GB
Oct 13 15:50:31 Starting candle/overloading/ml_kernel
Oct 13 16:06:05 Finished candle/overloading/ml_kernel                         15m33s   3GB
Oct 13 16:06:05 Starting candle/overloading/ml_checker
Oct 13 16:11:32 Finished candle/overloading/ml_checker                         5m26s   2GB
Oct 13 16:11:32 Starting candle/prover
Oct 13 16:33:40 Finished candle/prover                                        22m07s   3GB
Oct 13 16:33:40 Starting pancake
Oct 13 16:39:55 Finished pancake                                               6m14s   3GB
Oct 13 16:39:55 Starting pancake/ffi
Oct 13 16:39:56 Finished pancake/ffi                                              0s  11MB
Oct 13 16:39:56 Starting pancake/semantics
Oct 13 16:45:00 Finished pancake/semantics                                     5m03s   1GB
Oct 13 16:45:00 Starting pancake/proofs
Oct 13 16:51:10 Finished pancake/proofs                                        6m09s   1GB
Oct 13 16:51:11 Starting characteristic/examples
Oct 13 16:54:28 Finished characteristic/examples                               3m17s   2GB
Oct 13 16:54:28 Starting tutorial/solutions
Oct 13 17:30:03 Finished tutorial/solutions                                   35m33s   8GB
Oct 13 17:30:03 Starting translator/monadic/examples
Oct 13 17:36:48 Finished translator/monadic/examples                           6m44s   2GB
Oct 13 17:36:48 Starting examples
Oct 13 17:56:02 Finished examples                                             19m14s   4GB
Oct 13 17:56:03 Starting examples/compilation/x64
Oct 13 22:30:47 Finished examples/compilation/x64                           4h34m43s  18GB
Oct 13 22:30:47 Starting examples/compilation/x64/proofs
Oct 13 22:34:45 Finished examples/compilation/x64/proofs                       3m57s   3GB
Oct 13 22:34:45 Starting examples/compilation/ag32
Oct 13 23:49:53 Finished examples/compilation/ag32                          1h15m07s  10GB
Oct 13 23:49:53 Starting examples/compilation/ag32/proofs
Oct 13 23:51:38 Finished examples/compilation/ag32/proofs                      1m44s   3GB
Oct 13 23:51:38 Starting examples/compilation/to_word
Oct 13 23:58:14 Finished examples/compilation/to_word                          6m35s   5GB
Oct 13 23:58:14 Starting examples/lpr_checker
Oct 14 00:00:11 Finished examples/lpr_checker                                  1m56s 979MB
Oct 14 00:00:11 Starting examples/lpr_checker/array
Oct 14 01:16:43 Finished examples/lpr_checker/array                         1h16m31s   5GB
Oct 14 01:16:43 Starting examples/lpr_checker/array/compilation
Oct 14 02:42:47 Finished examples/lpr_checker/array/compilation             1h26m03s  50GB
Oct 14 02:42:47 Starting examples/lpr_checker/array/compilation/proofs
Oct 14 02:45:28 Finished examples/lpr_checker/array/compilation/proofs         2m40s   5GB
Oct 14 02:45:28 Starting examples/opentheory
Oct 14 03:08:03 Finished examples/opentheory                                  22m35s   5GB
Oct 14 03:08:04 Starting examples/opentheory
Oct 14 03:08:07 Finished examples/opentheory                                      3s  30MB
Oct 14 03:08:07 Starting examples/opentheory/compilation
Oct 14 04:30:49 Finished examples/opentheory/compilation                    1h22m41s  28GB
Oct 14 04:30:49 Starting examples/opentheory/compilation/proofs
Oct 14 04:32:37 Finished examples/opentheory/compilation/proofs                1m47s   4GB
Oct 14 04:32:37 Starting examples/opentheory/compilation/ag32
Oct 14 05:49:59 Finished examples/opentheory/compilation/ag32               1h17m21s  27GB
Oct 14 05:50:00 Starting examples/opentheory/compilation/ag32/proofs
Oct 14 05:53:35 Finished examples/opentheory/compilation/ag32/proofs           3m35s   5GB
Oct 14 05:53:36 Starting examples/sat_encodings
Oct 14 05:57:22 Finished examples/sat_encodings                                3m46s   1GB
Oct 14 05:57:22 Starting examples/sat_encodings/case_studies
Oct 14 06:00:50 Finished examples/sat_encodings/case_studies                   3m27s 925MB
Oct 14 06:00:50 Starting examples/sat_encodings/translation
Oct 14 06:12:33 Finished examples/sat_encodings/translation                   11m42s   3GB
Oct 14 06:12:33 Starting examples/sat_encodings/translation/compilation
Oct 14 07:37:37 Finished examples/sat_encodings/translation/compilation     1h25m03s  21GB
Oct 14 07:37:38 Starting examples/deflate
Oct 14 07:39:21 Finished examples/deflate                                      1m43s 791MB
Oct 14 07:39:21 Starting examples/deflate/translation
Oct 14 07:42:18 Finished examples/deflate/translation                          2m56s   2GB
Oct 14 07:42:18 Starting examples/deflate/translation/compilation
Oct 14 08:21:20 Finished examples/deflate/translation/compilation             39m01s  13GB
Oct 14 08:21:20 Starting translator/okasaki-examples
Oct 14 08:31:29 Finished translator/okasaki-examples                          10m08s   1GB
Oct 14 08:31:29 Starting translator/other-examples
Oct 14 08:36:19 Finished translator/other-examples                             4m49s   1GB
Oct 14 08:36:19 Starting compiler/parsing/tests
Oct 14 08:37:25 Finished compiler/parsing/tests                                1m05s 599MB
Oct 14 08:37:25 Starting compiler/inference/tests
Oct 14 08:54:01 Finished compiler/inference/tests                             16m35s   5GB
Oct 14 08:54:02 Starting compiler/printing/test
Oct 14 09:00:52 Finished compiler/printing/test                                6m50s   3GB
Oct 14 09:00:53 Starting icing/flover
Oct 14 10:35:23 Finished icing/flover                                       1h34m29s   1GB
Oct 14 10:35:23 Starting icing/
Oct 14 12:51:19 Finished icing/                                             2h15m55s   7GB
Oct 14 12:51:20 Starting icing/examples
Oct 14 12:54:40 Finished icing/examples                                        3m19s   7GB
Oct 14 12:54:40 Starting compiler/repl
Oct 14 13:13:38 Finished compiler/repl                                        18m58s   4GB
Oct 14 13:13:39 Starting unverified/sexpr-bootstrap/x64/64
Oct 14 13:36:56 Finished unverified/sexpr-bootstrap/x64/64                    23m17s  13GB
Oct 14 13:36:57 Starting unverified/sexpr-bootstrap/x64/32
Oct 14 13:55:25 Finished unverified/sexpr-bootstrap/x64/32                    18m28s  11GB
Oct 14 13:55:25 Starting compiler/benchmarks
Oct 14 13:55:31 Finished compiler/benchmarks                                      5s  41MB
Oct 14 13:55:31 Starting compiler/bootstrap/compilation/x64/64
Oct 15 15:15:30 Finished compiler/bootstrap/compilation/x64/64             25h19m58s 100GB
Oct 15 15:15:31 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 15 15:56:01 Finished compiler/bootstrap/compilation/x64/64/proofs         40m29s  22GB
Oct 15 15:56:01 Starting compiler/bootstrap/compilation/x64/32
Oct 16 05:36:12 Finished compiler/bootstrap/compilation/x64/32             13h40m11s  92GB
Oct 16 05:36:13 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 16 05:42:23 Finished compiler/bootstrap/compilation/x64/32/proofs          6m10s  12GB
Oct 16 05:42:23 Starting compiler/bootstrap/compilation/ag32/32
Oct 16 20:33:37 Finished compiler/bootstrap/compilation/ag32/32            14h51m13s 109GB
Oct 16 20:33:37 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 16 20:46:38 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m00s  37GB
Oct 16 20:46:38 SUCCESS