commandStart linter broken with `grind`

Stream: mathlib4

[Kim Morrison]

@Damiano Testa, I just noticed the commandStart linter is broken with grind.

We will need to add many annotations of the form @[grind =], but the commandStart linter says:

missing space in the source

This part of the code
  '=]
theorem'
should be written as
  '@[grind= ]
theorem'

note: this linter can be disabled with `set_option linter.style.commandStart false`

Can you make this problem go away for me? :-)

[Damiano Testa]

Can you share some working code where the linter complains?

[Damiano Testa]

Without knowing more about the syntax that grind produces, I can simply silence the linter on attributes, but if I could silence it more granularly, that would probably be better.

[Kim Morrison]

On nightly-testing, just write

axiom f  : Nat -> Nat
axiom g : Nat -> Nat
@[grind =] theorem foo (x : Nat) : f x = g x := sorry

[Damiano Testa]

Alternatively, if you prefer @[grind =] to @[grind= ], you can also change the pretty-printer for grind.

[Kim Morrison]

Oh, I see, it's a pretty-printer problem!

[Kim Morrison]

Okay, I will look into that.

[Damiano Testa]

Yes, the commandStart linter uses the pretty-printer to decide what should change.

[Kim Morrison]

I actually don't know how to pretty print attributes on declaration, any suggestions how to test?

[Damiano Testa]

But since the pretty-printer does not always get it right, the linter has an override option to ignore certain syntaxnodekinds.

[Damiano Testa]

This should be some syntax annotation where grind is defined.

[Kim Morrison]

Yes, but how do test my fix without going back to Mathlib?

[Damiano Testa]

Let me first get a version of nightly that works and take a look at the syntax.

[Kim Morrison]

I need to run the pretty printer in some way that will actually try to show an attribute.

[Damiano Testa]

Ah, I can extract what pretty-printed thing the linter would think in a moment!

[Damiano Testa]

Actually, while I download nightly-testing, the linter only needs import Lean.Elab.Command, so you could also simply copy the file into Lean and import it to see what it does.

[Kim Morrison]

I'd prefer not to touch your linter if possible. :-)

[Damiano Testa]

Ok, I am having problems building some files in nightly-testing. Give me a minute!

[Kim Morrison]

Do you know how to test the pretty printer on an attribute? e.g. running #print foo doesn't show any attributes.

[Damiano Testa]

I think that this is what the commandStart sees:

run_cmd
  let stx ← `(@[grind =] example := 0)
  let fmt : Option Format := ←
        liftCoreM <| PrettyPrinter.ppCategory `command stx
  if let some fmt := fmt then
  let st := fmt.pretty
  dbg_trace st

[Damiano Testa]

I probably should extract this to some standalone function for just this purpose.

[Kim Morrison]

Great, I can reproduce in Lean.

[Damiano Testa]

Ok, I am still having import problems: I don't seem to be able to actually restart files.

[Kim Morrison]

Ah, it's tricky to fix, because these syntax are used as both prefixes and suffixes.

We write @[grind =] theorem foo, but also grind [= foo].

[Kim Morrison]

The spaces are set up for the second use case, and so are wrong for the first.

[Damiano Testa]

Ok, I'll look up the syntaxnodekind and add an exception to the linter.

[Damiano Testa]

grind has some very persistent pretty-printing formatting! I could only make the linter silent by disabling entirely on attributes, not just grind. Anyway, this is what you can do:

diff --git a/Mathlib/Tactic/Linter/CommandStart.lean b/Mathlib/Tactic/Linter/CommandStart.lean
index c981cc7e6ce..fb8d4002299 100644
--- a/Mathlib/Tactic/Linter/CommandStart.lean
+++ b/Mathlib/Tactic/Linter/CommandStart.lean
@@ -242,6 +242,7 @@ abbrev unlintedNodes := #[

   -- The pretty-printer adds a space between the backticks and the actual name.
   ``Parser.Term.doubleQuotedName,
+  ``Parser.Term.attributes,
   ]

 /--

Do you want me to make a PR with this?

[Kim Morrison]

Still thinking about fixing it at the syntax end, I'll let you know if I get stuck.

[Damiano Testa]

