From 3ede96accc2d9ac1b41a9bda2dbd6c7af1aad608 Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Wed, 2 Jul 2025 19:14:21 +0200
Subject: [PATCH] fix: use `patternIgnore(...)` in grind syntax (#9158)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes the syntax of `grind` modifiers to use `patternIgnore` for
cases where both unicode and ascii variants are matched. This fixes an
issue where several variants of grind syntax weren't accepted (e.g.
`@[grind ← gen]`). Additionally, this reduces the chance that we get
another syntax matching bootstrap hell.
---
 src/Init/Grind/Tactics.lean          | 10 +++++-----
 src/Lean/Elab/Tactic/Grind.lean      |  2 ++
 src/Lean/Meta/Tactic/Grind/Attr.lean | 12 +++++-------
 stage0/src/stdlib_flags.h            |  2 +-
 4 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index d18829a728..5dfa8a565f 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -72,11 +72,11 @@ syntax grindGen    := ppSpace &"gen"
 syntax grindEq     := "=" (grindGen)?
 syntax grindEqBoth := atomic("_" "=" "_") (grindGen)?
 syntax grindEqRhs  := atomic("=" "_") (grindGen)?
-syntax grindEqBwd  := atomic("←" "=") <|> atomic("<-" "=")
-syntax grindBwd    := ("←" <|> "<-") (grindGen)?
-syntax grindFwd    := "→" <|> "->"
-syntax grindRL     := "⇐" <|> "<="
-syntax grindLR     := "⇒" <|> "=>"
+syntax grindEqBwd  := patternIgnore(atomic("←" "=") <|> atomic("<-" "="))
+syntax grindBwd    := patternIgnore("←" <|> "<-") (grindGen)?
+syntax grindFwd    := patternIgnore("→" <|> "->")
+syntax grindRL     := patternIgnore("⇐" <|> "<=")
+syntax grindLR     := patternIgnore("⇒" <|> "=>")
 syntax grindUsr    := &"usr"
 syntax grindCases  := &"cases"
 syntax grindCasesEager := atomic(&"cases" &"eager")
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index 1d8a8ba502..d6054884ce 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -12,6 +12,8 @@ import Lean.Elab.MutualDef
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Config
 
+set_option interpreter.prefer_native false -- TODO: remove
+
 namespace Lean.Elab.Tactic
 open Meta
 
diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean
index b4850c4c57..5a6d85055f 100644
--- a/src/Lean/Meta/Tactic/Grind/Attr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Attr.lean
@@ -17,24 +17,22 @@ inductive AttrKind where
   | infer
   | ext
 
+set_option interpreter.prefer_native false -- TODO: remove
+
 /-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
 def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   match stx with
   | `(Parser.Attr.grindMod|=) => return .ematch (.eqLhs false)
   | `(Parser.Attr.grindMod|= gen) => return .ematch (.eqLhs true)
-  | `(Parser.Attr.grindMod|→)
-  | `(Parser.Attr.grindMod|->) => return .ematch .fwd
-  | `(Parser.Attr.grindMod|←)
-  | `(Parser.Attr.grindMod|<-) => return .ematch (.bwd false)
-  | `(Parser.Attr.grindMod|<- gen) => return .ematch (.bwd true)
+  | `(Parser.Attr.grindMod|→) => return .ematch .fwd
+  | `(Parser.Attr.grindMod|←) => return .ematch (.bwd false)
+  | `(Parser.Attr.grindMod|← gen) => return .ematch (.bwd true)
   | `(Parser.Attr.grindMod|=_) => return .ematch (.eqRhs false)
   | `(Parser.Attr.grindMod|=_ gen) => return .ematch (.eqRhs true)
   | `(Parser.Attr.grindMod|_=_) => return .ematch (.eqBoth false)
   | `(Parser.Attr.grindMod|_=_ gen) => return .ematch (.eqBoth true)
   | `(Parser.Attr.grindMod|←=) => return .ematch .eqBwd
-  | `(Parser.Attr.grindMod|⇒)
   | `(Parser.Attr.grindMod|=>) => return .ematch .leftRight
-  | `(Parser.Attr.grindMod|⇐)
   | `(Parser.Attr.grindMod|<=) => return .ematch .rightLeft
   | `(Parser.Attr.grindMod|usr) => return .ematch .user
   | `(Parser.Attr.grindMod|gen) => return .ematch (.default true)
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..6b964da742 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -11,7 +11,7 @@ options get_default_options() {
     opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with