chore: staging temp hacks

src/Init/Grind/Tactics.lean

@@ -66,26 +66,26 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command
 
 namespace Attr
-syntax grindGen    := &"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 grindUsr    := &"usr "
-syntax grindCases  := &"cases "
-syntax grindCasesEager := atomic(&"cases" &"eager ")
-syntax grindIntro  := &"intro "
-syntax grindExt    := &"ext "
+syntax grindGen    := ppSpace &"gen"
+syntax grindEq     := "=" (grindGen)?
+syntax grindEqBoth := atomic("_" "=" "_") (grindGen)?
+syntax grindEqRhs  := atomic("=" "_") (grindGen)?
+syntax grindEqBwd  := atomic("←" "=") <|> atomic("<-" "=")
+syntax grindBwd    := ("← " <|> "←" <|> "<-") (grindGen)? -- TODO remove "← " after update stage 0
+syntax grindFwd    := "→ " <|> "→" <|> "->" -- TODO remove "→ " after update stage 0
+syntax grindRL     := "⇐" <|> "<="
+syntax grindLR     := "⇒" <|> "=>"
+syntax grindUsr    := &"usr"
+syntax grindCases  := &"cases"
+syntax grindCasesEager := atomic(&"cases" &"eager")
+syntax grindIntro  := &"intro"
+syntax grindExt    := &"ext"
 syntax grindMod :=
     grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen
-syntax (name := grind) "grind" (grindMod)? : attr
-syntax (name := grind?) "grind?" (grindMod)? : attr
+syntax (name := grind) "grind" ppSpace (grindMod)? : attr
+syntax (name := grind?) "grind?" ppSpace (grindMod)? : attr
 end Attr
 end Lean.Parser
 
@@ -204,7 +204,7 @@ namespace Lean.Parser.Tactic
 -/
 
 syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindMod)? ident
+syntax grindLemma := (Attr.grindMod ppSpace)? ident
 syntax grindParam := grindErase <|> grindLemma
 
 syntax (name := grind)

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -20,29 +20,36 @@ inductive AttrKind where
 /-- 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 (.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)
-  | `(Parser.Attr.grindMod| cases) => return .cases false
-  | `(Parser.Attr.grindMod| cases eager) => return .cases true
-  | `(Parser.Attr.grindMod| intro) => return .intro
-  | `(Parser.Attr.grindMod| ext) => return .ext
-  | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
+  | `(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 (.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)
+  | `(Parser.Attr.grindMod|cases) => return .cases false
+  | `(Parser.Attr.grindMod|cases eager) => return .cases true
+  | `(Parser.Attr.grindMod|intro) => return .intro
+  | `(Parser.Attr.grindMod|ext) => return .ext
+  | _ =>
+    -- TODO: remove after update stage0
+    let stx := stx[0]
+    if stx.isOfKind ``Parser.Attr.grindFwd then return .ematch .fwd
+    if stx.isOfKind ``Parser.Attr.grindBwd then return .ematch (.bwd false)
+    if stx.isOfKind ``Parser.Attr.grindRL then return .ematch .rightLeft
+    if stx.isOfKind ``Parser.Attr.grindLR then return .ematch .leftRight
+    throwError "unexpected `grind` theorem kind: `{stx}`"
 
 /-- Return theorem kind for `stx` of the form `(Attr.grindMod)?` -/
 def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do

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

tests/lean/run/grind_pp_attr.lean

@@ -0,0 +1,27 @@
+import Lean.Elab.Command
+
+open Lean Elab Command
+
+def test (stx : Syntax) : CommandElabM Unit := do
+  let fmt : Option Format := ←
+        liftCoreM <| PrettyPrinter.ppCategory `command stx
+  if let some fmt := fmt then
+  let st := fmt.pretty
+  dbg_trace st
+
+
+/--
+info: @[grind =]
+example :=
+  0
+-/
+#guard_msgs in
+run_cmd test (← `(@[grind =] example := 0))
+
+/--
+info: @[grind _=_]
+example :=
+  0
+-/
+#guard_msgs in
+run_cmd test (← `(@[grind _=_] example := 0))