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: Peter Vanderbilt <acm AT petervanderbilt.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top"
Date: Thu, 11 Feb 2016 15:06:00 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=acm AT petervanderbilt.com; spf=None smtp.mailfrom=acm AT petervanderbilt.com; spf=None smtp.helo=postmaster AT delivery.mailspamprotection.com
Ironport-phdr: 9a23:Fj503RQVq+/n90rEW4ZtuinYENpsv+yvbD5Q0YIujvd0So/mwa64YBGN2/xhgRfzUJnB7Loc0qyN4/+mAjBLuM/Z+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVOFkD3WPlKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxyJFHwXfpC/zWJv8qCH7svY1jCCROOXuQKw5Qyqr6atmUhXpjDtBPDk8pjKEwvdshb5W9Ury7yd0xJTZNdmY

On Feb 10, 2016, at 10:18 AM, Tej Chajed <tchajed AT mit.edu> wrote:

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.

Thanks for the pointer. This works for me.

A small issue: it seems to expect the 24.5 version of Emacs but I’m running Aquatics, which is based on 24.4.

How do I tell brew to link to that version?

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.

Great.

Thanks Tej,

Pete

[Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/09/2016
- 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