CakeML Regression Test

Job 2259

CakeML:593f113d68b42fd91c567936dc789b59385dae97
  ffiname: fix ag32 proofs [Dec 26 14:42:46]
#976 (ffiname)
Merging into:6dbde1638d8954eb5b8977247e781c0e7f92246f
  Fix for change in HOL [Dec 19 10:21:15]
HOL:d587e1c70b4c059edc079ed4a529b5b7423223b8
  Add ltree_every and ltree_finite_branching (#1172) [Dec 11 22:22:54]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Dec 29 12:21:38 Claimed job
Dec 29 12:21:40 Reusing HOL
Dec 29 12:22:21 Starting developers
Dec 29 12:22:26 Finished developers                                               5s 151MB
Dec 29 12:22:26 Starting developers/bin
Dec 29 12:22:32 Finished developers/bin                                           6s   1GB
Dec 29 12:22:33 Starting compiler/proofs
Dec 29 14:13:13 Finished compiler/proofs                                    1h50m40s  25GB
Dec 29 14:13:13 Starting compiler/bootstrap/translation
Dec 29 22:18:24 Finished compiler/bootstrap/translation                     8h05m10s  46GB
Dec 29 22:18:24 Starting semantics/ffi
Dec 29 22:18:29 Finished semantics/ffi                                            4s 388MB
Dec 29 22:18:29 Starting semantics
Dec 29 22:18:30 Finished semantics                                                1s  18MB
Dec 29 22:18:30 Starting semantics/proofs
Dec 29 22:19:03 Finished semantics/proofs                                        31s 752MB
Dec 29 22:19:03 Starting semantics/alt_semantics
Dec 29 22:19:35 Finished semantics/alt_semantics                                 31s 921MB
Dec 29 22:19:35 Starting semantics/alt_semantics/proofs
Dec 29 22:31:31 Finished semantics/alt_semantics/proofs                       11m56s   1GB
Dec 29 22:31:31 Starting basis/pure
Dec 29 22:31:33 Finished basis/pure                                               1s  23MB
Dec 29 22:31:33 Starting translator
Dec 29 22:33:24 Finished translator                                            1m50s   1GB
Dec 29 22:33:24 Starting compiler/parsing
Dec 29 22:33:25 Finished compiler/parsing                                         1s  20MB
Dec 29 22:33:25 Starting characteristic
Dec 29 22:33:27 Finished characteristic                                           1s  21MB
Dec 29 22:33:28 Starting translator/monadic
Dec 29 22:33:29 Finished translator/monadic                                       1s  22MB
Dec 29 22:33:30 Starting basis
Dec 29 22:37:11 Finished basis                                                 3m41s   3GB
Dec 29 22:37:11 Starting compiler/inference
Dec 29 22:37:13 Finished compiler/inference                                       1s  20MB
Dec 29 22:37:13 Starting compiler/backend/reg_alloc
Dec 29 22:37:14 Finished compiler/backend/reg_alloc                               1s  20MB
Dec 29 22:37:15 Starting compiler/backend/gc
Dec 29 22:37:17 Finished compiler/backend/gc                                      2s  24MB
Dec 29 22:37:17 Starting compiler/backend
Dec 29 22:37:29 Finished compiler/backend                                        11s 775MB
Dec 29 22:37:29 Starting compiler/encoders/asm
Dec 29 22:37:31 Finished compiler/encoders/asm                                    1s  24MB
Dec 29 22:37:31 Starting compiler/encoders/x64
Dec 29 22:37:33 Finished compiler/encoders/x64                                    1s  22MB
Dec 29 22:37:33 Starting compiler/encoders/arm7
Dec 29 22:37:35 Finished compiler/encoders/arm7                                   1s  21MB
Dec 29 22:37:35 Starting compiler/encoders/arm8
Dec 29 22:37:37 Finished compiler/encoders/arm8                                   1s  21MB
Dec 29 22:37:37 Starting compiler/encoders/arm8_asl
Dec 29 22:40:51 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Dec 29 22:40:51 Starting compiler/encoders/mips
Dec 29 22:40:53 Finished compiler/encoders/mips                                   1s  23MB
Dec 29 22:40:53 Starting compiler/encoders/riscv
Dec 29 22:40:55 Finished compiler/encoders/riscv                                  1s  21MB
Dec 29 22:40:55 Starting compiler/encoders/ag32
Dec 29 22:40:57 Finished compiler/encoders/ag32                                   1s  21MB
Dec 29 22:40:57 Starting compiler/backend/x64
Dec 29 22:40:59 Finished compiler/backend/x64                                     2s  26MB
Dec 29 22:40:59 Starting compiler/backend/arm7
Dec 29 22:41:02 Finished compiler/backend/arm7                                    2s  28MB
Dec 29 22:41:02 Starting compiler/backend/arm8
Dec 29 22:41:04 Finished compiler/backend/arm8                                    2s  25MB
Dec 29 22:41:04 Starting compiler/backend/mips
Dec 29 22:41:06 Finished compiler/backend/mips                                    2s  27MB
Dec 29 22:41:07 Starting compiler/backend/riscv
Dec 29 22:41:09 Finished compiler/backend/riscv                                   2s  23MB
Dec 29 22:41:09 Starting compiler/backend/ag32
Dec 29 22:42:34 Finished compiler/backend/ag32                                 1m24s   1GB
Dec 29 22:42:34 Starting compiler/parsing/proofs
Dec 29 22:42:35 Finished compiler/parsing/proofs                                  1s  18MB
Dec 29 22:42:35 Starting compiler/inference/proofs
Dec 29 22:42:37 Finished compiler/inference/proofs                                1s  24MB
Dec 29 22:42:37 Starting compiler/backend/semantics
Dec 29 22:43:50 Finished compiler/backend/semantics                            1m12s   1GB
Dec 29 22:43:51 Starting compiler/backend/reg_alloc/proofs
Dec 29 22:43:52 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Dec 29 22:43:53 Starting compiler/backend/proofs
Dec 29 22:44:54 Finished compiler/backend/proofs                               1m00s   2GB
Dec 29 22:44:54 Starting compiler/backend/serialiser
Dec 29 22:44:57 Finished compiler/backend/serialiser                              2s  31MB
Dec 29 22:44:57 Starting compiler/encoders/x64/proofs
Dec 29 22:54:47 Finished compiler/encoders/x64/proofs                          9m49s   6GB
Dec 29 22:54:47 Starting compiler/encoders/arm7/proofs
Dec 29 23:08:21 Finished compiler/encoders/arm7/proofs                        13m33s   5GB
Dec 29 23:08:21 Starting compiler/encoders/arm8/proofs
Dec 29 23:15:16 Finished compiler/encoders/arm8/proofs                         6m54s   1GB
Dec 29 23:15:16 Starting compiler/encoders/arm8_asl/proofs
Dec 29 23:31:10 Finished compiler/encoders/arm8_asl/proofs                    15m53s   2GB
Dec 29 23:31:10 Starting compiler/encoders/mips/proofs
Dec 29 23:41:41 Finished compiler/encoders/mips/proofs                        10m30s   2GB
Dec 29 23:41:41 Starting compiler/encoders/riscv/proofs
Dec 29 23:50:44 Finished compiler/encoders/riscv/proofs                        9m02s   1GB
Dec 29 23:50:44 Starting compiler/encoders/ag32/proofs
Dec 29 23:53:16 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Dec 29 23:53:16 Starting compiler/backend/x64/proofs
Dec 29 23:53:47 Finished compiler/backend/x64/proofs                             30s   1GB
Dec 29 23:53:47 Starting compiler/backend/arm7/proofs
Dec 29 23:54:21 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 29 23:54:21 Starting compiler/backend/arm8/proofs
Dec 29 23:54:51 Finished compiler/backend/arm8/proofs                            30s   1GB
Dec 29 23:54:52 Starting compiler/backend/arm8_asl
Dec 29 23:55:16 Finished compiler/backend/arm8_asl                               24s   2GB
Dec 29 23:55:16 Starting compiler/backend/mips/proofs
Dec 29 23:55:47 Finished compiler/backend/mips/proofs                            31s   1GB
Dec 29 23:55:47 Starting compiler/backend/riscv/proofs
Dec 29 23:56:21 Finished compiler/backend/riscv/proofs                           34s   2GB
Dec 29 23:56:21 Starting compiler/backend/ag32/proofs
Dec 30 00:10:07 Finished compiler/backend/ag32/proofs                         13m45s   3GB
Dec 30 00:10:07 Starting candle/set-theory
Dec 30 00:10:45 Finished candle/set-theory                                       38s   1GB
Dec 30 00:10:46 Starting candle/syntax-lib
Dec 30 00:10:47 Finished candle/syntax-lib                                        1s  18MB
Dec 30 00:10:47 Starting candle/standard/syntax
Dec 30 00:10:58 Finished candle/standard/syntax                                  10s 735MB
Dec 30 00:10:58 Starting candle/standard/semantics
Dec 30 00:12:57 Finished candle/standard/semantics                             1m58s   1GB
Dec 30 00:12:57 Starting candle/standard/monadic
Dec 30 00:12:59 Finished candle/standard/monadic                                  1s  21MB
Dec 30 00:12:59 Starting candle/standard/ml_kernel
Dec 30 00:14:34 Finished candle/standard/ml_kernel                             1m34s   2GB
Dec 30 00:14:34 Starting candle/overloading/syntax
Dec 30 00:17:57 Finished candle/overloading/syntax                             3m23s   1GB
Dec 30 00:17:57 Starting candle/overloading/semantics
Dec 30 00:30:32 Finished candle/overloading/semantics                         12m34s   2GB
Dec 30 00:30:32 Starting candle/overloading/monadic
Dec 30 00:33:16 Finished candle/overloading/monadic                            2m44s   2GB
Dec 30 00:33:16 Starting candle/overloading/ml_kernel
Dec 30 00:41:15 Finished candle/overloading/ml_kernel                          7m59s   3GB
Dec 30 00:41:16 Starting candle/overloading/ml_checker
Dec 30 00:44:01 Finished candle/overloading/ml_checker                         2m45s   2GB
Dec 30 00:44:01 Starting candle/prover
Dec 30 00:54:03 Finished candle/prover                                        10m01s   3GB
Dec 30 00:54:03 Starting pancake
Dec 30 00:54:47 Finished pancake                                                 43s 844MB
Dec 30 00:54:48 Starting pancake/ffi
Dec 30 00:54:48 Finished pancake/ffi                                              0s  13MB
Dec 30 00:54:48 Starting pancake/semantics
Dec 30 00:57:16 Finished pancake/semantics                                     2m27s   1GB
Dec 30 00:57:16 Starting pancake/parser
Dec 30 00:57:39 Finished pancake/parser                                          23s   1GB
Dec 30 00:57:39 Starting pancake/proofs
Dec 30 01:31:44 Finished pancake/proofs                                       34m04s   4GB
Dec 30 01:31:44 Starting characteristic/examples
Dec 30 01:33:22 Finished characteristic/examples                               1m37s   2GB
Dec 30 01:33:22 Starting tutorial/solutions
Dec 30 22:18:09 Resuming tutorial/solutions