search

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
395 stars 59 forks source link

Fix Nix build: krml -version is empty, incorrect extracted files header #390

Closed cmovcc closed 1 year ago

cmovcc commented 1 year ago

Currently, when F and KaRaMeL are built using Nix and FSTAR_HOME properly set to the result of the F derivation:

  1. krml -version provides us with an empty string;
  2. the header of extracted files contains the following line: F* version: <unknown>;
  3. the header of extracted files contains the following line: KaRaMeL version: <unknown>.

About 1. and 2.: the Nix build environment source of KaRaMeL is just the content of the specified revision of the git repository, not the git repository itself. Thus, make lib/Version.ml does not work properly, as git rev-parse HEAD fails. Fixed by adding the GIT_REV environment variable during a Nix build, and using it if git rev-parse HEAD fails.

About 3.: in lib/Driver.ml, if $FSTAR_HOME does not point to a git repository (e.g. when F is also built using Nix), fstar_rev is not set. This could be fixed by retrieving the F version using something like fstar.exe --version | grep commit | cut -d "=" -f 2 instead. What do you think about this? I can add a corresponding commit.

HACL does not have this issue, as the header is replaced by the HACL license and the versions of the different used binaries are added to dist/ manually into INFO.txt file , see .nix/hacl.nix file within HACL* repository.