Job 998

CakeML:8057740df8ad05a894a3add5c14bf7c3f20e49d2
  Fix some broken drule applications [Aug 13 01:00:20]
HOL:9cb0910724825080500e1bd8f653dd9dc748da02
  Document drule change from 812a08a5 [Aug 11 23:06:27]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 13 01:10:35 Claimed job
Aug 13 01:10:39 Building HOL
Aug 13 01:18:38 Starting developers
Aug 13 01:18:39 Finished developers                                               0s  20MB
Aug 13 01:18:39 Starting developers/bin
Aug 13 01:20:03 Finished developers/bin                                        1m23s 166MB
Aug 13 01:20:03 Starting semantics/ffi
Aug 13 01:20:37 Finished semantics/ffi                                           33s 318MB
Aug 13 01:20:37 Starting semantics
Aug 13 01:22:07 Finished semantics                                             1m29s   1GB
Aug 13 01:22:08 Starting semantics/proofs
Aug 13 01:25:05 Finished semantics/proofs                                      2m57s   1GB
Aug 13 01:25:06 Starting semantics/alt_semantics
Aug 13 01:25:12 Finished semantics/alt_semantics                                  5s 272MB
Aug 13 01:25:12 Starting semantics/alt_semantics/proofs
Aug 13 01:27:01 Finished semantics/alt_semantics/proofs                        1m48s 717MB
Aug 13 01:27:01 Starting basis/pure
Aug 13 01:30:31 Finished basis/pure                                            3m29s 721MB
Aug 13 01:30:31 Starting translator
Aug 13 01:32:17 Finished translator                                            1m44s   1GB
Aug 13 01:32:17 Starting compiler/parsing
Aug 13 01:33:14 Finished compiler/parsing                                        56s   1GB
Aug 13 01:33:15 Starting characteristic
Aug 13 01:38:21 Finished characteristic                                        5m05s   2GB
Aug 13 01:38:21 Starting translator/monadic
Aug 13 01:39:48 Finished translator/monadic                                    1m26s   1GB
Aug 13 01:39:48 Starting basis
Aug 13 01:40:54 FAILED: basis
]0;Holmake: pure]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: pure]0;Holmake: ~/regression/cakeml-998/misc]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-998/misc]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-9cb0910724825080500e1bd8f653dd9dc748da02/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-998/misc]0;Holmake: ~/regression/cakeml-998/developers]0;Holmake: ~/regression/cakeml-998/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-998/misc]0;Holmake: ~/regression/cakeml-998/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-998/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-998/misc]0;Holmake: ~/regression/cakeml-998/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: pure]0;Holmake: pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-998/characteristic]0;Holmake: ~/regression/cakeml-998/compiler/parsing]0;Holmake: ~/regression/cakeml-998/semantics]0;Holmake: ~/regression/cakeml-998/semantics/ffi]0;Holmake: ~/regression/cakeml-998/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-998/semantics]0;Holmake: ~/regression/cakeml-998/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-998/compiler/parsing]0;Holmake: ~/regression/cakeml-998/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-998/characteristic]0;Holmake: ~/regression/cakeml-998/semantics/proofs]0;Holmake: ~/regression/cakeml-998/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-998/characteristic]0;Holmake: ~/regression/cakeml-998/translator]0;Holmake: ~/regression/cakeml-998/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-998/characteristic]0;Holmake: ~/regression/cakeml-998/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-998/translator/monadic]0;Holmake: ~/regression/cakeml-998/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-998/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-998/translator/monadic]0;Holmake: ~/regression/cakeml-998/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/basis[0m
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
runtimeFFITheory                                                                                           OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                OK
MarshallingTheory                                                                                          OK
Starting work on fsFFITheory
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>
       (POSTv lv. &LIST_TYPE A ls lv * heap_inv)
 
 failed.
 Failed to prove theorem tabulate_aux_inv_spec.
 
 Exception raised at Tactic.MATCH_MP_TAC:
 No match (THEN1 on line 159) (THEN1 on line 171) (THEN1 on line 179) (THEN1 on line 181) (THEN1 on line 183)
 error in quse /home/myreen/regression/cakeml-998/basis/ListProgScript.sml : 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"}
 error in load ListProgScript : 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"}
 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