# HG changeset patch # User blanchet # Date 1282127175 -7200 # Node ID c9f2b1a91276111809b34463a076d2ea0a7756d5 # Parent bd9c4e8281ecbd58e2f501136600f5c1aebd3092# Parent 86170391fd2e46f719731bcd7ba3e3db43e22f28 merged diff -r bd9c4e8281ec -r c9f2b1a91276 doc-src/Nitpick/nitpick.tex diff -r bd9c4e8281ec -r c9f2b1a91276 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 12:19:27 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 12:26:15 2010 +0200 @@ -8,9 +8,9 @@ signature ATP_SYSTEMS = sig datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | - OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput | - MalformedOutput | UnknownError + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | + OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | + MalformedInput | MalformedOutput | UnknownError type prover_config = {exec: string * string, @@ -40,7 +40,7 @@ datatype failure = Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | - OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput | + SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput | MalformedOutput | UnknownError type prover_config = @@ -63,7 +63,7 @@ | string_for_failure CantConnect = "Can't connect to remote server." | string_for_failure TimedOut = "Timed out." | string_for_failure OutOfResources = "The ATP ran out of resources." - | string_for_failure OldSpass = + | string_for_failure SpassTooOld = "Isabelle requires a more recent version of SPASS with support for the \ \TPTP syntax. To install it, download and extract the package \ \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ @@ -72,7 +72,7 @@ (Path.variable "ISABELLE_HOME_USER" :: map Path.basic ["etc", "components"])))) ^ " on a line of its own." - | string_for_failure OldVampire = + | string_for_failure VampireTooOld = "Isabelle requires a more recent version of Vampire. To install it, follow \ \the instructions from the Sledgehammer manual (\"isabelle doc\ \ sledgehammer\")." @@ -170,7 +170,7 @@ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), - (OldSpass, "tptp2dfg")], + (SpassTooOld, "tptp2dfg")], max_new_relevant_facts_per_iter = 35 (* FIXME *), prefers_theory_relevant = true, explicit_forall = true} @@ -197,7 +197,7 @@ (TimedOut, "SZS status Timeout"), (Unprovable, "Satisfiability detected"), (OutOfResources, "Refutation not found"), - (OldVampire, "not a valid option")], + (VampireTooOld, "not a valid option")], max_new_relevant_facts_per_iter = 45 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} diff -r bd9c4e8281ec -r c9f2b1a91276 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 18 12:19:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 18 12:26:15 2010 +0200 @@ -156,6 +156,7 @@ datatype outcome = JavaNotInstalled | + JavaTooOld | KodkodiNotInstalled | Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | @@ -303,6 +304,7 @@ datatype outcome = JavaNotInstalled | + JavaTooOld | KodkodiNotInstalled | Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | @@ -1063,19 +1065,20 @@ |> perhaps (try (unsuffix ".")) |> perhaps (try (unprefix "Solve error: ")) |> perhaps (try (unprefix "Error: ")) + fun has_error s = + first_error |> Substring.full |> Substring.position s |> snd + |> Substring.isEmpty |> not in if null ps then if code = 2 then TimedOut js else if code = 0 then Normal ([], js, first_error) - else if first_error |> Substring.full - |> Substring.position "exec: java" |> snd - |> Substring.isEmpty |> not then + else if has_error "exec: java" then JavaNotInstalled - else if first_error |> Substring.full - |> Substring.position "NoClassDefFoundError" |> snd - |> Substring.isEmpty |> not then + else if has_error "UnsupportedClassVersionError" then + JavaTooOld + else if has_error "NoClassDefFoundError" then KodkodiNotInstalled else if first_error <> "" then Error (first_error, js) diff -r bd9c4e8281ec -r c9f2b1a91276 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 18 12:19:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 18 12:26:15 2010 +0200 @@ -315,6 +315,7 @@ in case solve_any_problem overlord NONE max_threads max_solutions problems of JavaNotInstalled => "unknown" + | JavaTooOld => "unknown" | KodkodiNotInstalled => "unknown" | Normal ([], _, _) => "none" | Normal _ => "genuine" diff -r bd9c4e8281ec -r c9f2b1a91276 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 18 12:19:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 18 12:26:15 2010 +0200 @@ -740,6 +740,9 @@ KK.JavaNotInstalled => (print_m install_java_message; (found_really_genuine, max_potential, max_genuine, donno + 1)) + | KK.JavaTooOld => + (print_m install_java_message; + (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.KodkodiNotInstalled => (print_m install_kodkodi_message; (found_really_genuine, max_potential, max_genuine, donno + 1)) diff -r bd9c4e8281ec -r c9f2b1a91276 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 12:19:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 12:26:15 2010 +0200 @@ -167,8 +167,8 @@ val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id - --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")" + $$ "(" |-- scan_integer --| $$ "," + -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" --| Scan.option ($$ ",") val parse_clause_formula_relation = Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" @@ -183,21 +183,21 @@ thm_names = if String.isSubstring set_ClauseFormulaRelationN output then (* This is a hack required for keeping track of axioms after they have been - clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part - of this hack. *) + clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also + part of this hack. *) let val j0 = hd (hd conjecture_shape) val seq = extract_clause_sequence output val name_map = extract_clause_formula_relation output fun renumber_conjecture j = - AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) + conjecture_prefix ^ Int.toString (j - j0) + |> AList.find (fn (s, ss) => member (op =) ss s) name_map |> map (fn s => find_index (curry (op =) s) seq + 1) in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the - |> try (unprefix axiom_prefix) of - SOME s' => undo_ascii_of s' - | NONE => "") + seq |> map (AList.lookup (op =) name_map #> these + #> map_filter (try (unprefix axiom_prefix)) + #> map undo_ascii_of #> space_implode " ") |> Vector.fromList) end else diff -r bd9c4e8281ec -r c9f2b1a91276 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 12:19:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 12:26:15 2010 +0200 @@ -55,8 +55,10 @@ let val do_term = combterm_from_term thy fun do_quant bs q s T t' = - do_formula ((s, T) :: bs) t' - #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + let val s = Name.variant (map fst bs) s in + do_formula ((s, T) :: bs) t' + #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + end and do_conn bs c t1 t2 = do_formula bs t1 ##>> do_formula bs t2 #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))