Job 2498

CakeML:222d83a5a94a8c7ec505e27d4e8d62d19c471046
  Update basis types [Jul 28 05:54:15]
#1023 (double-type-fix)
Merging into:05aaba52005899328d6b4f19faf319c26b7e5310
  Merge pull request #1022 from CakeML/pr/991 [Jul 26 04:58:05]
HOL:c37de731916a5fe5fdc6218d4b2e19234435e4ce
  Add lots of regexp matching regression tests for DBSearchParser [Jul 15 06:13:45]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Jul 28 06:37:34 Claimed job
Jul 28 06:37:37 Reusing HOL
Jul 28 06:38:22 Starting developers
Jul 28 06:38:27 Finished developers                                               5s  74MB
Jul 28 06:38:28 Starting developers/bin
Jul 28 06:38:34 Finished developers/bin                                           6s   1GB
Jul 28 06:38:35 Starting compiler/proofs
Jul 28 08:40:54 Finished compiler/proofs                                    2h02m19s  23GB
Jul 28 08:40:54 Starting compiler/bootstrap/translation
Jul 28 17:07:34 Finished compiler/bootstrap/translation                     8h26m39s  46GB
Jul 28 17:07:34 Starting semantics/ffi
Jul 28 17:07:40 Finished semantics/ffi                                            5s 431MB
Jul 28 17:07:40 Starting semantics
Jul 28 17:07:41 Finished semantics                                                1s  18MB
Jul 28 17:07:41 Starting semantics/proofs
Jul 28 17:08:16 Finished semantics/proofs                                        34s   1GB
Jul 28 17:08:16 Starting semantics/alt_semantics
Jul 28 17:08:49 Finished semantics/alt_semantics                                 33s 703MB
Jul 28 17:08:49 Starting semantics/alt_semantics/proofs
Jul 28 17:20:47 Finished semantics/alt_semantics/proofs                       11m57s   1GB
Jul 28 17:20:47 Starting basis/pure
Jul 28 17:20:49 Finished basis/pure                                               1s  18MB
Jul 28 17:20:49 Starting translator
Jul 28 17:22:41 Finished translator                                            1m51s   1GB
Jul 28 17:22:41 Starting compiler/parsing
Jul 28 17:22:43 Finished compiler/parsing                                         1s  18MB
Jul 28 17:22:43 Starting characteristic
Jul 28 17:22:45 Finished characteristic                                           1s  28MB
Jul 28 17:22:45 Starting translator/monadic
Jul 28 17:22:47 Finished translator/monadic                                       1s  23MB
Jul 28 17:22:47 Starting basis
Jul 28 17:26:22 Finished basis                                                 3m35s   3GB
Jul 28 17:26:23 Starting compiler/inference
Jul 28 17:26:25 Finished compiler/inference                                       1s  25MB
Jul 28 17:26:25 Starting compiler/backend/reg_alloc
Jul 28 17:26:26 Finished compiler/backend/reg_alloc                               1s  20MB
Jul 28 17:26:26 Starting compiler/backend/gc
Jul 28 17:26:29 Finished compiler/backend/gc                                      2s  24MB
Jul 28 17:26:29 Starting compiler/backend
Jul 28 17:26:43 Finished compiler/backend                                        14s 836MB
Jul 28 17:26:43 Starting compiler/encoders/asm
Jul 28 17:26:45 Finished compiler/encoders/asm                                    1s  26MB
Jul 28 17:26:45 Starting compiler/encoders/x64
Jul 28 17:26:47 Finished compiler/encoders/x64                                    1s  24MB
Jul 28 17:26:47 Starting compiler/encoders/arm7
Jul 28 17:26:49 Finished compiler/encoders/arm7                                   1s  22MB
Jul 28 17:26:49 Starting compiler/encoders/arm8
Jul 28 17:26:51 Finished compiler/encoders/arm8                                   1s  23MB
Jul 28 17:26:51 Starting compiler/encoders/arm8_asl
Jul 28 17:30:08 Finished compiler/encoders/arm8_asl                            3m16s   1GB
Jul 28 17:30:08 Starting compiler/encoders/mips
Jul 28 17:30:10 Finished compiler/encoders/mips                                   1s  26MB
Jul 28 17:30:10 Starting compiler/encoders/riscv
Jul 28 17:30:12 Finished compiler/encoders/riscv                                  1s  20MB
Jul 28 17:30:12 Starting compiler/encoders/ag32
Jul 28 17:30:14 Finished compiler/encoders/ag32                                   1s  19MB
Jul 28 17:30:14 Starting compiler/backend/x64
Jul 28 17:30:17 Finished compiler/backend/x64                                     2s  26MB
Jul 28 17:30:17 Starting compiler/backend/arm7
Jul 28 17:30:19 Finished compiler/backend/arm7                                    2s  27MB
Jul 28 17:30:19 Starting compiler/backend/arm8
Jul 28 17:30:22 Finished compiler/backend/arm8                                    2s  23MB
Jul 28 17:30:22 Starting compiler/backend/mips
Jul 28 17:30:24 Finished compiler/backend/mips                                    2s  25MB
Jul 28 17:30:24 Starting compiler/backend/riscv
Jul 28 17:30:27 Finished compiler/backend/riscv                                   2s  21MB
Jul 28 17:30:27 Starting compiler/backend/ag32
Jul 28 17:31:55 Finished compiler/backend/ag32                                 1m27s   1GB
Jul 28 17:31:55 Starting compiler/parsing/proofs
Jul 28 17:31:56 Finished compiler/parsing/proofs                                  1s  20MB
Jul 28 17:31:56 Starting compiler/inference/proofs
Jul 28 17:31:58 Finished compiler/inference/proofs                                1s  27MB
Jul 28 17:31:59 Starting compiler/backend/semantics
Jul 28 17:35:57 Finished compiler/backend/semantics                            3m58s   1GB
Jul 28 17:35:57 Starting compiler/backend/reg_alloc/proofs
Jul 28 17:35:59 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Jul 28 17:35:59 Starting compiler/backend/proofs
Jul 28 17:37:01 Finished compiler/backend/proofs                               1m01s   3GB
Jul 28 17:37:01 Starting compiler/backend/serialiser
Jul 28 17:37:03 Finished compiler/backend/serialiser                              2s  24MB
Jul 28 17:37:03 Starting compiler/encoders/x64/proofs
Jul 28 17:46:57 Finished compiler/encoders/x64/proofs                          9m53s   4GB
Jul 28 17:46:57 Starting compiler/encoders/arm7/proofs
Jul 28 18:00:54 Finished compiler/encoders/arm7/proofs                        13m56s   3GB
Jul 28 18:00:54 Starting compiler/encoders/arm8/proofs
Jul 28 18:07:51 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Jul 28 18:07:51 Starting compiler/encoders/arm8_asl/proofs
Jul 28 18:23:40 Finished compiler/encoders/arm8_asl/proofs                    15m48s   2GB
Jul 28 18:23:40 Starting compiler/encoders/mips/proofs
Jul 28 18:34:19 Finished compiler/encoders/mips/proofs                        10m38s   3GB
Jul 28 18:34:19 Starting compiler/encoders/riscv/proofs
Jul 28 18:43:14 Finished compiler/encoders/riscv/proofs                        8m55s   2GB
Jul 28 18:43:15 Starting compiler/encoders/ag32/proofs
Jul 28 18:45:50 Finished compiler/encoders/ag32/proofs                         2m35s   1GB
Jul 28 18:45:50 Starting compiler/backend/x64/proofs
Jul 28 18:46:23 Finished compiler/backend/x64/proofs                             33s   2GB
Jul 28 18:46:23 Starting compiler/backend/arm7/proofs
Jul 28 18:46:57 Finished compiler/backend/arm7/proofs                            33s   1GB
Jul 28 18:46:58 Starting compiler/backend/arm8/proofs
Jul 28 18:47:31 Finished compiler/backend/arm8/proofs                            33s   2GB
Jul 28 18:47:31 Starting compiler/backend/arm8_asl
Jul 28 18:47:56 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 28 18:47:56 Starting compiler/backend/mips/proofs
Jul 28 18:48:30 Finished compiler/backend/mips/proofs                            34s   1GB
Jul 28 18:48:30 Starting compiler/backend/riscv/proofs
Jul 28 18:49:07 Finished compiler/backend/riscv/proofs                           37s   2GB
Jul 28 18:49:08 Starting compiler/backend/ag32/proofs
Jul 28 19:03:47 Finished compiler/backend/ag32/proofs                         14m39s   3GB
Jul 28 19:03:47 Starting compiler/backend/cv_compute
Jul 28 19:05:06 Finished compiler/backend/cv_compute                           1m19s   2GB
Jul 28 19:05:06 Starting cv_translator
Jul 28 19:25:50 Finished cv_translator                                        20m44s   8GB
Jul 28 19:25:50 Starting candle/set-theory
Jul 28 19:26:34 Finished candle/set-theory                                       43s   1GB
Jul 28 19:26:34 Starting candle/syntax-lib
Jul 28 19:26:36 Finished candle/syntax-lib                                        1s  22MB
Jul 28 19:26:36 Starting candle/standard/syntax
Jul 28 19:26:48 Finished candle/standard/syntax                                  12s 798MB
Jul 28 19:26:48 Starting candle/standard/semantics
Jul 28 19:28:59 Finished candle/standard/semantics                             2m10s   1GB
Jul 28 19:28:59 Starting candle/standard/monadic
Jul 28 19:29:01 Finished candle/standard/monadic                                  1s  22MB
Jul 28 19:29:01 Starting candle/standard/ml_kernel
Jul 28 19:30:43 Finished candle/standard/ml_kernel                             1m41s   2GB
Jul 28 19:30:43 Starting candle/overloading/syntax
Jul 28 19:34:15 Finished candle/overloading/syntax                             3m32s   1GB
Jul 28 19:34:15 Starting candle/overloading/semantics
Jul 28 19:47:08 Finished candle/overloading/semantics                         12m52s   2GB
Jul 28 19:47:08 Starting candle/overloading/monadic
Jul 28 19:49:59 Finished candle/overloading/monadic                            2m51s   1GB
Jul 28 19:49:59 Starting candle/overloading/ml_kernel
Jul 28 19:58:04 Finished candle/overloading/ml_kernel                          8m04s   3GB
Jul 28 19:58:04 Starting candle/overloading/ml_checker
Jul 28 20:00:44 Finished candle/overloading/ml_checker                         2m39s   4GB
Jul 28 20:00:44 Starting candle/prover
Jul 28 20:11:11 Finished candle/prover                                        10m27s   3GB
Jul 28 20:11:11 Starting pancake
Jul 28 20:12:01 Finished pancake                                                 49s 977MB
Jul 28 20:12:01 Starting pancake/ffi
Jul 28 20:12:02 Finished pancake/ffi                                              0s  13MB
Jul 28 20:12:02 Starting pancake/semantics
Jul 28 20:15:03 Finished pancake/semantics                                     3m00s   1GB
Jul 28 20:15:03 Starting pancake/parser
Jul 28 20:15:33 Finished pancake/parser                                          30s 743MB
Jul 28 20:15:34 Starting pancake/proofs
Jul 28 20:50:47 Finished pancake/proofs                                       35m13s   4GB
Jul 28 20:50:47 Starting characteristic/examples
Jul 28 20:52:38 Finished characteristic/examples                               1m50s   3GB
Jul 28 20:52:38 Starting tutorial/solutions
Jul 28 20:55:12 Finished tutorial/solutions                                    2m33s   3GB
Jul 28 20:55:12 Starting translator/monadic/examples
Jul 28 20:59:36 Finished translator/monadic/examples                           4m23s   3GB
Jul 28 20:59:36 Starting examples
Jul 28 21:01:10 FAILED: examples
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/num/theories/cv_compute/automation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanned 34 directories
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                                                                                   (0s)     OK
Starting work on divTheory
lcsTheory                                                                                                  (20s)     OK
Starting work on diffTheory
diffTheory                                                                                                 (52s)     OK
Starting work on diffProgTheory
diffProgTheory                                                                                             (12s)FAIL<1>
 Run out of store - interrupting threads
 error in quse /home/cug/hk324/cml-regression/cakeml-2498/basis/CommandLineProofTheory.sml : Interrupt
 error in load $(CAKEMLDIR)/basis/CommandLineProofTheory : Interrupt
 error in load $(CAKEMLDIR)/basis/basis : Interrupt
 error in load /home/cug/hk324/cml-regression/cakeml-2498/examples/diffProgScript : Interrupt
 Uncaught exception: Interrupt
quicksortProgTheory                                                                                        (88s)MKILLED
catProgTheory                                                                                              (88s)MKILLED
divTheory                                                                                                  (88s)MKILLED