coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Chris Dams <chris.dams.nl AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Can useless warnings be switched off?
- Date: Tue, 2 Aug 2016 13:14:03 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f48.google.com
- Ironport-phdr: 9a23:ZhAZAheI4dcHzWMkajRdC6vzlGMj4u6mDksu8pMizoh2WeGdxc6+Zh7h7PlgxGXEQZ/co6odzbGH6+a/CSdZuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JXvkb/isMSKKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR/QMBzM/dmsx+cfDtB/ZTALJ6GFKAUsMlR8dKAjf7Qqycp70qWOuvepn2TLcMcTzVvYyXRyt6q5qTFnjjyJRZG1xy33elsEl1PETmxmmvREqm4M=
Thanks Jason! It is good to know that it will be possible to remove these warnings in the future.
2016-08-01 19:42 GMT+02:00 Jason Gross <jagro AT google.com>:
This feature will be available in Coq 8.6, with the -w flag. (as, e.g., -w "-deprecated-appcontext -notation-overridden") I don't believe there are plans to backport it to 8.5.On Mon, Aug 1, 2016 at 3:03 AM Chris Dams <chris.dams.nl AT gmail.com> wrote:Dear all,I recently upgraded to coq 8.5pl1. I compiled the one that comes from the arch-linux user repository (https://aur.archlinux.org/packages/coq/). I noticed that when running coq it prints quite a few warnings that look like
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked.This happens both when compiling using coqc and it will also prints these warnings to console when stepping through source using coqide. E.g., when stepping over "Require Import NArith" in coqide, it will print four of these warning message. These warnings are not helpful to me so I am wondering if they can be switched off or be disabled in some way. They obscure more useful output that might be present when I 'make' a coq project.Kind regards,Chris
- [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
- 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?, Pierre-Marie Pédrot, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/02/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Jason Gross, 08/01/2016
Archive powered by MHonArc 2.6.18.