build(hax): extract almost-upstream libcrux (mod hax v0.3.7)#238
Open
cfm wants to merge 5 commits into
Open
Conversation
48e99fd to
18332dd
Compare
18332dd to
ee56598
Compare
Member
Author
|
Incremental progress:
This seems to resolve the extraction blockers highlighted in #222 (comment) and cryspen/libcrux#1397 (comment). There are still verification blockers I'm looking into. |
Member
Author
|
Tomorrow I'll need to reconcile this with #260. |
c14675b to
c8195f2
Compare
f8bf46f to
f83113e
Compare
3605029 to
e2c9471
Compare
cfm
commented
May 30, 2026
Member
Author
|
The remaining verification failures here are the ones newly surfaced by #271:
|
Member
Author
e2c9471 to
54bf8a6
Compare
A non-exact requirement for wasm-bindgen-test can resolve to a version that will require a higher version of wasm-bindgen than we've specified, which leads to incompatibilities in the unstable wasm-bindgen format.
54bf8a6 to
9c4cbfc
Compare
Member
Author
|
I've finally got this extracting and verifying cleanly after #278, without any of the extra F* models I'd added in e2c9471. My fork |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #258, after a bit of run-around: see #238 (comment).
Following up on #222 (comment) per cryspen/libcrux#1397 (comment).