FStarLang/karamel

Better invocation header

franziskuskiefer opened this issue · 3 comments

franziskuskiefer commented

The invocation header

karamel/lib/Output.ml

Lines 60 to 62 in b76942a

KaRaMeL invocation: %s
F* version: %s
KaRaMeL version: %s

leads to unnecessary noise because it uses absolute paths for the invocation. How about making this relative to stay the same across different machines?

Further, the F* version is <unknown> when a release (non-git) version is used. Instead of trying to get it from git directly, something like fstar.exe --version | grep commit | sed 's/commit=\(.*\)/\1/' should work.

msprotz commented

karamel itself has an option called -header where you can pass something custom -- eurydice doesn't expose this option, would it help?

franziskuskiefer commented

Yeah that's an option as well. I think cleaning up the default would be nice as well, but exposing the -header option through eurydice we could set something less noisy ourselves.