CakeML Regression Test

Job 1423

CakeML:86bded59186b861ecdecf4a8f3019df160b74b98
  fix ramseyScript [Dec 30 02:27:27]
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 30 02:42:02 Claimed job
Dec 30 02:42:05 Reusing HOL
Dec 30 02:42:10 Starting developers
Dec 30 02:42:13 Finished developers                                               2s 107MB
Dec 30 02:42:13 Starting developers/bin
Dec 30 02:42:19 Finished developers/bin                                           5s   1GB
Dec 30 02:42:19 Starting semantics/ffi
Dec 30 02:42:29 Finished semantics/ffi                                            9s 284MB
Dec 30 02:42:30 Starting semantics
Dec 30 02:43:54 Finished semantics                                             1m24s   1GB
Dec 30 02:43:54 Starting semantics/proofs
Dec 30 02:47:11 Finished semantics/proofs                                      3m17s   1GB
Dec 30 02:47:12 Starting semantics/alt_semantics
Dec 30 02:47:19 Finished semantics/alt_semantics                                  7s 367MB
Dec 30 02:47:20 Starting semantics/alt_semantics/proofs
Dec 30 02:49:28 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Dec 30 02:49:28 Starting basis/pure
Dec 30 02:50:20 Finished basis/pure                                              52s   1GB
Dec 30 02:50:20 Starting translator
Dec 30 02:52:56 Finished translator                                            2m35s   1GB
Dec 30 02:52:56 Starting compiler/parsing
Dec 30 02:54:03 Finished compiler/parsing                                      1m06s   4GB
Dec 30 02:54:04 Starting characteristic
Dec 30 03:00:00 Finished characteristic                                        5m56s   3GB
Dec 30 03:00:00 Starting translator/monadic
Dec 30 03:01:44 Finished translator/monadic                                    1m43s   2GB
Dec 30 03:01:45 Starting basis
Dec 30 03:34:52 Finished basis                                                33m07s  25GB
Dec 30 03:34:52 Starting compiler/inference
Dec 30 03:35:55 Finished compiler/inference                                    1m02s   1GB
Dec 30 03:35:55 Starting compiler/backend/reg_alloc
Dec 30 03:37:01 Finished compiler/backend/reg_alloc                            1m05s   1GB
Dec 30 03:37:01 Starting compiler/backend/gc
Dec 30 03:40:21 Finished compiler/backend/gc                                   3m20s   3GB
Dec 30 03:40:21 Starting compiler/backend
Dec 30 03:45:16 Finished compiler/backend                                      4m54s   4GB
Dec 30 03:45:16 Starting compiler/encoders/asm
Dec 30 03:45:38 Finished compiler/encoders/asm                                   21s   1GB
Dec 30 03:45:38 Starting compiler/encoders/x64
Dec 30 03:46:05 Finished compiler/encoders/x64                                   26s   1GB
Dec 30 03:46:05 Starting compiler/encoders/arm7
Dec 30 03:46:56 Finished compiler/encoders/arm7                                  50s   1GB
Dec 30 03:46:56 Starting compiler/encoders/arm8
Dec 30 03:47:10 Finished compiler/encoders/arm8                                  13s   1GB
Dec 30 03:47:10 Starting compiler/encoders/mips
Dec 30 03:47:28 Finished compiler/encoders/mips                                  17s   1GB
Dec 30 03:47:28 Starting compiler/encoders/riscv
Dec 30 03:47:45 Finished compiler/encoders/riscv                                 16s   1GB
Dec 30 03:47:45 Starting compiler/encoders/ag32
Dec 30 03:48:03 Finished compiler/encoders/ag32                                  18s 962MB
Dec 30 03:48:04 Starting compiler/backend/x64
Dec 30 03:48:22 Finished compiler/backend/x64                                    17s   1GB
Dec 30 03:48:22 Starting compiler/backend/arm7
Dec 30 03:48:44 Finished compiler/backend/arm7                                   22s   1GB
Dec 30 03:48:44 Starting compiler/backend/arm8
Dec 30 03:49:05 Finished compiler/backend/arm8                                   20s   1GB
Dec 30 03:49:05 Starting compiler/backend/mips
Dec 30 03:49:25 Finished compiler/backend/mips                                   20s   1GB
Dec 30 03:49:25 Starting compiler/backend/riscv
Dec 30 03:49:46 Finished compiler/backend/riscv                                  20s   1GB
Dec 30 03:49:46 Starting compiler/backend/ag32
Dec 30 03:50:57 Finished compiler/backend/ag32                                 1m10s   2GB
Dec 30 03:50:57 Starting compiler/parsing/proofs
Dec 30 03:56:34 Finished compiler/parsing/proofs                               5m37s   2GB
Dec 30 03:56:34 Starting compiler/inference/proofs
Dec 30 03:59:05 Finished compiler/inference/proofs                             2m30s   2GB
Dec 30 03:59:05 Starting compiler/backend/semantics
Dec 30 04:26:10 Finished compiler/backend/semantics                           27m04s   5GB
Dec 30 04:26:10 Starting compiler/backend/reg_alloc/proofs
Dec 30 04:29:28 Finished compiler/backend/reg_alloc/proofs                     3m17s   1GB
Dec 30 04:29:28 Starting compiler/backend/proofs
Dec 30 05:23:28 Finished compiler/backend/proofs                              53m59s  20GB
Dec 30 05:23:28 Starting compiler/encoders/x64/proofs
Dec 30 05:32:49 Finished compiler/encoders/x64/proofs                          9m21s   9GB
Dec 30 05:32:50 Starting compiler/encoders/arm7/proofs
Dec 30 05:45:18 Finished compiler/encoders/arm7/proofs                        12m28s   5GB
Dec 30 05:45:19 Starting compiler/encoders/arm8/proofs
Dec 30 05:51:30 Finished compiler/encoders/arm8/proofs                         6m11s   3GB
Dec 30 05:51:30 Starting compiler/encoders/mips/proofs
Dec 30 06:01:27 Finished compiler/encoders/mips/proofs                         9m57s   3GB
Dec 30 06:01:28 Starting compiler/encoders/riscv/proofs
Dec 30 06:09:54 Finished compiler/encoders/riscv/proofs                        8m26s   3GB
Dec 30 06:09:55 Starting compiler/encoders/ag32/proofs
Dec 30 06:12:17 Finished compiler/encoders/ag32/proofs                         2m22s   1GB
Dec 30 06:12:17 Starting compiler/backend/x64/proofs
Dec 30 06:12:39 Finished compiler/backend/x64/proofs                             22s   1GB
Dec 30 06:12:39 Starting compiler/backend/arm7/proofs
Dec 30 06:13:02 Finished compiler/backend/arm7/proofs                            22s   1GB
Dec 30 06:13:03 Starting compiler/backend/arm8/proofs
Dec 30 06:13:23 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 30 06:13:23 Starting compiler/backend/mips/proofs
Dec 30 06:13:45 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 30 06:13:45 Starting compiler/backend/riscv/proofs
Dec 30 06:14:08 Finished compiler/backend/riscv/proofs                           23s   2GB
Dec 30 06:14:08 Starting compiler/backend/ag32/proofs
Dec 30 06:26:11 Finished compiler/backend/ag32/proofs                         12m03s   4GB
Dec 30 06:26:12 Starting compiler/proofs
Dec 30 06:27:51 Finished compiler/proofs                                       1m39s   6GB
Dec 30 06:27:51 Starting candle/set-theory
Dec 30 06:28:21 Finished candle/set-theory                                       29s   1GB
Dec 30 06:28:22 Starting candle/syntax-lib
Dec 30 06:28:33 Finished candle/syntax-lib                                       10s 822MB
Dec 30 06:28:33 Starting candle/standard/syntax
Dec 30 06:30:25 Finished candle/standard/syntax                                1m51s   1GB
Dec 30 06:30:25 Starting candle/standard/semantics Dec 30 06:30:25 123s