Job 2663

CakeML:a927d0bcbec87d7a481e11bd68e853276579c57b
  Increase Infixl in npbcScript [Oct 17 21:23:21]
#1072 (fix-npbc-grammar)
Merging into:b6191f1bbb09fcc35807b2f78582e8ed75393f5a
  Merge pull request #1069 from CakeML/remove-simple-qprove [Oct 16 18:48:00]
HOL:07c84bff2b89ddb2c81c57884f4141bbc37accdb
  Fix cv_compute regression test to cope with case-sensitive files [Oct 15 03:20:04]
Machine:pavlova

Oct 18 04:06:24 Claimed job
Oct 18 04:06:28 Reusing HOL
Oct 18 04:06:40 Starting developers
Oct 18 04:06:45 Finished developers                                               3s 234MB
Oct 18 04:06:46 Starting developers/bin
Oct 18 04:07:10 Finished developers/bin                                          22s   1GB
Oct 18 04:07:11 Starting compiler/proofs
Oct 18 05:50:06 Finished compiler/proofs                                    1h42m54s  37GB
Oct 18 05:50:07 Starting compiler/bootstrap/translation
Oct 18 14:48:46 Finished compiler/bootstrap/translation                     8h58m37s  87GB
Oct 18 14:48:47 Starting semantics/ffi
Oct 18 14:48:56 Finished semantics/ffi                                            8s 644MB
Oct 18 14:48:57 Starting semantics
Oct 18 14:48:58 Finished semantics                                                0s  69MB
Oct 18 14:48:59 Starting semantics/proofs
Oct 18 14:49:24 Finished semantics/proofs                                        23s 832MB
Oct 18 14:49:24 Starting semantics/alt_semantics
Oct 18 14:49:48 Finished semantics/alt_semantics                                 22s 662MB
Oct 18 14:49:49 Starting semantics/alt_semantics/proofs
Oct 18 15:00:09 Finished semantics/alt_semantics/proofs                       10m19s   2GB
Oct 18 15:00:10 Starting basis/pure
Oct 18 15:00:11 Finished basis/pure                                               0s  70MB
Oct 18 15:00:12 Starting translator
Oct 18 15:01:51 Finished translator                                            1m37s   3GB
Oct 18 15:01:52 Starting compiler/parsing
Oct 18 15:01:53 Finished compiler/parsing                                         0s  72MB
Oct 18 15:01:54 Starting characteristic
Oct 18 15:01:56 Finished characteristic                                           0s  93MB
Oct 18 15:01:57 Starting translator/monadic
Oct 18 15:01:59 Finished translator/monadic                                       0s  98MB
Oct 18 15:01:59 Starting basis
Oct 18 15:04:35 Finished basis                                                 2m34s   4GB
Oct 18 15:04:36 Starting compiler/inference
Oct 18 15:04:38 Finished compiler/inference                                       0s  93MB
Oct 18 15:04:39 Starting compiler/backend/reg_alloc
Oct 18 15:04:40 Finished compiler/backend/reg_alloc                               0s  64MB
Oct 18 15:04:41 Starting compiler/backend/gc
Oct 18 15:04:43 Finished compiler/backend/gc                                      1s 139MB
Oct 18 15:04:44 Starting compiler/backend
Oct 18 15:04:49 Finished compiler/backend                                         4s 327MB
Oct 18 15:04:50 Starting compiler/encoders/asm
Oct 18 15:04:52 Finished compiler/encoders/asm                                    0s  97MB
Oct 18 15:04:52 Starting compiler/encoders/x64
Oct 18 15:04:54 Finished compiler/encoders/x64                                    0s  98MB
Oct 18 15:04:55 Starting compiler/encoders/arm7
Oct 18 15:04:57 Finished compiler/encoders/arm7                                   0s  98MB
Oct 18 15:04:58 Starting compiler/encoders/arm8
Oct 18 15:04:59 Finished compiler/encoders/arm8                                   0s  99MB
Oct 18 15:05:00 Starting compiler/encoders/arm8_asl
Oct 18 15:08:17 Finished compiler/encoders/arm8_asl                            3m15s   1GB
Oct 18 15:08:18 Starting compiler/encoders/mips
Oct 18 15:08:20 Finished compiler/encoders/mips                                   0s  99MB
Oct 18 15:08:20 Starting compiler/encoders/riscv
Oct 18 15:08:22 Finished compiler/encoders/riscv                                  0s  98MB
Oct 18 15:08:23 Starting compiler/encoders/ag32
Oct 18 15:08:25 Finished compiler/encoders/ag32                                   0s  88MB
Oct 18 15:08:26 Starting compiler/backend/x64
Oct 18 15:08:28 Finished compiler/backend/x64                                     1s 139MB
Oct 18 15:08:29 Starting compiler/backend/arm7
Oct 18 15:08:31 Finished compiler/backend/arm7                                    1s 139MB
Oct 18 15:08:32 Starting compiler/backend/arm8
Oct 18 15:08:34 Finished compiler/backend/arm8                                    1s 138MB
Oct 18 15:08:34 Starting compiler/backend/mips
Oct 18 15:08:37 Finished compiler/backend/mips                                    1s 139MB
Oct 18 15:08:37 Starting compiler/backend/riscv
Oct 18 15:08:39 Finished compiler/backend/riscv                                   1s 139MB
Oct 18 15:08:40 Starting compiler/backend/ag32
Oct 18 15:09:56 Finished compiler/backend/ag32                                 1m14s   4GB
Oct 18 15:09:57 Starting compiler/parsing/proofs
Oct 18 15:09:58 Finished compiler/parsing/proofs                                  0s  74MB
Oct 18 15:09:59 Starting compiler/inference/proofs
Oct 18 15:10:01 Finished compiler/inference/proofs                                0s  91MB
Oct 18 15:10:02 Starting compiler/backend/semantics
Oct 18 15:13:20 Finished compiler/backend/semantics                            3m17s   3GB
Oct 18 15:13:21 Starting compiler/backend/reg_alloc/proofs
Oct 18 15:13:23 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Oct 18 15:13:24 Starting compiler/backend/proofs
Oct 18 15:14:19 Finished compiler/backend/proofs                                 54s   2GB
Oct 18 15:14:20 Starting compiler/backend/serialiser
Oct 18 15:14:22 Finished compiler/backend/serialiser                              1s 149MB
Oct 18 15:14:23 Starting compiler/encoders/x64/proofs
Oct 18 15:24:14 Finished compiler/encoders/x64/proofs                          9m50s   5GB
Oct 18 15:24:15 Starting compiler/encoders/arm7/proofs
Oct 18 15:37:24 Finished compiler/encoders/arm7/proofs                        13m07s   8GB
Oct 18 15:37:25 Starting compiler/encoders/arm8/proofs
Oct 18 15:44:19 Finished compiler/encoders/arm8/proofs                         6m53s   7GB
Oct 18 15:44:20 Starting compiler/encoders/arm8_asl/proofs
Oct 18 15:59:46 Finished compiler/encoders/arm8_asl/proofs                    15m25s   5GB
Oct 18 15:59:47 Starting compiler/encoders/mips/proofs
Oct 18 16:10:03 Finished compiler/encoders/mips/proofs                        10m15s  10GB
Oct 18 16:10:04 Starting compiler/encoders/riscv/proofs
Oct 18 16:18:33 Finished compiler/encoders/riscv/proofs                        8m27s   4GB
Oct 18 16:18:34 Starting compiler/encoders/ag32/proofs
Oct 18 16:21:29 Finished compiler/encoders/ag32/proofs                         2m54s   2GB
Oct 18 16:21:30 Starting compiler/backend/x64/proofs
Oct 18 16:22:17 Finished compiler/backend/x64/proofs                             46s   3GB
Oct 18 16:22:18 Starting compiler/backend/arm7/proofs
Oct 18 16:23:05 Finished compiler/backend/arm7/proofs                            45s   2GB
Oct 18 16:23:06 Starting compiler/backend/arm8/proofs
Oct 18 16:23:55 Finished compiler/backend/arm8/proofs                            47s   3GB
Oct 18 16:23:56 Starting compiler/backend/arm8_asl
Oct 18 16:24:25 Finished compiler/backend/arm8_asl                               28s   2GB
Oct 18 16:24:26 Starting compiler/backend/mips/proofs
Oct 18 16:25:16 Finished compiler/backend/mips/proofs                            49s   3GB
Oct 18 16:25:17 Starting compiler/backend/riscv/proofs
Oct 18 16:26:15 Finished compiler/backend/riscv/proofs                           57s   4GB
Oct 18 16:26:16 Starting compiler/backend/ag32/proofs
Oct 18 16:43:15 Finished compiler/backend/ag32/proofs                         16m58s   6GB
Oct 18 16:43:16 Starting compiler/backend/cv_compute
Oct 18 16:45:08 Finished compiler/backend/cv_compute                           1m51s   3GB
Oct 18 16:45:09 Starting cv_translator
Oct 18 17:04:55 Finished cv_translator                                        19m45s   9GB
Oct 18 17:04:56 Starting candle/set-theory
Oct 18 17:05:45 Finished candle/set-theory                                       47s   1GB
Oct 18 17:05:46 Starting candle/syntax-lib
Oct 18 17:05:47 Finished candle/syntax-lib                                        0s  69MB
Oct 18 17:05:48 Starting candle/standard/syntax
Oct 18 17:06:08 Finished candle/standard/syntax                                  19s   1GB
Oct 18 17:06:09 Starting candle/standard/semantics
Oct 18 17:09:01 Finished candle/standard/semantics                             2m51s   3GB
Oct 18 17:09:02 Starting candle/standard/monadic
Oct 18 17:09:04 Finished candle/standard/monadic                                  0s 101MB
Oct 18 17:09:05 Starting candle/standard/ml_kernel
Oct 18 17:11:12 Finished candle/standard/ml_kernel                             2m06s   5GB
Oct 18 17:11:13 Starting candle/overloading/syntax
Oct 18 17:14:53 Finished candle/overloading/syntax                             3m39s   3GB
Oct 18 17:14:54 Starting candle/overloading/semantics
Oct 18 17:26:30 Finished candle/overloading/semantics                         11m34s   4GB
Oct 18 17:26:31 Starting candle/overloading/monadic
Oct 18 17:28:59 Finished candle/overloading/monadic                            2m27s   2GB
Oct 18 17:29:00 Starting candle/overloading/ml_kernel
Oct 18 17:37:08 Finished candle/overloading/ml_kernel                          8m07s   7GB
Oct 18 17:37:09 Starting candle/overloading/ml_checker
Oct 18 17:40:00 Finished candle/overloading/ml_checker                         2m49s   7GB
Oct 18 17:40:00 Starting candle/prover
Oct 18 17:50:53 Finished candle/prover                                        10m51s   5GB
Oct 18 17:50:54 Starting pancake
Oct 18 17:51:22 Finished pancake                                                 27s 984MB
Oct 18 17:51:23 Starting pancake/ffi
Oct 18 17:51:24 Finished pancake/ffi                                              0s  22MB
Oct 18 17:51:25 Starting pancake/semantics
Oct 18 17:53:41 Finished pancake/semantics                                     2m15s   2GB
Oct 18 17:53:42 Starting pancake/parser
Oct 18 17:54:06 Finished pancake/parser                                          23s 827MB
Oct 18 17:54:07 Starting pancake/proofs
Oct 18 18:10:29 Finished pancake/proofs                                       16m20s   7GB
Oct 18 18:10:30 Starting compiler/dafny
Oct 18 18:13:15 Finished compiler/dafny                                        2m44s  10GB
Oct 18 18:13:16 Starting compiler/dafny/translation
Oct 18 18:42:34 Finished compiler/dafny/translation                           29m16s  15GB
Oct 18 18:42:35 Starting compiler/dafny/compilation
Oct 18 18:46:12 Finished compiler/dafny/compilation                            3m36s  15GB
Oct 18 18:46:13 Starting compiler/dafny/semantics
Oct 18 18:46:51 Finished compiler/dafny/semantics                                37s   1GB
Oct 18 18:46:52 Starting characteristic/examples
Oct 18 18:48:26 Finished characteristic/examples                               1m32s   5GB
Oct 18 18:48:27 Starting tutorial/solutions
Oct 18 18:51:19 Finished tutorial/solutions                                    2m50s   4GB
Oct 18 18:51:20 Starting translator/monadic/examples
Oct 18 18:54:34 Finished translator/monadic/examples                           3m13s   4GB
Oct 18 18:54:35 Starting examples
Oct 18 19:06:59 Finished examples                                             12m23s   5GB
Oct 18 19:07:00 Starting examples/compilation/x64
Oct 18 19:16:59 Finished examples/compilation/x64                              9m58s   7GB
Oct 18 19:17:00 Starting examples/compilation/x64/proofs
Oct 18 19:22:07 Finished examples/compilation/x64/proofs                       5m05s   7GB
Oct 18 19:22:08 Starting examples/compilation/ag32
Oct 18 19:24:52 Finished examples/compilation/ag32                             2m43s   5GB
Oct 18 19:24:53 Starting examples/compilation/ag32/proofs
Oct 18 19:26:47 Finished examples/compilation/ag32/proofs                      1m53s   8GB
Oct 18 19:26:48 Starting examples/compilation/to_word
Oct 18 19:31:08 Finished examples/compilation/to_word                          4m18s  14GB
Oct 18 19:31:08 Starting examples/lpr_checker
Oct 18 19:31:40 Finished examples/lpr_checker                                    30s   1GB
Oct 18 19:31:41 Starting examples/lpr_checker/array
Oct 18 19:58:22 Finished examples/lpr_checker/array                           26m39s  27GB
Oct 18 19:58:22 Starting examples/lpr_checker/array/compilation
Oct 18 20:01:03 Finished examples/lpr_checker/array/compilation                2m39s  10GB
Oct 18 20:01:03 Starting examples/lpr_checker/array/compilation/proofs
Oct 18 20:03:09 Finished examples/lpr_checker/array/compilation/proofs         2m04s   7GB
Oct 18 20:03:10 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 18 20:05:11 Finished examples/lpr_checker/array/compilation/proofsARM8     2m00s   6GB
Oct 18 20:05:12 Starting examples/xlrup_checker
Oct 18 20:05:46 Finished examples/xlrup_checker                                  33s   1GB
Oct 18 20:05:47 Starting examples/xlrup_checker/array
Oct 18 20:19:21 Finished examples/xlrup_checker/array                         13m32s  11GB
Oct 18 20:19:22 Starting examples/xlrup_checker/array/compilation
Oct 18 20:20:52 Finished examples/xlrup_checker/array/compilation              1m29s   6GB
Oct 18 20:20:53 Starting examples/xlrup_checker/array/compilation/proofs
Oct 18 20:22:48 Finished examples/xlrup_checker/array/compilation/proofs       1m54s   6GB
Oct 18 20:22:49 Starting examples/pseudo_bool
Oct 18 20:24:15 Finished examples/pseudo_bool                                  1m24s   1GB
Oct 18 20:24:15 Starting examples/pseudo_bool/cnf_encoding
Oct 18 20:24:57 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Oct 18 20:24:58 Starting examples/pseudo_bool/graph_encoding
Oct 18 20:25:54 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 18 20:25:55 Starting examples/pseudo_bool/array Oct 18 20:25:55 3942s