@@ -7,39 +7,48 @@ HAX_TARGETS += +securedrop_protocol_minimal::primitives::x25519::typed
77REPO_ROOT = $(shell git rev-parse --show-toplevel)
88PROOF_DIR = proofs/fstar/extraction
99
10+ .DEFAULT_GOAL := help
11+
1012.PHONY : clean
11- clean :
13+ clean : # # Clean the Cargo and F* caches.
1214 cargo clean
1315 cargo cache -a
1416 rm -rf $(REPO_ROOT ) /.fstar-cache
1517 rm -f $(PROOF_DIR ) /.depend
1618 rm -f $(PROOF_DIR ) /hax.fst.config.json
1719
1820.PHONY : compat
19- compat : compat-fstar
21+ compat : compat-fstar # # Check that hax depedencies are at the right versions.
2022
2123# Keep in sync with ".github/workflows/hax.yml":
2224FSTAR_EXPECTED_VERSION = F* 2025.12.15
2325FSTAR_ACTUAL_VERSION = $(shell fstar.exe --version 2>/dev/null | head -1)
2426.PHONY : compat-fstar
25- compat-fstar :
27+ compat-fstar : # Internal: Check F* version.
2628 @[ " $( FSTAR_ACTUAL_VERSION) " = " $( FSTAR_EXPECTED_VERSION) " ] || \
2729 { echo " Error: expected fstar.exe version '$( FSTAR_EXPECTED_VERSION) ', got '$( FSTAR_ACTUAL_VERSION) '" ; exit 1; }
2830
2931.PHONY : extract
30- extract :
32+ extract : # Internal/CI: Run hax extraction.
3133 cargo hax into -i ' $(HAX_TARGETS)' fstar
3234
3335.PHONY : hax
34- hax : compat extract verify
36+ hax : compat extract verify # # Run hax extraction, then type-check and verify extracted proofs.
3537
3638.PHONY : verify
37- verify :
39+ verify : # Internal/CI: Type-check and verify extracted proofs.
3840 # Type-check (fail fast):
3941 OTHERFLAGS=" --lax" $(MAKE ) -C $(PROOF_DIR )
4042 # Verify:
4143 $(MAKE ) -C $(PROOF_DIR )
4244
4345.PHONY : hax-lib-version
44- hax-lib-version :
45- @cargo pkgid hax-lib 2> /dev/null | sed ' s/.*@//'
46+ hax-lib-version : # Internal: Query Cargo for the hax-lib version.
47+ @cargo pkgid hax-lib 2> /dev/null | sed ' s/.*@//'
48+
49+ .PHONY : help
50+ help : # # Print this message.
51+ @printf " Subcommands:\n\n"
52+ @perl -F' :.*##\s+' -lanE ' $$F[1] and say "\033[36m$$F[0]\033[0m : $$F[1]"' $(MAKEFILE_LIST ) \
53+ | sort \
54+ | column -s ' :' -t
0 commit comments