coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General
Date: Tue, 26 May 2020 17:59:30 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f181.google.com
Ironport-phdr: 9a23:vcK96BF0QvGltnMaKmmjx51GYnF86YWxBRYc798ds5kLTJ7ypcmwAkXT6L1XgUPTWs2DsrQY0reQ6vq6EjxYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmssAndqNcajYRhJ6ot1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIOMuZWrYbzp1UAoxijCweyGOzhxSRFhmPv3aAgz+gtDR3K0Q4mEtkTsHrUttL1NKIKXO6vzanH0y/Db+lI1jzg9oXIdQ0hoeuQXbJxb8XR1FQkGgTdjlWRt4PlJSmV2foXv2eH6OpgSPivi3Imqw5vvzii3cgsiozTiYIUzlDI7zl2wIEwJdChTkNwfNGrHodKuS6AK4t2Xt0tQ3tuuCsi1LALvZC2cTQWxZg6xxPTdeGLfouL7x7/SuqcPCl0iXZqdr+xmxq//katxOLiW8WozVpEoTZIn8XPu30M1RHd5M6KQeZz8Eem3DaAzQHT6udcLEA7lKrbN54hwqMrmZYJrUvDGSr2lUPrh6GVbkUp4vak5/jjb7n8pZKRN5V4hhz/P6kvgMCzHOc1PhUIUmOG4+qzzqfj8lf8QLhSjv05jK3ZsJfCKMQevKG5AgtV3p8i6xa7EjuqydoYkWQEIV5YYh6HgI/pO1bBIPD8E/izmUijkDBux/zeP73hBIvCLmTbnbv/Ybpw71RQxQkzwNxF+p5ZC7AMLOjuVkLyqdDUFho5PBa1w+bjBtV9zIQeWWeXD6+BMaPdr0WI5vgxLOWWeIAVvyv9K+I55/7vk3A5hEQQfaas3ZQNaXC4Gu5qLFmeYXrpmtsBC3sFvhIiTOz2j12PSSJcZ3GrX64l+j47DJ+mApzYS4C2gL2B2T+7EYdMamBHDFCMC3boeJ+eV/cCciLBavNmxxcDTPCKT5IrnUWlsxa/wL56JMLV/DcZvNTtzo4myffUkEQK9DFuFcnV+GaQVX11k35AEyc30bplrAp2zUqZzal1ntRXENVS47VCVQJsZs2U9PBzF92nAlGJRdyOUlvzB4z+WWhsHOJ0+McHZgNGI/vnjh3H2HD0UboclrjOBZhtt6yFjyG3KMF6xHLLkqImigt+G5odBSidnqd6sjPrKcvMmkSdmbytcP1FjiHI/WaHi2GJuRMBCVIiYeD+RXkaI3Dug5Hh/EqbFu2hDL0mNk1KzsvQcqY=

Going back to this after testing.
When the "Suggest Proof Using" flag is set coq indeed displays the
warning about "Proof using" *even outside sections*. Is there a reason
or should I fill a bug report?

Best
Pierre Courtieu

Le dim. 24 mai 2020 à 02:06, Pierre Courtieu
<pierre.courtieu AT gmail.com> a écrit :

>
> Hi,
>
> If proofgeneral gives this message outside of a section this is a bug:
> it is supposed to be triggered by coq warning, which only happens
> inside sections. Please report it here:
> https://github.com/ProofGeneral/PG/issues.
>
> To answer your question: you can either go to the menu: Coq / proof
> using / never". Or do what is described in the CHANGES file and copied
> below.
>
> That said you are right the message is too noisy.
>
> Best
> Pierre
> ----------------8X--------------------------
> PG now supports the "Suggest Proof Using" by inserting
> (automatically or by contextual menu or by a command) the "Proof
> using" annotation suggested by Coq. This suggestion happens at
> "Qed" command. By default PG will only highlight the corresponding
> "Proof" keyword and let the user actively ask for insertion.
>
> You can customize this behaviour by setting the
> coq-accept-proof-using-suggestion to one of these values: 'always,
> 'highlight, 'ask, 'never. This is also settable from Coq menu. See
> documentation of this variable for an explanation of the different
> possible values and some more information.
>
>
> Le jeu. 21 mai 2020 à 09:15, Xuanrui Qi <xuanrui AT nagoya-u.jp> a écrit :
> >
> > Hi Coq-Clubbers,
> >
> > A quick question for Proof General users: the latest versions of PG
> > gives me a warning if I use `Proof` instead of `Proof using`:
> >
> > "Proof using" not set. M-x coq-insert-suggested-dependency or right
> > click to add it. See also ‘coq-accept-proof-using-suggestion
> >
> > Since I don't have any section variables, there's no point in doing
> > `Proof using`. Is there any way to disable this persistent warning,
> > which can be quite annoying?
> >
> > Best,
> > Xuanrui
> >

[Coq-Club] Get rid of "suggest Proof using" warning in new Proof General, Xuanrui Qi, 05/21/2020
- Re: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General, Pierre Courtieu, 05/24/2020
  - Re: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General, Pierre Courtieu, 05/26/2020