Closed tchajed closed 7 years ago
noextract
is used in 54 places in Hacl*.
Do you expect that it would break Hacl* if those uses were not extracted to OCaml?
I would expect so, considering the fact that the ML backend erases very little. This is easy enough to try - I think the change to noextract
you propose is easy to implement.
noextract
would be very helpful as a module qualifier, since it's burdensome to remember which files in a project should be realised and which should be extracted when passing them on a command line.
Beware: if you drop the declaration without even passing it to kremlin, then kremlin's internal checker will be confused and may have less type information at call-site, which may be break some invariants later on.
This is why the declaration is kept. Example:
noextract
let f x: option int = None
if you don't pass the type signature to kremlin, then kremlin's checker won't have enough information for:
match f x with
| None -> ...
and won't generate the proper monomorphization of option int
.
Perhaps noextract
should only be used for pure functions in conjunction with inline_for_extraction
Closing after I reverted @mtzguido 's change... noextract may be poorly named but we still need the stubs to type-check the code at the kremlin level in Low*
I wanted to create an issue to track discussion on the behavior of
noextract
. Currently this qualifier only impacts KreMLin, and even there a signature is still generated with a body that throws an error.Would it make sense to instead skip the entire extraction pipeline for this attribute, including F# and OCaml extraction? I ran into this in https://github.com/FStarLang/kremlin/issues/54 and as mentioned there Guido was able to change the behavior of extraction to bail out on
noextract
much earlier with a simple change.At this point changing the behavior is not too costly since this qualifier has very little usage so far.