Scott N. Walck (Jun 05 2024 at 16:05): Scott N. Walck (Jun 05 2024 at 16:05):Hi folks,
When using Coq 8.19.1 with Proof General 4.6-git and Emacs 29.3,
I use C-c RET (proof-goto-point) to navigate throughout a .v
file. When I've been editing awesome1.v and then I start editing
awesome2.v, Proof General asks if I want to retract the proving I
did on awesome1.v, and I say yes. Sometimes (but not all the
time) after this, Proof General gets into a state where it
complains that it doesn't understand the first plus + sign in the
file. It gives the error
Error: Syntax error: '.' expected after [gallina] (in [vernac_aux]).
Since the first plus sign is very near the top of a file that had been
loading correctly, it basically won't load anything.
How can I restart Proof General without restarting Emacs?
If there is a way to fix this, I would love to know about it.
Erik Martin-Dorel (Jun 05 2024 at 17:10):Hi Scott! Thanks for your post.
Restarting the ambient Coq session without closing Emacs can be done with C-u C-c C-x.
If you believe there is a "bug pattern" and the situation occurs again:
also take a look at the (end of the) special buffer *coq*(C-x b *coq* RET) then feel free to open an issue with this additional info…
Kind regards
Scott N. Walck (Jun 05 2024 at 19:12):Thanks Erik. The C-u C-c C-x did work to kill the coq process. Unfortunately, the problem continues to persist until I restart emacs. I'll open an issue.
Pierre Courtieu (Jun 05 2024 at 21:44):Please, in the issue give the exact files you are using.
Gaëtan Gilbert (Jun 05 2024 at 21:54):when is the autosuggested "retract" better than quitting? retract can get stuck if it hits a coq backtrack bug so it seems worse
easy way to get stuck:
Require Ltac2.Ltac2.
Set Warnings "+all".
(* run then retract -> pg gets stuck and only C-c C-x quit or killing the *coq* buffer unsticks it *)
This is new. And looks like a change in coqtop:
<prompt>Coq < 1 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof" "_equation" "R_" "_ind" "_rec".
<prompt>Coq < 2 || 0 < </prompt>Set Suggest Proof Using.
<prompt>Coq < 3 || 0 < </prompt>Set Printing Compact Contexts.
<prompt>Coq < 4 || 0 < </prompt>Set Printing Unfocused.
<prompt>Coq < 5 || 0 < </prompt>Set Diffs "off".
<prompt>Coq < 6 || 0 < </prompt>Set Printing Depth 50 .
<prompt>Coq < 7 || 0 < </prompt>Set Printing Width 94.
<prompt>Coq < 8 || 0 < </prompt>Set Silent.
<prompt>Coq < 9 || 0 < </prompt>Require Ltac2.Ltac2.
<prompt>Coq < 10 || 0 < </prompt>Set Warnings "+all".
<prompt>Coq < 11 || 0 < </prompt>Unset Silent.
<prompt>Coq < 12 || 0 < </prompt>BackTo 8 .
Error:
Anomaly
"edit_at 8: A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: Ltac2 Backtrace [summary-out-of-scope,dev]."
Please report at http://coq.inria.fr/bugs/.
<prompt>Coq < 8 || 0 < </prompt>BackTo 8 .
Error: Anomaly "Uncaught exception Stm.Vcs_aux.Expired."
Please report at http://coq.inria.fr/bugs/.
<prompt>Coq < 8 || 0 < </prompt>
Well it seems to date back to at least coq 8.13.
Pierre Courtieu (Jun 06 2024 at 06:22):Strange that no one got this bug before...
Pierre Courtieu (Jun 06 2024 at 06:29):That is a good point. We could restart coq indeed. Coq's message is strange though. Is it just that plugin cannot be unloaded?
Pierre Courtieu (Jun 06 2024 at 06:40):Oh now I see the "+all", no wonder this has not been detected before. I was a bit worried at first :-). The message still looks very strange to me: there is no section or any local scope involved.
Gaëtan Gilbert (Jun 06 2024 at 15:43):I mean after the retract prompted by changing files we also quit, so the retract was just doing useless work
same for proof-toggle-active-scripting (C-c C-s) which also retracts before quitting
Pierre Courtieu (Jun 07 2024 at 07:12):Right. Completely useless. I don't even know why we do that. I guess this is the generic proofgeneral behavior. I will fill a bug.
Last updated: Oct 13 2024 at 01:02 UTC