Language server allows `set_option`s that `lake` doesn't

Stream: lean4

[Thomas Murrills]

If you have a file called Foo which registers an option:

module
public import Lean

/-- the docstring! -/
public meta register_option foo : Bool := {
  defValue := true
  descr := "the descr!"
}

Then you import that file in Bar:

module
import Foo

Then you import that file in Baz:

module
import Bar

set_option foo true

the language server will not complain. However lake build Baz will fail with "Unknown option foo". (The previous file Bar would succeed if you wrote set_option foo true in it.)

Likewise, as you'd expect, the docstring for foo is not available in Baz; if you write and hover over set_option foo true in Bar, you will see the docstring!, but do so in Baz and you will see the descr!.

(Playing around with removing public and meta from register_option shift the failures to places that seem predictable, but I wanted to show that the issue here was not from a lack of proper modifers on a register_option.)

[Sebastian Ullrich]

This is the same issue as the second part of #mathlib4 > shake @ 💬. We definitely want to fix this, please consider opening an issue

[Thomas Murrills]

Sebastian Ullrich said:

This is the same issue as the second part of #mathlib4 > shake @ 💬. We definitely want to fix this, please consider opening an issue

lean4#12732