Spacemacs won't let me retract the proof buffer

Using Coq
1

I’m having an issue - it looks like a bug, but I don’t know what the proper reporting procedure is or how to express a minimal example so I’m hoping for some advice here.

I can use C^c RET to move the proof buffer past its current point, but not back to a previous point. C^c C^r doesn’t work either. When I do these, i get one of two different errors:
Error: the reference Backtrack was not found in the current environment
OR
Error: Syntax error illegal begin of toplevel:vernac_toplevel

Also, my cursor jumps forward to the first line of code after the end of the proof buffer

I think i updated coq and proof general. I dont know if there are other things i have to update? also I can’t find anything about these errors on google

Thanks!

2

You’re likely still running an outdated copy of Proof General. Try installing it from github or from MELPA, and see if the problem goes away. Make sure to uninstall system packages, too, since they’ll be loaded first otherwise.

1 Like
3

How do i install with MELPA? I did M-x package-list-packages RET r U x, and after that it told me there are no more packages to update. Is there something else I need to do? Or do i need to uninstall system packages, as you say? How do i do that?

4
  1. Add the following to your .emacs and restart Emacs:
    (require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
  2. M-x package-refresh-contents RET
  3. M-x package-install RET proof-general RET
5

Thanks! I tried this but it didn’t work :stuck_out_tongue:

6

Those changes to .emacs aren’t immediate to translate to Spacemacs; I don’t think Spacemacs uses .emacs at all.

It’d be great to know which versions of packages you are running, including Spacemacs.

What I do is use the develop branch of Spacemacs, install the Coq layer, then fix the configuration with workarounds for its known bugs. I’m not sure that’s something I’d advise over alternatives…

7

I had the exact same problem, albeit with regular emacs rather than Spacemacs.

The solution for me, as @cpitclaudel said, was to ensure I didn’t have a second, older copy of PG installed through my system’s package manager.

In my case this was dnf, and this system-wide installation was taking priority over the up-to-date version of PG installed in ~/.emacs.d through MELPA.

1 Like