Makefile.generic discovers multiple versions of hax-lib

[parrot7483]

Summary

The current logic in Makefile.generic for discovering F* libraries (specifically hax-lib) is problematic. It searches for F* modules everywhere, which results in multiple versions of hax-lib being found (e.g., in fstar.exe calls). This causes confusion and can load unintended versions of dependencies.

Details

• The Makefile's search logic finds multiple instances of hax-lib, especially in larger cargo workspaces where more than one version might exist.
• On a local machine Makefile.generic may find the hax versions of the workspace, of a sub crate, the hax fork used by charon and of entirely different projects.
• A workaround was attempted by making searching optional and manually setting HAX_HOME, but this is not a clean solution. https://github.com/cryspen/libcrux/pull/1101
• The ideal solution would be for the Makefile to reliably select the correct hax-lib tied to the target being compiled.

Why this is problematic

Whenever a new hax feature is needed before release, the whole libcrux workspace must update to a new git commit. Subprojects can't use different versions. This also does not solve the problem of a local development environment which might have many versions of hax installed.

Related Discussion

• Relevant PR comment

[parrot7483]

Instead of some shell script shenanigans it maybe is a good idea to have cargo hax have a command that point to its own hax-lib.

Something like cargo hax --hax-lib-path that returns the path to the hax-lib of that hax invocation.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.