# HG changeset patch # User blanchet # Date 1361346264 -3600 # Node ID 2654b3965c8d4c5bca234f308ed5179772c815da # Parent a55ef201b19d6aa429c297a17ab6fed598ff913e made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired diff -r a55ef201b19d -r 2654b3965c8d src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 08:44:24 2013 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Feb 20 08:44:24 2013 +0100 @@ -308,7 +308,7 @@ \textit{smt} method call. Rough timings are shown in parentheses, indicating how fast the call is. You can click the proof to insert it into the theory text. -In addition, you can ask Sledgehammer for an Isar text proof by passing the +In addition, you can ask Sledgehammer for an Isar text proof by enabling the \textit{isar\_proofs} option (\S\ref{output-format}): \prew @@ -367,7 +367,7 @@ if that helps. \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies -that Isar proofs should be generated, instead of one-liner \textit{metis} or +that Isar proofs should be generated, in addition to one-liner \textit{metis} or \textit{smt} proofs. The length of the Isar proofs can be controlled by setting \textit{isar\_compress} (\S\ref{output-format}). @@ -501,15 +501,15 @@ using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are strongly encouraged to report this to the author at \authoremail. -\point{Why are the generated Isar proofs so ugly/broken?} - -The current implementation of the Isar proof feature, -enabled by the \textit{isar\_proofs} option (\S\ref{output-format}), -is highly experimental. Work on a new implementation has begun. There is a large body of -research into transforming resolution proofs into natural deduction proofs (such -as Isar proofs), which we hope to leverage. In the meantime, a workaround is to -set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger -value or to try several provers and keep the nicest-looking proof. +%\point{Why are the generated Isar proofs so ugly/broken?} +% +%The current implementation of the Isar proof feature, +%enabled by the \textit{isar\_proofs} option (\S\ref{output-format}), +%is experimental. Work on a new implementation has begun. There is a large body of +%research into transforming resolution proofs into natural deduction proofs (such +%as Isar proofs), which we hope to leverage. In the meantime, a workaround is to +%set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger +%value or to try several provers and keep the nicest-looking proof. \point{How can I tell whether a suggested proof is sound?} @@ -1296,16 +1296,18 @@ \nopagebreak {\small See also \textit{overlord} (\S\ref{mode-of-operation}).} -\opfalse{isar\_proofs}{no\_isar\_proofs} +\opsmart{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-liner -\textit{metis} proofs. Isar proof construction is still experimental and often -fails; however, they are usually faster and sometimes more robust than -\textit{metis} proofs. +\textit{metis} proofs. The construction of Isar proof is still experimental and +may sometimes fail; however, when they succeed they are usually faster and more +intelligible than \textit{metis} proofs. If the option is set to \textit{smart} +(the default), Isar proofs are only generated when no working one-liner +\textit{metis} proof is available. \opdefault{isar\_compress}{int}{\upshape 10} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} -is enabled. A value of $n$ indicates that each Isar proof step should correspond -to a group of up to $n$ consecutive proof steps in the ATP proof. +is explicitly enabled. A value of $n$ indicates that each Isar proof step should +correspond to a group of up to $n$ consecutive proof steps in the ATP proof. \optrueonly{dont\_compress\_isar} Alias for ``\textit{isar\_compress} = 0''. diff -r a55ef201b19d -r 2654b3965c8d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Feb 20 08:44:24 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Feb 20 08:44:24 2013 +0100 @@ -94,7 +94,7 @@ ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), - ("isar_proofs", "false"), + ("isar_proofs", "smart"), ("isar_compress", "10"), ("slice", "true"), ("minimize", "smart"), @@ -313,7 +313,7 @@ val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" - val isar_proofs = lookup_bool "isar_proofs" + val isar_proofs = lookup_option lookup_bool "isar_proofs" val isar_compress = Real.max (1.0, lookup_real "isar_compress") val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = diff -r a55ef201b19d -r 2654b3965c8d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 20 08:44:24 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 20 08:44:24 2013 +0100 @@ -293,24 +293,21 @@ <= Config.get ctxt auto_minimize_max_time fun prover_fast_enough () = can_min_fast_enough run_time in - if isar_proofs then - ((prover_fast_enough (), (name, params)), preplay) - else - (case Lazy.force preplay of - Played (reconstr as Metis _, timeout) => - if can_min_fast_enough timeout then - (true, extract_reconstructor params reconstr - ||> (fn override_params => - adjust_reconstructor_params - override_params params)) - else - (prover_fast_enough (), (name, params)) - | Played (SMT, timeout) => - (* Cheat: assume the original prover is as fast as "smt" for - the goal it proved itself *) - (can_min_fast_enough timeout, (name, params)) - | _ => (prover_fast_enough (), (name, params)), - preplay) + (case Lazy.force preplay of + Played (reconstr as Metis _, timeout) => + if can_min_fast_enough timeout then + (true, extract_reconstructor params reconstr + ||> (fn override_params => + adjust_reconstructor_params override_params + params)) + else + (prover_fast_enough (), (name, params)) + | Played (SMT, timeout) => + (* Cheat: assume the original prover is as fast as "smt" for + the goal it proved itself *) + (can_min_fast_enough timeout, (name, params)) + | _ => (prover_fast_enough (), (name, params)), + preplay) end else ((false, (name, params)), preplay) diff -r a55ef201b19d -r 2654b3965c8d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 20 08:44:24 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 20 08:44:24 2013 +0100 @@ -34,7 +34,7 @@ fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, - isar_proofs : bool, + isar_proofs : bool option, isar_compress : real, slice : bool, minimize : bool option, @@ -323,7 +323,7 @@ fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, - isar_proofs : bool, + isar_proofs : bool option, isar_compress : real, slice : bool, minimize : bool option, @@ -795,7 +795,7 @@ fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name - val full_proof = debug orelse isar_proofs + val full_proof = debug orelse isar_proofs = SOME true val args = arguments ctxt full_proof extra (slice_timeout |> the_default one_day) diff -r a55ef201b19d -r 2654b3965c8d src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 08:44:24 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 08:44:24 2013 +0100 @@ -38,9 +38,10 @@ string list option val one_line_proof_text : int -> one_line_params -> string val isar_proof_text : - Proof.context -> bool -> isar_params -> one_line_params -> string + Proof.context -> bool option -> isar_params -> one_line_params -> string val proof_text : - Proof.context -> bool -> isar_params -> int -> one_line_params -> string + Proof.context -> bool option -> isar_params -> int -> one_line_params + -> string end; structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -831,7 +832,7 @@ else compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout - (if isar_proofs then isar_compress else 1000.0)) + (if isar_proofs = SOME true then isar_compress else 1000.0)) |>> cleanup_labels_in_proof val isar_text = string_for_proof ctxt type_enc lam_trans subgoal subgoal_count @@ -839,7 +840,7 @@ in case isar_text of "" => - if isar_proofs then + if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." else "" @@ -870,7 +871,7 @@ isar_proof_of () else case try isar_proof_of () of SOME s => s - | NONE => if isar_proofs then + | NONE => if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "" @@ -884,7 +885,8 @@ fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = - (if isar_proofs orelse isar_proof_would_be_a_good_idea preplay then + (if isar_proofs = SOME true orelse + (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then isar_proof_text ctxt isar_proofs isar_params else one_line_proof_text num_chained) one_line_params