Since I'll have to leave soon, I'll make a PR with the blanket change up there: feel free to incorporate or ignore!

I also thought that the linter had a pretty fine-grained method for allowing exceptions, but grind is proving me wrong, so I'd like to see what I should be improving anyway.

[Kim Morrison]

So far I have persuaded it to pretty print as @[grind = ]... i.e. a space on both sides.

[Damiano Testa]

To be fair, it is not unreasonable for the pretty-printer to do this, but I agree that skipping the final space would look better.

[Damiano Testa]

By the way, the linter already special cases something else for a similar reason (although it is not an attribute):

  -- notation for `Finset.slice`, the pretty-printer prefers `𝒜 #r` over `𝒜 # r` (mathlib style)
  `Finset.«term_#_»,

[Damiano Testa]

#26196 and I've asked for your review.

[Damiano Testa]

I will only have a few scattered moments throughout the day where I can act on things, so I wanted to leave this in a state where there was at least one solution available! :slight_smile:

[Kim Morrison]

Thank you! Prompt help very much appreciated. :-)

[Robin Arnez]

I wanted to fix this in lean#8424, basically:

src/Init/Grind/Tactics.lean
@@ -15,22 +15,22 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command

 namespace Attr
-syntax grindEq     := "= "
-syntax grindEqBoth := atomic("_" "=" "_ ")
-syntax grindEqRhs  := atomic("=" "_ ")
-syntax grindEqBwd  := atomic("←" "= ") <|> atomic("<-" "= ")
-syntax grindBwd    := "← " <|> "-> "
-syntax grindFwd    := "→ " <|> "<- "
-syntax grindRL     := "⇐ " <|> "<= "
-syntax grindLR     := "⇒ " <|> "=> "
-syntax grindUsr    := &"usr "
-syntax grindCases  := &"cases "
-syntax grindCasesEager := atomic(&"cases" &"eager ")
-syntax grindIntro  := &"intro "
-syntax grindExt    := &"ext "
+syntax grindEq     := "="
+syntax grindEqBoth := atomic("_" "=" "_")
+syntax grindEqRhs  := atomic("=" "_")
+syntax grindEqBwd  := atomic("←" "=") <|> atomic("<-" "=")
+syntax grindBwd    := "←" <|> "<-"
+syntax grindFwd    := "→" <|> "->"
+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
-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

@@ -139,19 +139,19 @@ namespace Lean.Parser.Tactic
 `grind` tactic and related tactics.
 -/

 syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindMod)? ident
+syntax grindLemma := (Attr.grindMod ppSpace)? ident
 syntax grindParam := grindErase <|> grindLemma

 syntax (name := grind)
   "grind" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  ("on_failure " term)? : tactic
+  (&" on_failure " term)? : tactic


 syntax (name := grindTrace)
   "grind?" optConfig (&" only")?
   (" [" withoutPosition(grindParam,*) "]")?
-  ("on_failure " term)? : tactic
+  (&" on_failure " term)? : tactic

 end Lean.Parser.Tactic

[Robin Arnez]

Oh I see you already did most of this and ran into the same bootstrapping issue :-)

[Kim Morrison]

Gah... bootstrapping sucks, I'm quite frustrated by this PR.

[Kevin Buzzard]

(lean#8424)

[Damiano Testa]

If someone would like to get involved in more annoying syntaxpretty-printing fixing, here is another issue unearthed by the commandStart linter of a similar nature:

import Lean.Elab.Command

/--
info: @[simp← ]
example :=
  0
-/
#guard_msgs in
run_cmd
  let stx ← `(@[simp ←] example := 0)
  Lean.logInfo stx

Note how @[simp ←] gets pretty-printed as @[simp← ].

[Damiano Testa]

Would anyone be kind enough to fix this? :slight_smile:

[Yaël Dillies]

Damiano Testa said:

If someone would like to get involved in more annoying syntaxpretty-printing fixing, here is another issue unearthed by the commandStart linter of a similar nature:

import Lean.Elab.Command

/--
info: @[simp← ]
example :=
  0
-/
#guard_msgs in
run_cmd
  let stx ← `(@[simp ←] example := 0)
  Lean.logInfo stx

Note how @[simp ←] gets pretty-printed as @[simp← ].

This came up in #27064