Callan McGill (Jun 28 2022 at 00:20): 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?
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.
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.)
Karl Palmskog (Jun 28 2022 at 09:18):the usual recommendation is to install ProofGeneral via MELPA, or update via MELPA if already installed
Callan McGill (Jun 28 2022 at 15:56):Thanks, I did update my version and that cleared things up!
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.
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
Notification Bot (Jun 28 2022 at 23:59):Erik Martin-Dorel has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC