Job 1796

CakeML:42596dd3aaa8b5ce1a7b27086d9b979fe5f7838a
  Fixes following changes to Define in HOL [Feb 24 20:23:43]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 24 20:35:09 Claimed job
Feb 24 20:35:11 Reusing HOL
Feb 24 20:35:23 Starting developers
Feb 24 20:35:27 Finished developers                                               4s 141MB
Feb 24 20:35:27 Starting developers/bin
Feb 24 20:35:32 Finished developers/bin                                           4s 675MB
Feb 24 20:35:32 Starting semantics/ffi
Feb 24 20:35:42 Finished semantics/ffi                                            9s 247MB
Feb 24 20:35:42 Starting semantics
Feb 24 20:37:45 Finished semantics                                             2m02s   1GB
Feb 24 20:37:45 Starting semantics/proofs
Feb 24 20:41:23 Finished semantics/proofs                                      3m37s   1GB
Feb 24 20:41:23 Starting semantics/alt_semantics
Feb 24 20:41:39 Finished semantics/alt_semantics                                 16s 492MB
Feb 24 20:41:39 Starting semantics/alt_semantics/proofs
Feb 24 20:44:07 Finished semantics/alt_semantics/proofs                        2m27s   1GB
Feb 24 20:44:07 Starting basis/pure
Feb 24 20:45:09 Finished basis/pure                                            1m02s 893MB
Feb 24 20:45:09 Starting translator
Feb 24 20:48:11 Finished translator                                            3m01s   1GB
Feb 24 20:48:11 Starting compiler/parsing
Feb 24 20:49:26 Finished compiler/parsing                                      1m14s   2GB
Feb 24 20:49:26 Starting characteristic
Feb 24 20:55:49 Finished characteristic                                        6m22s   1GB
Feb 24 20:55:49 Starting translator/monadic
Feb 24 20:57:43 Finished translator/monadic                                    1m54s   1GB
Feb 24 20:57:44 Starting basis
Feb 24 21:44:24 Finished basis                                                46m39s  15GB
Feb 24 21:44:24 Starting compiler/inference
Feb 24 21:45:44 Finished compiler/inference                                    1m20s   1GB
Feb 24 21:45:44 Starting compiler/backend/reg_alloc
Feb 24 21:47:29 Finished compiler/backend/reg_alloc                            1m44s   2GB
Feb 24 21:47:29 Starting compiler/backend/gc
Feb 24 21:51:47 Finished compiler/backend/gc                                   4m18s   2GB
Feb 24 21:51:48 Starting compiler/backend
Feb 24 21:57:14 Finished compiler/backend                                      5m26s   2GB
Feb 24 21:57:15 Starting compiler/encoders/asm
Feb 24 21:57:45 Finished compiler/encoders/asm                                   30s 702MB
Feb 24 21:57:45 Starting compiler/encoders/x64
Feb 24 21:58:14 Finished compiler/encoders/x64                                   29s   1GB
Feb 24 21:58:14 Starting compiler/encoders/arm7
Feb 24 21:59:09 Finished compiler/encoders/arm7                                  54s 827MB
Feb 24 21:59:09 Starting compiler/encoders/arm8
Feb 24 21:59:25 Finished compiler/encoders/arm8                                  16s 955MB
Feb 24 21:59:26 Starting compiler/encoders/arm8_asl
Feb 24 22:01:58 Finished compiler/encoders/arm8_asl                            2m32s   1GB
Feb 24 22:01:58 Starting compiler/encoders/mips
Feb 24 22:02:19 Finished compiler/encoders/mips                                  21s   1GB
Feb 24 22:02:19 Starting compiler/encoders/riscv
Feb 24 22:02:39 Finished compiler/encoders/riscv                                 19s 843MB
Feb 24 22:02:39 Starting compiler/encoders/ag32
Feb 24 22:03:01 Finished compiler/encoders/ag32                                  21s 675MB
Feb 24 22:03:01 Starting compiler/backend/x64
Feb 24 22:03:24 Finished compiler/backend/x64                                    22s   1GB
Feb 24 22:03:24 Starting compiler/backend/arm7
Feb 24 22:03:47 Finished compiler/backend/arm7                                   23s   1GB
Feb 24 22:03:47 Starting compiler/backend/arm8
Feb 24 22:04:09 Finished compiler/backend/arm8                                   21s   1GB
Feb 24 22:04:09 Starting compiler/backend/mips
Feb 24 22:04:31 Finished compiler/backend/mips                                   22s   1GB
Feb 24 22:04:32 Starting compiler/backend/riscv
Feb 24 22:04:54 Finished compiler/backend/riscv                                  22s   1GB
Feb 24 22:04:54 Starting compiler/backend/ag32
Feb 24 22:06:19 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 24 22:06:19 Starting compiler/parsing/proofs
Feb 24 22:10:03 Finished compiler/parsing/proofs                               3m44s   1GB
Feb 24 22:10:03 Starting compiler/inference/proofs
Feb 24 22:12:36 Finished compiler/inference/proofs                             2m32s   1GB
Feb 24 22:12:36 Starting compiler/backend/semantics
Feb 24 22:41:06 Finished compiler/backend/semantics                           28m30s   1GB
Feb 24 22:41:07 Starting compiler/backend/reg_alloc/proofs
Feb 24 22:44:39 Finished compiler/backend/reg_alloc/proofs                     3m29s   1GB
Feb 24 22:44:40 Starting compiler/backend/proofs
Feb 24 23:36:24 Finished compiler/backend/proofs                              51m43s  18GB
Feb 24 23:36:24 Starting compiler/backend/serialiser
Feb 24 23:38:00 Finished compiler/backend/serialiser                           1m36s   2GB
Feb 24 23:38:00 Starting compiler/encoders/x64/proofs
Feb 24 23:47:35 Finished compiler/encoders/x64/proofs                          9m31s   4GB
Feb 24 23:47:35 Starting compiler/encoders/arm7/proofs
Feb 25 00:00:32 Finished compiler/encoders/arm7/proofs                        12m56s   6GB
Feb 25 00:00:32 Starting compiler/encoders/arm8/proofs
Feb 25 00:07:16 Finished compiler/encoders/arm8/proofs                         6m44s   1GB
Feb 25 00:07:16 Starting compiler/encoders/arm8_asl/proofs
Feb 25 00:22:25 Finished compiler/encoders/arm8_asl/proofs                    15m08s   2GB
Feb 25 00:22:25 Starting compiler/encoders/mips/proofs
Feb 25 00:32:16 Finished compiler/encoders/mips/proofs                         9m50s   2GB
Feb 25 00:32:16 Starting compiler/encoders/riscv/proofs
Feb 25 00:40:53 Finished compiler/encoders/riscv/proofs                        8m37s   1GB
Feb 25 00:40:53 Starting compiler/encoders/ag32/proofs
Feb 25 00:43:28 Finished compiler/encoders/ag32/proofs                         2m34s 814MB
Feb 25 00:43:28 Starting compiler/backend/x64/proofs
Feb 25 00:43:56 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 25 00:43:56 Starting compiler/backend/arm7/proofs
Feb 25 00:44:24 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 25 00:44:24 Starting compiler/backend/arm8/proofs
Feb 25 00:44:52 Finished compiler/backend/arm8/proofs                            27s   1GB
Feb 25 00:44:52 Starting compiler/backend/arm8_asl
Feb 25 00:45:13 Finished compiler/backend/arm8_asl                               21s   1GB
Feb 25 00:45:13 Starting compiler/backend/mips/proofs
Feb 25 00:45:42 Finished compiler/backend/mips/proofs                            28s   1GB
Feb 25 00:45:42 Starting compiler/backend/riscv/proofs
Feb 25 00:46:11 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 25 00:46:11 Starting compiler/backend/ag32/proofs
Feb 25 00:59:30 Finished compiler/backend/ag32/proofs                         13m18s   2GB
Feb 25 00:59:30 Starting compiler/proofs Feb 25 00:59:30 1376s