fix(lean): make lake build actually compile and pass + gitignore build artifacts - #23
Merged
Merged
Conversation
The repo had no .gitignore, so reproducing CI locally (cargo build, lake update, lake build) left untracked build output at the top of git status: parser/target/ (Rust), core/lean/.lake/ (Lean/mathlib build cache, ~5.7GB), core/lean/AutoGen/ (generated Lean files from the .cat pipeline), and lake-manifest.json.
`lake build` (CI's proof-check step) was failing to compile Core.lean against the pinned mathlib (v4.21.0-rc2): - EpsFunctor.comp_ok: composition order was backwards (`g ≫ f` when f : A ⟶ B, g : B ⟶ C₁ don't compose that way) - swapped to `f ≫ g`, matching functoriality. - EpsFunctor's distortion metric `d` was typed over morphisms of `C` (the source category) instead of `D` (the target category) - only accidentally type-checked in IdFunctor because C = D = UnitCat there. Retyped it over D, matching what comp_ok actually measures. - IdFunctor's `EpsFunctor (d := PhaseDist) 0` left C/D as stuck metavariables during typeclass search; made them explicit via `@EpsFunctor UnitCat UnitCat _ _ PhaseDist 0`. - IdFunctor's comp_ok proof: `simp [PhaseDist]` couldn't unfold the HasPhase instance's constant-0 `phase` field on its own; replaced with `show |(0:ℝ) - 0| ≤ (0:ℝ)` (defeq, since the instance always returns 0) followed by `norm_num`. Also adds .gitignore for build artifacts (parser/target/, core/lean/.lake/, core/lean/AutoGen/) - the repo had none, so reproducing CI locally left them as untracked output. Verified with a clean `lake update && lake build` locally - green.
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
2 participants
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.
Summary
Same CI investigation as #22 (already merged on
feature/gemini-proposal), applied tomain. Notemain'score/lean/Core.leanis a different (single-file) revision of the design than the one onfeature/gemini-proposal, so the fixes here are specific to this version, not a copy-paste of #22.lake build(CI's proof-check step) was failing to compileCore.leanagainst the pinned mathlib (v4.21.0-rc2):EpsFunctor.comp_ok: composition order was backwards (g ≫ fwhenf : A ⟶ B,g : B ⟶ C₁don't compose that way) — swapped tof ≫ g, matching functoriality.EpsFunctor's distortion metricdwas typed over morphisms ofC(the source category) instead ofD(the target category) — only accidentally type-checked inIdFunctorbecauseC = D = UnitCatthere. Retyped it overD, matching whatcomp_okactually measures.IdFunctor'sEpsFunctor (d := PhaseDist) 0leftC/Das stuck metavariables during typeclass search; made them explicit via@EpsFunctor UnitCat UnitCat _ _ PhaseDist 0.IdFunctor'scomp_okproof:simp [PhaseDist]couldn't unfold theHasPhaseinstance's constant-0phasefield on its own; replaced withshow |(0:ℝ) - 0| ≤ (0:ℝ)(defeq, since the instance always returns 0) followed bynorm_num.Also adds
.gitignorefor build artifacts (parser/target/,core/lean/.lake/,core/lean/AutoGen/) — the repo had none, so reproducing CI locally left them as untracked output.Test plan
lake update && lake buildlocally on this branch — clean build (one harmless unused-variable warning only).Known remaining gap (out of scope here)
CatPrism_examples.leanreferencesverify_comp(no such tactic exists anywhere in this branch's Lean project) and names likeExample1.ProjectionFunctor/GroupCatthat aren't defined. It's not a CI default target so it doesn't block this fix, but it doesn't actually build. Left for a follow-up.Generated by Claude Code