Zulip Chat Archive

Stream: lean4

Topic: disable linter in elab


Patrick Massot (Sep 28 2022 at 20:14):

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 (Sep 28 2022 at 20:27):

set_option linter.unusedVariables false

Mario Carneiro (Sep 28 2022 at 20:34):

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

Patrick Massot (Sep 28 2022 at 20:41):

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

Patrick Massot (Sep 28 2022 at 20:43):

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 (Sep 28 2022 at 20:47):

can you make a MWE?

Patrick Massot (Sep 28 2022 at 20:49):

Sorry, I'll work on a MWE

Mario Carneiro (Sep 28 2022 at 20:54):

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 (Sep 28 2022 at 20:54):

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 (Sep 28 2022 at 20:55):

Indeed yours is more minimal :rolling_eyes:

Patrick Massot (Sep 28 2022 at 20:56):

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

Mario Carneiro (Sep 28 2022 at 20:56):

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 (Sep 28 2022 at 20:57):

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 (Sep 28 2022 at 20:59):

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

Patrick Massot (Sep 28 2022 at 21:00):

And it also works in my real case, thanks!

Mario Carneiro (Sep 28 2022 at 21:00):

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 (Sep 28 2022 at 21:00):

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


Last updated: Dec 20 2023 at 11:08 UTC