9eb249e38c
This PR adds a check that rejects Lake configurations where multiple executables share the same root module name. Previously, Lake would silently compile the root module once and link it into all executables, producing identical binaries regardless of differing `srcDir` settings. Lake (and Lean) rely on module names being unique within a package. Rather than attempting to support duplicate module names, Lake now produces a clear error at configuration load time, for both TOML and Lean configuration files. Closes #13013 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| debug.lean | ||
| lakefile.toml | ||
| lean-toolchain | ||
| release.lean | ||
| run_test.sh | ||