--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed May 23 21:19:48 2012 +0200
@@ -481,15 +481,6 @@
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time |> Time.toMilliseconds
val msg = message (preplay ()) ^ message_tail
- val (outcome, used_facts) =
- (* Repair incomplete or missing proofs. Better do it here and not in
- Sledgehammer, so that actual Sledgehammer users get a chance to report
- the issue. FIXME: This is a temporary hack. *)
- if outcome = SOME ATP_Proof.ProofIncomplete orelse
- outcome = SOME ATP_Proof.ProofMissing then
- (NONE, [])
- else
- (outcome, used_facts)
in
case outcome of
NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed May 23 21:19:48 2012 +0200
@@ -188,6 +188,8 @@
is_axiom_used_in_proof is_typed_helper_name atp_proof
val leo2_ext = "extcnf_equal_neg"
+val leo2_unfold_def = "unfold_def"
+
val isa_ext = Thm.get_name_hint @{thm ext}
val isa_short_ext = Long_Name.base_name isa_ext
@@ -198,17 +200,24 @@
else
isa_ext
+fun add_all_defs fact_names accum =
+ Vector.foldl (fn (facts, factss) =>
+ filter (fn (_, (_, status)) => status = Def) facts @ factss)
+ accum fact_names
+
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
(if rule = leo2_ext then
insert (op =) (ext_name ctxt, (Global, General))
+ else if rule = leo2_unfold_def then
+ (* LEO 1.3.3 does not record definitions properly, leading to missing
+ dependencies in the TSTP proof. Remove the next line once this is
+ fixed. *)
+ add_all_defs fact_names
else if rule = satallax_unsat_coreN then
(fn [] =>
(* Satallax doesn't include definitions in its unsatisfiable cores,
so we assume the worst and include them all here. *)
- Vector.foldl (fn (facts, factss) =>
- filter (fn (_, (_, status)) => status = Def) facts
- @ factss)
- [(ext_name ctxt, (Global, General))] fact_names
+ [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
| facts => facts)
else
I)
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed May 23 21:19:48 2012 +0200
@@ -337,11 +337,7 @@
"--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
proof_delims = tstp_proof_delims,
known_failures =
- [(* LEO 1.3.3 does not record definitions properly, leading to missing
- dependencies in the TSTP proof. Remove the next line once this is
- fixed. *)
- (ProofIncomplete, "_def,definition,"),
- (TimedOut, "CPU time limit exceeded, terminating"),
+ [(TimedOut, "CPU time limit exceeded, terminating"),
(GaveUp, "No.of.Axioms")] @
known_szs_status_failures,
prem_kind = Hypothesis,