Skip to content

feat: expand byte array api - #8165

Open
Rob23oba wants to merge 20 commits into
leanprover:masterfrom
Rob23oba:byte-array-additions
Open

feat: expand byte array api#8165
Rob23oba wants to merge 20 commits into
leanprover:masterfrom
Rob23oba:byte-array-additions

Conversation

@Rob23oba

@Rob23oba Rob23oba commented Apr 29, 2025 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR adds functions ByteArray.setSize, ByteArray.fill, ByteArray.sliceEq, ByteArray.replicate, ByteArray.getUIntN(LE|BE) and ByteArray.setUIntN(LE|BE) to the byte array api.

@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 29, 2025
@ghost

ghost commented Apr 29, 2025 •
edited by ghost
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0afcda86548867c231cbf7b66a8eb28a8acc3773 --onto 2929d547dcc7ad3e947fc0a5ec8e79d07e0bcb2e. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-29 17:50:47)
  • 💥 Mathlib branch lean-pr-testing-8165 build failed against this PR. (2025-04-29 21:43:09) View Log
  • 💥 Mathlib branch lean-pr-testing-8165 build failed against this PR. (2025-07-28 12:02:54) View Log

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 29, 2025
leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8165
afaf37a
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 29, 2025
leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8165
d60c0b2
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 29, 2025
@Rob23oba Rob23oba mentioned this pull request Jul 25, 2025
Closed
@leanprover-bot

leanprover-bot commented Jul 28, 2025 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-27 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-07-28 11:19:04)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-28 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. (2026-03-29 13:16:20)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3facd362febfedef5d1711297f541806a51abe1a --onto c8e19cca2547a89c3aba401afaab9a8808f490a2. You can force reference manual CI using the force-manual-ci label. (2026-09-02 04:59:37)

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jul 28, 2025
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8165
45afbbc
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 28, 2025
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8165
061e500
@Rob23oba
Rob23oba marked this pull request as ready for review July 28, 2025 16:03
@Rob23oba
Rob23oba requested a review from kim-em as a code owner July 28, 2025 16:03
@github-actions github-actions Bot added the changelog-library Library label Jul 28, 2025
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Sep 4, 2025
@Rob23oba
Rob23oba requested a review from TwoFX as a code owner March 29, 2026 12:23
@Rob23oba
Rob23oba requested a review from mhuisi as a code owner March 29, 2026 13:05
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Mar 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-29 13:16:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3facd362febfedef5d1711297f541806a51abe1a --onto c8e19cca2547a89c3aba401afaab9a8808f490a2. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-02 04:59:35)

@Rob23oba Rob23oba mentioned this pull request Jun 17, 2026
Draft
Rob23oba and others added 3 commits July 27, 2026 02:51
@Rob23oba
Merge remote-tracking branch 'upstream/master' into byte-array-additions
18e5691
Kim Morrison
Merge remote-tracking branch 'upstream/master' into byte-array-additions
1fe9cb3
Kim Morrison @claude
chore: mark the ByteArray deprecations as changing type
40d9379 
`getUInt64LE!` and `getUInt64BE!` take an offset, so they are
`ByteArray → Nat → UInt64` where the deprecated definitions are
`ByteArray → UInt64`. The check for this landed after the branch was
last built.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner
@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner
@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library P-medium We may work on this issue if we find the time 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

@Rob23oba @leanprover-bot