The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Pete,

On 02/10/2016 11:01 AM, Peter Vanderbilt wrote:
> I strongly suspect that I need to get the flags ‘-R "." Top’ to coqtop, but 
> I don’t know how.

You could add this "-R Top" to the `coq-prog-args' variable, in a 
.dir-locals.el. But that's much more complicated than just adding a 
_CoqProject.

> Does Proof General work for you using Coq8.5 with multiple files and 
> “Require Export”?

Yes, it seems to work fine.

> What do you have in your .emacs file for Coq and PG?

   (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")

(I also have (add-hook 'coq-mode-hook #'company-coq-mode), but that's beyond 
PG)

> I don’t use a _CoqProject file.  Would that help?

Yes, it should help. But not with the version of PG that you're currently 
using :)

> More details:
> 
> I’m using Version 4.2 of Proof General obtained via brew (Homebrew for Mac, 
> which is where I get Coq).

4.2 dates back to October 2012. Pierre Courtieu has been actively maintaining 
the Coq part of it since then, but we don't have access to the website, so we 
can't update it. And I don't know who makes the homebrew packages either, so 
I'm not sure who to ask to update them.

> The Github PG you refer to is “version 4.2 (prerelease)”.  Is that more or 
> less recent than what I have?
> Its COMPATIBILITY file says, “This version of Proof General has been tested 
> with … (main) prover versions:  Coq 8.3, Isabelle2011[-1]”.
> Has it been tested with Coq 8.5?

Someone should have updated that file a long time ago; I just did. PG has 
been tested and updated to work with 8.5.

> I’m running Aquamacs 3.2 which is based on GNU Emacs 24.4.51.2.  I get the 
> following message:
> 
>> Warning (emacs): Proof General compiled for GNU Emacs 24.2 but running on 
>> GNU Emacs 24.4: “make clean; make" is recommended.

Indeed, which is another reason why installing PG via homebrew is not 
recommended :)

> However, I don’t know how to do what it suggests (given that it’s built by 
> brew).
> 
> I’ll see about trying the Github PG and/or coming up with a small example.

Thanks!

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature