CakeML Regression Test

Job 1420

CakeML:38e03fa709c0a30200ee5542b1ebedf4a4e61b30
  fix broken proofs in backend/ [Dec 28 16:15:23]
HOL:5921a959757a023b13010b448a2cd05222e641b6
  Prove the converse of PERM_BIJ [Dec 27 00:55:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 28 16:30:11 Claimed job
Dec 28 16:30:18 Building HOL
Dec 28 16:44:09 Starting developers
Dec 28 16:44:11 Finished developers                                               2s  86MB
Dec 28 16:44:11 Starting developers/bin
Dec 28 16:44:17 Finished developers/bin                                           5s   1GB
Dec 28 16:44:17 Starting semantics/ffi
Dec 28 16:44:27 Finished semantics/ffi                                            9s 284MB
Dec 28 16:44:27 Starting semantics
Dec 28 16:46:00 Finished semantics                                             1m32s   1GB
Dec 28 16:46:01 Starting semantics/proofs
Dec 28 16:49:21 Finished semantics/proofs                                      3m19s   1GB
Dec 28 16:49:21 Starting semantics/alt_semantics
Dec 28 16:49:28 Finished semantics/alt_semantics                                  7s 415MB
Dec 28 16:49:29 Starting semantics/alt_semantics/proofs
Dec 28 16:51:37 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Dec 28 16:51:37 Starting basis/pure
Dec 28 16:54:19 Finished basis/pure                                            2m42s   1GB
Dec 28 16:54:19 Starting translator
Dec 28 16:56:57 Finished translator                                            2m37s   2GB
Dec 28 16:56:58 Starting compiler/parsing
Dec 28 16:58:06 Finished compiler/parsing                                      1m08s   3GB
Dec 28 16:58:06 Starting characteristic
Dec 28 17:04:01 Finished characteristic                                        5m54s   3GB
Dec 28 17:04:01 Starting translator/monadic
Dec 28 17:05:48 Finished translator/monadic                                    1m47s   2GB
Dec 28 17:05:49 Starting basis
Dec 28 17:38:54 Finished basis                                                33m04s  21GB
Dec 28 17:38:54 Starting compiler/inference
Dec 28 17:40:02 Finished compiler/inference                                    1m08s   1GB
Dec 28 17:40:02 Starting compiler/backend/reg_alloc
Dec 28 17:41:06 Finished compiler/backend/reg_alloc                            1m03s   1GB
Dec 28 17:41:06 Starting compiler/backend/gc
Dec 28 17:44:41 Finished compiler/backend/gc                                   3m34s   3GB
Dec 28 17:44:41 Starting compiler/backend
Dec 28 17:49:43 Finished compiler/backend                                      5m01s   5GB
Dec 28 17:49:43 Starting compiler/encoders/asm
Dec 28 17:50:04 Finished compiler/encoders/asm                                   21s 997MB
Dec 28 17:50:05 Starting compiler/encoders/x64
Dec 28 17:51:06 Finished compiler/encoders/x64                                 1m01s   1GB
Dec 28 17:51:06 Starting compiler/encoders/arm7
Dec 28 17:53:08 Finished compiler/encoders/arm7                                2m01s   1GB
Dec 28 17:53:09 Starting compiler/encoders/arm8
Dec 28 17:53:47 Finished compiler/encoders/arm8                                  38s   1GB
Dec 28 17:53:47 Starting compiler/encoders/mips
Dec 28 17:55:11 Finished compiler/encoders/mips                                1m23s   1GB
Dec 28 17:55:11 Starting compiler/encoders/riscv
Dec 28 17:56:47 Finished compiler/encoders/riscv                               1m35s   1GB
Dec 28 17:56:47 Starting compiler/encoders/ag32
Dec 28 17:57:06 Finished compiler/encoders/ag32                                  18s 962MB
Dec 28 17:57:06 Starting compiler/backend/x64
Dec 28 17:57:24 Finished compiler/backend/x64                                    17s   1GB
Dec 28 17:57:24 Starting compiler/backend/arm7
Dec 28 17:57:46 Finished compiler/backend/arm7                                   21s   1GB
Dec 28 17:57:46 Starting compiler/backend/arm8
Dec 28 17:58:06 Finished compiler/backend/arm8                                   19s   1GB
Dec 28 17:58:06 Starting compiler/backend/mips
Dec 28 17:58:26 Finished compiler/backend/mips                                   20s   1GB
Dec 28 17:58:27 Starting compiler/backend/riscv
Dec 28 17:58:48 Finished compiler/backend/riscv                                  21s   1GB
Dec 28 17:58:48 Starting compiler/backend/ag32
Dec 28 17:59:59 Finished compiler/backend/ag32                                 1m10s   1GB
Dec 28 17:59:59 Starting compiler/parsing/proofs
Dec 28 18:05:29 Finished compiler/parsing/proofs                               5m29s   2GB
Dec 28 18:05:29 Starting compiler/inference/proofs
Dec 28 18:08:01 Finished compiler/inference/proofs                             2m31s   2GB
Dec 28 18:08:01 Starting compiler/backend/semantics
Dec 28 18:34:54 Finished compiler/backend/semantics                           26m52s   4GB
Dec 28 18:34:54 Starting compiler/backend/reg_alloc/proofs
Dec 28 18:38:14 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
Dec 28 18:38:14 Starting compiler/backend/proofs
Dec 28 19:32:14 Finished compiler/backend/proofs                              54m00s  27GB
Dec 28 19:32:14 Starting compiler/encoders/x64/proofs
Dec 28 19:41:37 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Dec 28 19:41:37 Starting compiler/encoders/arm7/proofs
Dec 28 19:54:22 Finished compiler/encoders/arm7/proofs                        12m45s   4GB
Dec 28 19:54:22 Starting compiler/encoders/arm8/proofs
Dec 28 20:00:46 Finished compiler/encoders/arm8/proofs                         6m23s   3GB
Dec 28 20:00:46 Starting compiler/encoders/mips/proofs
Dec 28 20:10:43 Finished compiler/encoders/mips/proofs                         9m57s   3GB
Dec 28 20:10:43 Starting compiler/encoders/riscv/proofs
Dec 28 20:19:08 Finished compiler/encoders/riscv/proofs                        8m24s   4GB
Dec 28 20:19:08 Starting compiler/encoders/ag32/proofs
Dec 28 20:21:31 Finished compiler/encoders/ag32/proofs                         2m22s   1GB
Dec 28 20:21:31 Starting compiler/backend/x64/proofs
Dec 28 20:21:53 Finished compiler/backend/x64/proofs                             22s   1GB
Dec 28 20:21:53 Starting compiler/backend/arm7/proofs
Dec 28 20:22:16 Finished compiler/backend/arm7/proofs                            22s   1GB
Dec 28 20:22:16 Starting compiler/backend/arm8/proofs
Dec 28 20:22:36 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 28 20:22:36 Starting compiler/backend/mips/proofs
Dec 28 20:22:58 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 28 20:22:58 Starting compiler/backend/riscv/proofs
Dec 28 20:23:21 Finished compiler/backend/riscv/proofs                           23s   2GB
Dec 28 20:23:21 Starting compiler/backend/ag32/proofs
Dec 28 20:35:20 Finished compiler/backend/ag32/proofs                         11m58s   4GB
Dec 28 20:35:21 Starting compiler/proofs
Dec 28 20:37:13 Finished compiler/proofs                                       1m52s   5GB
Dec 28 20:37:13 Starting candle/set-theory
Dec 28 20:37:43 Finished candle/set-theory                                       29s   1GB
Dec 28 20:37:43 Starting candle/syntax-lib
Dec 28 20:37:54 Finished candle/syntax-lib                                       11s 788MB
Dec 28 20:37:54 Starting candle/standard/syntax
Dec 28 20:39:46 Finished candle/standard/syntax                                1m51s   2GB
Dec 28 20:39:46 Starting candle/standard/semantics
Dec 28 20:41:32 Finished candle/standard/semantics                             1m46s   2GB
Dec 28 20:41:32 Starting candle/standard/monadic
Dec 29 06:25:38 Resuming candle/standard/monadic