Check at top of coq.el doesn't work properly when proof-assistant is not bound

[rswarbrick]

trafficstars

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 (and (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 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?

[cpitclaudel]

Th problem is rather that coq.el should require its dependencies, rather than assuming they were loaded first

[hendriktews]

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...

[rswarbrick]

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)).

[monnier]

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))

The recommended way would be rather to (require 'pg-vars) beforehand.

    Stefan