# HG changeset patch
# User blanchet
# Date 1337800788 -7200
# Node ID 96c9b8381909a368b5386c4731975942229143e4
# Parent  2aea51a142008e76b94c51d954b6467216f224bc
better handling of incomplete TSTP proofs

diff -r 2aea51a14200 -r 96c9b8381909 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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,6 +481,15 @@
            | 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))
diff -r 2aea51a14200 -r 96c9b8381909 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed May 23 21:19:48 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed May 23 21:19:48 2012 +0200
@@ -541,7 +541,7 @@
   | atp_proof_from_tstplike_proof problem output tstp =
     tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
     |> parse_proof problem (extract_spass_name_vector output)
-    |> sort (step_name_ord o pairself step_name)
+    |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen
diff -r 2aea51a14200 -r 96c9b8381909 src/HOL/Tools/ATP/atp_systems.ML
--- 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
@@ -305,9 +305,9 @@
         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
-     known_szs_status_failures @
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
-      (TimedOut, "time limit exceeded")],
+      (TimedOut, "time limit exceeded")] @
+     known_szs_status_failures,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      let val heuristic = effective_e_selection_heuristic ctxt in
@@ -337,9 +337,13 @@
         "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
-     known_szs_status_failures @
-     [(TimedOut, "CPU time limit exceeded, terminating"),
-      (GaveUp, "No.of.Axioms")],
+     [(* 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"),
+      (GaveUp, "No.of.Axioms")] @
+     known_szs_status_failures,
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
@@ -390,7 +394,6 @@
      |> sos = sosN ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
-     known_perl_failures @
      [(OldSPASS, "SPASS V 3.5"),
       (OldSPASS, "SPASS V 3.7"),
       (GaveUp, "SPASS beiseite: Completion found"),
@@ -399,7 +402,8 @@
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (Unprovable, "No formulae and clauses found in input file"),
-      (InternalError, "Please report this error")],
+      (InternalError, "Please report this error")] @
+      known_perl_failures,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -467,12 +471,12 @@
       ("% SZS output start Refutation", "% SZS output end Refutation"),
       ("% SZS output start Proof", "% SZS output end Proof")],
    known_failures =
-     known_szs_status_failures @
      [(GaveUp, "UNPROVABLE"),
       (GaveUp, "CANNOT PROVE"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
-      (Interrupted, "Aborted by signal SIGINT")],
+      (Interrupted, "Aborted by signal SIGINT")] @
+     known_szs_status_failures,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)