Fix Nix build header: F* and krml versions empty

[cmovcc]

Use fstar.exe --version instead of git rev-parse HEAD in $FSTAR_HOME directory. Indeed, when building the F*+KaRaMeL toolchain in a Nix environment, $FSTAR_HOME does not point to a git repository. I foresee a few discussions.

• This is perhaps a convoluted way to retrieve the git revision (List.nth (...) 5), I was unsure about the portability of grep usage, for example when using MacOS. As a consequence, we rely on the current output pattern of fstar.exe --version, should this be documented somewhere ? Does this choice seem reasonable?
• Additionally, this adds a git_rev_length variable to control the length of F*/KaRaMeL revisions that are present in the KaRaMeL default header and raise it from 8 to 10. Perhaps this could/should be raised further, e.g. to 40, to be future-proof without any need to bump it?
• Do you think any of this should be wrapped within an exception handler?

[msprotz]

Additionally, this adds a git_rev_length variable to control the length of F*/KaRaMeL revisions that are present in the KaRaMeL default header and raise it from 8 to 10. Perhaps this could/should be raised further, e.g. to 40, to be future-proof without any need to bump it?

What problem are you trying to solve? Have you seen hash collisions?

This is perhaps a convoluted way to retrieve the git revision (List.nth (...) 5), I was unsure about the portability of grep usage, for example when using MacOS. As a consequence, we rely on the current output pattern of fstar.exe --version, should this be documented somewhere ? Does this choice seem reasonable?

@mtzguido @tahina-pro is this output expected to be stable?

Do you think any of this should be wrapped within an exception handler?

unless you can show me a situation where an exception will be raised, no

[cmovcc]

What problem are you trying to solve? Have you seen hash collisions?

No, I haven't, and it remains very unlikely, even the Linux kernel keeps revision of length 12 without any ambiguity issue, afaik. I think that the header purpose is to provide one with information about the toolchain that has been used to produce the corresponding file, possibly long after the extraction. As I don't think the header would be less readable/practical with full git revisions, why shouldn't it be changed to use full git revisions? By the way, krml -version already yields the full git revision.

@mtzguido @tahina-pro is this output expected to be stable?

Do you think any of this should be wrapped within an exception handler?

unless you can show me a situation where an exception will be raised, no

I guess it depends on the previous question (thanks for cc-ing).

[mtzguido]

This is perhaps a convoluted way to retrieve the git revision (List.nth (...) 5), I was unsure about the portability of grep usage, for example when using MacOS. As a consequence, we rely on the current output pattern of fstar.exe --version, should this be documented somewhere ? Does this choice seem reasonable?

@mtzguido @tahina-pro is this output expected to be stable?

While I don't foresee any changes, I wouldn't want to close the door on adding/removing/reordering some lines in it. Could this code just try to read each line and find the one that starts with commit=?

[msprotz]

Good suggestion, Guido -- thanks.

Regarding the commit hash: for the sake of keeping things readable, let's hardcode 12 as the length (what is good for Linux is good for us). Do not use a global variable, just leave 12 in the code, and let's not bikeshed on this -- this is entirely opinion-driven, unrelated to the goal of this PR, and does not solve any problem encountered in the wild.

[msprotz]

@cmovcc: KString.starts_with is the helper you want here, something like

KList.filter_some (fun l -> if KString.starts_with l "commit=" then Some (String.sub ... l ...) else None) lines (sketch)

[cmovcc]

Thanks for the hint!