experiment: hammer/premise selection benchmarks

Mathlib/Tactic/Common.lean

@@ -8,6 +8,7 @@ Authors: Kim Morrison
 import Aesop
 import Qq
 import Plausible
+-- import Canonical
 
 -- Tools for analysing imports, like `#find_home`, `#minimize_imports`, ...
 import ImportGraph.Imports
@@ -147,3 +148,5 @@ register_hint (priority := 200) omega
 register_hint (priority := 200) fun_prop
 
 end Hint
+
+-- example : True := by canonical +suggestions

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -176,6 +176,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[
   (`MathlibTest.Header, `Plausible),
   (`MathlibTest.Header, `ProofWidgets),
   (`MathlibTest.Header, `Qq),
+  (`MathlibTest.Header, `Canonical),
   -- (`MathlibTest.Header, `Mathlib.Tactic),
   -- (`MathlibTest.Header, `Mathlib.Deprecated),
   (`MathlibTest.Header, `Batteries),
@@ -649,13 +650,14 @@ def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageDa
   else
     -- We always allow imports in the same directory (for each matching prefix),
     -- from `Init`, `Lean` and `Std`, as well as imports in `Aesop`, `Qq`, `Plausible`,
-    -- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (as these are imported in Tactic.Common).
+    -- `ImportGraph`, `ProofWidgets`, `LeanSearchClient` and `Canonical`
+    -- (as these are imported in Tactic.Common).
     -- We also allow transitive imports of Mathlib.Init, as well as Mathlib.Init itself.
     let initImports := (← findImports ("Mathlib" / "Init.lean")).append
       #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames]
     let exclude := [
       `Init, `Std, `Lean,
-      `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient
+      `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient, `Canonical
     ]
     let importsToCheck := imports.filter (fun imp ↦ !exclude.any (·.isPrefixOf imp))
       |>.filter (fun imp ↦ !matchingPrefixes.any (·.isPrefixOf imp))

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -8,6 +8,7 @@ import Mathlib.Tactic.ExtractGoal
 import Mathlib.Tactic.MinImports
 import Lean.Elab.Tactic.Meta
 import Lean.Elab.Command
+import Aesop
 
 /-!
 # Tactic linters
@@ -322,6 +323,18 @@ def tryAtEachStepAesop := tryAtEachStep
   fun _ _ => return ⟨TSyntax.raw <|
     mkNode `Aesop.Frontend.Parser.aesopTactic #[mkAtom "aesop", mkNullNode]⟩
 
+-- /-- Run `canonical` at every step in proofs, reporting where it succeeds. -/
+-- register_option linter.tacticAnalysis.tryAtEachStepCanonical : Bool := {
+--   defValue := false
+-- }
+
+-- @[tacticAnalysis linter.tacticAnalysis.tryAtEachStepCanonical,
+--    inherit_doc linter.tacticAnalysis.tryAtEachStepCanonical]
+-- def tryAtEachStepCanonical := tryAtEachStep
+--   -- As `canonical` isn't imported here, we construct the tactic syntax manually.
+--   fun _ _ => return ⟨TSyntax.raw <|
+--     mkNode `Mathlib.Tactic.Canonical.canonical #[mkAtom "canonical", mkNullNode]⟩
+
 /-- Run `grind +suggestions` at every step in proofs, reporting where it succeeds. -/
 register_option linter.tacticAnalysis.tryAtEachStepGrindSuggestions : Bool := {
   defValue := false
@@ -338,7 +351,19 @@ register_option linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions : Bool :=
 
 @[tacticAnalysis linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions,
    inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions]
-def tryAtEachStepSimpAllSuggestions := tryAtEachStep fun _ _ => `(tactic| simp_all? +suggestions)
+def tryAtEachStepSimpAllSuggestions := tryAtEachStep fun _ _ => `(tactic| try simp_all? +suggestions)
+
+-- /-- Run `canonical +suggestions` at every step in proofs, reporting where it succeeds. -/
+-- register_option linter.tacticAnalysis.tryAtEachStepCanonicalSuggestions : Bool := {
+--   defValue := false
+-- }
+
+-- @[tacticAnalysis linter.tacticAnalysis.tryAtEachStepCanonicalSuggestions,
+--    inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions]
+-- def tryAtEachStepCanonicalSuggestions := tryAtEachStep
+--   -- As `canonical` isn't imported here, we construct the tactic syntax manually.
+--   fun _ _ => return ⟨TSyntax.raw <|
+--     mkNode `Mathlib.Tactic.Canonical.canonical #[mkAtom "canonical", mkNullNode]⟩
 
 -- TODO: add compatibility with `rintro` and `intros`
 /-- Suggest merging two adjacent `intro` tactics which don't pattern match. -/

MathlibTest/canonical.lean

@@ -0,0 +1,46 @@
+import Mathlib.Data.Real.Basic
+
+-- From https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Canonical/near/538098556
+
+/--
+info: Try this:
+  [apply] exact
+    Exists.intro 2
+      (by simp only [Nat.zero_add, Nat.zero_mul, Nat.succ_mul, Nat.succ.injEq, Nat.succ_add] <;> exact Eq.refl Nat.zero)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : ∃ n : Nat, n * n = 4 := by
+  canonical
+
+-- From https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Canonical/near/538228811
+
+def continuous_function_at (f : ℝ → ℝ) (x₀ : ℝ) :=
+∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
+
+def sequence_tendsto (u : ℕ → ℝ) (l : ℝ) :=
+∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
+
+/--
+info: Try this:
+  [apply] exact fun ε a ↦
+    Exists.intro (hu (hf ε a).choose (Exists.choose_spec (hf ε a)).1).choose fun n a_1 ↦
+      (Exists.choose_spec (hf ε a)).2 (u n)
+        (Exists.choose_spec (hu (hf ε a).choose (Exists.choose_spec (hf ε a)).1) n a_1)
+---
+warning: declaration uses 'sorry'
+---
+warning: unused variable `hf`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+---
+warning: unused variable `hu`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+-/
+#guard_msgs in
+example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
+    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
+    sequence_tendsto (f ∘ u) (f x₀) := by
+  canonical

lakefile.lean

@@ -17,6 +17,7 @@ require "leanprover-community" / "proofwidgets" @ git "v0.0.77" -- ProofWidgets
 require "leanprover-community" / "importGraph" @ git "main"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
 require "leanprover-community" / "plausible" @ git "nightly-testing"
+-- require "chasenorman" / "Canonical" @ git "nightly-2025-11-03"
 
 
 /-!
@@ -31,6 +32,11 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
+  -- ⟨`linter.tacticAnalysis.tryAtEachStepAesop, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepSimpAll, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepGrind, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepGrindSuggestions, true⟩,
   -- ⟨`linter.nightlyRegressionSet, true⟩,
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
 ]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-11-03
+leanprover/lean4-pr-releases:pr-release-11064

scripts/README.md

@@ -79,6 +79,9 @@ to learn about it as well!
   Generates `unused.md` containing a markdown table showing the unused imports,
   and suggests `lake exe graph` commands to visualize the largest "rectangles" of unused imports.
 
+**Analyzing hammer tactic suggestions**
+- `analyze_hammer_suggestions.py` analyzes which tactics can replace existing tactics at each location, with and without +suggestions. By default analyzes simp_all and grind on all of Mathlib. Use `--aesop` and `--canonical` to enable additional tactics, or `--no-<tactic>` to disable defaults. Use `--raw` for location:tactic pairs instead of summary tables.
+
 **CI workflow**
 - `lake-build-with-retry.sh`
   Runs `lake build` on a target until `lake build --no-build` succeeds. Used in the main build workflows.