Skip to content

feat: upstream environment linters to core lean#13356

Merged
wkrozowski merged 7 commits intoleanprover:masterfrom
wkrozowski:wojciech/envlinter_upstream1
Apr 13, 2026
Merged

feat: upstream environment linters to core lean#13356
wkrozowski merged 7 commits intoleanprover:masterfrom
wkrozowski:wojciech/envlinter_upstream1

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

@wkrozowski wkrozowski commented Apr 10, 2026

This PR upstreams environment linters of batteries to core lean.

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label Apr 10, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 10, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Apr 10, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a07649a4c6f29617954294ebe40a6d26024944c9 --onto 4f6bcc5adac8d6234a9e3def3675402cb89823c6. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-10 11:42:13)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a07649a4c6f29617954294ebe40a6d26024944c9 --onto d76e5a1886956bb38dc6bd2868260550dc66c309. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-13 13:45:46)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 10, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a07649a4c6f29617954294ebe40a6d26024944c9 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-10 11:42:14)

@wkrozowski wkrozowski added this pull request to the merge queue Apr 13, 2026
Merged via the queue into leanprover:master with commit 1c9e264 Apr 13, 2026
19 checks passed
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
@wkrozowski @volodeyka
feat: upstream environment linters to core lean (#13356)
c3084bf 
This PR upstreams environment linters of batteries to core lean.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@wkrozowski @leanprover-bot