feat: add Cslib.Init module and checkInitImports linter #131

jessealama · 2025-10-26T13:45:02Z

Closes #122

This PR implements Cslib.Init following Mathlib's pattern, along with a checkInitImports linter to ensure modules are connected to the library's import graph.

Changes

Created Cslib/Init.lean importing Mathlib.Init and Cslib.Foundations.Lint.Basic
Added checkInitImports environment linter
Integrated validation into lake test via new test scripts in scripts/
Added import Cslib.Init to 10 foundational modules

Files excluded from import

Some files could not import Cslib.Init due to technical constraints:

Cslib.Foundations.Lint.Basic: Circular dependency (imported by Cslib.Init)
Cslib.Foundations.Data.FinFun: Notation conflict with Mathlib.Finsupp (both use →₀)
Cslib.Foundations.Semantics.LTS.Basic: Causes type elaboration issues in downstream Automata files
Cslib.Logics.LinearLogic.CLL.Basic: Syntax elaboration conflicts

TODO comments have been added to document these issues for future investigation.

This commit implements Cslib.Init following Mathlib's pattern, along with a checkInitImports linter to ensure modules are connected to the library's import graph. Changes: - Created Cslib/Init.lean importing Mathlib.Init and Cslib.Foundations.Lint.Basic - Added checkInitImports environment linter to Cslib/Foundations/Lint/Basic.lean - Created scripts/check-init-imports.lean for text-based CI validation - Updated lakefile.toml comments - Added import Cslib.Init to 10 foundational modules (3 Syntax files + 7 others) Files excluded from import due to technical constraints: - Cslib.Foundations.Lint.Basic: Circular dependency (imported by Cslib.Init) - Cslib.Foundations.Data.FinFun: Notation conflict with Mathlib.Finsupp (both use →₀) - Cslib.Foundations.Semantics.LTS.Basic: Causes type elaboration issues in downstream files - Cslib.Logics.LinearLogic.CLL.Basic: Syntax elaboration conflicts TODO comments have been added to document these issues for future investigation.

Cslib/Foundations/Lint/Basic.lean

scripts/check-init-imports.lean

scripts/CheckInitImports.lean

lakefile.toml

@chenson2018

This commit addresses feedback from @chenson2018 on PR leanprover#131: 1. Removed the environment linter approach - Environment linters fire on every declaration, causing spam - Import connectivity is a whole-graph property, not per-declaration 2. Improved the script to use Mathlib's findImports - Now uses Lean.parseImports' internally (robust parser) - Replaced brittle text parsing with proper Lean parser 3. Updated lakefile.toml comments - Clarified that we use a script-based approach, not env linter - Matches Mathlib's pattern (script-based, not environment linter) The script works correctly and identifies the 4 modules that don't import any Cslib module (as documented in the PR description).

Add an allowlist of 4 modules that cannot import Cslib.Init due to technical constraints: - Cslib.Foundations.Lint.Basic: Circular dependency (imported by Init) - Cslib.Foundations.Data.FinFun: Notation conflict with Mathlib (→₀) - Cslib.Foundations.Semantics.LTS.Basic: Type elaboration issues - Cslib.Logics.LinearLogic.CLL.Basic: Syntax elaboration conflicts This follows Mathlib's pattern, which also maintains an allowlist of modules excluded from their missingInitImports check. The script now passes in CI while still catching new orphaned modules. Tested by creating a test orphan module - correctly detected.

Refactor to match Mathlib's exact pattern of using chained .erase calls instead of an upfront allowedExclusions array. This mirrors how Mathlib's missingInitImports handles exceptions. Tested: script still passes and correctly detects new orphan modules.

jessealama · 2025-10-27T07:15:51Z

Thanks! I think I've addressed the feedback. Can you take another look?

Remove `Elab Command` opens that were added for the environment linter but are no longer needed after its removal.

Revert comment-only changes to simplify PR review. The configuration itself is unchanged.

Move copyright header before the import statement to follow standard Lean file convention.

scripts/check-init-imports.lean

chenson2018 · 2025-10-28T06:07:03Z

Thanks for the work, I think this is moving in the right direction! A couple of follow up questions.

Regarding the logic for checking imports, let me make sure I have it straight:

