Overview

Job 1802

CakeML:f99af5a3ce396207686cb57a9c71820469fbc64c
  fix the broken proofs
#861 (pan-to-mc_updated)
Merging into:46ea63eec171a69d8344514f2c0b9688e63edfae
  Get basis to build again
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
  Refine definition of what it is to be a vacuous pattern
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               4s 112MB
 Starting developers/bin
 Finished developers/bin                                           5s 670MB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s 227MB
 Starting semantics
 Finished semantics                                             2m34s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      4m19s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 19s 468MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m55s 823MB
 Starting basis/pure
 Finished basis/pure                                            3m28s 815MB
 Starting translator
 Finished translator                                            4m06s   2GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m48s   2GB
 Starting characteristic
 Finished characteristic                                        7m23s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    2m12s   1GB
 Starting basis
 Finished basis                                                53m44s   9GB
 Starting compiler/inference
 Finished compiler/inference                                    1m38s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            2m00s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   5m44s   1GB
 Starting compiler/backend
 Finished compiler/backend                                      7m24s   1GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   34s 880MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m20s 656MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                2m28s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  48s 933MB
 Starting compiler/encoders/arm8_asl
 Finished compiler/encoders/arm8_asl                         2h39m42s  10GB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                2m00s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               2m22s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  27s 745MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    28s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   27s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   27s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   27s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  27s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m53s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m41s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m18s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           41m25s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     4m21s 726MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h15m12s   7GB
 Starting compiler/backend/serialiser
 Finished compiler/backend/serialiser                           1m46s   2GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         11m43s   1GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        15m11s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         7m39s   1GB
 Starting compiler/encoders/arm8_asl/proofs
 Finished compiler/encoders/arm8_asl/proofs                    58m44s   5GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        12m24s 917MB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       11m14s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         3m27s 515MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             33s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            34s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            34s   1GB
 Starting compiler/backend/arm8_asl
 Finished compiler/backend/arm8_asl                               27s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            34s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           34s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         16m57s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       3m00s   4GB
 Starting candle/set-theory
 Finished candle/set-theory                                       44s 892MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       15s 589MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                2m32s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m17s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m26s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             8m36s   2GB
 Starting candle/overloading/syntax
 Finished candle/overloading/syntax                             4m06s 936MB
 Starting candle/overloading/semantics
 Finished candle/overloading/semantics                         14m38s   2GB
 Starting candle/overloading/monadic
 Finished candle/overloading/monadic                            2m53s   1GB
 Starting candle/overloading/ml_kernel
 Finished candle/overloading/ml_kernel                          8m25s   3GB
 Starting candle/overloading/ml_checker
 Finished candle/overloading/ml_checker                         2m43s   3GB
 Starting candle/prover
 Finished candle/prover                                         8m47s   3GB
 Starting pancake
 Finished pancake                                               4m18s   2GB
 Starting pancake/ffi
 Finished pancake/ffi                                              0s  17MB
 Starting pancake/semantics
 Finished pancake/semantics                                     3m01s   1GB
 Starting pancake/proofs
 Finished pancake/proofs                                       14m20s   7GB
 Starting characteristic/examples
 Finished characteristic/examples                               2m02s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   21m24s   5GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           5m11s   2GB
 Starting examples
 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