The Coq mailing list

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

Great!

On 02/11/2016 06:10 PM, Peter Vanderbilt wrote:
> 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.
>>
> 
> .
>

Attachment: signature.asc
Description: OpenPGP digital signature