Job 1001

CakeML:ad1ba92699c16992f4dd0a2b075465eb2eb44a03
  Provide old_dxrule in preamble; continue fixing broken scripts [Aug 14 06:46:10]
HOL:ea47c77c31d0bce19dc95254ee42d589d1ef0bea
  Provide Triviality syntax as alias for Theorem[local] [Aug 14 06:42:27]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 15 01:30:16 Claimed job
Aug 15 01:30:20 Building HOL
Aug 15 01:39:48 Starting developers
Aug 15 01:39:50 Finished developers                                               2s  19MB
Aug 15 01:39:50 Starting developers/bin
Aug 15 01:39:57 Finished developers/bin                                           6s 960MB
Aug 15 01:39:57 Starting semantics/ffi
Aug 15 01:40:36 Finished semantics/ffi                                           38s 492MB
Aug 15 01:40:36 Starting semantics
Aug 15 01:42:11 Finished semantics                                             1m35s   1GB
Aug 15 01:42:12 Starting semantics/proofs
Aug 15 01:45:13 Finished semantics/proofs                                      3m01s 955MB
Aug 15 01:45:14 Starting semantics/alt_semantics
Aug 15 01:45:22 Finished semantics/alt_semantics                                  8s 263MB
Aug 15 01:45:22 Starting semantics/alt_semantics/proofs
Aug 15 01:47:11 Finished semantics/alt_semantics/proofs                        1m48s 875MB
Aug 15 01:47:11 Starting basis/pure
Aug 15 01:50:49 Finished basis/pure                                            3m37s 682MB
Aug 15 01:50:49 Starting translator
Aug 15 01:52:35 Finished translator                                            1m45s   1GB
Aug 15 01:52:35 Starting compiler/parsing
Aug 15 01:53:32 Finished compiler/parsing                                        57s   1GB
Aug 15 01:53:32 Starting characteristic
Aug 15 01:58:52 Finished characteristic                                        5m19s   1GB
Aug 15 01:58:53 Starting translator/monadic
Aug 15 02:00:25 Finished translator/monadic                                    1m32s   1GB
Aug 15 02:00:25 Starting basis
Aug 15 02:01:33 FAILED: basis
]0;Holmake: pure]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: pure]0;Holmake: ~/oven/regression/cakeml-1001/misc]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-1001/misc]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-1001/misc]0;Holmake: ~/oven/regression/cakeml-1001/developers]0;Holmake: ~/oven/regression/cakeml-1001/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-1001/misc]0;Holmake: ~/oven/regression/cakeml-1001/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1001/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-1001/misc]0;Holmake: ~/oven/regression/cakeml-1001/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-1001/characteristic]0;Holmake: ~/oven/regression/cakeml-1001/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1001/semantics]0;Holmake: ~/oven/regression/cakeml-1001/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1001/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-1001/semantics]0;Holmake: ~/oven/regression/cakeml-1001/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-1001/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1001/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-1001/characteristic]0;Holmake: ~/oven/regression/cakeml-1001/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1001/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-1001/characteristic]0;Holmake: ~/oven/regression/cakeml-1001/translator]0;Holmake: ~/oven/regression/cakeml-1001/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-1001/characteristic]0;Holmake: ~/oven/regression/cakeml-1001/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-1001/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1001/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-1001/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-1001/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1001/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
MarshallingTheory                                                            OK
Starting work on fsFFITheory
runtimeFFITheory                                                             OK
Starting work on README.md
README.md                                                                    OK
Starting work on basis_ffi.o
clFFITheory                                                                  OK
basis_ffi.o                                                                  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