From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: John Wiegley Newsgroups: gmane.emacs.bugs Subject: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop Date: Mon, 29 Feb 2016 18:02:35 -0800 Message-ID: NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain X-Trace: ger.gmane.org 1456797803 19004 80.91.229.3 (1 Mar 2016 02:03:23 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 1 Mar 2016 02:03:23 +0000 (UTC) To: 22865@debbugs.gnu.org Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Tue Mar 01 03:03:10 2016 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1aaZeY-0000fS-0w for geb-bug-gnu-emacs@m.gmane.org; Tue, 01 Mar 2016 03:03:10 +0100 Original-Received: from localhost ([::1]:40224 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1aaZeW-0008AJ-UO for geb-bug-gnu-emacs@m.gmane.org; Mon, 29 Feb 2016 21:03:08 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:47454) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1aaZeT-00089J-HC for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:03:06 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1aaZeQ-0002Vb-Ad for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:03:05 -0500 Original-Received: from debbugs.gnu.org ([208.118.235.43]:57281) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1aaZeQ-0002VU-6c for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:03:02 -0500 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84) (envelope-from ) id 1aaZeP-0000hE-Uc for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:03:01 -0500 X-Loop: help-debbugs@gnu.org Resent-From: John Wiegley Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Tue, 01 Mar 2016 02:03:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 22865 X-GNU-PR-Package: emacs X-GNU-PR-Keywords: X-Debbugs-Original-To: bug-gnu-emacs@gnu.org Original-Received: via spool by submit@debbugs.gnu.org id=B.14567977732657 (code B ref -1); Tue, 01 Mar 2016 02:03:01 +0000 Original-Received: (at submit) by debbugs.gnu.org; 1 Mar 2016 02:02:53 +0000 Original-Received: from localhost ([127.0.0.1]:54408 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1aaZeG-0000gm-Sa for submit@debbugs.gnu.org; Mon, 29 Feb 2016 21:02:53 -0500 Original-Received: from eggs.gnu.org ([208.118.235.92]:56441) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1aaZeE-0000ga-MG for submit@debbugs.gnu.org; Mon, 29 Feb 2016 21:02:50 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1aaZe8-0002TY-NP for submit@debbugs.gnu.org; Mon, 29 Feb 2016 21:02:45 -0500 Original-Received: from lists.gnu.org ([2001:4830:134:3::11]:55080) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1aaZe8-0002TU-Kg for submit@debbugs.gnu.org; Mon, 29 Feb 2016 21:02:44 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:47412) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1aaZe7-00087B-Nb for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:02:44 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1aaZe4-0002TG-H9 for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:02:43 -0500 Original-Received: from mail-pa0-x229.google.com ([2607:f8b0:400e:c03::229]:35780) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1aaZe4-0002TB-AK for bug-gnu-emacs@gnu.org; Mon, 29 Feb 2016 21:02:40 -0500 Original-Received: by mail-pa0-x229.google.com with SMTP id bj10so33103759pad.2 for ; Mon, 29 Feb 2016 18:02:39 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=from:to:subject:date:message-id:mail-followup-to:mime-version :user-agent; bh=ZvAkdeX2dv6wXqVZDXY8QEvu//7Su81deV2e+LmkWbk=; b=x/Q+tl30u79iYNv/PXgTPuTlrUlbwrTUAwfV1NAgwSd+zZOz0FAUBkQ8NacPeD1i4j f7DfT3rUjxO5xZNRHGlzmDVrePlutVeEuRfFanEk42y9ejLQNfNRVD3w5dLlC/T5IRVY 6PT9Al6p2mAZQEChC8DPZbMqXB+hHr+g9cODruaC+Ww/MGzKDtuoBS17BnPHjZxmwD1t 9qSA///JP1cbS2v1BKHN0EaaIJ0SMpQk7gbMb7FbbQNWTCvs1y3VTBZVRZAKzbVIt5O3 Opa7r+lgPJEgUOC6AarMWksqBy24TPsqnd5V216bP/oO8JsdO9rCKoXQcdzhqBTbaJX7 FWGw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:from:to:subject:date:message-id:mail-followup-to :mime-version:user-agent; bh=ZvAkdeX2dv6wXqVZDXY8QEvu//7Su81deV2e+LmkWbk=; b=XJHCEEKlMhfZYb17T7wMx9d2TqzLap30Q4r4rVkN4nqtBkj/+BqpbPaLe6deqmTWPp f0DDchaqjlRWoBeOgmUi71nDDqMSUPRIa56a1KzrB4EuwMOy1cphh+p71fIEOEhBSyhS +iXB4aJAfNLznlZusHmWKCj64Brhz2LA9j63IaiMqCDGe3096KaOYpubKpMOUZexxK6k vH5s9ZCR1iaKBbIWB/Z5ytGksuWNroPnLv5cqQ7OugFCZjz+m8gunhacJJ9Bbsw4uLjy IHs3Zbt1oXpKRvhSJNEOlinfhN/v0rS+XpnCKrmH4V7mZdPbMqylx6+MicHyw5Ir7wIr mrNQ== X-Gm-Message-State: AD7BkJJwD3kGHsofshfzhyN/0NqSDfQbgC/mtKrkEefok+lPSesTnDWR1yeyJXV1n8Z/3g== X-Received: by 10.66.158.232 with SMTP id wx8mr27269090pab.159.1456797758923; Mon, 29 Feb 2016 18:02:38 -0800 (PST) Original-Received: from Vulcan.local (76-234-68-79.lightspeed.frokca.sbcglobal.net. [76.234.68.79]) by smtp.gmail.com with ESMTPSA id z5sm9592378par.21.2016.02.29.18.02.38 for (version=TLS1 cipher=AES128-SHA bits=128/128); Mon, 29 Feb 2016 18:02:38 -0800 (PST) X-Google-Original-From: John Wiegley Original-Received: by Vulcan.local (Postfix, from userid 501) id 816DA132ED245; Mon, 29 Feb 2016 18:02:37 -0800 (PST) Mail-Followup-To: bug-gnu-emacs@gnu.org User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/25.0.91 (darwin) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 208.118.235.43 X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Original-Sender: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.bugs:114194 Archived-At: 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