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. Makefile improvement #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.