Repository navigation
chore(build): silence Lake's module-system warning with allowNonModules - #39
Merged
Merged
Conversation
Mathlib sets requiresModuleSystem, so Lake warns on every Mathlib import from a file without a `module` header. The chapters stay out of the module system on purpose; declare that in CSwL's lakefile and in the lakefile of the generated per-variant projects. Adopting the module system is tracked in #38. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author.
Contributor
There was a problem hiding this comment.
🟢 Approval recommended
Both configuration changes consistently implement the intended warning suppression, with no blocking issues identified.
No open issues 🎉
What changed in this PR
Suppresses Lake’s module-system warnings while keeping chapters outside the module system, pending the decision tracked in #38.
Changes:
- Enables
allowNonModulesin the main package and generated variant projects. - Documents the reason for the opt-out.
| File | Description |
|---|---|
lakefile.toml |
Enables and explains package-wide warning suppression. |
CSwLMeta/Save/Project.lean |
Adds the same setting to generated project configurations. |
Review effort: Balanced
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
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.
Mathlib sets
requiresModuleSystem, so since v4.35.0 Lake warns on every Mathlib import from a file without amoduleheader ("consider addingmoduleto the start of this file"). The chapters stay out of the module system on purpose for now; this setsallowNonModules = trueinlakefile.tomland in the lakefile template of the generated per-variant projects (CSwLMeta/Save/Project.lean).Adopting the module system is tracked in #38.
Verified locally:
make allbuilds all four variants with no module-system warnings; the generated projects carryallowNonModules = true, and thesolutionsproject compiles standalone.This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author.