The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Thank you for your answers.

However, I notice that, if the file F.v of L1 is in a subdirectory, say 
D, then L1.F does not work. Instead we need to use L1.D.F.

Best regards,

Frédéric.

Le 04/02/2015 18:15, Guillaume Melquiond a écrit :
> On 04/02/2015 18:04, Pierre Courtieu wrote:
> > Hi Frédéric, here is what I understand, people will correct me if I 
> > am wrong.
> >
> > This is a complex question since you may not be the author of the
> > libraries. Ideally each library should be compiled with option -R
>
> If the libraries already work (when installed separately in 
> user-contrib), they presumably were compiled using -R. Coq would be 
> unable to load them otherwise, if I am not mistaken.
>
> > (or the new -Q option, but it is broken currently in 8.5beta).
>
> Oh?
>
> > Then compiling L1 should give for example:
> >
> > coqc -R L1 L1 L1/F.v
> >
> > same for L2:
> >
> > coqc -R L2 L2 L2/F.v
> >
> > and the two "make install" should do the equivalent of:
> >
> > cp L1/F.vo lib/coq/user-contrib/L1/
> > cp -r L2/F.vo lib/coq/user-contrib/L2/
> >
> > Then "L1.F" and "L2.F" should work OK.
> >
> > Of course the libraries need to be adapted to these compilation
> > options, they should "Require L1.F" themselves for example.
>
> Only if they are being compiled using -Q. If they are compiled using 
> -R, they do not need to (unless there is an ambiguity inside a library 
> itself).
>
> Best regards,
>
> Guillaume