Job 2013

CakeML: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:stove+4.15.0-143-generic+x86_64+GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Oct 11 22:29:53 Claimed job
Oct 11 22:29:59 Building+HOL
Oct 11 22:41:21 Starting+developers
Oct 11 22:41:26 Finished+developers++++++++++++++++++++++++++++++++++++++++5.13+131352
Oct 11 22:41:26 Starting+developers/bin
Oct 11 22:41:32 Finished+developers/bin++++++++++++++++++++++++++++++++++++5.89+1244216
Oct 11 22:41:33 Starting+compiler/proofs
Oct 12 00:28:36 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++6421.05+15927852
Oct 12 00:28:36 Starting+compiler/bootstrap/translation
Oct 12 05:23:43 Finished+compiler/bootstrap/translation++++++++++++++++++++17705.70+64394360
Oct 12 05:23:43 Starting+semantics/ffi
Oct 12 05:23:48 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++4.72+142284
Oct 12 05:23:49 Starting+semantics
Oct 12 05:23:50 Finished+semantics+++++++++++++++++++++++++++++++++++++++++1.44+19024
Oct 12 05:23:50 Starting+semantics/proofs
Oct 12 05:24:21 Finished+semantics/proofs++++++++++++++++++++++++++++++++++31.13+855284
Oct 12 05:24:22 Starting+semantics/alt_semantics
Oct 12 05:24:49 Finished+semantics/alt_semantics+++++++++++++++++++++++++++27.35+526208
Oct 12 05:24:49 Starting+semantics/alt_semantics/proofs
Oct 12 05:36:25 Finished+semantics/alt_semantics/proofs++++++++++++++++++++695.23+1889732
Oct 12 05:36:25 Starting+basis/pure
Oct 12 05:36:26 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++1.50+19520
Oct 12 05:36:27 Starting+translator
Oct 12 05:38:13 Finished+translator++++++++++++++++++++++++++++++++++++++++106.34+1746364
Oct 12 05:38:13 Starting+compiler/parsing
Oct 12 05:38:15 Finished+compiler/parsing++++++++++++++++++++++++++++++++++1.50+17632
Oct 12 05:38:15 Starting+characteristic
Oct 12 05:38:17 Finished+characteristic++++++++++++++++++++++++++++++++++++1.85+20516
Oct 12 05:38:17 Starting+translator/monadic
Oct 12 05:38:19 Finished+translator/monadic++++++++++++++++++++++++++++++++1.74+30212
Oct 12 05:38:19 Starting+basis
Oct 12 05:41:46 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++206.41+2852692
Oct 12 05:41:46 Starting+compiler/inference
Oct 12 05:41:48 Finished+compiler/inference++++++++++++++++++++++++++++++++1.57+30696
Oct 12 05:41:48 Starting+compiler/backend/reg_alloc
Oct 12 05:41:49 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++1.43+18876
Oct 12 05:41:49 Starting+compiler/backend/gc
Oct 12 05:41:52 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++2.14+34784
Oct 12 05:41:52 Starting+compiler/backend
Oct 12 05:42:03 Finished+compiler/backend++++++++++++++++++++++++++++++++++10.90+677188
Oct 12 05:42:03 Starting+compiler/encoders/asm
Oct 12 05:42:05 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++1.65+20020
Oct 12 05:42:05 Starting+compiler/encoders/x64
Oct 12 05:42:07 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++1.64+33172
Oct 12 05:42:07 Starting+compiler/encoders/arm7
Oct 12 05:42:09 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++1.67+23480
Oct 12 05:42:09 Starting+compiler/encoders/arm8
Oct 12 05:42:11 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++1.67+19860
Oct 12 05:42:11 Starting+compiler/encoders/arm8_asl
Oct 12 08:03:53 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++8501.51+44363740
Oct 12 08:03:54 Starting+compiler/encoders/mips
Oct 12 08:03:55 Finished+compiler/encoders/mips++++++++++++++++++++++++++++1.66+20116
Oct 12 08:03:55 Starting+compiler/encoders/riscv
Oct 12 08:03:57 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++1.69+29896
Oct 12 08:03:57 Starting+compiler/encoders/ag32
Oct 12 08:03:59 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++1.66+20772
Oct 12 08:03:59 Starting+compiler/backend/x64
Oct 12 08:04:02 Finished+compiler/backend/x64++++++++++++++++++++++++++++++2.03+33888
Oct 12 08:04:02 Starting+compiler/backend/arm7
Oct 12 08:04:04 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++2.03+34760
Oct 12 08:04:04 Starting+compiler/backend/arm8
Oct 12 08:04:06 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++2.01+34996
Oct 12 08:04:06 Starting+compiler/backend/mips
Oct 12 08:04:09 Finished+compiler/backend/mips+++++++++++++++++++++++++++++2.02+34908
Oct 12 08:04:09 Starting+compiler/backend/riscv
Oct 12 08:04:11 Finished+compiler/backend/riscv++++++++++++++++++++++++++++2.00+34828
Oct 12 08:04:11 Starting+compiler/backend/ag32
Oct 12 08:05:37 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++86.16+1434316
Oct 12 08:05:37 Starting+compiler/parsing/proofs
Oct 12 08:05:39 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++1.54+33928
Oct 12 08:05:39 Starting+compiler/inference/proofs
Oct 12 08:05:41 Finished+compiler/inference/proofs+++++++++++++++++++++++++1.69+35104
Oct 12 08:05:41 Starting+compiler/backend/semantics
Oct 12 08:06:47 Finished+compiler/backend/semantics++++++++++++++++++++++++65.70+1516940
Oct 12 08:06:47 Starting+compiler/backend/reg_alloc/proofs
Oct 12 08:06:49 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++1.80+35160
Oct 12 08:06:49 Starting+compiler/backend/proofs
Oct 12 08:07:43 Finished+compiler/backend/proofs+++++++++++++++++++++++++++53.34+2982828
Oct 12 08:07:43 Starting+compiler/backend/serialiser
Oct 12 08:07:46 Finished+compiler/backend/serialiser+++++++++++++++++++++++2.64+34788
Oct 12 08:07:46 Starting+compiler/encoders/x64/proofs
Oct 12 08:17:33 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++587.38+5954528
Oct 12 08:17:34 Starting+compiler/encoders/arm7/proofs
Oct 12 08:31:09 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++815.12+5452280
Oct 12 08:31:09 Starting+compiler/encoders/arm8/proofs
Oct 12 08:38:15 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++425.64+1383852
Oct 12 08:38:15 Starting+compiler/encoders/arm8_asl/proofs
Oct 12 09:30:03 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++3105.29+9837156
Oct 12 09:30:04 Starting+compiler/encoders/mips/proofs
Oct 12 09:40:36 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++631.29+2934788
Oct 12 09:40:36 Starting+compiler/encoders/riscv/proofs
Oct 12 09:49:46 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++549.47+1225584
Oct 12 09:49:46 Starting+compiler/encoders/ag32/proofs
Oct 12 09:52:29 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++163.16+759080
Oct 12 09:52:29 Starting+compiler/backend/x64/proofs
Oct 12 09:52:55 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++25.33+1686304
Oct 12 09:52:55 Starting+compiler/backend/arm7/proofs
Oct 12 09:53:22 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++26.95+1445732
Oct 12 09:53:22 Starting+compiler/backend/arm8/proofs
Oct 12 09:53:49 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++26.41+1624576
Oct 12 09:53:49 Starting+compiler/backend/arm8_asl
Oct 12 09:54:09 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++19.97+1308444
Oct 12 09:54:09 Starting+compiler/backend/mips/proofs
Oct 12 09:54:36 Finished+compiler/backend/mips/proofs++++++++++++++++++++++26.27+2190968
Oct 12 09:54:36 Starting+compiler/backend/riscv/proofs
Oct 12 09:55:03 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++27.09+1711820
Oct 12 09:55:03 Starting+compiler/backend/ag32/proofs
Oct 12 10:08:32 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++808.79+2611256
Oct 12 10:08:33 Starting+candle/set-theory
Oct 12 10:09:07 Finished+candle/set-theory+++++++++++++++++++++++++++++++++34.44+1059252
Oct 12 10:09:07 Starting+candle/syntax-lib
Oct 12 10:09:09 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++1.45+34820
Oct 12 10:09:09 Starting+candle/standard/syntax
Oct 12 10:09:18 Finished+candle/standard/syntax++++++++++++++++++++++++++++8.90+559236
Oct 12 10:09:18 Starting+candle/standard/semantics
Oct 12 10:11:02 Finished+candle/standard/semantics+++++++++++++++++++++++++103.48+1159896
Oct 12 10:11:02 Starting+candle/standard/monadic
Oct 12 10:11:04 Finished+candle/standard/monadic+++++++++++++++++++++++++++1.79+34664
Oct 12 10:11:04 Starting+candle/standard/ml_kernel
Oct 12 10:12:34 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++89.24+2580284
Oct 12 10:12:34 Starting+candle/overloading/syntax
Oct 12 10:44:48 Resuming candle/overloading/syntax
Oct 12 10:45:49 Finished candle/overloading/syntax                             1m01s   1GB
Oct 12 10:45:49 Starting candle/overloading/semantics
Oct 12 10:57:53 Finished candle/overloading/semantics                         12m03s   2GB
Oct 12 10:57:53 Starting candle/overloading/monadic
Oct 12 11:00:31 Finished candle/overloading/monadic                            2m38s   2GB
Oct 12 11:00:31 Starting candle/overloading/ml_kernel
Oct 12 11:07:59 Finished candle/overloading/ml_kernel                          7m27s   4GB
Oct 12 11:07:59 Starting candle/overloading/ml_checker
Oct 12 11:10:31 Finished candle/overloading/ml_checker                         2m31s   3GB
Oct 12 11:10:31 Starting candle/prover
Oct 12 11:20:05 Finished candle/prover                                         9m33s   3GB
Oct 12 11:20:05 Starting pancake
Oct 12 11:23:09 Finished pancake                                               3m03s   2GB
Oct 12 11:23:09 Starting pancake/ffi
Oct 12 11:23:10 Finished pancake/ffi                                              0s  13MB
Oct 12 11:23:10 Starting pancake/semantics
Oct 12 11:25:33 Finished pancake/semantics                                     2m23s   1GB
Oct 12 11:25:34 Starting pancake/proofs
Oct 12 11:37:50 Finished pancake/proofs                                       12m16s   5GB
Oct 12 11:37:50 Starting characteristic/examples
Oct 12 11:39:18 Finished characteristic/examples                               1m27s   2GB
Oct 12 11:39:18 Starting tutorial/solutions
Oct 12 11:55:28 Finished tutorial/solutions                                   16m09s   8GB
Oct 12 11:55:28 Starting translator/monadic/examples
Oct 12 11:59:14 Finished translator/monadic/examples                           3m45s   2GB
Oct 12 11:59:14 Starting examples
Oct 12 12:09:22 Finished examples                                             10m07s   4GB
Oct 12 12:09:23 Starting examples/compilation/x64
Oct 12 14:15:39 Finished examples/compilation/x64                           2h06m14s  14GB
Oct 12 14:15:40 Starting examples/compilation/x64/proofs
Oct 12 14:17:59 Finished examples/compilation/x64/proofs                       2m19s   3GB
Oct 12 14:17:59 Starting examples/compilation/ag32
Oct 12 14:51:58 Finished examples/compilation/ag32                            33m58s   8GB
Oct 12 14:51:58 Starting examples/compilation/ag32/proofs
Oct 12 14:52:50 Finished examples/compilation/ag32/proofs                        51s   3GB
Oct 12 14:52:50 Starting examples/compilation/to_word
Oct 12 14:55:51 Finished examples/compilation/to_word                          3m01s   6GB
Oct 12 14:55:52 Starting examples/lpr_checker
Oct 12 14:56:49 Finished examples/lpr_checker                                    57s   1GB
Oct 12 14:56:50 Starting examples/lpr_checker/array
Oct 12 15:30:15 Finished examples/lpr_checker/array                           33m24s  10GB
Oct 12 15:30:15 Starting examples/lpr_checker/array/compilation
Oct 12 16:09:31 Finished examples/lpr_checker/array/compilation               39m15s  31GB
Oct 12 16:09:31 Starting examples/lpr_checker/array/compilation/proofs
Oct 12 16:10:51 Finished examples/lpr_checker/array/compilation/proofs         1m19s   6GB
Oct 12 16:10:51 Starting examples/opentheory
Oct 12 16:21:07 Finished examples/opentheory                                  10m15s   5GB
Oct 12 16:21:07 Starting examples/opentheory
Oct 12 16:21:09 Finished examples/opentheory                                      1s  35MB
Oct 12 16:21:09 Starting examples/opentheory/compilation
Oct 12 16:58:33 Finished examples/opentheory/compilation                      37m22s  27GB
Oct 12 16:58:33 Starting examples/opentheory/compilation/proofs
Oct 12 16:59:40 Finished examples/opentheory/compilation/proofs                1m06s   3GB
Oct 12 16:59:40 Starting examples/opentheory/compilation/ag32
Oct 12 17:34:30 Finished examples/opentheory/compilation/ag32                 34m50s  32GB
Oct 12 17:34:30 Starting examples/opentheory/compilation/ag32/proofs
Oct 12 17:36:54 Finished examples/opentheory/compilation/ag32/proofs           2m22s   2GB
Oct 12 17:36:54 Starting examples/sat_encodings
Oct 12 17:38:42 Finished examples/sat_encodings                                1m47s 774MB
Oct 12 17:38:42 Starting examples/sat_encodings/case_studies
Oct 12 17:40:20 Finished examples/sat_encodings/case_studies                   1m37s 776MB
Oct 12 17:40:20 Starting examples/sat_encodings/translation
Oct 12 17:46:05 Finished examples/sat_encodings/translation                    5m45s   5GB
Oct 12 17:46:06 Starting examples/sat_encodings/translation/compilation
Oct 12 18:33:27 Finished examples/sat_encodings/translation/compilation       47m20s  19GB
Oct 12 18:33:27 Starting examples/deflate
Oct 12 18:34:20 Finished examples/deflate                                        52s 827MB
Oct 12 18:34:20 Starting examples/deflate/translation
Oct 12 18:35:51 Finished examples/deflate/translation                          1m30s   2GB
Oct 12 18:35:51 Starting examples/deflate/translation/compilation
Oct 12 18:56:56 Finished examples/deflate/translation/compilation             21m04s  13GB
Oct 12 18:56:56 Starting translator/okasaki-examples
Oct 12 19:01:54 Finished translator/okasaki-examples                           4m57s   2GB
Oct 12 19:01:54 Starting translator/other-examples
Oct 12 19:04:17 Finished translator/other-examples                             2m22s   1GB
Oct 12 19:04:17 Starting compiler/parsing/tests
Oct 12 19:04:47 Finished compiler/parsing/tests                                  30s 695MB
Oct 12 19:04:47 Starting compiler/inference/tests
Oct 12 19:13:20 Finished compiler/inference/tests                              8m32s   3GB
Oct 12 19:13:20 Starting compiler/printing/test
Oct 12 19:16:47 Finished compiler/printing/test                                3m26s   3GB
Oct 12 19:16:47 Starting icing/flover
Oct 12 20:01:46 Finished icing/flover                                         44m57s   1GB
Oct 12 20:01:46 Starting icing/
Oct 12 21:01:31 Finished icing/                                               59m45s   8GB
Oct 12 21:01:31 Starting icing/examples
Oct 12 21:03:15 Finished icing/examples                                        1m42s   4GB
Oct 12 21:03:15 Starting compiler/repl
Oct 12 21:11:31 Finished compiler/repl                                         8m16s   4GB
Oct 12 21:11:31 Starting unverified/sexpr-bootstrap/x64/64
Oct 12 21:23:58 Finished unverified/sexpr-bootstrap/x64/64                    12m25s  13GB
Oct 12 21:23:58 Starting unverified/sexpr-bootstrap/x64/32
Oct 12 21:34:01 Finished unverified/sexpr-bootstrap/x64/32                    10m02s  11GB
Oct 12 21:34:01 Starting compiler/benchmarks
Oct 12 21:34:05 Finished compiler/benchmarks                                      4s  39MB
Oct 12 21:34:05 Starting compiler/bootstrap/compilation/x64/64
Oct 13 09:05:42 Finished compiler/bootstrap/compilation/x64/64             11h31m35s  64GB
Oct 13 09:05:42 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 13 09:24:10 Finished compiler/bootstrap/compilation/x64/64/proofs         18m28s  25GB
Oct 13 09:24:10 Starting compiler/bootstrap/compilation/x64/32
Oct 13 15:56:34 Finished compiler/bootstrap/compilation/x64/32              6h32m21s  63GB
Oct 13 15:56:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 13 15:59:26 Finished compiler/bootstrap/compilation/x64/32/proofs          2m52s  14GB
Oct 13 15:59:27 Starting compiler/bootstrap/compilation/ag32/32
Oct 13 22:43:01 Finished compiler/bootstrap/compilation/ag32/32             6h43m33s  64GB
Oct 13 22:43:01 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 13 22:49:05 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m03s  26GB
Oct 13 22:49:05 SUCCESS