Job 1802

CakeML:f99af5a3ce396207686cb57a9c71820469fbc64c
  fix the broken proofs [Feb 25 03:30:48]
#861 (pan-to-mc_updated)
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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 25 15:45:01 Claimed job
Feb 25 15:45:12 Building HOL
Feb 25 15:56:28 Starting developers
Feb 25 15:56:33 Finished developers                                               4s 112MB
Feb 25 15:56:33 Starting developers/bin
Feb 25 15:56:39 Finished developers/bin                                           5s 670MB
Feb 25 15:56:39 Starting semantics/ffi
Feb 25 15:56:50 Finished semantics/ffi                                           11s 227MB
Feb 25 15:56:50 Starting semantics
Feb 25 15:59:25 Finished semantics                                             2m34s   1GB
Feb 25 15:59:26 Starting semantics/proofs
Feb 25 16:03:45 Finished semantics/proofs                                      4m19s   1GB
Feb 25 16:03:45 Starting semantics/alt_semantics
Feb 25 16:04:05 Finished semantics/alt_semantics                                 19s 468MB
Feb 25 16:04:05 Starting semantics/alt_semantics/proofs
Feb 25 16:07:01 Finished semantics/alt_semantics/proofs                        2m55s 823MB
Feb 25 16:07:01 Starting basis/pure
Feb 25 16:10:29 Finished basis/pure                                            3m28s 815MB
Feb 25 16:10:29 Starting translator
Feb 25 16:14:36 Finished translator                                            4m06s   2GB
Feb 25 16:14:36 Starting compiler/parsing
Feb 25 16:16:25 Finished compiler/parsing                                      1m48s   2GB
Feb 25 16:16:25 Starting characteristic
Feb 25 16:23:49 Finished characteristic                                        7m23s   1GB
Feb 25 16:23:49 Starting translator/monadic
Feb 25 16:26:04 Finished translator/monadic                                    2m12s   1GB
Feb 25 16:26:04 Starting basis
Feb 25 17:19:49 Finished basis                                                53m44s   9GB
Feb 25 17:19:49 Starting compiler/inference
Feb 25 17:21:28 Finished compiler/inference                                    1m38s   1GB
Feb 25 17:21:28 Starting compiler/backend/reg_alloc
Feb 25 17:23:29 Finished compiler/backend/reg_alloc                            2m00s   1GB
Feb 25 17:23:29 Starting compiler/backend/gc
Feb 25 17:29:15 Finished compiler/backend/gc                                   5m44s   1GB
Feb 25 17:29:16 Starting compiler/backend
Feb 25 17:36:40 Finished compiler/backend                                      7m24s   1GB
Feb 25 17:36:41 Starting compiler/encoders/asm
Feb 25 17:37:15 Finished compiler/encoders/asm                                   34s 880MB
Feb 25 17:37:15 Starting compiler/encoders/x64
Feb 25 17:38:36 Finished compiler/encoders/x64                                 1m20s 656MB
Feb 25 17:38:36 Starting compiler/encoders/arm7
Feb 25 17:41:05 Finished compiler/encoders/arm7                                2m28s   1GB
Feb 25 17:41:05 Starting compiler/encoders/arm8
Feb 25 17:41:54 Finished compiler/encoders/arm8                                  48s 933MB
Feb 25 17:41:54 Starting compiler/encoders/arm8_asl
Feb 25 20:21:37 Finished compiler/encoders/arm8_asl                         2h39m42s  10GB
Feb 25 20:21:38 Starting compiler/encoders/mips
Feb 25 20:23:38 Finished compiler/encoders/mips                                2m00s   1GB
Feb 25 20:23:39 Starting compiler/encoders/riscv
Feb 25 20:26:01 Finished compiler/encoders/riscv                               2m22s   1GB
Feb 25 20:26:01 Starting compiler/encoders/ag32
Feb 25 20:26:28 Finished compiler/encoders/ag32                                  27s 745MB
Feb 25 20:26:29 Starting compiler/backend/x64
Feb 25 20:26:57 Finished compiler/backend/x64                                    28s   1GB
Feb 25 20:26:57 Starting compiler/backend/arm7
Feb 25 20:27:25 Finished compiler/backend/arm7                                   27s   1GB
Feb 25 20:27:25 Starting compiler/backend/arm8
Feb 25 20:27:53 Finished compiler/backend/arm8                                   27s   1GB
Feb 25 20:27:53 Starting compiler/backend/mips
Feb 25 20:28:21 Finished compiler/backend/mips                                   27s   1GB
Feb 25 20:28:21 Starting compiler/backend/riscv
Feb 25 20:28:49 Finished compiler/backend/riscv                                  27s   1GB
Feb 25 20:28:49 Starting compiler/backend/ag32
Feb 25 20:30:43 Finished compiler/backend/ag32                                 1m53s   1GB
Feb 25 20:30:43 Starting compiler/parsing/proofs
Feb 25 20:35:24 Finished compiler/parsing/proofs                               4m41s   1GB
Feb 25 20:35:24 Starting compiler/inference/proofs
Feb 25 20:38:43 Finished compiler/inference/proofs                             3m18s   1GB
Feb 25 20:38:44 Starting compiler/backend/semantics
Feb 25 21:20:10 Finished compiler/backend/semantics                           41m25s   2GB
Feb 25 21:20:10 Starting compiler/backend/reg_alloc/proofs
Feb 25 21:24:33 Finished compiler/backend/reg_alloc/proofs                     4m21s 726MB
Feb 25 21:24:33 Starting compiler/backend/proofs
Feb 25 22:39:46 Finished compiler/backend/proofs                            1h15m12s   7GB
Feb 25 22:39:46 Starting compiler/backend/serialiser
Feb 25 22:41:33 Finished compiler/backend/serialiser                           1m46s   2GB
Feb 25 22:41:33 Starting compiler/encoders/x64/proofs
Feb 25 22:53:17 Finished compiler/encoders/x64/proofs                         11m43s   1GB
Feb 25 22:53:17 Starting compiler/encoders/arm7/proofs
Feb 25 23:08:30 Finished compiler/encoders/arm7/proofs                        15m11s   3GB
Feb 25 23:08:30 Starting compiler/encoders/arm8/proofs
Feb 25 23:16:09 Finished compiler/encoders/arm8/proofs                         7m39s   1GB
Feb 25 23:16:09 Starting compiler/encoders/arm8_asl/proofs
Feb 26 00:14:56 Finished compiler/encoders/arm8_asl/proofs                    58m44s   5GB
Feb 26 00:14:56 Starting compiler/encoders/mips/proofs
Feb 26 00:27:20 Finished compiler/encoders/mips/proofs                        12m24s 917MB
Feb 26 00:27:20 Starting compiler/encoders/riscv/proofs
Feb 26 00:38:36 Finished compiler/encoders/riscv/proofs                       11m14s   1GB
Feb 26 00:38:36 Starting compiler/encoders/ag32/proofs
Feb 26 00:42:03 Finished compiler/encoders/ag32/proofs                         3m27s 515MB
Feb 26 00:42:04 Starting compiler/backend/x64/proofs
Feb 26 00:42:37 Finished compiler/backend/x64/proofs                             33s   1GB
Feb 26 00:42:38 Starting compiler/backend/arm7/proofs
Feb 26 00:43:12 Finished compiler/backend/arm7/proofs                            34s   1GB
Feb 26 00:43:12 Starting compiler/backend/arm8/proofs
Feb 26 00:43:47 Finished compiler/backend/arm8/proofs                            34s   1GB
Feb 26 00:43:48 Starting compiler/backend/arm8_asl
Feb 26 00:44:15 Finished compiler/backend/arm8_asl                               27s   1GB
Feb 26 00:44:15 Starting compiler/backend/mips/proofs
Feb 26 00:44:50 Finished compiler/backend/mips/proofs                            34s   1GB
Feb 26 00:44:50 Starting compiler/backend/riscv/proofs
Feb 26 00:45:24 Finished compiler/backend/riscv/proofs                           34s   1GB
Feb 26 00:45:24 Starting compiler/backend/ag32/proofs
Feb 26 01:02:22 Finished compiler/backend/ag32/proofs                         16m57s   2GB
Feb 26 01:02:23 Starting compiler/proofs
Feb 26 01:05:23 Finished compiler/proofs                                       3m00s   4GB
Feb 26 01:05:23 Starting candle/set-theory
Feb 26 01:06:07 Finished candle/set-theory                                       44s 892MB
Feb 26 01:06:07 Starting candle/syntax-lib
Feb 26 01:06:24 Finished candle/syntax-lib                                       15s 589MB
Feb 26 01:06:24 Starting candle/standard/syntax
Feb 26 01:08:57 Finished candle/standard/syntax                                2m32s   1GB
Feb 26 01:08:57 Starting candle/standard/semantics
Feb 26 01:11:15 Finished candle/standard/semantics                             2m17s   1GB
Feb 26 01:11:15 Starting candle/standard/monadic
Feb 26 01:13:42 Finished candle/standard/monadic                               2m26s   1GB
Feb 26 01:13:42 Starting candle/standard/ml_kernel
Feb 26 01:22:19 Finished candle/standard/ml_kernel                             8m36s   2GB
Feb 26 01:22:19 Starting candle/overloading/syntax
Feb 26 01:26:26 Finished candle/overloading/syntax                             4m06s 936MB
Feb 26 01:26:26 Starting candle/overloading/semantics
Feb 26 01:41:05 Finished candle/overloading/semantics                         14m38s   2GB
Feb 26 01:41:05 Starting candle/overloading/monadic
Feb 26 01:43:59 Finished candle/overloading/monadic                            2m53s   1GB
Feb 26 01:43:59 Starting candle/overloading/ml_kernel
Feb 26 01:52:25 Finished candle/overloading/ml_kernel                          8m25s   3GB
Feb 26 01:52:25 Starting candle/overloading/ml_checker
Feb 26 01:55:09 Finished candle/overloading/ml_checker                         2m43s   3GB
Feb 26 01:55:09 Starting candle/prover
Feb 26 02:03:56 Finished candle/prover                                         8m47s   3GB
Feb 26 02:03:56 Starting pancake
Feb 26 02:08:15 Finished pancake                                               4m18s   2GB
Feb 26 02:08:15 Starting pancake/ffi
Feb 26 02:08:16 Finished pancake/ffi                                              0s  17MB
Feb 26 02:08:16 Starting pancake/semantics
Feb 26 02:11:18 Finished pancake/semantics                                     3m01s   1GB
Feb 26 02:11:18 Starting pancake/proofs
Feb 26 02:25:39 Finished pancake/proofs                                       14m20s   7GB
Feb 26 02:25:40 Starting characteristic/examples
Feb 26 02:27:43 Finished characteristic/examples                               2m02s   1GB
Feb 26 02:27:43 Starting tutorial/solutions
Feb 26 02:49:07 Finished tutorial/solutions                                   21m24s   5GB
Feb 26 02:49:07 Starting translator/monadic/examples
Feb 26 02:54:19 Finished translator/monadic/examples                           5m11s   2GB
Feb 26 02:54:20 Starting examples
Feb 26 02:57:19 FAILED: examples
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
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  (2s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                             examples/bootstrap  (1s)     OK
Starting work on parsingTheory
regexp_parserTheory              examples/formal-languages/regular (15s)     OK
Starting work on printingTheory
printingTheory                                  examples/bootstrap  (6s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]   (15.983s) 
Starting work on lcsTheory
parsingTheory                                   examples/bootstrap (30s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (40.830s) 
Starting work on divTheory
lcsTheory                                                 examples (25s)     OK
Starting work on diffTheory
diffTheory                                                examples (66s)     OK
Starting work on diffProgTheory
catProgTheory                                             examples(123s)     OK
Starting work on doubleProgTheory
quicksortProgTheory                                       examples(137s)     OK
Starting work on array_searchProgTheory
divTheory                                                 examples(134s)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/cake/oven/regression/cakeml-1802/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/cake/oven/regression/cakeml-1802/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 (53s)MKILLED
doubleProgTheory                                          examples (45s)MKILLED
array_searchProgTheory                                    examples (33s)MKILLED