fix: wrap sibling-problem helpers in per-problem inner namespaces#319
Merged
Conversation
After the §38/§40/§42/§45 sibling PRs merged, validate-manifest and generate fail with `environment already contains LeanEval.Geometry.IsMetricCompatible` from sibling-problem files defining the same helper at the same namespace path. Individual PRs passed CI because the LeanEval lib file does not import any of these modules, but the lean-eval CLI loads every @[eval_problem] module together at validate time. Each colliding pair (Levi-Civita/Koszul, Morse/WeakMorse, Platonic/Schlafli, Darboux/LiouvilleArnold) is fixed by inserting an inner `namespace <ProblemName>` wrapper around the file's helper defs and main theorem. The eval-problem matching is by basename (so hole = "levi_civita" still resolves to the wrapped theorem); the manifest module path is by file path (unchanged). Verified: - `lake build` for all 8 files succeeds with only the expected sorry warnings. - `lake exe lean-eval validate-manifest` reports "consistent". - `lake exe lean-eval generate` produces 92 workspaces. - Per-problem generated workspaces (e.g. `levi_civita_exists_unique`, `morse_inequality`) build clean. Files touched: - LeanEval/Geometry/LeviCivita.lean - LeanEval/Geometry/KoszulFormula.lean - LeanEval/Geometry/MorseInequalities.lean - LeanEval/Geometry/WeakMorseInequality.lean - LeanEval/Geometry/PlatonicClassification.lean - LeanEval/Geometry/SchlafliClassification.lean - LeanEval/Geometry/Darboux.lean - LeanEval/Geometry/LiouvilleArnold.lean Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Main is broken:
lake exe lean-eval validate-manifestandlake exe lean-eval generateboth fail withafter the recent batch of sibling Knill PRs merged.
Cause: Levi-Civita / Koszul, Morse / Weak Morse, Platonic / Schläfli,
and Darboux / Liouville-Arnold each define identical helper-def names
(
IsMetricCompatible,IsCriticalPoint,ConvexPolytope,E,idxP,idxQ, …) at the sameLeanEval.Geometrynamespace path.Individual PRs were CI-green because
LeanEval.lean(the lib glob)doesn't import these modules, but
lake exe lean-evalloads every@[eval_problem]module together for inventory validation, whichtrips the collision. 25 colliding decl names total across 8 files.
Fix: wrap each file's helpers + main theorem in an inner
namespace <ProblemName>(e.g.LeanEval.Geometry.LeviCivita.*).The
@[eval_problem]matching is bybasename, soholes = [\"levi_civita\"]still resolves correctly. Manifest modulepath is by file path — unchanged.
Verified:
lake buildfor all 8 files: success, only expected sorry warnings.lake exe lean-eval validate-manifest: "Manifest and @[eval_problem]declarations are consistent."
lake exe lean-eval generate: produces 92 workspaces.levi_civita_exists_unique,morse_inequality) build clean.🤖 Prepared with Claude Code