coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top"

From: Christian Doczkal <doczkal AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top"
Date: Wed, 10 Feb 2016 16:39:32 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=doczkal AT ps.uni-saarland.de; spf=None smtp.mailfrom=doczkal AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT mo4-p05-ob.smtp.rzone.de
Ironport-phdr: 9a23:yozFCx0AYUOHi5+0smDT+DRfVm0co7zxezQtwd8ZsegSLfad9pjvdHbS+e9qxAeQG96LtLQf0aGJ6ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZ/tnL/rs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCCP/HoHTmQflFJkBAPX7xj+FsP9tSDoteN58DGBe9DwTPUvUD24665tRFnkhXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

Hello

> How do I get the coqtop in emacs to have the right flags?

If you name the input file to coq_makefile _CoqProject ist is
automatically picked up by ProofGeneral and Require works again.

For my projects, I use a generic Makefile that generates a Coq Makefile
from the _CoqProject file as follows:

The _CoqProject file can then use a more descriptive name than "Top"
(i.e. -R . MyProject)

--------------------

all: Makefile.coq
+make -f Makefile.coq all

clean: Makefile.coq
+make -f Makefile.coq clean
rm -f Makefile.coq

Makefile.coq: _CoqProject
coq_makefile -f _CoqProject >Makefile.coq

.PHONY: all clean

----------------------

Cheers,
Christian

Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", (continued)
- Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Frédéric Blanqui, 02/10/2016
  - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Clément Pit--Claudel, 02/10/2016
    - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/10/2016
      - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Clément Pit--Claudel, 02/10/2016
        
        Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/12/2016
        
        Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Clément Pit--Claudel, 02/12/2016
        
        [Coq-Club] GitHub's ProofGeneral has old version number, Peter Vanderbilt, 02/13/2016
        
        Re: [Coq-Club] GitHub's ProofGeneral has old version number, Clément Pit--Claudel, 02/13/2016
      - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Tej Chajed, 02/10/2016
        
        Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/12/2016
- Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Christian Doczkal, 02/10/2016