coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] PG losing sync with Coq 8.12

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] PG losing sync with Coq 8.12
Date: Thu, 3 Sep 2020 18:33:17 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f180.google.com
Ironport-phdr: 9a23:yhdN3R3gsH/kJjuGsmDT+DRfVm0co7zxezQtwd8ZseMWIvad9pjvdHbS+e9qxAeQG9mCtbQd0bad4/mocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTuwbalvIBmoogjducobjZZ/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+gqJVrgy8qRJ8xIDbb52aOvVlc6PBf94XX3ZNU9xNWyBfBI63cosBD/AGPeZdt4TxqVkOrRy4BQmtB+Pg1DtIiWHo0qAh3OQhFBvJ3A0kH94UrHvUq9D1OKkPWu2yzqnIyjPDb/JV2Tjj7IjHbA4urOqDXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkCvGaH9eRvT/6vi3I5pAFrpDii3togh4nJiI8a1F3I6Tl0zYY3KNC2VEN2bsKoHZtNuy+UK4d7RsIvTWFrtSsk1rELpYO2cDYIxZk72hPSZfyKfYaO7xn+V+iROS91iGx5dL+7nRq/8kitxvfhWsS1zFpGtDdJn9rQunwVyRDe69SLRuZ480u83TuAywXe5+5FLEwoiabWLpAszaAwm5cWv0nOHTL6lUrzgaCKeUgk9Oao5uHpYrr4u5OQKop5hRrgPas0h8OyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07iqzZv4rbJcQfv6K5GhNV3ps65xaxEjur08gUkWMILFJCfxKHgIzpNE/ULP/kCve/hkygkDZtx//YIr3sGovBImTHnbv7frtw61RQxBcywNxD/Z5YF7IMLO7rVk/0rtPYDxs5MwKuw+bgDdVwzoEeWWWJAq+YM6Pdr1uI6fwxLOSXa48VvSzyK/kh5/L0kXA5nlodcbGz3ZQLcHC4AuhmI0KBbHXwhdcBCH4GsRY6TOz3k1KPSiVTZna3X6Ik/D43EoOmDYHZRoCsmrONxim7HocFLlxBX1uLCDLjc5iOE6MHbzvXKct8mBQFU6KgQskvz0f9mhX9zu8tLO3S+y4VsZ/u/Ndw7uzX0xo18HY8W8aa1WCOQmV5k0sHQjY32OZ0pkkrmQTL6rRxn/ENTY8b3PhOSApvbceNndw/MMj7X0f6RvnMTV+nRtu8BjRoF4A+xtYPZwB2HNDw10mfjRrvOKcckvmwPLJx6rjVhiGjKMN0ynKA364k3QF/H5l/cFa+j6s6zDD9Qo7El0LDyfSvfKUYmTfRrSKNlDrW+k5fVwF0XOPOWnVNPkY=

Is anyone else noticing an issue where ProofGeneral sometimes loses
synchronization with Coq 8.12 when stepping through proofs? The proof
state sometimes fails to show up in the *goals* buffer, or it does but
forward steps don't update it. This is not always happening, but isn't
very rare either. However, it is rare enough such that it is difficult
to establish which options and parts of my configuration are at fault by
trial-and-error.

My current configuration is Emacs 26.1, Debian 10.5, PG 4.5-git, Coq
8.12.0 with Ocaml 4.10.0. With company-coq installed from mepl. I
don't know how to determine the company-coq version.

The desyncing can be remedied by a single undo step, but is
none-the-less annoying.

Thanks,
Jonathan

[Coq-Club] PG losing sync with Coq 8.12, jonikelee AT gmail.com, 09/04/2020
- Re: [Coq-Club] PG losing sync with Coq 8.12, Erik Martin-Dorel, 09/04/2020