I've put together a small example of a problem I'm encountering with ocaml extraction in Coq, and I'm wondering if anybody has any insight.
The gist of it is that I have some modules set up in Coq, but when I go to extract these modules to ocaml I get a
.mli file with a type error.
File "ml/extracted/MyModules.mli", lines 243-244, characters 8-41: 243 | ........type value_byte = MEM'.Byte.value_byte = 244 | | ExtractByte of LP.V.value * nat Error: This variant or record definition does not match that of type MEM'.Byte.value_byte Constructors do not match: ExtractByte of LP'.V.value * Datatypes.nat is not the same as: ExtractByte of LP.V.value * Datatypes.nat The type LP'.V.value is not equal to the type LP.V.value
I believe the interesting part of the Coq file is contained within this snippet:
Module Type Memory (LP: LanguageParams). Import LP. Import V. Module Byte := MakeByte LP. End Memory. Module MakeMemory (LP : LanguageParams) <: Memory LP. Include Memory LP. End MakeMemory. Module Type Lang (LP: LanguageParams). Export LP. (* Memory *) Declare Module MEM : Memory LP. Export MEM. End Lang. Module Make_Lang (LP : LanguageParams) (MEM' : Memory LP) <: Lang LP with Module MEM := MEM'. Include Lang LP with Module MEM := MEM'. End Make_Lang. Module Type InterpreterStack_common (LP : LanguageParams) (MEM : Memory LP). (* Lang seems to be necessary to cause the bug *) Module Language := Make_Lang LP MEM. Import LP.V. End InterpreterStack_common. Module Type InterpreterStack. Declare Module LP : LanguageParams. Declare Module MEM : Memory LP. Include InterpreterStack_common LP MEM. End InterpreterStack. Module Make_InterpreterStack (LP' : LanguageParams) (MEM' : Memory LP') <: InterpreterStack with Module LP := LP' with Module MEM := MEM'. Include InterpreterStack with Module LP := LP' with Module MEM := MEM'. End Make_InterpreterStack.
It seems like the problem might have something to do with
Declare Module and using
with Module in the
Make_InterpreterStack module. It seems like when the ocaml
mli gets extracted it loses the information that the
LP module in
Make_InterpreterStack should be the same as
Does anybody have any idea what's going on? Because this works in Coq, I assume it's an ocaml extraction bug, but are there any workarounds for this issue? Currently we're manually patching the
.mli files with
sed, but these patches are kind of fragile and annoying, and it would be great if we didn't have to do them, or at least better understood what caused the problem in the first place!
.mli breaking while being compiled by OCaml compiler is a long-standing issue, see for example: https://github.com/coq/coq/issues/16169
I'm not familiar with any workarounds besides modifying the extracted
.mli via something like sed. The next generation of extraction will probably target a lower level OCaml interface though, so then the problem likely goes away (see for example this)
Thanks for the response! Glad it's a known issue and I'm not alone, at least. Hopefully the future work you pointed to ends up resolving this so we can have fewer load bearing Perl and sed scripts :sweat_smile:.
Last updated: Oct 04 2023 at 22:01 UTC