The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Thanks! Defining environment variables is indeed the way, but it took me a 
while to get it to work. The caveats (I am working with Coq 8.4):

* You need to put a space around the equal sign or it does not work
* You should put quotes ("") around the the definition of the variable if it 
consists of more than one word

The two solutions you proposed do work. For the first one, I found there is a 
more convenient way to do it by defining OCAMLC and OCAMLOPT instead of CAMLC 
and CAMLOPT (because the definitions of CAMLC, CAMLOPT, CAMLLINK and 
CAMLOPTLINK use OCAMLC and OCAMLOPT):

    OCAMLFIND = ocamlfind
    OCAMLC = "$(OCAMLFIND) ocamlc"
    OCAMLOPT = "$(OCAMLFIND) ocamlopt"
    OCAMLLIBS = "-package yojson"

The second solution, which does not use ocamlfind, also works great:

    OCAMLLIBS = "$(shell ocamlfind query -i-format yojson)"

Now to choose between the two...

Thanks again for your help!

Ali

----- Original Message -----
> From: "Pierre Boutillier" 
> <pierre.boutillier AT pps.univ-paris-diderot.fr>
> To: 
> coq-club AT inria.fr
> Sent: Wednesday, April 1, 2015 11:15:42 AM
> Subject: Re: [Coq-Club] coq_makefile and ocamlfind
> 
> Hi, beware ugly adhoc hacks ...
> > Le 1 avr. 2015 à 10:54, Ali Assaf 
> > <ali.assaf AT inria.fr>
> >  a écrit :
> > 
> > Hello,
> > 
> > I am trying to compile a coq plugin that depends on an external library. 
> > In
> > particular, one of the modules of the plugin depends on the Yojson library
> > (Opam installed, but that is not relevant I think). I can compile the
> > module using ocamlfind, but how can I tell coq_makefile to use ocamlfind?
> You could put in your input file for coq_makefile (called _CoqProject if you
> want coqide or proof general total advantage of it)
> CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread
> CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread
> CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread
> CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread
> and
> OCAMLLIBS?=```-I « . » or whatever you need for your ml file``` -package
> yojson
> 
> OK, we’re not home yet, there is still an issue with ocamldep !
> Then, I think the answer is « support my claim that ocamlfind is a 
> reasonable
> dependency for Coq and therefore I can make coq 8.6 on it » :-)
> >  Is there another portable way to tell coq_makefile to use the library?
> Well maybe just redefine OCAMLLIBS with something like
> OCAMLLIBS = -I src_dirs_in_the_dev $(shell ocamlfind query -i-format yojson)
> 
> > 
> > Thanks,
> > 
> > Ali Assaf
> Pierre B.