author | blanchet |

Wed, 17 Aug 2022 18:20:10 +0200 | |

changeset 75873 | 5f7d22354a65 |

parent 75872 | 8bfad7bc74cb |

child 75874 | 77cbf472fcc9 |

tweaked generation of Isar proofs

--- a/NEWS Wed Aug 17 15:09:53 2022 +0200 +++ b/NEWS Wed Aug 17 18:20:10 2022 +0200 @@ -146,6 +146,8 @@ - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions in TH0 and TH1. - Added support for cvc5. + - Generate Isar proofs by default when and only when the one-liner proof + fails to replay and the Isar proof succeeds. - Replaced option "sledgehammer_atp_dest_dir" by "sledgehammer_atp_problem_dest_dir", for problem files, and "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY.

--- a/src/Doc/Sledgehammer/document/root.tex Wed Aug 17 15:09:53 2022 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Aug 17 18:20:10 2022 +0200 @@ -1129,9 +1129,9 @@ \opsmart{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-line 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 -one-line proofs. If the option is set to \textit{smart} (the default), Isar -proofs are only generated when no working one-line proof is available. +however, when they succeed they can be faster and sometimes more intelligible +than one-line proofs. If the option is set to \textit{smart} (the default), Isar +proofs are generated only when no working one-line proof is available. \opdefault{compress}{int}{smart} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 17 15:09:53 2022 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 17 18:20:10 2022 +0200 @@ -494,9 +494,12 @@ (if do_preplay then [string_of_play_outcome play_outcome] else []) in one_line_proof_text ctxt 0 one_line_params ^ - "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ - Active.sendback_markup_command - (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) + (if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then + "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ + Active.sendback_markup_command + (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) + else + "") end) end end