The Coq mailing list

[Erik Martin-Dorel <e.mdorel AT gmail.com>]

Hi,

Maybe this is related: it happens I had opened a PR to extend the PG integration tests (CI) with Coq 8.12 and it didn't seem to work as expected:

https://github.com/ProofGeneral/PG/actions/runs/153948280

(see https://github.com/ProofGeneral/PG/pull/503#issuecomment-647769626 for some details on exploring the CI logs / re-running the tests locally)

Unfortunately I didn't have the time to dive into this issue, and I was hoping this was only a spurious failure…

but your coq-club mail tends to show that the issue is more pervasive, maybe there's an issue related to a change on Coq's side(?)

(I'm a bit swamped these days but I Cc Pierre and Clément in case they'd have more clues on that issue…)

> I don't know how to determine the company-coq version.

you should be able to get the (date) version of company-coq by evaluating this glob _expression_ in a terminal:

$ echo ~/.emacs.d/elpa/company-coq-*

BTW, note that PG can also be obtained from MELPA (not melpa stable)

Best regards,

Erik

Le ven. 4 sept. 2020 à 00:33, jonikelee AT gmail.com <jonikelee AT gmail.com> a écrit :

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

--

Érik Martin-Dorel

http://erik.martin-dorel.org/