The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi, 

The output of coq -config should output all the relevant information.

Best,
—
Frédéric

> On 03 Aug 2016, at 11:46, Jeehoon Kang 
> <jeehoon.kang AT sf.snu.ac.kr>
>  wrote:
> 
> Dear Ralf,
> 
> I also wonder if how I can check which of camlp4 or camlp5 is used in my 
> Coq binary..  But if you installed Coq via opam or from tarball, it is 
> highly likely that your Coq uses camlp5.  It is the default option.
> 
> Note that you can `opam install coq.8.5.2~camlp4` to obtain the 
> camlp4-based version of Coq.
> 
> Jeehoon
> 
> 
> 2016-08-03 18:37 GMT+09:00 Ralf Jung 
> <jung AT mpi-sws.org>:
> Hi,
> 
> > Those warnings are not produced by Coq, but rather by CAMLP4/5, and
> > therefore the warning mechanism is useless here.
> >
> > Warnings cannot be turned off in CAMLP4 because the relevant API has
> > been missing for ages, whereas it is possible in CAMLP5 (if they appear
> > in Coq otherwise it's a bug, and it may well be one in your example). In
> > any case, I advise you to switch to CAMLP5 if you didn't do so already.
> 
> It seems I have both CAMLP4 and CAMLP5 installed. How can I tell which
> one Coq is using? "coqc --version" only shows the ocaml version:
> 
> > $ coqc --version
> > The Coq Proof Assistant, version 8.5pl2 (July 2016)
> > compiled on Jul 21 2016 11:30:45 with OCaml 4.02.3
> 
> Kind regards,
> Ralf
> 
> 
> 
> -- 
> Jeehoon Kang (Ph.D. student)
> Software Foundations Laboratory
> Seoul National University