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

Better invocation header #447

Closed franziskuskiefer closed 3 months ago

franziskuskiefer commented 3 months ago

The invocation header

https://github.com/FStarLang/karamel/blob/b76942a3fa36c016a7fb1da96ce924c71964488a/lib/Output.ml#L60-L62

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 3 months ago

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

franziskuskiefer commented 3 months ago

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.

msprotz commented 3 months ago

https://github.com/AeneasVerif/eurydice/pull/43 should fix this