1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed May 23 21:19:48 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed May 23 21:19:48 2012 +0200
     1.3 @@ -481,6 +481,15 @@
     1.4             | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     1.5      val time_prover = run_time |> Time.toMilliseconds
     1.6      val msg = message (preplay ()) ^ message_tail
     1.7 +    val (outcome, used_facts) =
     1.8 +      (* Repair incomplete or missing proofs. Better do it here and not in
     1.9 +         Sledgehammer, so that actual Sledgehammer users get a chance to report
    1.10 +         the issue. FIXME: This is a temporary hack. *)
    1.11 +      if outcome = SOME ATP_Proof.ProofIncomplete orelse
    1.12 +         outcome = SOME ATP_Proof.ProofMissing then
    1.13 +        (NONE, [])
    1.14 +      else
    1.15 +        (outcome, used_facts)
    1.16    in
    1.17      case outcome of
    1.18        NONE => (msg, SH_OK (time_isa, time_prover, used_facts))

     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed May 23 21:19:48 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed May 23 21:19:48 2012 +0200
     2.3 @@ -541,7 +541,7 @@
     2.4    | atp_proof_from_tstplike_proof problem output tstp =
     2.5      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
     2.6      |> parse_proof problem (extract_spass_name_vector output)
     2.7 -    |> sort (step_name_ord o pairself step_name)
     2.8 +    |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
     2.9  
    2.10  fun clean_up_dependencies _ [] = []
    2.11    | clean_up_dependencies seen

     3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 21:19:48 2012 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 21:19:48 2012 +0200
     3.3 @@ -305,9 +305,9 @@
     3.4          "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
     3.5     proof_delims = tstp_proof_delims,
     3.6     known_failures =
     3.7 -     known_szs_status_failures @
     3.8       [(TimedOut, "Failure: Resource limit exceeded (time)"),
     3.9 -      (TimedOut, "time limit exceeded")],
    3.10 +      (TimedOut, "time limit exceeded")] @
    3.11 +     known_szs_status_failures,
    3.12     prem_kind = Conjecture,
    3.13     best_slices = fn ctxt =>
    3.14       let val heuristic = effective_e_selection_heuristic ctxt in
    3.15 @@ -337,9 +337,13 @@
    3.16          "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
    3.17     proof_delims = tstp_proof_delims,
    3.18     known_failures =
    3.19 -     known_szs_status_failures @
    3.20 -     [(TimedOut, "CPU time limit exceeded, terminating"),
    3.21 -      (GaveUp, "No.of.Axioms")],
    3.22 +     [(* LEO 1.3.3 does not record definitions properly, leading to missing
    3.23 +         dependencies in the TSTP proof. Remove the next line once this is
    3.24 +         fixed. *)
    3.25 +      (ProofIncomplete, "_def,definition,"),
    3.26 +      (TimedOut, "CPU time limit exceeded, terminating"),
    3.27 +      (GaveUp, "No.of.Axioms")] @
    3.28 +     known_szs_status_failures,
    3.29     prem_kind = Hypothesis,
    3.30     best_slices =
    3.31       (* FUDGE *)
    3.32 @@ -390,7 +394,6 @@
    3.33       |> sos = sosN ? prefix "-SOS=1 ",
    3.34     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    3.35     known_failures =
    3.36 -     known_perl_failures @
    3.37       [(OldSPASS, "SPASS V 3.5"),
    3.38        (OldSPASS, "SPASS V 3.7"),
    3.39        (GaveUp, "SPASS beiseite: Completion found"),
    3.40 @@ -399,7 +402,8 @@
    3.41        (MalformedInput, "Undefined symbol"),
    3.42        (MalformedInput, "Free Variable"),
    3.43        (Unprovable, "No formulae and clauses found in input file"),
    3.44 -      (InternalError, "Please report this error")],
    3.45 +      (InternalError, "Please report this error")] @
    3.46 +      known_perl_failures,
    3.47     prem_kind = Conjecture,
    3.48     best_slices = fn ctxt =>
    3.49       (* FUDGE *)
    3.50 @@ -467,12 +471,12 @@
    3.51        ("% SZS output start Refutation", "% SZS output end Refutation"),
    3.52        ("% SZS output start Proof", "% SZS output end Proof")],
    3.53     known_failures =
    3.54 -     known_szs_status_failures @
    3.55       [(GaveUp, "UNPROVABLE"),
    3.56        (GaveUp, "CANNOT PROVE"),
    3.57        (Unprovable, "Satisfiability detected"),
    3.58        (Unprovable, "Termination reason: Satisfiable"),
    3.59 -      (Interrupted, "Aborted by signal SIGINT")],
    3.60 +      (Interrupted, "Aborted by signal SIGINT")] @
    3.61 +     known_szs_status_failures,
    3.62     prem_kind = Conjecture,
    3.63     best_slices = fn ctxt =>
    3.64       (* FUDGE *)