The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

That’s the “sore” point, I basically make a list of all the modules in A 
(extracted using Extraction Library, so they have everything) and remove all 
that from B’s extracted files.

-- Matthieu

> Le 31 oct. 2019 à 20:17, Clément Pit-Claudel 
> <cpitclaudel AT gmail.com>
>  a écrit :
> 
>> On 2019-10-31 13:32, Matthieu Sozeau wrote:
>> We do something like this in the MetaCoq project: using `Separate 
>> Extraction` or `Extraction Library` to extract module B, knowing that I 
>> have an mlpack implementing A on which B depends, and then calling `ocamlc 
>> -open Myplugin.A -I …/user-contrib/myplugin B.ml` to compile the « 
>> extension » code. With `Separate Extraction`, it’s a matter of removing 
>> all the generated code for `A` and its dependencies that is produced by 
>> extraction. With `Extraction Library` the user has to be careful that he 
>> extracts all the libraries he needs but doesn’t need . No unsafe type 
>> casts are inserted this way.
> 
> Hi Matthieu,
> 
> Thanks, that's very interesting feedback.
> How do you handle dependencies on part of the standard library of Coq? Do 
> you make sure to include it all in the mlpack for A?  More generally, how 
> do you distinguish between modules that you need to keep in B and modules 
> that are already in A?
> 
> Clément.