lake shake removes imports needed by open statements

Description

lake shake can remove imports that are required for open statements to resolve, violating the invariant that lake build && lake shake --fix && lake build should always succeed.

The root cause is that lake shake determines import necessity by scanning constants in compiled .olean files and tracking elaboration dependencies via recordExtraModUse. However, open Foo(bar) statements resolve names during elaboration without recording those resolutions as module dependencies. If the opened name is not referenced by any compiled constant (e.g., it's opened but unused, or all uses resolve through dot notation), shake considers the providing import unnecessary and removes it.

Minimal Reproduction

Create a project with the following files:

lean-toolchain:

leanprover/lean4:v4.28.0

lakefile.lean:

import Lake
open Lake DSL

package «shake-repro» where
  leanOptions := #[
    ⟨`experimental.module, true⟩,
    ⟨`backward.privateInPublic, false⟩
  ]

lean_lib ShakeRepro where
  roots := #[`ShakeRepro]

ShakeRepro.lean:

module
public import ShakeRepro.Defs
public import ShakeRepro.Extra
public import ShakeRepro.User

ShakeRepro/Defs.lean:

module

public section

namespace Repro

def List.sum' (xs : List Nat) : Nat := xs.foldl (· + ·) 0

end Repro

ShakeRepro/Extra.lean:

module

public section

namespace Repro

def greet (s : String) : String := s!"Hello, {s}!"

end Repro

ShakeRepro/User.lean:

module

import ShakeRepro.Defs
import ShakeRepro.Extra

open Repro(List.sum')

def test : String := Repro.greet "world"

Then run:

lake build ShakeRepro                # succeeds
lake shake --force --fix ShakeRepro  # removes import ShakeRepro.Defs
lake build ShakeRepro                # FAILS: Unknown constant 'Repro.List.sum''

Expected Behavior

lake shake should not remove imports that are required for open statements to resolve. The invariant lake build && lake shake --fix && lake build should hold.

Proposed Fix

Add recordExtraModUseFromDecl calls in Lean.Elab.OpenDecl.elabOpenDecl (in src/Lean/Elab/Open.lean) for each name resolved by explicit open statements (open ns (ids), open ns hiding ids, open ns renaming ...). This records the elaboration-time dependency so that shake knows the import is needed.

I have a working patch that resolves this for the explicit open variants. Happy to submit a PR if desired.

Additional Context

In a large real-world project using the module system, lake shake produces additional failures beyond the open tracking issue, including:

• Public meta import visibility: shake adds meta import X (private meta) when public meta import X is needed for public meta definitions that transitively reference constants from X
• Parser extension dependencies: syntax ident : mySyntaxCat references parser extensions that aren't tracked as dependencies

These may warrant separate issues.

Versions

• Lean: v4.28.0
• OS: Linux

Start with src/Lean/Elab/Open.lean and inspect Lean.Elab.OpenDecl.elabOpenDecl, then reproduce the failure with the lake build and lake shake commands in the issue. Check the explicit open variants described there and verify that lake build succeeds before and after lake shake --fix.