first you grab all the imports from Cslib.lean
you then check that the only of these without a Cslib import are the current exceptions for Mathlib compatibility
this implies that they all import Cslib.Init (because this is the only file excluded from Cslib.lean??)

With the exceptions existing though, do you need to change hasCslibImport to check for an import that is in the Cslib namespace and isn't on the exception list? Does this still work if you add Cslib.Init to Cslib.lean?

I also don't think you've made scripts/check-init-imports.lean run for lake test?

It would also be nice to go ahead and address #125 here since it affects the logic of checking Cslib.Init dependency. This should be much simpler in comparison. Edit: To answer your question from over there, I think maybe it is easiest if you write a short Lean function that checks this?

Replace pattern matching on name components with the more idiomatic Lean.Name.getRoot method.

- Refactor CheckInitImports with clearer exception handling - Add CheckCslibComplete to verify all modules in Cslib.lean (leanprover#125) - Create RunTests driver to execute both checks via `lake test` - Rename scripts to PascalCase for lakefile.toml compatibility

jessealama · 2025-10-28T09:31:59Z

Thanks for the work, I think this is moving in the right direction! A couple of follow up questions.

Regarding the logic for checking imports, let me make sure I have it straight:

first you grab all the imports from Cslib.lean

you then check that the only of these without a Cslib import are the current exceptions for Mathlib compatibility

this implies that they all import Cslib.Init (because this is the only file excluded from Cslib.lean??)

With the exceptions existing though, do you need to change hasCslibImport to check for an import that is in the Cslib namespace and isn't on the exception list? Does this still work if you add Cslib.Init to Cslib.lean?

I also don't think you've made scripts/check-init-imports.lean run for lake test?

It would also be nice to go ahead and address #125 here since it affects the logic of checking Cslib.Init dependency. This should be much simpler in comparison. Edit: To answer your question from over there, I think maybe it is easiest if you write a short Lean function that checks this?

Thanks! I've refactored the import checking logic to filter out exceptions upfront, and added that to lake test (with a new test driver). I think I've addressed the issue in #125, too. Can you take another look when you have a moment?

- Use filter instead of imperative loops - Add Cslib itself to exceptions list - Remove issue reference from documentation

… add-cslib-init

chenson2018 · 2025-10-29T07:48:11Z

I just pushed a commit that made some alterations to scripts/CheckInitImports.lean to ensure it checks transitive imports. (I used the ImportGraph module, which I think simplifies what we were doing by hand).

I will take a look at scripts/CheckCslibComplete.lean and the test runner next.

chenson2018 · 2025-10-29T10:46:13Z

@jessealama Okay, I think we are nearly done here. I would appreciate you taking a look and testing. Here are the highlights of what I just pushed:

I realized your initial suggestion of using lake exe mk_all --check was the right thing to do, and in fact there is already an option for this in lean-action, so I've enabled this and removed scripts/CheckCslibComplete.lean. Sorry for the churn, I should have realized this earlier!
following suit with Mathlib, I do require Cslib.Init to be imported in Cslib.lean.
The test runner you added was missing the original tests from CslibTests, I have added this back.

I am pretty happy with everything here. My only hesitation is being unsure about the setup of the test runner, which feels a bit nonstandard in how it includes a lean_exe target and uses IO.Process.spawn. I have asked a related question on Zulip. Let's wait a bit to see if that generates any useful suggestions.

chenson2018 · 2025-10-29T11:19:42Z

One final consideration: do we actually remove the weak from lakefile options? Either way is not great for beginners IMO:

if we keep weak and someone doesn't import Init, they find out in CI and potentially get slammed with lint errors
if we remove them, it maybe gets caught earlier, but with a confusing error message

chenson2018 · 2025-10-29T18:36:11Z

@fmontesi Can you please review this before merging anything else? Because a change to testing merged at the same time as some other PRs, there are some failures on main. Since this also changes testing, I'd like to fix this here (and ask that folks merge main on other open PRs)

jessealama requested review from chenson2018, fmontesi and kim-em as code owners October 26, 2025 13:45

jessealama force-pushed the add-cslib-init branch from 4966ada to ece20ae Compare October 26, 2025 13:46

chenson2018 requested changes Oct 26, 2025

View reviewed changes

Cslib/Foundations/Lint/Basic.lean Outdated Show resolved Hide resolved

scripts/check-init-imports.lean Outdated Show resolved Hide resolved

scripts/CheckInitImports.lean Outdated Show resolved Hide resolved

lakefile.toml Outdated Show resolved Hide resolved

jessealama added 3 commits October 27, 2025 07:47

jessealama requested a review from chenson2018 October 27, 2025 07:15

jessealama added 3 commits October 27, 2025 08:40

chore: remove unused namespace opens

b1e53e5

Remove `Elab Command` opens that were added for the environment linter but are no longer needed after its removal.

chore: revert lakefile.toml comment changes

a7d8804

Revert comment-only changes to simplify PR review. The configuration itself is unchanged.

style: move copyright to beginning of file

5020ca3

Move copyright header before the import statement to follow standard Lean file convention.

chenson2018 reviewed Oct 28, 2025

View reviewed changes

scripts/check-init-imports.lean Outdated Show resolved Hide resolved

jessealama added 2 commits October 28, 2025 10:01

refactor: use getRoot to check namespace prefix

831b7cb

Replace pattern matching on name components with the more idiomatic Lean.Name.getRoot method.

jessealama requested a review from chenson2018 October 28, 2025 10:31

jessealama and others added 3 commits October 28, 2025 13:08

refactor: simplify CheckCslibComplete with functional style

e83f03e

- Use filter instead of imperative loops - Add Cslib itself to exceptions list - Remove issue reference from documentation

use ImportGraph to account for transitive imports

b20382e

Merge remote-tracking branch 'refs/remotes/jesse/add-cslib-init' into…

e7cf196

… add-cslib-init

chenson2018 added 6 commits October 29, 2025 05:30

work on CheckCslibComplete, put back Jesse's better error messages

830f76f

import Cslib.Init in Cslib.lean

acdc4c8

include CslibTests in runner

5941474

Merge remote-tracking branch 'upstream/main' into add-cslib-init

586a125

add Cslib.Init

836aba5

mk_all-check arg in CI

d60f1d2

remove CheckCslibComplete

5841b3a

format TODOs for the bot

5ce159f

chenson2018 linked an issue Oct 29, 2025 that may be closed by this pull request

check that all directories are imported in Cslib.lean #125

Closed

chenson2018 added 3 commits October 29, 2025 14:03

Merge remote-tracking branch 'upstream/main' into add-cslib-init

36f89d2

alpha order

70a8d59

some CI failures after merge

e80fd0a

chenson2018 approved these changes Oct 29, 2025

View reviewed changes

chenson2018 mentioned this pull request Oct 29, 2025

chore: make various automata accept Language _ rather than Set (List _) #135

Merged

fmontesi approved these changes Oct 29, 2025

View reviewed changes

fmontesi merged commit 9dd5453 into leanprover:main Oct 29, 2025
3 checks passed

fmontesi added the CI Change label Oct 29, 2025

jessealama deleted the add-cslib-init branch October 30, 2025 09:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: add Cslib.Init module and checkInitImports linter #131

feat: add Cslib.Init module and checkInitImports linter #131

Uh oh!

jessealama commented Oct 26, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jessealama commented Oct 27, 2025

Uh oh!

Uh oh!

chenson2018 commented Oct 28, 2025 •

edited

Loading

Uh oh!

jessealama commented Oct 28, 2025

Uh oh!

chenson2018 commented Oct 29, 2025

Uh oh!

chenson2018 commented Oct 29, 2025 •

edited

Loading

Uh oh!

chenson2018 commented Oct 29, 2025

Uh oh!

chenson2018 commented Oct 29, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

feat: add Cslib.Init module and checkInitImports linter #131

feat: add Cslib.Init module and checkInitImports linter #131

Uh oh!

Conversation

jessealama commented Oct 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Files excluded from import

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jessealama commented Oct 27, 2025

Uh oh!

Uh oh!

chenson2018 commented Oct 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jessealama commented Oct 28, 2025

Uh oh!

chenson2018 commented Oct 29, 2025

Uh oh!

chenson2018 commented Oct 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chenson2018 commented Oct 29, 2025

Uh oh!

chenson2018 commented Oct 29, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jessealama commented Oct 26, 2025 •

edited

Loading

chenson2018 commented Oct 28, 2025 •

edited

Loading

chenson2018 commented Oct 29, 2025 •

edited

Loading