Linter error in Web editor

Stream: general

[Michael Stoll]

import Mathlib

set_option trace.Meta.synthInstance true

This produces

Forbidden set_option `trace.Meta.synthInstance`; please remove
note: this linter can be disabled with `set_option linter.setOption false`

when pasted into the web editor.

It looks like the Mathlib linters are activated there by mistake?

[Michael Stoll]

(Without the import, the message goes away.)

[Michael Rothgang]

Indeed, this is a (very recent) mathlib linter firing. Should this not happen?

[Michael Rothgang]

Alternatively, it wouldn't be hard to scope the linter to Mathlib only. Would this be better?

[Michael Stoll]

You want to be able to trace/profile/... stuff without being bothered by warnings also in the Web Editor, I would think.

[Michael Stoll]

My understanding is that this is a linter that should make sure that files submitted to Mathlib do not contain noisy commands. But it should not be active in files that just use Mathlib.

[Damiano Testa]

Other linters (e.g. the hash-command linter, I think), only emit a warning if the linted command is silent. If you are tracing, you probably are getting a trace message, so there is no need for further flagging.

[Damiano Testa]

(This may avoid special-casing mathlib vs everything else.)

[Jon Eugster]

The same linter warning triggers in any project depending on mathlib, doesn't it? So there is nothing specific about the webeditor, is there?

I think it shouldn't be hard to just disable it in the webeditor, but I'm not convinced the current version in mathlib is desired in begin with, so maybe it's best to address the issues directly in mathlib.

[Jon Eugster]

I am completely unfamiliar with linters, but why is this a linter that's always active and not one that is triggered by #lint? And why does it for example not trigger on the following?

import Mathlib

set_option trace.Meta.synthInstance true in

variable (n : Nat)

(but it triggers when removing the in)

[Jon Eugster]

(deleted)

[Eric Wieser]

Syntax linter are always active, only environment linters are triggered by #lint

[Damiano Testa]

Also, the in is actually the "head" of the syntax, so, from the perspective of the linter, set_option ... in ... really looks like in ... so it is quite different from set_option ... [not in].

[Damiano Testa]

(I am not sure that it really is defined like this, but in is like an infix.)

[Damiano Testa]

Here is how the syntax trees look like without in and with in:

/-
inspect: 'set_option autoImplicit false'

node Lean.Parser.Command.set_option, none
|-atom original: ⟨⟩⟨ ⟩-- 'set_option'
|-ident original: ⟨⟩⟨ ⟩-- (autoImplicit,autoImplicit)
|-node null, none
|-atom original: ⟨⟩⟨\n\n\n⟩-- 'false'
-/
set_option autoImplicit false
#eval "" -- note that this `#eval` is not "captured" by the `set_option`

/-
inspect: 'set_option autoImplicit false in #eval ""'

node Lean.Parser.Command.in, none
|-node Lean.Parser.Command.set_option, none
|   |-atom original: ⟨⟩⟨ ⟩-- 'set_option'
|   |-ident original: ⟨⟩⟨ ⟩-- (autoImplicit,autoImplicit)
|   |-node null, none
|   |-atom original: ⟨⟩⟨ ⟩-- 'false'
|-atom original: ⟨⟩⟨\n⟩-- 'in'
|-node Lean.Parser.Command.eval, none
|   |-atom original: ⟨⟩⟨ ⟩-- '#eval'
|   |-node str, none
|   |   |-atom original: ⟨⟩⟨\n\n⟩-- '""'
-/
set_option autoImplicit false in
#eval ""

[Michael Stoll]

Jon Eugster said:

The same linter warning triggers in any project depending on mathlib, doesn't it? So there is nothing specific about the webeditor, is there?

I haven't yet tried to set options in a project that depends on a recent Mathlib, so I encountered this first in the web editor. But I'd also find it annoying in projects.