Job 1800

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:46ea63eec171a69d8344514f2c0b9688e63edfae
  Get basis to build again [Feb 25 12:09:48]
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
  Refine definition of what it is to be a vacuous pattern [Feb 25 06:46:55]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 25 12:13:00 Claimed job
Feb 25 12:13:02 Reusing HOL
Feb 25 12:13:16 Starting developers
Feb 25 12:13:20 Finished developers                                               4s 111MB
Feb 25 12:13:20 Starting developers/bin
Feb 25 12:13:25 Finished developers/bin                                           4s 674MB
Feb 25 12:13:25 Starting semantics/ffi
Feb 25 12:13:36 Finished semantics/ffi                                           10s 264MB
Feb 25 12:13:36 Starting semantics
Feb 25 12:15:38 Finished semantics                                             2m02s   1GB
Feb 25 12:15:39 Starting semantics/proofs
Feb 25 12:19:17 Finished semantics/proofs                                      3m38s 938MB
Feb 25 12:19:18 Starting semantics/alt_semantics
Feb 25 12:19:34 Finished semantics/alt_semantics                                 16s 538MB
Feb 25 12:19:34 Starting semantics/alt_semantics/proofs
Feb 25 12:22:03 Finished semantics/alt_semantics/proofs                        2m28s   1GB
Feb 25 12:22:03 Starting basis/pure
Feb 25 12:23:05 Finished basis/pure                                            1m02s   1GB
Feb 25 12:23:05 Starting translator
Feb 25 12:26:08 Finished translator                                            3m02s   1GB
Feb 25 12:26:08 Starting compiler/parsing
Feb 25 12:27:23 Finished compiler/parsing                                      1m14s   2GB
Feb 25 12:27:23 Starting characteristic
Feb 25 12:33:43 Finished characteristic                                        6m19s   2GB
Feb 25 12:33:43 Starting translator/monadic
Feb 25 12:35:38 Finished translator/monadic                                    1m55s   1GB
Feb 25 12:35:38 Starting basis
Feb 25 13:21:40 Finished basis                                                46m00s  25GB
Feb 25 13:21:40 Starting compiler/inference
Feb 25 13:23:09 Finished compiler/inference                                    1m28s   1GB
Feb 25 13:23:09 Starting compiler/backend/reg_alloc
Feb 25 13:24:53 Finished compiler/backend/reg_alloc                            1m43s   1GB
Feb 25 13:24:53 Starting compiler/backend/gc
Feb 25 13:29:14 Finished compiler/backend/gc                                   4m20s   2GB
Feb 25 13:29:14 Starting compiler/backend
Feb 25 13:34:43 Finished compiler/backend                                      5m28s   2GB
Feb 25 13:34:43 Starting compiler/encoders/asm
Feb 25 13:35:13 Finished compiler/encoders/asm                                   30s 872MB
Feb 25 13:35:13 Starting compiler/encoders/x64
Feb 25 13:36:20 Finished compiler/encoders/x64                                 1m06s 889MB
Feb 25 13:36:20 Starting compiler/encoders/arm7
Feb 25 13:38:32 Finished compiler/encoders/arm7                                2m11s   1GB
Feb 25 13:38:32 Starting compiler/encoders/arm8
Feb 25 13:39:14 Finished compiler/encoders/arm8                                  41s   1GB
Feb 25 13:39:14 Starting compiler/encoders/arm8_asl
Feb 25 15:50:57 Finished compiler/encoders/arm8_asl                         2h11m40s  41GB
Feb 25 15:50:58 Starting compiler/encoders/mips
Feb 25 15:52:28 Finished compiler/encoders/mips                                1m30s   1GB
Feb 25 15:52:28 Starting compiler/encoders/riscv
Feb 25 15:54:15 Finished compiler/encoders/riscv                               1m46s   1GB
Feb 25 15:54:15 Starting compiler/encoders/ag32
Feb 25 15:54:37 Finished compiler/encoders/ag32                                  21s 690MB
Feb 25 15:54:37 Starting compiler/backend/x64
Feb 25 15:54:59 Finished compiler/backend/x64                                    21s   1GB
Feb 25 15:54:59 Starting compiler/backend/arm7
Feb 25 15:55:23 Finished compiler/backend/arm7                                   23s   1GB
Feb 25 15:55:23 Starting compiler/backend/arm8
Feb 25 15:55:45 Finished compiler/backend/arm8                                   22s   1GB
Feb 25 15:55:45 Starting compiler/backend/mips
Feb 25 15:56:08 Finished compiler/backend/mips                                   22s   1GB
Feb 25 15:56:08 Starting compiler/backend/riscv
Feb 25 15:56:31 Finished compiler/backend/riscv                                  22s   1GB
Feb 25 15:56:31 Starting compiler/backend/ag32
Feb 25 15:57:55 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 25 15:57:55 Starting compiler/parsing/proofs
Feb 25 16:01:40 Finished compiler/parsing/proofs                               3m44s   1GB
Feb 25 16:01:40 Starting compiler/inference/proofs
Feb 25 16:04:11 Finished compiler/inference/proofs                             2m30s   1GB
Feb 25 16:04:11 Starting compiler/backend/semantics
Feb 25 16:31:59 Finished compiler/backend/semantics                           27m47s   2GB
Feb 25 16:31:59 Starting compiler/backend/reg_alloc/proofs
Feb 25 16:35:33 Finished compiler/backend/reg_alloc/proofs                     3m34s 882MB
Feb 25 16:35:33 Starting compiler/backend/proofs
Feb 25 17:27:36 Finished compiler/backend/proofs                              52m01s  16GB
Feb 25 17:27:36 Starting compiler/backend/serialiser
Feb 25 17:29:12 Finished compiler/backend/serialiser                           1m36s   1GB
Feb 25 17:29:13 Starting compiler/encoders/x64/proofs
Feb 25 17:38:41 Finished compiler/encoders/x64/proofs                          9m28s   6GB
Feb 25 17:38:41 Starting compiler/encoders/arm7/proofs
Feb 25 17:51:46 Finished compiler/encoders/arm7/proofs                        13m04s   3GB
Feb 25 17:51:46 Starting compiler/encoders/arm8/proofs
Feb 25 17:58:41 Finished compiler/encoders/arm8/proofs                         6m55s   1GB
Feb 25 17:58:41 Starting compiler/encoders/arm8_asl/proofs
Feb 25 18:50:33 Finished compiler/encoders/arm8_asl/proofs                    51m50s   4GB
Feb 25 18:50:33 Starting compiler/encoders/mips/proofs
Feb 25 19:00:35 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Feb 25 19:00:36 Starting compiler/encoders/riscv/proofs
Feb 25 19:09:20 Finished compiler/encoders/riscv/proofs                        8m44s   1GB
Feb 25 19:09:20 Starting compiler/encoders/ag32/proofs
Feb 25 19:11:56 Finished compiler/encoders/ag32/proofs                         2m36s 716MB
Feb 25 19:11:57 Starting compiler/backend/x64/proofs
Feb 25 19:12:25 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 25 19:12:25 Starting compiler/backend/arm7/proofs
Feb 25 19:12:53 Finished compiler/backend/arm7/proofs                            27s   1GB
Feb 25 19:12:53 Starting compiler/backend/arm8/proofs
Feb 25 19:13:22 Finished compiler/backend/arm8/proofs                            28s   2GB
Feb 25 19:13:22 Starting compiler/backend/arm8_asl
Feb 25 19:13:45 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 25 19:13:45 Starting compiler/backend/mips/proofs
Feb 25 19:14:12 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 25 19:14:13 Starting compiler/backend/riscv/proofs
Feb 25 19:14:40 Finished compiler/backend/riscv/proofs                           26s   1GB
Feb 25 19:14:40 Starting compiler/backend/ag32/proofs
Feb 25 19:27:30 Finished compiler/backend/ag32/proofs                         12m49s   3GB
Feb 25 19:27:30 Starting compiler/proofs
Feb 25 19:29:57 Finished compiler/proofs                                       2m27s   4GB
Feb 25 19:29:57 Starting candle/set-theory
Feb 25 19:30:31 Finished candle/set-theory                                       33s   1GB
Feb 25 19:30:32 Starting candle/syntax-lib
Feb 25 19:30:44 Finished candle/syntax-lib                                       12s 659MB
Feb 25 19:30:44 Starting candle/standard/syntax
Feb 25 19:32:46 Finished candle/standard/syntax                                2m01s   1GB
Feb 25 19:32:46 Starting candle/standard/semantics
Feb 25 19:34:34 Finished candle/standard/semantics                             1m47s   1GB
Feb 25 19:34:34 Starting candle/standard/monadic
Feb 25 19:36:26 Finished candle/standard/monadic                               1m51s   1GB
Feb 25 19:36:26 Starting candle/standard/ml_kernel
Feb 25 19:42:29 Finished candle/standard/ml_kernel                             6m02s   3GB
Feb 25 19:42:29 Starting candle/overloading/syntax
Feb 25 19:45:40 Finished candle/overloading/syntax                             3m11s   1GB
Feb 25 19:45:40 Starting candle/overloading/semantics
Feb 25 19:57:19 Finished candle/overloading/semantics                         11m37s   2GB
Feb 25 19:57:19 Starting candle/overloading/monadic
Feb 25 19:59:54 Finished candle/overloading/monadic                            2m35s   1GB
Feb 25 19:59:54 Starting candle/overloading/ml_kernel
Feb 25 20:06:56 Finished candle/overloading/ml_kernel                          7m02s   4GB
Feb 25 20:06:57 Starting candle/overloading/ml_checker
Feb 25 20:09:30 Finished candle/overloading/ml_checker                         2m33s   2GB
Feb 25 20:09:30 Starting candle/prover
Feb 25 20:17:01 Finished candle/prover                                         7m30s   2GB
Feb 25 20:17:01 Starting pancake
Feb 25 20:19:40 Finished pancake                                               2m38s   2GB
Feb 25 20:19:40 Starting pancake/ffi
Feb 25 20:19:40 Finished pancake/ffi                                              0s  35MB
Feb 25 20:19:40 Starting pancake/semantics
Feb 25 20:22:10 Finished pancake/semantics                                     2m30s   1GB
Feb 25 20:22:10 Starting pancake/proofs
Feb 25 20:34:12 Finished pancake/proofs                                       12m01s   5GB
Feb 25 20:34:12 Starting characteristic/examples
Feb 25 20:35:35 Finished characteristic/examples                               1m23s   3GB
Feb 25 20:35:35 Starting tutorial/solutions
Feb 25 20:52:29 Finished tutorial/solutions                                   16m53s   9GB
Feb 25 20:52:29 Starting translator/monadic/examples
Feb 25 20:56:17 Finished translator/monadic/examples                           3m48s   3GB
Feb 25 20:56:17 Starting examples
Feb 25 20:58:22 FAILED: examples
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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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 30 directories
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
README.md                                                 examples  (0s)     OK
Starting work on catProgTheory
source_valuesTheory                             examples/bootstrap  (1s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                             examples/bootstrap  (0s)     OK
Starting work on parsingTheory
regexp_parserTheory              examples/formal-languages/regular (11s)     OK
Starting work on printingTheory
printingTheory                                  examples/bootstrap  (4s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]   (11.320s) 
Starting work on lcsTheory
parsingTheory                                   examples/bootstrap (22s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (29.630s) 
Starting work on divTheory
lcsTheory                                                 examples (17s)     OK
Starting work on diffTheory
diffTheory                                                examples (47s)     OK
Starting work on diffProgTheory
catProgTheory                                             examples (84s)     OK
Starting work on doubleProgTheory
quicksortProgTheory                                       examples (97s)     OK
Starting work on array_searchProgTheory
divTheory                                                 examples (92s)FAIL<1>
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 321, character 2 and line 322, character 59:
 at Defn.parse_quote:
 at boolSyntax.dest_eq(_ty):
 not an "="
 error in quse /home/cug/hk324/cml-regression/cakeml-1800/examples/divScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 321, character 2 and line 322, character 59:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1800/examples/divScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 321, character 2 and line 322, character 59:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 321, character 2 and line 322, character 59:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
diffProgTheory                                            examples (35s)MKILLED
doubleProgTheory                                          examples (33s)MKILLED
array_searchProgTheory                                    examples (21s)MKILLED