noextract only impacts KreMLin function bodies

[tchajed]

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 FStarLang/karamel#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.

[ad-l]

noextract is used in 54 places in Hacl*.

[tchajed]

Do you expect that it would break Hacl* if those uses were not extracted to OCaml?

[ad-l]

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.

[A-Manning]

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.

[msprotz]

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

[msprotz]

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*