|
From: | GNU bug Tracking System |
Subject: | [debbugs-tracker] bug#22865: closed (25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop) |
Date: | Sat, 05 Mar 2016 17:23:02 +0000 |
Your message dated Sat, 5 Mar 2016 09:22:28 -0800 with message-id <address@hidden> and subject line Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop has caused the debbugs.gnu.org bug report #22865, regarding 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop to be marked as done. (If you believe you have received this mail in error, please contact address@hidden) -- 22865: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=22865 GNU Bug Tracking System Contact address@hidden with problems
--- Begin Message ---Subject: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop Date: Mon, 29 Feb 2016 18:02:35 -0800 User-agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/25.0.91 (darwin) I'm afraid this could be difficult to debug, but here is my scenario: 1. Open a .v (Coq) file within my project. 2. Ask Proof General to evaluate the file to the end. 3. Before a certain definition, PG will hang waiting on a response from "coqtop", the evaluator. Checking the process list shows that this process is not doing anything. 4. Once this happens, C-g or C-c C-c to abort the evaluation leaves me in a broken state where nothing can evaluate anymore. The only recourse is to "killall coqtop", and then attempt the evaluation again. However, the same definition always causes it to hang. There is no common factor about the definitions that I can see, but it happens reliably every time for each file where it does occur. if I switch to 24.5, everything evaluates fine. It happens quite frequently with emacs-25, but never with 24.5. Now, this could be 25.1, or it could be Mac port vs. NeXTstep, or it could be some other subtle interaction with my environment. Unfortunately this will take time to narrow down, and I have to get the Coq code written, so for now this is a placeholder and I must revert to using 24.5. I hope to come back to this later, especially if others have ideas on where to look. John
--- End Message ---
--- Begin Message ---Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop Date: Sat, 5 Mar 2016 09:22:28 -0800 In <http://lists.gnu.org/archive/html/emacs-devel/2016-03/msg00087.html> YAMAMOTO Mitsuharu wrote: User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 This part has been changed to the following one in https://github.com/ProofGeneral/PG/blob/master/generic/proof-config.el, ... and it seems to work for 25.0.92.Thanks for checking this. As it appears that the bug has been fixed on the Proof General side, I'm closing the bug report.
--- End Message ---
[Prev in Thread] | Current Thread | [Next in Thread] |