# HG changeset patch # User blanchet # Date 1305888478 -7200 # Node ID e336ef6313aa1e4921c4cdc328445b8e03a9357d # Parent d1aad0957eb2360ab16c30f617f6d7cc6b9715a7 more informative message when Sledgehammer finds an unsound proof diff -r d1aad0957eb2 -r e336ef6313aa src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri May 20 12:35:44 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri May 20 12:47:58 2011 +0200 @@ -3,7 +3,7 @@ Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen -Abstract representation of ATP proofs and TSTP/Vampire/SPASS syntax. +Abstract representation of ATP proofs and TSTP/SPASS syntax. *) signature ATP_PROOF = @@ -15,7 +15,7 @@ Unprovable | IncompleteUnprovable | ProofMissing | - UnsoundProof of bool | + UnsoundProof of bool * string list | CantConnect | TimedOut | OutOfResources | @@ -64,7 +64,7 @@ Unprovable | IncompleteUnprovable | ProofMissing | - UnsoundProof of bool | + UnsoundProof of bool * string list | CantConnect | TimedOut | OutOfResources | @@ -117,20 +117,24 @@ " appears to be missing. You will need to install it if you want to invoke \ \remote provers." +fun involving [] = "" + | involving ss = "involving " ^ commas_quote ss ^ " " + fun string_for_failure Unprovable = "The problem is unprovable." | string_for_failure IncompleteUnprovable = "The prover gave up." | string_for_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." - | string_for_failure (UnsoundProof false) = - "The prover found a type-unsound proof (or, very unlikely, your axioms \ - \are inconsistent). Try passing the \"full_types\" option to Sledgehammer \ - \to avoid such spurious proofs." - | string_for_failure (UnsoundProof true) = - "The prover found a type-unsound proof even though a supposedly type-sound \ - \encoding was used (or, very unlikely, your axioms are inconsistent). You \ - \might want to report this to the Isabelle developers." + | string_for_failure (UnsoundProof (false, ss)) = + "The prover found a type-unsound proof " ^ involving ss ^ + "(or, less likely, your axioms are inconsistent). Try passing the \ + \\"full_types\" option to Sledgehammer to avoid such spurious proofs." + | string_for_failure (UnsoundProof (true, ss)) = + "The prover found a type-unsound proof " ^ involving ss ^ + "even though a supposedly type-sound encoding was used (or, less likely, \ + \your axioms are inconsistent). You might want to report this to the \ + \Isabelle developers." | string_for_failure CantConnect = "Cannot connect to remote server." | string_for_failure TimedOut = "Timed out." | string_for_failure OutOfResources = "The prover ran out of resources." diff -r d1aad0957eb2 -r e336ef6313aa src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:35:44 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:47:58 2011 +0200 @@ -27,9 +27,9 @@ val used_facts_in_atp_proof : type_system -> int -> (string * locality) list vector -> string proof -> (string * locality) list - val is_unsound_proof : + val used_facts_in_unsound_atp_proof : type_system -> int list list -> int -> (string * locality) list vector - -> string proof -> bool + -> string proof -> string list option val apply_on_subgoal : string -> int -> int -> string val command_call : string -> string list -> string val try_command_line : string -> string -> string @@ -181,10 +181,18 @@ exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name | _ => false) -fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names = - not o is_conjecture_referred_to_in_proof conjecture_shape andf - forall (is_locality_global o snd) - o used_facts_in_atp_proof type_sys facts_offset fact_names +fun used_facts_in_unsound_atp_proof type_sys conjecture_shape facts_offset + fact_names atp_proof = + let + val used_facts = used_facts_in_atp_proof type_sys facts_offset fact_names + atp_proof + in + if forall (is_locality_global o snd) used_facts andalso + not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then + SOME (map fst used_facts) + else + NONE + end (** Soft-core proof reconstruction: Metis one-liner **) diff -r d1aad0957eb2 -r e336ef6313aa src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:35:44 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:47:58 2011 +0200 @@ -577,11 +577,11 @@ val outcome = case outcome of NONE => - if is_unsound_proof type_sys conjecture_shape facts_offset - fact_names atp_proof then - SOME (UnsoundProof (is_type_sys_virtually_sound type_sys)) - else - NONE + used_facts_in_unsound_atp_proof type_sys + conjecture_shape facts_offset fact_names atp_proof + |> Option.map (fn facts => + UnsoundProof (is_type_sys_virtually_sound type_sys, + facts)) | SOME Unprovable => if null blacklist then outcome else SOME IncompleteUnprovable @@ -609,7 +609,7 @@ fun maybe_blacklist_facts_and_retry iter blacklist (result as ((_, _, facts_offset, fact_names, _), (_, _, type_sys, atp_proof, - SOME (UnsoundProof false)))) = + SOME (UnsoundProof (false, _))))) = (case used_facts_in_atp_proof type_sys facts_offset fact_names atp_proof of [] => result