Open JasonGross opened 4 years ago
:/. having never used ocaml extraction, I don't know what to look at here
I think this is the Coq bug https://github.com/coq/coq/issues/4875. I guess it's possible that enough Extraction Inline
directives will fix it locally? The other approach (which I guess is sort-of similar to Extraction Inline
) is to try to make the relevant things Notation
s rather than Definition
s
Indeed, adding Extraction Inline coqutil.Map.SortedListString.map
fixes the issue. idk if you want to record this anywhere or anything, or just close this issue, or what
is there a reason not to put that directive right after the definition?
I think you need to Require Import Coq.extraction.Extraction
in order for the directive to be valid. Otherwise, no, no reason to not do it. (Unless for some reason you want it to not be inlined in other languages where not inlining won't result in an error, such as Haskell)
If you're fine with adding Require Import Coq.extraction.Extraction
, then I'd suggest adding the directive right after the definition with a note referencing the Coq bug
This is currently blocking https://github.com/mit-plv/fiat-crypto/pull/686 (cc @jadephilipoom )
If I do
I get:
Running
ocamlc foo.ml
gives: