From b14d8952a75d5e245408eb441af0c28e811b59f1 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 15 Aug 2024 18:22:13 +0000 Subject: [PATCH] fix: silence `aesop` in `cfc_cont_tac` (#15847) If `aesop` fails to discharge a goal in one branch of `fun_prop`, as implemened in `cfc_cont_tac`, it can emit a warning saying it failed to close the goal. If `fun_prop (disch := aesop)` then *succeeds* in a later branch of the same call, then the proof succeeds, but the warning is still emitted, causing the file to be noisy. Even worse, because this is called as an `autoParam`, there is no syntax in the file on which to emit the warning, so it just gets emitted at the top of the file. This changes the configuration of `aesop` to `warnOnNonterminal := false` when used in `cfc_cont_tac`. Note: this won't affect debugging or proof writing, because in that case the user will need to disable the use of the `autoParam` anyway by writing their own terms (or `fun_prop` calls). --- Mathlib/Tactic/ContinuousFunctionalCalculus.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Tactic/ContinuousFunctionalCalculus.lean b/Mathlib/Tactic/ContinuousFunctionalCalculus.lean index d65a4da1a676c..0adbd41b52a2f 100644 --- a/Mathlib/Tactic/ContinuousFunctionalCalculus.lean +++ b/Mathlib/Tactic/ContinuousFunctionalCalculus.lean @@ -26,7 +26,10 @@ macro_rules specifically concerning continuity of the functions involved. -/ syntax (name := cfcContTac) "cfc_cont_tac" : tactic macro_rules - | `(tactic| cfc_cont_tac) => `(tactic| try (first | fun_prop (disch := aesop) | assumption)) + | `(tactic| cfc_cont_tac) => + `(tactic| try (first + | fun_prop (disch := aesop (config := {warnOnNonterminal := false})) + | assumption)) /-- A tactic used to automatically discharge goals relating to the non-unital continuous functional calculus, specifically concerning whether `f 0 = 0`. -/