Extraction code is no longer compiled in Coq8.4pl4

[jeehoonkang]

• This is rather a "question" than an "issue"..
• Background: to compile our simplberry based on the new vellvm-legacy, we had to restore extraction_core.v and extraction_dom.v, which was removed in vellvm-legacy.
• Problem: Compilation fails with:

File "/opt/devel/jeehoon.kang/Works/simplberry/lib/vellvm/src/Extraction/extraction_core.v", line 303, characters 0-38:
Error: The informative inductive type prod has a Prop instance.
This happens when a sort-polymorphic singleton inductive type
has logical parameters, such as (I,I) : (True * True) : Prop.
The Ocaml extraction cannot handle this situation yet.
Instead, use a sort-monomorphic type such as (True /\ True)
or extract to Haskell.

• AFAIK this check is introduced to avoid extracting invalid OCaml code, but I do not know what is the essence of the problem in our case.
• Do you have any idea? Or would you please share your experience that migration of extractor was not easy, in other respects?

Thank you, Jeehoon

[jeehoonkang]

To share this issue with my boss, I added @gilhur to vellvm users group :-)

[dgarbuzov]

I ran into this problem earlier. It's quite annoying that Coq only gives a line number for the extraction command that failed rather than the location of the actual error.

This used to also happen with, for example, Recursive Extraction interpreter.interInsn but I partially fixed it in 813c6cd78cfae520e62780b54fed89fbf9692138. My approach was to manually proceed down the call tree, recursively extracting each definition until I reached the offending one. It turned out there was some confusion between universes in some mutual induction principles.

Unfortunately, although calling Recursive Extraction <ident> for each definition in interpreter.v now succeeds. Recursive Extraction Library as you pointed out, still fails. I still have no idea why this is, and am not sure how to track down the problem. As a work around, it might be possible to simply extract the particular definitions you need rather than using Recursive Exctraction Library.

[dgarbuzov]

I experimented a bit more with this last night: it was simple to fix extraction of analysis.v (see: 842cddb398b77e1f0e376628785b0789d8b4d73c) but it appears that the equations plugin introduces the same error in Values, so any module depending on it (e.g. interpreter) will not extract with Extraction Library.

Like I mentioned above, Recursive Extraction and Separate Extraction appear to be slightly more selective in what actually gets extracted, and can be used for now. To completely fix this, we would have to remove the Equations plugin #4.