Open rswarbrick opened 3 years ago
Th problem is rather that coq.el should require
its dependencies, rather than assuming they were loaded first
I believe the problem comes from coq-mode not being defined in coq.el - this was introduced by @monnier in f7cc8f1f76baf5e517e51f1db47510ed605064e8. Other assistants rely on the stub that is created from proof-assistant-table
in proof-site, which calls proof-ready-for-assistant
. For Coq, coq-mode
is now an auto loaded function...
Following up on this, I fixed my installation, so this isn't urgent. But the code above is intrinsically wrong: there are two ways to get onto the error path, and one causes the error reporting to fail.
I'm not sure what the check is supposed to do: if it's just checking that proof-assistant
hasn't already been assigned to some other tool, maybe the check should actually be:
(if (or (not (boundp 'proof-assistant))
(member proof-assistant '(nil "" "Coq" "coq")))
(proof-ready-for-assistant 'coq)
(message "Coq-PG error: Proof General already in use for %s" proof-assistant))
If running proof-ready-for-assistant
won't work before sourcing pg-vars.el
, it should probably instead be something like this:
(if (boundp 'proof-assistant)
(if (member proof-assistant '(nil "" "Coq" "coq"))
(proof-ready-for-assistant 'coq)
(message "Coq-PG error: Proof General already in use for %s" proof-assistant))
(message "Coq-PG error: Cannot load coq.el before pg-vars.el" proof-assistant))
or, if we're happy to emit actual errors, this:
(unless (boundp 'proof-assistant)
(error "Cannot load coq.el before pg-vars.el"))
(unless (member proof-assistant '(nil "" "Coq" "coq"))
(error "Proof General already in use for %s" proof-assistant))
(proof-ready-for-assistant 'coq)
(maybe replacing the first form with (require 'pg-vars)
).
If running
proof-ready-for-assistant
won't work before sourcingpg-vars.el
, it should probably instead be something like this:(if (boundp 'proof-assistant) (if (member proof-assistant '(nil "" "Coq" "coq")) (proof-ready-for-assistant 'coq) (message "Coq-PG error: Proof General already in use for %s" proof-assistant)) (message "Coq-PG error: Cannot load coq.el before pg-vars.el" proof-assistant))
The recommended way would be rather to (require 'pg-vars) beforehand.
Stefan
I've got a broken proof-general install, which I'm trying to debug and sort out. However, this is tickling a bug at the top of
coq.el
, which has the following code:If
proof-assistant
isn't bound, this falls through and explodes when it's trying to generate the error message. Does the error case need splitting in two?