Job 2088

CakeML:8c8f91d0ab4733db699d2b7b8cd1060ccd0daf3a
  pancake: misc lemmas for pan_to_target proof [Jan 23 22:52:16]
#923 (pan_misc_lemmas)
Merging into:0a80d59e3ef322e4ad28193e97b5d425c5fd2df4
  Merge pull request #922 from CakeML/unzip-fix [Jan 22 17:17:11]
HOL:b449b82bffe8efeaf753c77d8132f37c38d0e1a7
  Undo 27187edc1 [Jan 28 03:02:55]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 31 12:01:31 Claimed job
Jan 31 12:01:38 Building HOL
Jan 31 12:14:04 Starting developers
Jan 31 12:14:09 Finished developers                                               5s 156MB
Jan 31 12:14:09 Starting developers/bin
Jan 31 12:14:15 Finished developers/bin                                           6s   1GB
Jan 31 12:14:15 Starting compiler/proofs
Jan 31 14:04:39 Finished compiler/proofs                                    1h50m22s  17GB
Jan 31 14:04:39 Starting compiler/bootstrap/translation
Jan 31 22:10:49 Finished compiler/bootstrap/translation                     8h06m08s  32GB
Jan 31 22:10:49 Starting semantics/ffi
Jan 31 22:10:55 Finished semantics/ffi                                            6s 222MB
Jan 31 22:10:55 Starting semantics
Jan 31 22:10:57 Finished semantics                                                1s  22MB
Jan 31 22:10:57 Starting semantics/proofs
Jan 31 22:11:29 Finished semantics/proofs                                        32s 722MB
Jan 31 22:11:29 Starting semantics/alt_semantics
Jan 31 22:12:00 Finished semantics/alt_semantics                                 30s 743MB
Jan 31 22:12:00 Starting semantics/alt_semantics/proofs
Jan 31 22:23:53 Finished semantics/alt_semantics/proofs                       11m52s   1GB
Jan 31 22:23:53 Starting basis/pure
Jan 31 22:23:54 Finished basis/pure                                               1s  24MB
Jan 31 22:23:54 Starting translator
Jan 31 22:25:43 Finished translator                                            1m48s   2GB
Jan 31 22:25:43 Starting compiler/parsing
Jan 31 22:25:44 Finished compiler/parsing                                         1s  19MB
Jan 31 22:25:44 Starting characteristic
Jan 31 22:25:46 Finished characteristic                                           1s  29MB
Jan 31 22:25:46 Starting translator/monadic
Jan 31 22:25:48 Finished translator/monadic                                       1s  21MB
Jan 31 22:25:48 Starting basis
Jan 31 22:29:09 Finished basis                                                 3m20s   3GB
Jan 31 22:29:09 Starting compiler/inference
Jan 31 22:29:11 Finished compiler/inference                                       1s  20MB
Jan 31 22:29:11 Starting compiler/backend/reg_alloc
Jan 31 22:29:13 Finished compiler/backend/reg_alloc                               1s  21MB
Jan 31 22:29:13 Starting compiler/backend/gc
Jan 31 22:29:15 Finished compiler/backend/gc                                      2s  27MB
Jan 31 22:29:15 Starting compiler/backend
Jan 31 22:29:28 Finished compiler/backend                                        12s 772MB
Jan 31 22:29:28 Starting compiler/encoders/asm
Jan 31 22:29:29 Finished compiler/encoders/asm                                    1s  25MB
Jan 31 22:29:30 Starting compiler/encoders/x64
Jan 31 22:29:31 Finished compiler/encoders/x64                                    1s  24MB
Jan 31 22:29:31 Starting compiler/encoders/arm7
Jan 31 22:29:33 Finished compiler/encoders/arm7                                   1s  21MB
Jan 31 22:29:33 Starting compiler/encoders/arm8
Jan 31 22:29:35 Finished compiler/encoders/arm8                                   1s  20MB
Jan 31 22:29:35 Starting compiler/encoders/arm8_asl
Feb 01 00:57:55 Finished compiler/encoders/arm8_asl                         2h28m18s  35GB
Feb 01 00:57:55 Starting compiler/encoders/mips
Feb 01 00:57:57 Finished compiler/encoders/mips                                   1s  21MB
Feb 01 00:57:57 Starting compiler/encoders/riscv
Feb 01 00:57:59 Finished compiler/encoders/riscv                                  1s  22MB
Feb 01 00:57:59 Starting compiler/encoders/ag32
Feb 01 00:58:01 Finished compiler/encoders/ag32                                   1s  20MB
Feb 01 00:58:01 Starting compiler/backend/x64
Feb 01 00:58:03 Finished compiler/backend/x64                                     2s  21MB
Feb 01 00:58:03 Starting compiler/backend/arm7
Feb 01 00:58:05 Finished compiler/backend/arm7                                    2s  28MB
Feb 01 00:58:05 Starting compiler/backend/arm8
Feb 01 00:58:08 Finished compiler/backend/arm8                                    2s  22MB
Feb 01 00:58:08 Starting compiler/backend/mips
Feb 01 00:58:10 Finished compiler/backend/mips                                    2s  27MB
Feb 01 00:58:10 Starting compiler/backend/riscv
Feb 01 00:58:12 Finished compiler/backend/riscv                                   2s  23MB
Feb 01 00:58:12 Starting compiler/backend/ag32
Feb 01 00:59:41 Finished compiler/backend/ag32                                 1m28s   1GB
Feb 01 00:59:41 Starting compiler/parsing/proofs
Feb 01 00:59:43 Finished compiler/parsing/proofs                                  1s  18MB
Feb 01 00:59:43 Starting compiler/inference/proofs
Feb 01 00:59:44 Finished compiler/inference/proofs                                1s  20MB
Feb 01 00:59:45 Starting compiler/backend/semantics
Feb 01 01:00:59 Finished compiler/backend/semantics                            1m14s   1GB
Feb 01 01:00:59 Starting compiler/backend/reg_alloc/proofs
Feb 01 01:01:01 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Feb 01 01:01:01 Starting compiler/backend/proofs
Feb 01 01:02:01 Finished compiler/backend/proofs                                 59s   2GB
Feb 01 01:02:01 Starting compiler/backend/serialiser
Feb 01 01:02:04 Finished compiler/backend/serialiser                              2s  40MB
Feb 01 01:02:04 Starting compiler/encoders/x64/proofs
Feb 01 01:12:12 Finished compiler/encoders/x64/proofs                         10m08s   4GB
Feb 01 01:12:12 Starting compiler/encoders/arm7/proofs
Feb 01 01:25:51 Finished compiler/encoders/arm7/proofs                        13m39s   5GB
Feb 01 01:25:51 Starting compiler/encoders/arm8/proofs
Feb 01 01:32:46 Finished compiler/encoders/arm8/proofs                         6m53s   1GB
Feb 01 01:32:46 Starting compiler/encoders/arm8_asl/proofs
Feb 01 02:24:42 Finished compiler/encoders/arm8_asl/proofs                    51m55s   5GB
Feb 01 02:24:42 Starting compiler/encoders/mips/proofs
Feb 01 02:35:17 Finished compiler/encoders/mips/proofs                        10m34s   2GB
Feb 01 02:35:17 Starting compiler/encoders/riscv/proofs
Feb 01 02:44:11 Finished compiler/encoders/riscv/proofs                        8m53s   2GB
Feb 01 02:44:11 Starting compiler/encoders/ag32/proofs
Feb 01 02:46:52 Finished compiler/encoders/ag32/proofs                         2m41s 956MB
Feb 01 02:46:52 Starting compiler/backend/x64/proofs
Feb 01 02:47:23 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 01 02:47:23 Starting compiler/backend/arm7/proofs
Feb 01 02:47:56 Finished compiler/backend/arm7/proofs                            32s   2GB
Feb 01 02:47:56 Starting compiler/backend/arm8/proofs
Feb 01 02:48:28 Finished compiler/backend/arm8/proofs                            31s   2GB
Feb 01 02:48:28 Starting compiler/backend/arm8_asl
Feb 01 02:48:52 Finished compiler/backend/arm8_asl                               24s   2GB
Feb 01 02:48:52 Starting compiler/backend/mips/proofs
Feb 01 02:49:24 Finished compiler/backend/mips/proofs                            31s   1GB
Feb 01 02:49:24 Starting compiler/backend/riscv/proofs
Feb 01 02:49:57 Finished compiler/backend/riscv/proofs                           33s   2GB
Feb 01 02:49:58 Starting compiler/backend/ag32/proofs
Feb 01 03:03:34 Finished compiler/backend/ag32/proofs                         13m36s   3GB
Feb 01 03:03:34 Starting candle/set-theory
Feb 01 03:04:13 Finished candle/set-theory                                       38s   1GB
Feb 01 03:04:13 Starting candle/syntax-lib
Feb 01 03:04:15 Finished candle/syntax-lib                                        1s  17MB
Feb 01 03:04:15 Starting candle/standard/syntax
Feb 01 03:04:26 Finished candle/standard/syntax                                  10s 769MB
Feb 01 03:04:26 Starting candle/standard/semantics
Feb 01 03:06:25 Finished candle/standard/semantics                             1m58s   1GB
Feb 01 03:06:25 Starting candle/standard/monadic
Feb 01 03:06:27 Finished candle/standard/monadic                                  1s  28MB
Feb 01 03:06:27 Starting candle/standard/ml_kernel
Feb 01 03:08:03 Finished candle/standard/ml_kernel                             1m36s   2GB
Feb 01 03:08:03 Starting candle/overloading/syntax
Feb 01 03:11:26 Finished candle/overloading/syntax                             3m22s   1GB
Feb 01 03:11:26 Starting candle/overloading/semantics
Feb 01 03:23:32 Finished candle/overloading/semantics                         12m05s   2GB
Feb 01 03:23:32 Starting candle/overloading/monadic
Feb 01 03:26:15 Finished candle/overloading/monadic                            2m41s   1GB
Feb 01 03:26:15 Starting candle/overloading/ml_kernel
Feb 01 03:34:05 Finished candle/overloading/ml_kernel                          7m50s   3GB
Feb 01 03:34:06 Starting candle/overloading/ml_checker
Feb 01 03:36:41 Finished candle/overloading/ml_checker                         2m35s   3GB
Feb 01 03:36:41 Starting candle/prover
Feb 01 03:46:26 Finished candle/prover                                         9m44s   3GB
Feb 01 03:46:26 Starting pancake
Feb 01 03:49:54 Finished pancake                                               3m27s   4GB
Feb 01 03:49:54 Starting pancake/ffi
Feb 01 03:49:55 Finished pancake/ffi                                              0s  13MB
Feb 01 03:49:55 Starting pancake/semantics
Feb 01 03:52:26 Finished pancake/semantics                                     2m30s   1GB
Feb 01 03:52:26 Starting pancake/proofs
Feb 01 03:56:44 Finished pancake/proofs                                        4m17s   2GB
Feb 01 03:56:44 Starting characteristic/examples
Feb 01 03:58:17 Finished characteristic/examples                               1m33s   2GB
Feb 01 03:58:17 Starting tutorial/solutions
Feb 01 04:13:19 Finished tutorial/solutions                                   15m01s   9GB
Feb 01 04:13:19 Starting translator/monadic/examples
Feb 01 04:17:21 Finished translator/monadic/examples                           4m01s   3GB
Feb 01 04:17:21 Starting examples
Feb 01 04:33:23 Finished examples                                             16m00s   4GB
Feb 01 04:33:23 Starting examples/compilation/x64
Feb 01 06:32:27 Finished examples/compilation/x64                           1h59m03s  14GB
Feb 01 06:32:27 Starting examples/compilation/x64/proofs
Feb 01 06:35:01 Finished examples/compilation/x64/proofs                       2m33s   4GB
Feb 01 06:35:01 Starting examples/compilation/ag32
Feb 01 07:05:45 Finished examples/compilation/ag32                            30m43s   7GB
Feb 01 07:05:45 Starting examples/compilation/ag32/proofs
Feb 01 07:06:47 Finished examples/compilation/ag32/proofs                      1m02s   5GB
Feb 01 07:06:47 Starting examples/compilation/to_word
Feb 01 07:10:04 Finished examples/compilation/to_word                          3m16s   6GB
Feb 01 07:10:04 Starting examples/lpr_checker
Feb 01 07:11:08 Finished examples/lpr_checker                                  1m04s   1GB
Feb 01 07:11:09 Starting examples/lpr_checker/array
Feb 01 07:46:10 Finished examples/lpr_checker/array                           35m00s   6GB
Feb 01 07:46:10 Starting examples/lpr_checker/array/compilation
Feb 01 08:24:18 Finished examples/lpr_checker/array/compilation               38m07s  24GB
Feb 01 08:24:18 Starting examples/lpr_checker/array/compilation/proofs
Feb 01 08:25:50 Finished examples/lpr_checker/array/compilation/proofs         1m31s   7GB
Feb 01 08:25:50 Starting examples/opentheory
Feb 01 08:36:48 Finished examples/opentheory                                  10m58s   3GB
Feb 01 08:36:48 Starting examples/opentheory
Feb 01 08:36:50 Finished examples/opentheory                                      1s  30MB
Feb 01 08:36:50 Starting examples/opentheory/compilation
Feb 01 09:14:07 Finished examples/opentheory/compilation                      37m14s  32GB
Feb 01 09:14:07 Starting examples/opentheory/compilation/proofs
Feb 01 09:15:09 Finished examples/opentheory/compilation/proofs                1m02s   4GB
Feb 01 09:15:09 Starting examples/opentheory/compilation/ag32
Feb 01 09:48:04 Finished examples/opentheory/compilation/ag32                 32m54s  28GB
Feb 01 09:48:04 Starting examples/opentheory/compilation/ag32/proofs
Feb 01 09:49:54 Finished examples/opentheory/compilation/ag32/proofs           1m49s   6GB
Feb 01 09:49:54 Starting examples/sat_encodings
Feb 01 09:51:53 Finished examples/sat_encodings                                1m59s 876MB
Feb 01 09:51:53 Starting examples/sat_encodings/case_studies
Feb 01 09:53:41 Finished examples/sat_encodings/case_studies                   1m47s 965MB
Feb 01 09:53:41 Starting examples/sat_encodings/translation Feb 01 09:53:41 412s