Job 2090

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

Feb 02 18:57:55 Claimed job
Feb 02 18:57:58 Reusing HOL
Feb 02 18:58:38 Starting developers
Feb 02 18:58:43 Finished developers                                               5s 136MB
Feb 02 18:58:43 Starting developers/bin
Feb 02 18:58:50 Finished developers/bin                                           6s   1GB
Feb 02 18:58:50 Starting compiler/proofs
Feb 02 20:46:46 Finished compiler/proofs                                    1h47m55s  17GB
Feb 02 20:46:47 Starting compiler/bootstrap/translation
Feb 03 04:10:44 Finished compiler/bootstrap/translation                     7h23m56s  37GB
Feb 03 04:10:44 Starting semantics/ffi
Feb 03 04:10:49 Finished semantics/ffi                                            4s 437MB
Feb 03 04:10:49 Starting semantics
Feb 03 04:10:50 Finished semantics                                                1s  19MB
Feb 03 04:10:50 Starting semantics/proofs
Feb 03 04:11:25 Finished semantics/proofs                                        34s   1GB
Feb 03 04:11:25 Starting semantics/alt_semantics
Feb 03 04:11:56 Finished semantics/alt_semantics                                 30s 879MB
Feb 03 04:11:56 Starting semantics/alt_semantics/proofs
Feb 03 04:23:46 Finished semantics/alt_semantics/proofs                       11m49s   1GB
Feb 03 04:23:46 Starting basis/pure
Feb 03 04:23:48 Finished basis/pure                                               1s  23MB
Feb 03 04:23:48 Starting translator
Feb 03 04:25:38 Finished translator                                            1m50s   1GB
Feb 03 04:25:38 Starting compiler/parsing
Feb 03 04:25:40 Finished compiler/parsing                                         1s  25MB
Feb 03 04:25:40 Starting characteristic
Feb 03 04:25:42 Finished characteristic                                           1s  23MB
Feb 03 04:25:42 Starting translator/monadic
Feb 03 04:25:44 Finished translator/monadic                                       1s  21MB
Feb 03 04:25:45 Starting basis
Feb 03 04:29:11 Finished basis                                                 3m26s   2GB
Feb 03 04:29:11 Starting compiler/inference
Feb 03 04:29:13 Finished compiler/inference                                       1s  19MB
Feb 03 04:29:13 Starting compiler/backend/reg_alloc
Feb 03 04:29:15 Finished compiler/backend/reg_alloc                               1s  20MB
Feb 03 04:29:15 Starting compiler/backend/gc
Feb 03 04:29:17 Finished compiler/backend/gc                                      2s  28MB
Feb 03 04:29:17 Starting compiler/backend
Feb 03 04:29:30 Finished compiler/backend                                        12s 773MB
Feb 03 04:29:30 Starting compiler/encoders/asm
Feb 03 04:29:32 Finished compiler/encoders/asm                                    1s  22MB
Feb 03 04:29:32 Starting compiler/encoders/x64
Feb 03 04:29:33 Finished compiler/encoders/x64                                    1s  21MB
Feb 03 04:29:34 Starting compiler/encoders/arm7
Feb 03 04:29:35 Finished compiler/encoders/arm7                                   1s  26MB
Feb 03 04:29:35 Starting compiler/encoders/arm8
Feb 03 04:29:37 Finished compiler/encoders/arm8                                   1s  20MB
Feb 03 04:29:37 Starting compiler/encoders/arm8_asl
Feb 03 04:32:53 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Feb 03 04:32:53 Starting compiler/encoders/mips
Feb 03 04:32:54 Finished compiler/encoders/mips                                   1s  20MB
Feb 03 04:32:55 Starting compiler/encoders/riscv
Feb 03 04:32:56 Finished compiler/encoders/riscv                                  1s  25MB
Feb 03 04:32:57 Starting compiler/encoders/ag32
Feb 03 04:32:58 Finished compiler/encoders/ag32                                   1s  19MB
Feb 03 04:32:58 Starting compiler/backend/x64
Feb 03 04:33:01 Finished compiler/backend/x64                                     2s  29MB
Feb 03 04:33:01 Starting compiler/backend/arm7
Feb 03 04:33:03 Finished compiler/backend/arm7                                    2s  29MB
Feb 03 04:33:03 Starting compiler/backend/arm8
Feb 03 04:33:05 Finished compiler/backend/arm8                                    2s  25MB
Feb 03 04:33:05 Starting compiler/backend/mips
Feb 03 04:33:08 Finished compiler/backend/mips                                    2s  25MB
Feb 03 04:33:08 Starting compiler/backend/riscv
Feb 03 04:33:10 Finished compiler/backend/riscv                                   2s  23MB
Feb 03 04:33:10 Starting compiler/backend/ag32
Feb 03 04:34:37 Finished compiler/backend/ag32                                 1m26s   1GB
Feb 03 04:34:37 Starting compiler/parsing/proofs
Feb 03 04:34:39 Finished compiler/parsing/proofs                                  1s  18MB
Feb 03 04:34:39 Starting compiler/inference/proofs
Feb 03 04:34:41 Finished compiler/inference/proofs                                1s  20MB
Feb 03 04:34:41 Starting compiler/backend/semantics
Feb 03 04:35:55 Finished compiler/backend/semantics                            1m13s   1GB
Feb 03 04:35:55 Starting compiler/backend/reg_alloc/proofs
Feb 03 04:35:57 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Feb 03 04:35:57 Starting compiler/backend/proofs Feb 03 04:35:57 54s