Skip to content
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

fix: reference implementation ByteArray.copySlice #2967

Merged
merged 4 commits into from
Dec 16, 2023
Merged

fix: reference implementation ByteArray.copySlice #2967

merged 4 commits into from
Dec 16, 2023

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Nov 27, 2023

Fixes reference implementation of ByteArray.copySlice, as reported #2966.

Adds tests.

@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Nov 27, 2023
nomeata
nomeata approved these changes Nov 27, 2023
View reviewed changes
Copy link
Collaborator

@nomeata nomeata left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice test. Maybe later we can even write a generic testNativeFunction tactic that we can use to test all the functions.

@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 27, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Nov 27, 2023 •
edited
Loading

  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-27' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-27 08:49:33)
  • 🟡 Mathlib branch lean-pr-testing-2967 build against this PR was cancelled. (2023-12-16 16:50:19) View Log
  • ✅ Mathlib branch lean-pr-testing-2967 has successfully built against this PR. (2023-12-16 18:02:18) View Log
  • ✅ Mathlib branch lean-pr-testing-2967 has successfully built against this PR. (2023-12-16 18:40:40) View Log

@leodemoura leodemoura removed the awaiting-review Waiting for someone to review the PR label Dec 1, 2023
@leodemoura leodemoura enabled auto-merge December 1, 2023 14:38
@nomeata
Copy link
Collaborator

nomeata commented Dec 16, 2023

Auto-merge was enabled, but this PR is rather old and not all required checks exist already.

I’ll merge current master.

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 16, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2967
7c8be42
@nomeata nomeata disabled auto-merge December 16, 2023 16:29
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 16, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2967
f84a4a0
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 16, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 16, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2967
ae5abb1
@nomeata nomeata added this pull request to the merge queue Dec 16, 2023
Merged via the queue into master with commit 8475ec7 Dec 16, 2023
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata approved these changes

@Kha Kha Kha approved these changes

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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
@kim-em @leanprover-community-mathlib4-bot @nomeata @Kha @leodemoura