coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync

From: Yannick Zakowski <zakowski AT seas.upenn.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync
Date: Thu, 22 Aug 2019 21:18:07 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=zakowski AT seas.upenn.edu; spf=Pass smtp.mailfrom=zakowski AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-wm1-f50.google.com
Ironport-phdr: 9a23:8V5bgRMczJzGzGZUcxkl6mtUPXoX/o7sNwtQ0KIMzox0Ivn5rarrMEGX3/hxlliBBdydt6sezbOK7euxACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagf79+Ngi6oArQu8UZhYZuN7s6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxGvhyhqRxxzY3abo6bO/VxfL/ScMgASmZdRMtcTTBND42+YoYJEuEPPfxYr474p1YWrxSxHw+sBOXuyjBUhX/9wK413P4iEQHB0g0gBNEOsHXJp9jyNaYdS+O1zK7GzDXYbPNW2Czw6JPWfR87uvGAR69wcdLPxkkpEQPJlEufppH4Pz6M0OkGrmaV7+1lVe21im4nrRl8rSSoxsc2jInGmIYVylTe+Spn3Yk1ONu1Q1N4b968CJZcqT2WOo9sTs4hQ2xkojs2xqMFtJKhfCUG1IwrywDFZPCbboSF5w7sW/2MLTtlgX9oeLOyiAu3/ES+1+LwStW43VNOoyVYj9XAqHUA2h3d58ecV/dw+1qu1DKA2g3X7+xJI104mrbFJ5Mn37U+jIAcsV7ZES/zgEj2jLGZdkEj+uWw7uToeLTmppuFO456jwHyL70imsK/DOgkKAQOUG+b+eOz1L3n40L1WqlFjvozkqXBsZDaI9oUprKhDgNLzoou7wyzAjSm3dgCgHULMlFIdAiHgoT1I13OJer3Dfa7g1SiijdrwPXGM6XgA5rXLXjDl7ngfa1+605d0wcz1s5Q6IhPCr0bPfLzQlH+tNreDhMjLQO73vvnBM1n1owCQWKPHrOZMKTKvFCU4eIvOvCAa5MRuDbgMPco/OXujH88mV8FZ6alx5oXaHaiHvRnOUqVe3Tsgs1SWVsN6wE5VanhjECIeT9VfXe7GawmtR8hD4fzPI7FQIGmg/Sz1SS8AYZVZygSGFmPFmjzdISsQPoFc2SPOsJnlHoJWaX3GNxp7g2nqAKvk+kvFeHT4CBN7cuyhugw3PXakFQJzRIxCs2c12+XSGQtwDETSjYtmr1nrEp7jFqPzPoh2qAKJZlo//pMFzwCG9vE1eUjVYLpVwvaOMqRRVCgBNiqHGNpF49j85o1e094Xu6aoFXD0i6tWeJHkrWKANkr9/uZ0SWpYcl6zHnC2e8qiFx0GsY=

I do not know if there's an easy way to avoid the goal ever being out of sync, but if I understand your question correctly as being a case of the displayed goal being out of sync despite the computation being finished, the function "proof-prf" from PG refreshes it. So binding it to a quick shortcut is a convenient palliative to the issue.

Best,
Yannick

On 8/22/19 9:11 PM, Abhishek Anand wrote:

While using proof-general with company-coq, I often get confused because the goal window is showing a stale proof state, even several minutes after the processing has finished. I think there are instances in the proof-general/company-coq code where the proof goal would not be updated ever.

Is there a way to configure the editor system so that the proof goal window is always kept in sync, except of course when Coq is processing the commands, and except a few seconds after the processing is finished.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] proof-general/company-coq: always keeping goal window in sync, Abhishek Anand, 08/22/2019
- Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync, Yannick Zakowski, 08/22/2019
  - Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync, Christian Doczkal, 08/23/2019
    - Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync, Pierre Courtieu, 08/23/2019