Plugins produced by setup-file for module Foo include Foo

Description

lakefile.toml

name = "lakewat"
precompileModules = true

[[lean_lib]]
name = "Lakewat"
srcDir = "src/"

lean-toolchain

leanprover/lean4:nightly-2026-07-30

src/Lakewat.lean

import Lakewat.Foo

src/Lakewat/Basic.lean

src/Lakewat/Foo.lean

import Lakewat.Basic

#eval nonsense

Steps to Reproduce

> lake setup-file src/Lakewat/Foo.lean
✖ [5/11] Building Lakewat.Foo

Expected behavior: setup-file succeeds and includes the precompiled module for Basic.

Actual behavior: setup-file circularly tries to build Foo.

Versions

Lean (version 4.34.0-nightly-2026-07-30, x86_64-unknown-linux-gnu, commit 5fe7f2454c32fe1605c6910f7140ce1f0a04f43b, Release)

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start by reproducing the issue with lakefile.toml, lean-toolchain, src/Lakewat/Foo.lean, and src/Lakewat/Basic.lean using lake setup-file src/Lakewat/Foo.lean. Trace the setup-file plugin build path and verify that it succeeds by using the precompiled Basic module without circularly building Foo.