Skip to content

feat: lint coercions that are deprecated or banned in core #11163

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
datokrat wants to merge 20 commits into from
Closed

feat: lint coercions that are deprecated or banned in core #11163

datokrat wants to merge 20 commits into from

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Nov 13, 2025 •
edited
Loading

This PR implements a linter that warns when a deprecated coercion is applied. It also warns when the Option coercion or the Subarray-to-Array coercion is used in Init or Std. The linter is currently limited to Coe instances; CoeFun instances etc. are not considered.

The linter works by collecting the Coe instance declaration names that are being expanded in expandCoe? and storing them in the info tree. The linter itself then analyzes the info tree and checks for banned or deprecated coercions.

@datokrat datokrat added the changelog-library Library label Nov 13, 2025
@datokrat
Copy link
Contributor Author

datokrat commented Nov 13, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 13, 2025 •
edited
Loading

Benchmark results for 2f2f127 against 2b85e29 are in! @datokrat

@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 Nov 14, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 14, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11163
d66bc4c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 14, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11163
cb2c2f8
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Nov 14, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#11163
87f479a
@leanprover-bot leanprover-bot added the breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. label Nov 14, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 14, 2025 •
edited
Loading

Reference manual CI status:

  • 💥 Reference manual branch lean-pr-testing-11163 build failed against this PR. (2025-11-14 11:10:00) View Log
  • 🟡 Reference manual branch lean-pr-testing-11163 build against this PR didn't complete normally. (2025-11-14 11:10:08) View Log
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-04 12:54:06)

@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 14, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 14, 2025 •
edited
Loading

Mathlib CI status (docs):

datokrat added a commit to datokrat/aesop that referenced this pull request Nov 16, 2025
@datokrat
adaptation for leanprover/lean4#11163
adddbdf
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 16, 2025
@datokrat datokrat force-pushed the paul/slices/subarraycopy branch from 68a4aa4 to a9f5920 Compare December 2, 2025 14:28
@datokrat datokrat changed the title refactor: remove coercion from Subarray to Array refactor: lint deprecated coercions and coercions banned in core Dec 2, 2025
@datokrat datokrat changed the title refactor: lint deprecated coercions and coercions banned in core feat: lint coercions that are deprecated or banned in core Dec 2, 2025
@datokrat datokrat changed the base branch from master to nightly-with-mathlib December 2, 2025 14:37
@datokrat
Copy link
Contributor Author

datokrat commented Dec 2, 2025

The warnings currently look like this:

screenshot

@datokrat
Copy link
Contributor Author

datokrat commented Dec 2, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 2, 2025 •
edited
Loading

Benchmark results for 8493245 against 5bd331e are in! @datokrat

Runs (2)
  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

@datokrat
Copy link
Contributor Author

datokrat commented Dec 2, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 2, 2025 •
edited
Loading

Benchmark results for 75c7082 against 5bd331e are in! @datokrat

@datokrat datokrat force-pushed the paul/slices/subarraycopy branch from 9d038a0 to 6c5afe9 Compare December 2, 2025 19:44
@datokrat datokrat changed the base branch from nightly-with-mathlib to paul/base/slices/subarraycopy December 4, 2025 09:15
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 4, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11163
e738030
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 4, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#11163
af8b0be
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Dec 4, 2025
@datokrat datokrat closed this Dec 4, 2025
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

breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library 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.

5 participants

@datokrat @leanprover-radar @leanprover-bot @leanprover-community-bot