Skip to content

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Dec 1, 2025

This PR renames the namespace Std.Range to Std.Legacy.Range. Instead of using Std.Range and [a:b] notation, the new range type Std.Rco and its corresponding a...b notation should be used. There are also other ranges with open/closed/infinite boundary shapes in Std.Data.Range.Polymorphic and the new range notation also works for Int, Int8, UInt8, Fin etc.

@datokrat datokrat added the changelog-library Library label Dec 1, 2025
@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 Dec 1, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 1, 2025

Mathlib CI status (docs):

  • ❗ Batteries 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-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 12:02:03)
  • 💥 Mathlib branch lean-pr-testing-11438 build failed against this PR. (2025-12-04 18:21:29) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-13 00:18:06)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 1, 2025

Reference manual CI status:

  • ❗ 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-01 12:02:05)
  • 💥 Reference manual branch lean-pr-testing-11438 build failed against this PR. (2025-12-04 17:36:38) View Log
  • 🟡 Reference manual branch lean-pr-testing-11438 build against this PR didn't complete normally. (2025-12-04 17:37:23) View Log
  • ✅ Reference manual branch lean-pr-testing-11438 has successfully built against this PR. (2025-12-12 23:14:14) View Log
  • 🟡 Reference manual branch lean-pr-testing-11438 build against this PR didn't complete normally. (2025-12-12 23:15:45) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5339c47555cb65958259b1c4c4c687c3863a08be --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-13 00:18:07)

@datokrat datokrat force-pushed the paul/ranges/namespace-old-ranges branch from 521d6bd to da5c24c Compare December 4, 2025 16:10
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 4, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 4, 2025
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 4, 2025
@leanprover-bot leanprover-bot added the breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. label Dec 4, 2025
@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 Dec 4, 2025
@datokrat datokrat force-pushed the paul/ranges/namespace-old-ranges branch from da5c24c to f437216 Compare December 12, 2025 22:44
@leanprover-bot leanprover-bot added builds-manual CI has verified that the Lean Language Reference builds against this PR and removed breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. labels Dec 12, 2025
@datokrat datokrat force-pushed the paul/ranges/namespace-old-ranges branch from f437216 to bd30453 Compare December 12, 2025 23:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants