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: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync
Date: Fri, 23 Aug 2019 12:19:14 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Autocrypt: addr=christian.doczkal AT ens-lyon.fr; prefer-encrypt=mutual; keydata= mQINBFIuNbYBEADAiZlQsnkRrXHOkaZ2mZIVNxzcBha3+HhZ8IhtxF4t5QXRNWFLtdwBuE8u D0GMB/Lacm/LujwcI756cPM/7PhrUFAyn1IrYHYsK4/O5gBEgbSBRjD0X8mJ0V3oIm/PtjMC YiXBJwzOMNXOeWp+HcyCR0eh2sQD94gbF9SUOKDoamNB3DbLEHKjYPJ9O3zQw/Xai624OXB0 Wk5yIW77I1mGWhwbWxeHOJ/NmhHEU38YfbxXSzCLeMv98bNTej4oA+cPtMZ94AZOSy/oroMh rsr6wA9PL7NS+B1kRbgv6a5KL9latAI7zPeXcVsYw076rL850PLez/SXDuIr9mud4v8Zvcp9 65vTK4lTAD4C4vneNRGt4iwCOIgGsAN6BgqEgr7EwLX8dAX57OXPKZj0/0TdCbu+qsoSrQ3u +Ul6k374jFeIndqg/e9NiJbHjYAuug3cZZ6mH24SXWtTd4hGWi6f26tQQcRyGiduZkw5Wn26 g0UVgps7o2zHwlp9LJVjL3pCw7a9tKOfZaH+h7dV5JsA/Oq+7F3PhTbyNagi4A9igw+0qU+n Ws/nZDVMRiUv+1HY4PG8q6iEGSfHHjwW8InYS+Ah3stTddJ0sLc+0AGutx8ueTE2Ks14c4c8 aNW5y9bNFI/6/UQmOOwGmBeYC/kjZhjhsC3dTJ9uX4pXlMhpLQARAQABtDFDaHJpc3RpYW4g RG9jemthbCA8Y2hyaXN0aWFuLmRvY3prYWxAZW5zLWx5b24uZnI+iQJUBBMBCAA+AhsDBQsJ CAcCBhUKCQgLAgQWAgMBAh4BAheAFiEE6jiiZvHNwp19meaCj7B3SJxkuY0FAluX/3QFCQtK /T4ACgkQj7B3SJxkuY24UQ/+L9DFIx/Z8+SGhA6h8+JvfM/N3l2IT9fsDfPTLVLoyYk6j0CR T/DTGOzmh9fCCcYJbxeNeR63vwo13B0nCKfJE1sudpJCqM/6xMMeq4IcQo4Sump24iP3V9Dg iicyXowcaMTAonwadhRyGoykdXWkaHTLLbFtuF10oO0geoyM0gy/quVmONvDZVDX6WRk0DHN vx/fRCnr3pHFm1TDp5XatQbxwDH7MqX7zS5P9onkro3lqIJiekXyPeeUVZn1OWI4Ai8RgUTZ w5RNgoj/iPtCdu0yVrL5EwEikSRrrPwqp/VLNw+hslgrdI9rtv6bf2x4AshjBoi/S4MUt3s5 3hTiLhkxMeD6iPFv70SKYdYqkhN1Y7owb0L4u9/gdODvCOofo97mv0UCTvY0hpDpiyYDM/tr 6fwSVGObSYLmjzVjrwWB1gQaDsn+ghSwwGutGEHSPdwHIy4e5qCYDaUPRWSdfxfGx3ZOO9f4 s28ufT9tJbvZK2/DPpxhGEcVQE+vMoopWJma8NoZW4IbQzqg/8vFd4w9MsMDqDsbhgOlKtpv 3GEixafUMF5wJDHEpYQaWKWf1lLg7u8FIefCaJC9E/0Wl7XhmhYx0wPQ71fOhEGmf7P1DUdy OTrZtS+O3RcM54zQjlK9lweIOPYpwW8BvgNI4+E/ev1Fv31duTniNbxSeku5Ag0EUi41tgEQ ALKCkrZVjm7Jr6wZkeYMPs+OCtICbILfcRODKsM/JxEdcxbr99UA5GGi94OXGxvkQf5yLQxG hCzrLJVbrpBvl+stg72/8DrYGCCSl72gxLTTInfFxEvH3xGpBP/oMXdGjk+jxWA48opzsaar Bd9PxvFNZoWjB9jdgzBPpNMa/ykw4ATVC2fzC5xuo4fwUsl1Wu8DFLbMVwSHGXCqmV6QYUXf 0i3EKnNkKRH3a3rd7JsrC0/6lBL8sLoT54K3J6NGii6dzalhOycsSI4R8czclof3RIy5Mh/Z /rqv4d0OgY2b7QOYnGrITVtyC5UqzGMZx0dnQr5Bm7YOHaCML/LjMoYj2ovFh2zjaU6I/smx 3stVkMRpmqB7/cYPktkpGV8K9S0l6Cgiepn9pymU0/NCBFKXrPuoorKz0+X6j6YsSy7PJ1KC EIh2nSPdhB7/4ezw3DB/COfTE8EY+xbPpTF4DfI+4ARrbP953C4Z2JC7xHUGqH+D/TQ2qYiT mfHdZTrzvWYHCERApZKq1Erdpl7mHfFnwyoDB8OqS9QWfwz3Ql8TeoFPP5LdS4PHkEqog2vH j6njJnLDLUcU5OGKVrGiu8qdMGyIJNeyY6eGcl+4RR+iNJaCVSwLDB+otbxCg2cemGAfvTI4 GGpwxXuf8/r8JL9l9Jgr/zw2WroiZwOJDhPpABEBAAGJAjwEGAECACYCGwwWIQTqOKJm8c3C nX2Z5oKPsHdInGS5jQUCW5f/dAUJC0r9PgAKCRCPsHdInGS5jbhiEACnBN29HGmlJLqLyh3H /lbZDKXWQg1KzlTiMcL/EUwrUhYLK0Lm9tsHNggQfqtnAJTW+0g/Q9wGsLDAyTaHtgPUym8j FWtPv45YfHElSwdUSzy80ZKxcw5WsD4ofpvKite4j7ehzegJF0nJ1JlPFGwRDaRoVig+cQDq jtK3fCOflsTgIcqt4gB/44x79zWSfdqag64RLMmthVWq+eRCQzFNaOH6nSUcpmXe/OTMRYx3 weqsmtLAm4kcHRdGR6bmlmOcng5gleT2TImwiW3KbRzDGFIzj/gcx6XvsonEdKGv/VgUWYvq xSnktd9/YWVUQaj+XN+C7S2p8VThkwzTxbG30jU8rgjCgci3dObipm5wkvXdI2Ojrk5wz2yD tQS1DHjE4GeC0fP2XinC3IeH8uXl1ggCxH7emzETZgM+hiM1Ijt4M80nhjbMB989q8CheOhl T/6R0G7BWKAoFo/nx+KqzWNoRX2tWPaNrbxiPdTwe3l6imJ0LYqMoNGG52+WCE98JsihXE5x 62m2vEFztbJ/CyyyIAgcdQdnVeh9N2Bhx99LdKWmxb1DLGi4nsBdtlOr4nGHbO36PbBvPp0U hMGMe8UQs41NBGp2u4avbPdQYcMBdURHHgcVPMUTQIN7D1zGPNKw/31f11BY4o3BdbLXAggJ 3dGbm2ZAnj3OQRK3Sg==
Ironport-phdr: 9a23:Or8VKxGPOMfZi/WGur3Ja51GYnF86YWxBRYc798ds5kLTJ7zos2wAkXT6L1XgUPTWs2DsrQY0rCQ6vywEjZbqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAncucobjYR8Jqs/1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrgyvpxJ/3oDaY4+bO/RxcazfYdwXXmVBUtpLWiJGHo+xYYkCAuwcNuhYtYn9oF4OoAOgCAmsHuPvyyRIhmP33aIg1eQqDA/I3As8ENMPs3TbttH1P7oVXO+pzKnI1zTDb+hK2Tf88ofIdAotruyLXb1scMvRylMgFwfeg1qOr4zlJCqZ1uANsmic6epsT+yvi3Q+pgx3vzOhyMAsiozTiYIUzFDJ7Tl2wIEvJd2+VkF7ZdqkHIFOuC6HKot6WswiQ2B0uCY6170JooS3czQNyJQiwRPUdv+Jc5CQ7x7+W+udPS10iXBndb6lmhq/8EqtxvfiWsWqzlpGtilInsfWunwT1xHf99KLRuVg8kqiwzqDyh7f5+JCLEspj6TUMYQhzaQ1lpcLsUTMACv2mELuga+SbEor4fOn5Pr9brr4oJ+cLJZ4igX+M6QpnMyzG+o4MhIWU2ia/+SzyqHj8FXkTLhFkvE6iKvUvZLAKcgGp6O0ARVZ3pg95xqhFzum1c4XnXgDLFJLYhKHiI3pNknSL/D4F/e/gk+skCtqx//cOL3tGIjCLn/fn7bgfrZy8UpcxREtwtBZ/JJYE7UBIfL0Wk/3rtDYAAU5PxSuw+n7ENV9yp8eWWWXD6CFN6PSqEaE6f4rI+mRf4AYoy39Kvgg5/72l3A1g14dfa+z3ZsWcn+0BPpmI1/KKUbr19wGCCIBuhc0ZO3sklyLFzBJNFioWKdpzTEhCZm6DI7FDqyqi66C1SPzSpZWfGFdFlGFFzHkcI6WWP4IQC+UOYplgzsCE7a7HdxynSqyvRP3nuI0ZtHf/TcV4Mq6hYpFotbLnBR3zgRaSsGU0mWDVWZxxzhaSjktmaRupko7xE3RiPEk0cwdLsRa4rZyail/LYTVlrcoBtbpHwbQedHPRkz0Goz7UwF0dco4xpo1W2g4G9imiUmSjS6jCbUY0bGNH9kw46XamXbrdZ5w
Openpgp: preference=signencrypt

I have been having the same issue. By default, "proof-prf" is already bound
to C-x C-p, and pressing this combination whenever the goal doesn't feel
quite right has become something of an automatism for me.

I never really investigated the issue, but there is an open issue [1] (that I
can indeed reproduce) that mentions the *goals* buffer not being updated when
using "proof-goto-point" when the point is right behind a comment.

If the problem occurs in other situations as well, maybe you should file a
separate bug there.

Best,
Christian

1. https://github.com/ProofGeneral/PG/issues/204

On 8/22/19 9:18 PM, Yannick Zakowski wrote:
> 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/

Attachment: signature.asc
Description: OpenPGP digital signature

[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