The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

You may need to run "opam update" to see the 8.7.0 package.

And you may need to run "eval `opam config env`" to get the right coqtop and coqc in your PATH. Just check that you are running the right version with "coqtop -v" and "coqc -v" before launching Proof-General (from the terminal).

You may want to add the above command to your .profile or your .bashrc.

Théo

Le sam. 28 oct. 2017 à 11:42, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> a écrit :

For autodetection of opam executables you may need to restart emacs for
it to get the right PATH.

You can also look at variables coq-dependency-analyzer and coq-compiler.

Gaëtan Gilbert

On 28/10/2017 08:07, Chris Brinkley wrote:
> I tried adding (setq coq-prog-name "~/opam-coq.8.6/4.01.0/bin/coqtop") to init.el.
>
> Emacs seems to accept the initialization and I no longer get the error executing interactively, but I still get an error compiling a file containing a "Set Warnings" command , which makes me doubt if ProofGeneral is using coqc 8.6, even though it now seems to be using coqtop 8.6.
>
> Is there an analogous way to control the coqc version ProofGeneral will use?
>
> Clément Pit-Claudel wrote:
>> You can customize coq-prog-name; alternatively, make sure that running coqtop in your shell runs the right version of Coq.
>
>> On 2017-10-27 23:28, Chris Brinkley wrote:
>>> But now when I run the troublesome command from Software Foundations 5.3, I still get the same error, which makes me think ProofGeneral is not seeing the new Coq version.
> ________________________________
>   This message (including any attachments) may contain confidential information intended for a specific individual and purpose. If you are not the intended recipient, you should delete this message and any attachments.
>