Skip to content

Add support for native_compute on ARM64 processors. - #22447

Open
silene wants to merge 5 commits into
rocq-prover:masterfrom
silene:arm64-native
Open

Add support for native_compute on ARM64 processors.#22447
silene wants to merge 5 commits into
rocq-prover:masterfrom
silene:arm64-native

Conversation

@silene

@silene silene commented Sep 8, 2026

Copy link
Copy Markdown
Contributor
  • Added changelog.

@silene silene added the kind: feature New user-facing feature request or implementation. label Sep 8, 2026
@silene
silene requested review from a team as code owners September 8, 2026 14:54
@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 8, 2026
@SkySkimmer
SkySkimmer requested a review from a team as a code owner September 8, 2026 14:58
@silene

silene commented Sep 8, 2026

Copy link
Copy Markdown
Contributor Author

Hmm... "Dune could not be found, please ensure you have a working OCaml enviroment" (with a typo, btw).

silene
silene commented Sep 8, 2026
View reviewed changes
Comment thread .github/workflows/ci-github.yml Outdated
@SkySkimmer @silene
Update .github/workflows/ci-github.yml
d2dcd71 
Co-authored-by: Guillaume Melquiond <guillaume.melquiond@gmail.com>
@SkySkimmer

SkySkimmer commented Sep 8, 2026

Copy link
Copy Markdown
Contributor 
Undefined symbols for architecture arm64:
  "_rocq_curry2_1", referenced from:
      _rocq_curry2_1_addr in libcoqrun_stubs.a[2](rocq_values.o)
  "caml_curry2_1", referenced from:
      rocq_curry2_1 in libcoqrun_stubs.a[2](rocq_values.o)

SkySkimmer
SkySkimmer reviewed Sep 8, 2026
View reviewed changes
Comment thread .github/workflows/ci-github.yml
SkySkimmer and others added 2 commits September 8, 2026 18:07
@SkySkimmer
Apply batched suggestions from code review
bf13346 
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
@silene
Try randomly adding underscores.
76374d0
@silene

silene commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

@amahboubi This is ready for testing. Whichever system you use to install it, make sure it runs ./configure -native-compiler yes before building Rocq.

@SkySkimmer SkySkimmer assigned SkySkimmer and unassigned SkySkimmer Sep 9, 2026
@SkySkimmer SkySkimmer added this to the 9.4+rc1 milestone Sep 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@SkySkimmer SkySkimmer

Labels

kind: feature New user-facing feature request or implementation. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: native compiler

Projects

None yet

Milestone

9.4+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@silene @SkySkimmer