Stream: Proof General users

Topic: PG does not position to error

Vadim Zaliva (Jun 28 2024 at 21:21):

As the last resort, asking here for support. My proof general stopped pointing to errors as I step through the code. It shows error message in response buffer but fails to position cursor to the error position. It was working before and I am unsure what broke. I see no error messages or warnings. Coq 8.18, Proof general 4.6-git (latest ELPA). Anybody else experienced something like this? Any suggestions how to fix?

Erik Martin-Dorel (Jun 28 2024 at 22:49):

Just to be sure, can you run this and paste the output?
ls -dl ~/.emacs.d/elpa/proof-general-*

I suspect that you have proof-general-20240619.1209 and thus you just faced a regression due to a recent bugfix for this issue: namely, I was able to reproduce your issue, so the bugfix was incomplete.

But no worries, we'll be able to take a look to properly fix this!

Erik Martin-Dorel (Jun 28 2024 at 22:59):

Meanwhile, you might want to locally revert the incomplete bugfix by doing this:

• rm ~/.emacs.d/elpa/proof-general-*/coq/coq.elc
• open ~/.emacs.d/elpa/proof-general-*/coq/coq.el
• remove the line proof-shell-strip-crs-from-input nil
• save and restart emacs

Vadim Zaliva (Jun 28 2024 at 23:00):

yes, it is proof-general-20240619.1209

Vadim Zaliva (Jun 28 2024 at 23:04):

Thank you! Your hotfix helped.

Vadim Zaliva (Jul 30 2024 at 17:52):

@Erik Martin-Dorel I think it is happening again....

Erik Martin-Dorel (Aug 25 2024 at 21:55):

Dear @Vadim Zaliva, thanks for your message (I wanted to reply earlier but I was busy and then forgot, sorry for that)

Can you try this workaround? https://github.com/ProofGeneral/PG/issues/781#issuecomment-2296820634

Erik Martin-Dorel (Aug 25 2024 at 21:56):

Anyway we are fully aware of the issue; @Pierre Courtieu started to work on a fix, which is not ready yet as the fix happens to be involved, but… stay tuned.

Erik Martin-Dorel (Sep 10 2024 at 21:43):

@Vadim Zaliva just in case you didn't see my previous message and the closing of the issue:

the fix has been merged a couple of days ago, so feel free to test

after upgrading PG by using package.el or M-x proof-upgrade-elpa-packages RET

Vadim Zaliva (Sep 11 2024 at 04:42):

Thanks.

Last updated: Oct 13 2024 at 01:02 UTC