The Coq mailing list

[Peter Vanderbilt <acm AT petervanderbilt.com>]

Hi Clément,

With the new README for PG on Github, I got it to compile and it works just 
fine (with a newly crafted _CoqProject file).

Thanks.

Pete

> On Feb 10, 2016, at 9:21 AM, Clément Pit--Claudel 
> <clement.pit AT gmail.com>
>  wrote:
> 
> 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.
>