The Coq mailing list

[Peter Vanderbilt <acm AT petervanderbilt.com>]

Hi Clément,

Thanks for your response.

I strongly suspect that I need to get the flags ‘-R "." Top’ to coqtop, but I 
don’t know how.

Does Proof General work for you using Coq8.5 with multiple files and “Require 
Export”?
What do you have in your .emacs file for Coq and PG?

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

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).

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
>>> 
>> 
>> 
>