Skip to content

feat: SIntX as native ABI types #10996

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
Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

feat: SIntX as native ABI types #10996

wants to merge 5 commits into from

Conversation

@hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Oct 28, 2025 •
edited
Loading

This PR adds SIntX types natively to our ABI. This is a slight breaking change for the FFI if you are using the SIntX types.

@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Oct 28, 2025
@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Oct 28, 2025
@hargoniX
Copy link
Contributor Author

hargoniX commented Oct 28, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Oct 28, 2025 •
edited
Loading

Benchmark results for 64b3217 against 8ff5b8e are in! @hargoniX

@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 Oct 28, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 28, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8ff5b8ec2cf755ddaa0b8cebdfb8f9ed65c0364e --onto 3a42ee0c3060e2a8365927d205ead5990366053d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-28 15:08:50)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 28, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8ff5b8ec2cf755ddaa0b8cebdfb8f9ed65c0364e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-28 15:08:52)

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

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-compiler Compiler, runtime, and FFI changes-stage0 Contains stage0 changes, merge manually using rebase 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

@hargoniX @leanprover-radar @leanprover-community-bot @leanprover-bot