Stream: Proof General users

Topic: ✔ update proof general when updating coq


view this post on Zulip Callan McGill (Jun 28 2022 at 00:20):

I am trying to update my version of coq but when I open proof general it now says:
"Symbol's value as variable is void: coq-debug"
What is the recommended thing to do?

view this post on Zulip Notification Bot (Jun 28 2022 at 05:33):

This topic was moved here from #Coq users > update proof general when updating coq by Karl Palmskog.

view this post on Zulip Ana de Almeida Borges (Jun 28 2022 at 08:36):

Have you updated emacs / proof general? (To be clear, I don't know if that's the problem, it just seems sensible to try.)

view this post on Zulip Karl Palmskog (Jun 28 2022 at 09:18):

the usual recommendation is to install ProofGeneral via MELPA, or update via MELPA if already installed

view this post on Zulip Callan McGill (Jun 28 2022 at 15:56):

Thanks, I did update my version and that cleared things up!

view this post on Zulip Stefan Monnier (Jun 28 2022 at 19:33):

the usual recommendation is to install ProofGeneral via MELPA, or update via MELPA if already installed

Nowadays it can also be installed from NonGNU ELPA, which is configured out of the box in Emacs since Emscs-28.

view this post on Zulip Erik Martin-Dorel (Jun 28 2022 at 23:58):

FWIW, whatever is the (M)ELPA distribution you chose, it is easy to automatically update proof-general (and sibling packages) by typing:

M-x p-u-e-p RET or M-x proof-upgrade-elpa-packages RET

cf. https://proofgeneral.github.io/#keeping-proof-general-up-to-date

view this post on Zulip Notification Bot (Jun 28 2022 at 23:59):

Erik Martin-Dorel has marked this topic as resolved.


Last updated: Mar 29 2024 at 14:01 UTC