build: containerize hax for local use - #326
Open
cfm wants to merge 4 commits into
Open
Conversation
- hax: "cargo pkgid" via "make hax-lib-version" - F*: "versions.env" (after "lint-tools/versions.env")
There was a problem hiding this comment.
Pull request overview
This PR aims to make local hax extraction more reliable by centralizing tool version declarations and optionally running extraction inside a version-tagged hax container, reducing the likelihood of subtle cargo-hax/hax-lib incompatibilities.
Changes:
- Introduces
versions.envto define the F* version in one place. - Updates
protocol-minimal/Makefileto read versions fromversions.envand optionally runmake extractin ahax:$HAX_VERSIONcontainer whenCONTAINERis set. - Updates
.github/workflows/hax.ymlto resolve F*/hax versions dynamically and feed them intohax-actions.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
securedrop-protocol/protocol-minimal/versions.env |
Adds a single source of truth for the F* version used by Make and CI. |
securedrop-protocol/protocol-minimal/Makefile |
Adds containerized extraction support and version compatibility checks. |
.github/workflows/hax.yml |
Makes CI derive tool versions from repo state instead of hardcoding them in the workflow. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
This no longer requires a local Dockerfile to layer Make on top of cryspen/hax's Dockerfile, but I'll leave that commit in history in case it's useful in the future.
cfm
force-pushed
the
284-containerize-hax
branch
from
July 31, 2026 00:35
ca45688 to
82ce958
Compare
cfm
marked this pull request as ready for review
July 31, 2026 00:35
1 task
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.
Closes #284 by:
cargo-haxavailable must match the installed version ofhax-lib, and F* is defined once in a newversions.env; andmake extractrun in ahaxcontainer when prefixed withCONTIANER=1. This is optional: for example, CI is unchanged and continues to use thecargo-haxandfstarbinaries installed via GitHub Actions.As we found in #238 (comment), it's possible to run a version of
cargo-haxthat's just subtly incompatible with the installedhax-liband therefore fails in mysterious and confounding ways. This should make that state a little harder to get into by accident.