[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent

From: Anders Lindgren
Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
Date: Fri, 4 Mar 2016 22:54:44 +0100


I think you will need to "dumb it down" for me (as I have no experience with Coq). Are there any external Emacs packages used? (When I open the file in a stock Emacs, verilog-mode is used, which doesn't sound right.) How do I evaluate a definition etc.

If possible, I would prefer a step by step description from "emacs -Q".

    -- Anders

On Fri, Mar 4, 2016 at 10:03 PM, John Wiegley <address@hidden> wrote:
>>>>> Anders Lindgren <address@hidden> writes:

> However, I would need a recipe, including where to get and how to install the
> external programs, and the steps you take in Emacs to reproduce the problem.

Hi Anders, Clément,

I am using ProofGeneral-4.3pre150313, and Coq 8.4pl6. I've tried setting
coq-prog-name to both "coqtop" and "coqtop.opt", with no change in behavior.

If you download Software Foundations from:


And open the file ImpParser.v, it hangs for me while attempting to evaluate
the definition parsePrimaryExp.

Note that I build and install all of this through Nix, so if you're interested
in those details, let me know.

John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2

reply via email to

[Prev in Thread] Current Thread [Next in Thread]