CakeML Regression Test

Job 2678

CakeML:f18c7250703325a9dd318fbc1d03a4afa8090dd8
  fix cnfProofTheory [Oct 15 01:31:37]
#1068 (preserve)
Merging into:b94ca1db7fb392d05ab143a451a30f7a5ba3390d
  Adjust @myreen's editor settings [Oct 18 21:56:34]
HOL:07c84bff2b89ddb2c81c57884f4141bbc37accdb
  Fix cv_compute regression test to cope with case-sensitive files [Oct 15 03:20:04]
Machine:pavlova

Oct 21 22:02:33 Claimed job
Oct 21 22:02:37 Reusing HOL
Oct 21 22:02:49 Starting developers
Oct 21 22:02:53 Finished developers                                               3s 212MB
Oct 21 22:02:54 Starting developers/bin
Oct 21 22:03:16 Finished developers/bin                                          20s   1GB
Oct 21 22:03:17 Starting compiler/proofs
Oct 21 23:47:24 Finished compiler/proofs                                    1h44m05s  32GB
Oct 21 23:47:25 Starting compiler/bootstrap/translation
Oct 22 08:47:54 Finished compiler/bootstrap/translation                     9h00m28s  87GB
Oct 22 08:47:55 Starting semantics/ffi
Oct 22 08:48:05 Finished semantics/ffi                                            9s 735MB
Oct 22 08:48:05 Starting semantics
Oct 22 08:48:07 Finished semantics                                                0s  69MB
Oct 22 08:48:08 Starting semantics/proofs
Oct 22 08:48:32 Finished semantics/proofs                                        23s 813MB
Oct 22 08:48:33 Starting semantics/alt_semantics
Oct 22 08:48:57 Finished semantics/alt_semantics                                 23s 929MB
Oct 22 08:48:58 Starting semantics/alt_semantics/proofs
Oct 22 08:59:28 Finished semantics/alt_semantics/proofs                       10m29s   3GB
Oct 22 08:59:29 Starting basis/pure
Oct 22 08:59:30 Finished basis/pure                                               0s  71MB
Oct 22 08:59:31 Starting translator
Oct 22 09:01:12 Finished translator                                            1m39s   3GB
Oct 22 09:01:13 Starting compiler/parsing
Oct 22 09:01:14 Finished compiler/parsing                                         0s  72MB
Oct 22 09:01:15 Starting characteristic
Oct 22 09:01:17 Finished characteristic                                           0s  95MB
Oct 22 09:01:18 Starting translator/monadic
Oct 22 09:01:20 Finished translator/monadic                                       0s  99MB
Oct 22 09:01:20 Starting basis
Oct 22 09:03:42 Finished basis                                                 2m20s   4GB
Oct 22 09:03:43 Starting compiler/inference
Oct 22 09:03:45 Finished compiler/inference                                       0s  95MB
Oct 22 09:03:46 Starting compiler/backend/reg_alloc
Oct 22 09:03:47 Finished compiler/backend/reg_alloc                               0s  64MB
Oct 22 09:03:48 Starting compiler/backend/gc
Oct 22 09:03:50 Finished compiler/backend/gc                                      1s 141MB
Oct 22 09:03:51 Starting compiler/backend
Oct 22 09:03:56 Finished compiler/backend                                         4s 373MB
Oct 22 09:03:57 Starting compiler/encoders/asm
Oct 22 09:03:59 Finished compiler/encoders/asm                                    0s  90MB
Oct 22 09:04:00 Starting compiler/encoders/x64
Oct 22 09:04:02 Finished compiler/encoders/x64                                    0s  94MB
Oct 22 09:04:03 Starting compiler/encoders/arm7
Oct 22 09:04:04 Finished compiler/encoders/arm7                                   0s  99MB
Oct 22 09:04:05 Starting compiler/encoders/arm8
Oct 22 09:04:07 Finished compiler/encoders/arm8                                   0s  99MB
Oct 22 09:04:08 Starting compiler/encoders/arm8_asl
Oct 22 11:31:32 Finished compiler/encoders/arm8_asl                         2h27m23s  42GB
Oct 22 11:31:33 Starting compiler/encoders/mips
Oct 22 11:31:35 Finished compiler/encoders/mips                                   0s  92MB
Oct 22 11:31:35 Starting compiler/encoders/riscv
Oct 22 11:31:37 Finished compiler/encoders/riscv                                  0s  99MB
Oct 22 11:31:38 Starting compiler/encoders/ag32
Oct 22 11:31:40 Finished compiler/encoders/ag32                                   0s  89MB
Oct 22 11:31:41 Starting compiler/backend/x64
Oct 22 11:31:43 Finished compiler/backend/x64                                     1s 140MB
Oct 22 11:31:44 Starting compiler/backend/arm7
Oct 22 11:31:46 Finished compiler/backend/arm7                                    1s 139MB
Oct 22 11:31:46 Starting compiler/backend/arm8
Oct 22 11:31:48 Finished compiler/backend/arm8                                    1s 139MB
Oct 22 11:31:49 Starting compiler/backend/mips
Oct 22 11:31:51 Finished compiler/backend/mips                                    1s 131MB
Oct 22 11:31:52 Starting compiler/backend/riscv
Oct 22 11:31:54 Finished compiler/backend/riscv                                   1s 131MB
Oct 22 11:31:55 Starting compiler/backend/ag32
Oct 22 11:33:09 Finished compiler/backend/ag32                                 1m12s   3GB
Oct 22 11:33:10 Starting compiler/parsing/proofs
Oct 22 11:33:11 Finished compiler/parsing/proofs                                  0s  75MB
Oct 22 11:33:12 Starting compiler/inference/proofs
Oct 22 11:33:14 Finished compiler/inference/proofs                                0s  99MB
Oct 22 11:33:15 Starting compiler/backend/semantics
Oct 22 11:36:33 Finished compiler/backend/semantics                            3m17s   3GB
Oct 22 11:36:34 Starting compiler/backend/reg_alloc/proofs
Oct 22 11:36:36 Finished compiler/backend/reg_alloc/proofs                        0s 101MB
Oct 22 11:36:37 Starting compiler/backend/proofs
Oct 22 11:37:37 Finished compiler/backend/proofs                                 58s   5GB
Oct 22 11:37:38 Starting compiler/backend/serialiser
Oct 22 11:37:40 Finished compiler/backend/serialiser                              1s 152MB
Oct 22 11:37:41 Starting compiler/encoders/x64/proofs
Oct 22 11:47:53 Finished compiler/encoders/x64/proofs                         10m11s   5GB
Oct 22 11:47:54 Starting compiler/encoders/arm7/proofs
Oct 22 12:01:02 Finished compiler/encoders/arm7/proofs                        13m07s  11GB
Oct 22 12:01:03 Starting compiler/encoders/arm8/proofs
Oct 22 12:08:21 Finished compiler/encoders/arm8/proofs                         7m17s   5GB
Oct 22 12:08:22 Starting compiler/encoders/arm8_asl/proofs
Oct 22 12:59:14 Finished compiler/encoders/arm8_asl/proofs                    50m50s  11GB
Oct 22 12:59:15 Starting compiler/encoders/mips/proofs
Oct 22 13:09:34 Finished compiler/encoders/mips/proofs                        10m17s   7GB
Oct 22 13:09:35 Starting compiler/encoders/riscv/proofs
Oct 22 13:17:58 Finished compiler/encoders/riscv/proofs                        8m22s   5GB
Oct 22 13:17:59 Starting compiler/encoders/ag32/proofs
Oct 22 13:20:56 Finished compiler/encoders/ag32/proofs                         2m55s   2GB
Oct 22 13:20:57 Starting compiler/backend/x64/proofs
Oct 22 13:21:43 Finished compiler/backend/x64/proofs                             46s   3GB
Oct 22 13:21:44 Starting compiler/backend/arm7/proofs
Oct 22 13:22:33 Finished compiler/backend/arm7/proofs                            47s   2GB
Oct 22 13:22:34 Starting compiler/backend/arm8/proofs
Oct 22 13:23:22 Finished compiler/backend/arm8/proofs                            47s   3GB
Oct 22 13:23:23 Starting compiler/backend/arm8_asl
Oct 22 13:23:55 Finished compiler/backend/arm8_asl                               31s   2GB
Oct 22 13:23:56 Starting compiler/backend/mips/proofs
Oct 22 13:24:46 Finished compiler/backend/mips/proofs                            48s   3GB
Oct 22 13:24:47 Starting compiler/backend/riscv/proofs
Oct 22 13:25:44 Finished compiler/backend/riscv/proofs                           56s   4GB
Oct 22 13:25:45 Starting compiler/backend/ag32/proofs
Oct 22 13:43:15 Finished compiler/backend/ag32/proofs                         17m28s   6GB
Oct 22 13:43:15 Starting compiler/backend/cv_compute
Oct 22 13:45:07 Finished compiler/backend/cv_compute                           1m50s   3GB
Oct 22 13:45:08 Starting cv_translator
Oct 22 14:05:12 Finished cv_translator                                        20m03s  10GB
Oct 22 14:05:13 Starting candle/set-theory
Oct 22 14:06:00 Finished candle/set-theory                                       46s   1GB
Oct 22 14:06:01 Starting candle/syntax-lib
Oct 22 14:06:03 Finished candle/syntax-lib                                        0s  69MB
Oct 22 14:06:04 Starting candle/standard/syntax
Oct 22 14:06:24 Finished candle/standard/syntax                                  19s   1GB
Oct 22 14:06:24 Starting candle/standard/semantics
Oct 22 14:09:16 Finished candle/standard/semantics                             2m50s   3GB
Oct 22 14:09:17 Starting candle/standard/monadic
Oct 22 14:09:18 Finished candle/standard/monadic                                  0s 102MB
Oct 22 14:09:19 Starting candle/standard/ml_kernel
Oct 22 14:11:29 Finished candle/standard/ml_kernel                             2m08s   5GB
Oct 22 14:11:30 Starting candle/overloading/syntax
Oct 22 14:15:11 Finished candle/overloading/syntax                             3m40s   3GB
Oct 22 14:15:12 Starting candle/overloading/semantics
Oct 22 14:26:55 Finished candle/overloading/semantics                         11m42s   4GB
Oct 22 14:26:56 Starting candle/overloading/monadic
Oct 22 14:29:25 Finished candle/overloading/monadic                            2m27s   2GB
Oct 22 14:29:26 Starting candle/overloading/ml_kernel
Oct 22 14:37:41 Finished candle/overloading/ml_kernel                          8m13s   6GB
Oct 22 14:37:42 Starting candle/overloading/ml_checker
Oct 22 14:40:31 Finished candle/overloading/ml_checker                         2m48s   7GB
Oct 22 14:40:32 Starting candle/prover
Oct 22 14:51:27 Finished candle/prover                                        10m53s   5GB
Oct 22 14:51:28 Starting pancake
Oct 22 14:51:56 Finished pancake                                                 26s 994MB
Oct 22 14:51:57 Starting pancake/ffi
Oct 22 14:51:57 Finished pancake/ffi                                              0s  22MB
Oct 22 14:51:58 Starting pancake/semantics
Oct 22 14:54:13 Finished pancake/semantics                                     2m13s   2GB
Oct 22 14:54:14 Starting pancake/parser
Oct 22 14:54:38 Finished pancake/parser                                          23s 796MB
Oct 22 14:54:39 Starting pancake/proofs
Oct 22 15:11:03 Finished pancake/proofs                                       16m22s   7GB
Oct 22 15:11:04 Starting compiler/dafny
Oct 22 15:13:54 Finished compiler/dafny                                        2m48s  10GB
Oct 22 15:13:55 Starting compiler/dafny/translation
Oct 22 15:42:58 Finished compiler/dafny/translation                           29m02s  14GB
Oct 22 15:42:59 Starting compiler/dafny/compilation
Oct 22 15:46:30 Finished compiler/dafny/compilation                            3m30s  14GB
Oct 22 15:46:31 Starting compiler/dafny/semantics
Oct 22 15:47:09 Finished compiler/dafny/semantics                                37s   1GB
Oct 22 15:47:10 Starting characteristic/examples
Oct 22 15:48:40 Finished characteristic/examples                               1m29s   5GB
Oct 22 15:48:41 Starting tutorial/solutions
Oct 22 15:51:31 Finished tutorial/solutions                                    2m48s   4GB
Oct 22 15:51:32 Starting translator/monadic/examples
Oct 22 15:54:40 Finished translator/monadic/examples                           3m07s   4GB
Oct 22 15:54:41 Starting examples
Oct 22 16:07:07 Finished examples                                             12m24s   4GB
Oct 22 16:07:08 Starting examples/compilation/x64
Oct 22 16:17:05 Finished examples/compilation/x64                              9m56s   7GB
Oct 22 16:17:06 Starting examples/compilation/x64/proofs
Oct 22 16:22:08 Finished examples/compilation/x64/proofs                       5m01s   7GB
Oct 22 16:22:09 Starting examples/compilation/ag32
Oct 22 16:24:57 Finished examples/compilation/ag32                             2m47s   5GB
Oct 22 16:24:58 Starting examples/compilation/ag32/proofs
Oct 22 16:26:58 Finished examples/compilation/ag32/proofs                      1m59s   7GB
Oct 22 16:26:59 Starting examples/compilation/to_word
Oct 22 16:31:23 Finished examples/compilation/to_word                          4m23s  14GB
Oct 22 16:31:24 Starting examples/lpr_checker
Oct 22 16:31:55 Finished examples/lpr_checker                                    30s   1GB
Oct 22 16:31:56 Starting examples/lpr_checker/array
Oct 22 16:58:26 Finished examples/lpr_checker/array                           26m29s  24GB
Oct 22 16:58:27 Starting examples/lpr_checker/array/compilation
Oct 22 17:01:09 Finished examples/lpr_checker/array/compilation                2m40s  10GB
Oct 22 17:01:10 Starting examples/lpr_checker/array/compilation/proofs
Oct 22 17:03:19 Finished examples/lpr_checker/array/compilation/proofs         2m07s   9GB
Oct 22 17:03:20 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 22 17:05:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m57s   9GB
Oct 22 17:05:19 Starting examples/xlrup_checker
Oct 22 17:05:54 Finished examples/xlrup_checker                                  34s   1GB
Oct 22 17:05:55 Starting examples/xlrup_checker/array
Oct 22 17:19:35 Finished examples/xlrup_checker/array                         13m38s  13GB
Oct 22 17:19:36 Starting examples/xlrup_checker/array/compilation
Oct 22 17:21:06 Finished examples/xlrup_checker/array/compilation              1m29s   7GB
Oct 22 17:21:07 Starting examples/xlrup_checker/array/compilation/proofs
Oct 22 17:22:54 Finished examples/xlrup_checker/array/compilation/proofs       1m46s   7GB
Oct 22 17:22:55 Starting examples/pseudo_bool
Oct 22 17:24:30 Finished examples/pseudo_bool                                  1m34s   2GB
Oct 22 17:24:31 Starting examples/pseudo_bool/cnf_encoding
Oct 22 17:25:14 Finished examples/pseudo_bool/cnf_encoding                       42s   1GB
Oct 22 17:25:15 Starting examples/pseudo_bool/graph_encoding
Oct 22 17:26:11 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 22 17:26:12 Starting examples/pseudo_bool/array
Oct 22 18:34:37 Finished examples/pseudo_bool/array                         1h08m23s  47GB
Oct 22 18:34:38 Starting examples/pseudo_bool/array/compilation
Oct 22 18:49:20 Finished examples/pseudo_bool/array/compilation               14m41s  33GB
Oct 22 18:49:21 Starting examples/pseudo_bool/array/compilation/proofs
Oct 22 18:53:49 Finished examples/pseudo_bool/array/compilation/proofs         4m27s  10GB
Oct 22 18:53:50 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 22 18:55:47 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m56s   9GB
Oct 22 18:55:48 Starting examples/opentheory
Oct 22 19:04:26 Finished examples/opentheory                                   8m36s   5GB
Oct 22 19:04:27 Starting examples/opentheory
Oct 22 19:04:29 Finished examples/opentheory                                      1s 126MB
Oct 22 19:04:30 Starting examples/opentheory/compilation
Oct 22 19:06:39 Finished examples/opentheory/compilation                       2m08s   9GB
Oct 22 19:06:40 Starting examples/opentheory/compilation/proofs
Oct 22 19:08:36 Finished examples/opentheory/compilation/proofs                1m54s   8GB
Oct 22 19:08:37 Starting examples/opentheory/compilation/ag32
Oct 22 19:10:49 Finished examples/opentheory/compilation/ag32                  2m11s   9GB
Oct 22 19:10:50 Starting examples/opentheory/compilation/ag32/proofs
Oct 22 19:13:28 Finished examples/opentheory/compilation/ag32/proofs           2m36s  12GB
Oct 22 19:13:29 Starting examples/sat_encodings
Oct 22 19:14:31 Finished examples/sat_encodings                                1m01s 977MB
Oct 22 19:14:32 Starting examples/sat_encodings/case_studies
Oct 22 19:16:45 Finished examples/sat_encodings/case_studies                   2m12s   2GB
Oct 22 19:16:46 Starting examples/sat_encodings/translation
Oct 22 19:20:31 Finished examples/sat_encodings/translation                    3m43s   4GB
Oct 22 19:20:32 Starting examples/sat_encodings/translation/compilation
Oct 22 19:23:05 Finished examples/sat_encodings/translation/compilation        2m32s   7GB
Oct 22 19:23:06 Starting examples/deflate
Oct 22 19:23:34 Finished examples/deflate                                        27s 782MB
Oct 22 19:23:35 Starting examples/deflate/translation
Oct 22 19:24:36 Finished examples/deflate/translation                            59s   2GB
Oct 22 19:24:36 Starting examples/deflate/translation/compilation
Oct 22 19:25:47 Finished examples/deflate/translation/compilation              1m09s   6GB
Oct 22 19:25:48 Starting examples/vipr
Oct 22 19:29:24 Finished examples/vipr                                         3m34s   4GB
Oct 22 19:29:25 Starting examples/vipr/compilation
Oct 22 19:30:46 Finished examples/vipr/compilation                             1m20s   6GB
Oct 22 19:30:47 Starting translator/okasaki-examples
Oct 22 19:35:04 Finished translator/okasaki-examples                           4m15s   3GB
Oct 22 19:35:05 Starting translator/other-examples
Oct 22 19:40:06 Finished translator/other-examples                             5m00s   3GB
Oct 22 19:40:07 Starting compiler/parsing/tests
Oct 22 19:40:47 Finished compiler/parsing/tests                                  38s   1GB
Oct 22 19:40:47 Starting compiler/inference/tests
Oct 22 19:41:35 Finished compiler/inference/tests                                46s   3GB
Oct 22 19:41:36 Starting compiler/printing/test
Oct 22 19:43:18 Finished compiler/printing/test                                1m41s   6GB
Oct 22 19:43:19 Starting icing/flover
Oct 22 20:20:42 Finished icing/flover                                         37m22s   4GB
Oct 22 20:20:43 Starting icing/
Oct 22 20:48:28 Finished icing/                                               27m43s  10GB
Oct 22 20:48:29 Starting icing/examples
Oct 22 20:50:28 Finished icing/examples                                        1m57s   8GB
Oct 22 20:50:29 Starting compiler/repl
Oct 22 20:59:39 Finished compiler/repl                                         9m08s  11GB
Oct 22 20:59:39 Starting unverified/sexpr-bootstrap/x64/64
Oct 22 21:13:23 Finished unverified/sexpr-bootstrap/x64/64                    13m42s  17GB
Oct 22 21:13:24 Starting unverified/sexpr-bootstrap/x64/32
Oct 22 21:24:31 Finished unverified/sexpr-bootstrap/x64/32                    11m06s  15GB
Oct 22 21:24:32 Starting compiler/benchmarks
Oct 22 21:25:17 Finished compiler/benchmarks                                     44s 711MB
Oct 22 21:25:18 Starting compiler/bootstrap/compilation/x64/64
Oct 22 22:14:03 Finished compiler/bootstrap/compilation/x64/64                48m43s 146GB
Oct 22 22:14:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 22 22:39:23 Finished compiler/bootstrap/compilation/x64/64/proofs         25m18s  56GB
Oct 22 22:39:24 Starting compiler/bootstrap/compilation/x64/32
Oct 22 23:20:23 Finished compiler/bootstrap/compilation/x64/32                40m57s 105GB
Oct 22 23:20:24 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 22 23:25:34 Finished compiler/bootstrap/compilation/x64/32/proofs          5m09s  25GB
Oct 22 23:25:35 Starting compiler/bootstrap/compilation/arm8/64
Oct 23 00:24:28 Finished compiler/bootstrap/compilation/arm8/64               58m51s 121GB
Oct 23 00:24:29 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 23 00:30:01 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m31s  29GB
Oct 23 00:30:02 Starting compiler/bootstrap/compilation/ag32/32
Oct 23 01:12:52 Finished compiler/bootstrap/compilation/ag32/32               42m48s 109GB
Oct 23 01:12:53 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 23 01:18:44 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m50s  30GB
Oct 23 01:18:45 SUCCESS