coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can useless warnings be switched off?

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Can useless warnings be switched off?
Date: Wed, 3 Aug 2016 11:37:05 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:gVMpGx2mWvmi7tD8smDT+DRfVm0co7zxezQtwd8ZsegUL/ad9pjvdHbS+e9qxAeQG96Ks7Qb2qGP6PqocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+kQsiN3o/ujLr60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7vkm7otLVbjwV6U+V71RSjo8YE4v48i+jxDHQ0Ot+30TGjEUjxxHKw3d7VThQYy3tTH14LkukBKGNNH7GOhnEQ+p6L1mHUfl

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

[Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/01/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Jason Gross, 08/01/2016
  - Re: [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/02/2016
    - Re: [Coq-Club] Can useless warnings be switched off?, Pierre-Marie Pédrot, 08/03/2016
      - Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/03/2016
        
        Re: [Coq-Club] Can useless warnings be switched off?, Jeehoon Kang, 08/03/2016
        
        Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/03/2016
        
        RE: [Coq-Club] Can useless warnings be switched off?, Soegtrop, Michael, 08/03/2016
        
        Re: [Coq-Club] Can useless warnings be switched off?, Matej Kosik, 08/03/2016
        
        Re: [Coq-Club] Can useless warnings be switched off?, Frédéric Besson, 08/03/2016
        
        Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/04/2016
        Re: [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/18/2016