Opam package fails to build

[Johanmyst]

Hi!

I'm posting this issue regarding this Slack discussion. In its current form, the Opam package fails to build under any configuration. The normal build procedure through the ./everest karamel make script works; the environment appears not to be the issue.

Issue #300 already mentions the non-existence of any karamel Opam package (though kremlin does exist). A new package can be manually created and given a remote source using opam pin add git@github.com:FStarLang/karamel.git or opam pin add karamel git@github.com:FStarLang/karamel.git --dev-repo. However, building this package fails.

Failure if fstar installed with --dev-repo

The karamel package depends on the fstar package. If that package is installed using opam pin add fstar --dev-repo, the build fails because it cannot find this Makefile. The path that the Opam build tries to find is ~/.opam/<switch_name>/share/karamel/misc/Makefile.basic.

However, the main Makefile only creates/installs this directory in the install target. Before the install, the Makefile.basic can be found in the karamel package directory under ~/.opam/<switch_name>/.opam-switch/.... When building through Opam, the Makefile should use these directories rather than the installation target.

Failure if fstar installed without --dev-repo

If the fstar package is installed through Opam without the --dev-repo flag (this is advised against by the installation/build guide for F* though), the build fails because the installed F* version does not contain the no_auto_projectors attribute.

Kindly,

Johannes

[msprotz]

@R1kM I seem to remember you had thoughts on how to fix this?

[R1kM]

Yes, I added a karamel package to opam, which should therefore fix this issue. Please feel free to repoen if this is not the case.