The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

On Wed, Feb 10, 2016 at 11:01 AM, Peter Vanderbilt <acm AT petervanderbilt.com> wrote:

More details:

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

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?

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.

However, I don’t know how to do what it suggests (given that it’s built by brew).

Using Homebrew you can get a more recent version of Proof General (from Sep 30, 2015) by installing with brew install --devel proof-general. This will also result in a compile (rather than using a Homebrew bottle, a pre-built distribution), which should link against your version of Emacs. It runs the "make clean; make" that Proof General is asking you to do.

I'm working on supporting installation of PG from source in Homebrew, so that brew install --HEAD proof-general will install from the GitHub repo. The pull request is at https://github.com/Homebrew/homebrew/pull/49038.

 

I’ll see about trying the Github PG and/or coming up with a small example.

Pete

> On Feb 10, 2016, at 5:32 AM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:
>
> Which version of Proof General are you using? Does using the latest version at https://github.com/ProofGeneral/PG fix the problem? If not, can you raise an issue there with a small example?
>
> Clément.
>
> On 02/10/2016 05:23 AM, Frédéric Blanqui wrote:
>> Hello. I also raised this problem in
>>
>> https://coq.inria.fr/bugs/show_bug.cgi?id=4541  .
>>
>>
>> Le 09/02/2016 19:55, Peter Vanderbilt a écrit :
>>> In Coq8.5, coq_makefile adds "-R . Top” to COQLIBS and COQDOCLIBS.  Why?
>>> Doing so breaks coqtop in Emacs (Aquamacs), because the Require statements fail — it expects module “X” but gets “Top.X”.
>>>
>>> How do I get coq_makefile to not add  "-R . Top” (as in 8.4)?
>>> OR
>>> How do I get the coqtop in emacs to have the right flags?
>>>
>>> Pete
>>>
>>
>>
>