disable linter in elab

Stream: lean4

[Patrick Massot]

When using the elab command to define some new command, is there a way to tell Lean I want to disable the unused variable linter while processing each time this new command will be used?

[Henrik Böving]

set_option linter.unusedVariables false

[Mario Carneiro]

that is, you should put set_option linter.unusedVariables false inside the generated syntax quotation

[Patrick Massot]

I don't know where is "inside the generated syntax quotation"

[Patrick Massot]

My code contains

open Lean Meta Elab Command Term

declare_syntax_cat mydecl
syntax "(" ident ":" term ")" : mydecl

elab "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
-- lots of stuff

and I don't want Lean to complain about unused variables when users use this Message command.

[Mario Carneiro]

can you make a MWE?

[Patrick Massot]

Sorry, I'll work on a MWE

[Mario Carneiro]

Here's one

import Lean
open Lean Meta Elab Command Term

elab "Message" goal:term : command => do
  discard <| runTermElabM fun _ => do elabTerm goal none

Message fun x => () -- unused variable

[Patrick Massot]

Removing everything indeed doesn't show the bug, so here is a somewhat MWE (I cut of lot so don't try to make sense of this code):

import Lean

open Lean Meta Elab Command Term

declare_syntax_cat mydecl
syntax "(" ident ":" term ")" : mydecl

def getIdent : TSyntax `mydecl → Ident
| `(mydecl| ($n:ident : $_t:term)) => n
| _ => default

def getType : TSyntax `mydecl → Term
| `(mydecl| ($_n:ident : $t:term)) => t
| _ => default

/-- From a term `s` and a list of pairs `(i, t) ; Ident × Term`, create the syntax
where `s` is preceded with universal quantifiers `∀ i : t`. -/
def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
| [] => return s

elab "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
  let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList
  let _ ← liftTermElabM $ elabTerm g none
  let _ := msg


Message (a : Nat) (h : a = 0) : True => ""

[Patrick Massot]

Indeed yours is more minimal :rolling_eyes:

[Patrick Massot]

Hopefully my question now makes sense. How do I get rid of this linter here?

[Mario Carneiro]

I was going to suggest

elab "Message" goal:term : command => do
  discard <| runTermElabM fun _ => do
    withOptions (fun o => o.setBool `linter.unusedVariables false) do
      elabTerm goal none

but it doesn't work, the linter runs on the input syntax

[Mario Carneiro]

this works:

elab "Message'" goal:term : command => do
  discard <| runTermElabM fun _ => do elabTerm goal none

macro "Message" goal:term : command =>
  `(set_option linter.unusedVariables false in Message' $goal)

Message fun x => () -- ok

[Mario Carneiro]

there is also a general system in the linter.unusedVariables implementation for blacklisting identifiers in specific positions

[Patrick Massot]

And it also works in my real case, thanks!

[Mario Carneiro]

which is probably a better solution since it means you can localize the suppression to just the a in the (a : Nat) binders in your example

[Mario Carneiro]

you can also use a local elab to make it so users can't write the internal syntax