Language server diverges from `lake build`

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the module system, the language server loads more data than lake build does on the command line, resulting in divergence in behavior between the two.

For example, this may cause the language server to succeed while the command line fails, leading to users being unaware of command-line build failures while editing interactively.

Context

This issue has reared its head when shake modifies imports and when options are imported, since they are registered with initialize.

Steps to Reproduce

To inline the example from the second discussion:

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.)

(The hover on foo in Baz also shows that the docstring is not available, as it falls back to displaying "the descr".)

Expected behavior: In Baz, the user sees an error "Unknown option foo" in both the language server and on the command line.

Actual behavior: In Baz, the user sees an error "Unknown option foo" on the command line, but no error and suboptimal hovers in the language server.

Versions

4.29.0-rc2, nightly-2026-2-25, macOS

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the Foo, Bar, and Baz reproduction from the issue and run it with both the language server and lake build on the latest nightly. Trace how the module imports and registered option are loaded in each path; done means both paths report the unknown option consistently and provide equivalent hover information.