Overview

Job 999

CakeML:df1f93720f2c2199f983713e5b4358e95ccdced0
  Fix drule applications by using old_drule from preamble
HOL:9cb0910724825080500e1bd8f653dd9dc748da02
  Document drule change from 812a08a5
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s  20MB
 Starting developers/bin
 Finished developers/bin                                           6s 960MB
 Starting semantics/ffi
 Finished semantics/ffi                                           38s 507MB
 Starting semantics
 Finished semantics                                             1m36s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m00s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  8s 265MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        1m47s 707MB
 Starting basis/pure
 Finished basis/pure                                            3m37s 696MB
 Starting translator
 Finished translator                                            1m45s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        57s   2GB
 Starting characteristic
 Finished characteristic                                        5m13s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m33s   1GB
 Starting basis
 FAILED: basis
]0;Holmake: pure]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: pure]0;Holmake: ~/oven/regression/cakeml-999/misc]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-999/misc]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-999/misc]0;Holmake: ~/oven/regression/cakeml-999/developers]0;Holmake: ~/oven/regression/cakeml-999/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-999/misc]0;Holmake: ~/oven/regression/cakeml-999/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-999/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-999/misc]0;Holmake: ~/oven/regression/cakeml-999/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-999/characteristic]0;Holmake: ~/oven/regression/cakeml-999/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-999/semantics]0;Holmake: ~/oven/regression/cakeml-999/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-999/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-999/semantics]0;Holmake: ~/oven/regression/cakeml-999/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-999/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-999/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-999/characteristic]0;Holmake: ~/oven/regression/cakeml-999/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-999/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-999/characteristic]0;Holmake: ~/oven/regression/cakeml-999/translator]0;Holmake: ~/oven/regression/cakeml-999/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-999/characteristic]0;Holmake: ~/oven/regression/cakeml-999/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-999/translator/monadic]0;Holmake: ~/oven/regression/cakeml-999/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-999/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-999/translator/monadic]0;Holmake: ~/oven/regression/cakeml-999/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/basis
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
runtimeFFITheory                                                             OK
Starting work on README.md
MarshallingTheory                                                            OK
Starting work on fsFFITheory
README.md                                                                    OK
Starting work on basis_ffi.o
basis_ffi.o                                                                  OK
clFFITheory                                                                  OK
RuntimeProgTheory                                                            OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                  OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                             OK
Starting work on ListProgTheory
RuntimeProofTheory                                                           OK
ListProgTheory                                                      FAILED! <1>
     ls = REVERSE acc ++ GENLIST (f  FUNPOW SUC n) (m  n) 
     (i iv.
          NUM i iv  n  i  i < m 
          app p fv [iv] heap_inv (POSTv v. &A (... ... ) v * heap_inv)) 
     app p tabulate_aux_v [nv; mv; fv; accv] heap_inv
       (POSTv lv. &LIST_TYPE A ls lv * heap_inv)
 
 failed.
 Failed to prove theorem tabulate_aux_inv_spec.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 159) (THEN1 on line 171) (THEN1 on line 179) (THEN1 on line 181) (THEN1 on line 183)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
fsFFIPropsTheory                                                       M-KILLED