remove canonical mentions for now

Author: kim-em

Mathlib/Tactic/Common.lean

@@ -151,5 +151,3 @@ register_hint 200 omega
 register_hint 200 fun_prop
 
 end Hint
-
--- example : True := by canonical +suggestions

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -181,7 +181,6 @@ 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),
@@ -658,14 +657,13 @@ 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`, `LeanSearchClient` and `Canonical`
-    -- (as these are imported in Tactic.Common).
+    -- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (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, `Canonical
+      `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient
     ]
     let importsToCheck := imports.filter (fun imp ↦ !exclude.any (·.isPrefixOf imp))
       |>.filter (fun imp ↦ !matchingPrefixes.any (·.isPrefixOf imp))

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -333,18 +333,6 @@ 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
@@ -365,18 +353,6 @@ register_option linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions : Bool :=
 -- in `Logic/Equiv/Defs.lean` at `def cast` that I don't understand.
 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. -/
 register_option linter.tacticAnalysis.introMerge : Bool := {

MathlibTest/canonical.lean

@@ -17,7 +17,6 @@ require "leanprover-community" / "proofwidgets" @ git "v0.0.83-pre2" -- ProofWid
 require "leanprover-community" / "importGraph" @ git "nightly-testing"
 require "leanprover-community" / "LeanSearchClient" @ git "nightly-testing"
 require "leanprover-community" / "plausible" @ git "nightly-testing"
--- require "chasenorman" / "Canonical" @ git "nightly-2025-11-03"
 
 
 /-!