From unknown Sun Aug 17 09:10:54 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#22865 <22865@debbugs.gnu.org> To: bug#22865 <22865@debbugs.gnu.org> Subject: Status: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop Reply-To: bug#22865 <22865@debbugs.gnu.org> Date: Sun, 17 Aug 2025 16:10:54 +0000 retitle 22865 25.0.91; Use Proof General with emacs-25 on OS X frequent han= gs coqtop reassign 22865 emacs submitter 22865 John Wiegley severity 22865 normal tag 22865 moreinfo thanks From debbugs-submit-bounces@debbugs.gnu.org Mon Feb 29 21:02:53 2016 Received: (at submit) by debbugs.gnu.org; 1 Mar 2016 02:02:53 +0000 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 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 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 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,FREEMAIL_FROM, T_DKIM_INVALID autolearn=disabled version=3.3.2 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 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 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 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 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) 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) From: John Wiegley X-Google-Original-From: John Wiegley Received: by Vulcan.local (Postfix, from userid 501) id 816DA132ED245; Mon, 29 Feb 2016 18:02:37 -0800 (PST) To: bug-gnu-emacs@gnu.org 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 Message-ID: Mail-Followup-To: bug-gnu-emacs@gnu.org MIME-Version: 1.0 Content-Type: text/plain 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-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -4.0 (----) 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 From debbugs-submit-bounces@debbugs.gnu.org Fri Mar 04 14:55:52 2016 Received: (at 22865) by debbugs.gnu.org; 4 Mar 2016 19:55:52 +0000 Received: from localhost ([127.0.0.1]:34086 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1abvpI-0000W8-56 for submit@debbugs.gnu.org; Fri, 04 Mar 2016 14:55:52 -0500 Received: from mail-pf0-f176.google.com ([209.85.192.176]:33242) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1abvpG-0000Vv-3e for 22865@debbugs.gnu.org; Fri, 04 Mar 2016 14:55:50 -0500 Received: by mail-pf0-f176.google.com with SMTP id 124so40786168pfg.0 for <22865@debbugs.gnu.org>; Fri, 04 Mar 2016 11:55:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=from:to:cc:subject:in-reply-to:date:message-id:references :user-agent:reply-to:mime-version:content-transfer-encoding; bh=fGx8YOY8JRF2htFCgaNh1cMi2KLNWeB9+bXI7Mkri1s=; b=j0UCek1t3rW2rY+vi4aa3DbJR6m0aBefIijhtlXrpmtFrWhTVmJ28enQH6V++klVhu yETaQSWINobFWQAq9XzUfJ9V/wTmVc/xWGPsJJVzf/O5ABJzD0zVe+EOq8i3JUQLNSbu yghCUcfV7rn5Gqj/L1DeBENrRcwQulqgMfWc8iZqswX33XEXCaPd4Ru96ecUwdUe4ECw IppideKW/tap6iD7aa4BeBLB9S7RFJeewwVs/sJfKNd0B5bFiuAHRxmYntEfIrg/JmsX luBCNU5UkjHq4I1MrhMYtCvdx9wdjaBMHrFYWp5Yw5WcSK+JQdhWQafor/7FpwWeuJV5 d6Ug== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:from:to:cc:subject:in-reply-to:date:message-id :references:user-agent:reply-to:mime-version :content-transfer-encoding; bh=fGx8YOY8JRF2htFCgaNh1cMi2KLNWeB9+bXI7Mkri1s=; b=f0EqMVsijiP5QtkafZddG4J+Ktm8/RkO9+W28JD5ZtsaQa3RoH6XXnmeqhx+OH0zuN hlfYhn1JH4U769+4mw5I6yU239FlsjKZjuY+7hHACrZNP/tpC8NWuKgKMDaCwq24FKCu sa/+qMSYAu3jQNww057wZxOKJfqNBzW9XIBCS/mGExMLdbt7+SraKDAuBpOaDQaZvwx6 lgzj1glCPph8vmABu4+zOeUtt+cKWpRRGh0NZEpzW17MQoRxWtxcN1ANE6VoDuskg8Mr utve0NRBxAFiaSL2mhpngaRGGwfq4iU7TvVl8eI0CQRod4Cw0TGolXCH+xk4j5w2nQGL tkSg== X-Gm-Message-State: AD7BkJIEDUj+yeFvrs+NcPNcHx272F+oH6vilxBDT2/WkfIJjgRYpyNIs4gybnivjGHepw== X-Received: by 10.98.66.75 with SMTP id p72mr14909430pfa.50.1457121344057; Fri, 04 Mar 2016 11:55:44 -0800 (PST) Received: from Vulcan.local (76-234-68-79.lightspeed.frokca.sbcglobal.net. [76.234.68.79]) by smtp.gmail.com with ESMTPSA id kw10sm7395122pab.0.2016.03.04.11.55.43 (version=TLS1 cipher=AES128-SHA bits=128/128); Fri, 04 Mar 2016 11:55:43 -0800 (PST) From: John Wiegley X-Google-Original-From: "John Wiegley" Received: by Vulcan.local (Postfix, from userid 501) id A45CA133EACD5; Fri, 4 Mar 2016 11:55:42 -0800 (PST) To: 22865@debbugs.gnu.org Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop In-Reply-To: (John Wiegley's message of "Mon, 29 Feb 2016 18:02:35 -0800") Date: Fri, 04 Mar 2016 11:55:41 -0800 Message-ID: References: User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/24.5 (darwin) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 22865 Cc: =?utf-8?Q?Cl=C3=A9ment_Pit--Claudel?= X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: John Wiegley Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.7 (/) Cl=C3=A9ment, have you seen this bug on your side? Is it possible that thi= s only happens on OS X? --=20 John Wiegley GPG fingerprint =3D 4710 CF98 AF9B 327B B80F http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2 From debbugs-submit-bounces@debbugs.gnu.org Fri Mar 04 15:25:39 2016 Received: (at 22865) by debbugs.gnu.org; 4 Mar 2016 20:25:39 +0000 Received: from localhost ([127.0.0.1]:34114 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1abwI7-0001Ea-IB for submit@debbugs.gnu.org; Fri, 04 Mar 2016 15:25:39 -0500 Received: from mout.kundenserver.de ([212.227.17.10]:58786) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1abwI5-0001EL-Q7 for 22865@debbugs.gnu.org; Fri, 04 Mar 2016 15:25:38 -0500 Received: from [18.189.68.195] ([18.189.68.195]) by mrelayeu.kundenserver.de (mreue103) with ESMTPSA (Nemesis) id 0LiWYm-1a1UXd1wZo-00cf3j; Fri, 04 Mar 2016 21:25:29 +0100 Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop To: John Wiegley , 22865@debbugs.gnu.org References: From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= Message-ID: <56D9EF37.9070602@live.com> Date: Fri, 4 Mar 2016 15:25:27 -0500 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="tI2AQXpNJluTirvsWwBCITw8D9KkCPapt" X-Provags-ID: V03:K0:QKPvtzV0ZaeuxXnF3edX6gH5cZrbWACmE6yoXKGGtR3bWnXXHZx Hg9zrZrIMB6RHmFpalI+uuV2VY0gMt8lp9qAWLkZEDAyBsZE80KL1npycW7Y8ynk+Ds7EwV HqTGCOy58wt4omHV93P6+kGRMYnUHboYl5clyYCnreR/KMA8DcEVSu7xXJgbekfyIBY1MgJ vM0SDA+GtZotSbAU+FTzQ== X-UI-Out-Filterresults: notjunk:1;V01:K0:akZlzI3ESpk=:N37K0SOm8jfAzgfIlfg+Rv /bYQ3uhSz6BQHZhdYQYf+/k/FFBvVTRG7cyNom503H2+KsW1seCmYiFHpgs9utKx5IHNY+jyF DKkqgsT/OYxIvEyFWDfsVveaiQ33wtnyk8nFrBkVhvglWUZ8hr0x5ZAlWnUAxpiQOQcKLUKp0 r5/ngERjgOsYHCEX67elADBmlzHfVD0W/DWaqQmfco5czSXQxfsr+XBXMcQdIPRlejO9GOaI0 U0S6h6Bh9TGv1gIDCbNdxckksXoI4MQqz5+er7xTpKREoC6/atnPDGIZUv7JCEGpIj8xjczXK 1SyDJI3IV9Fub0kEKMWtGQbpED3kULrL27oVL/1lPF/vIda7tR6s8O3hx+93rk7QMdQLLasCf OLGMyXsSO0FTVL5zfCvTSy8tmN0X5aCnE1NfrPbk6uBfRNiflnOoIZnCyeRcZdSHwGxRZRGb/ FAkpiJ3rSNw89+9Uh29L4Za/qde4NqGNd4s/swO4O5NZDNzldEln3AfreKoaQnsOjmTZ8sF4z F3enk8JCF5ljdHUwklkCr4jejnufpnrNa/JzY74DTovUO4yQdMvEG7pXstIKSCuPQKvgMBnSG 5B6e3kBNMse2OVMcGGedsgsBDYhgx052BFKpRcjyaLRCK7Hf+PS5U3LDknw+0wSRly6TA7hAF MM+yylnKJGCYnrfXzn0ATzfZvMaj/wq1SNkcyJGaVT+TSJ23vpwy2Ve7xmCfj8M/G48k= X-Spam-Score: 0.3 (/) X-Debbugs-Envelope-To: 22865 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.3 (/) This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --tI2AQXpNJluTirvsWwBCITw8D9KkCPapt Content-Type: multipart/mixed; boundary="hUDeJMJqi5RlRBrG3bgIMkjlmWM38bqNK" From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= To: John Wiegley , 22865@debbugs.gnu.org Message-ID: <56D9EF37.9070602@live.com> Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop References: In-Reply-To: --hUDeJMJqi5RlRBrG3bgIMkjlmWM38bqNK Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 03/04/2016 02:55 PM, John Wiegley wrote: > Cl=C3=A9ment, have you seen this bug on your side? Is it possible that= this only > happens on OS X? Definitely OS X only; I haven't seen it in over 6 months using of Emacs 2= 5 w/ PG and Coq. --hUDeJMJqi5RlRBrG3bgIMkjlmWM38bqNK-- --tI2AQXpNJluTirvsWwBCITw8D9KkCPapt Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.22 (GNU/Linux) iQIcBAEBAgAGBQJW2e83AAoJEPqg+cTm90wjFv8P/0lsjgE43/a0wi1mTpq83Pb7 33yQoqm5LuIp/miLZtPhBYq4MUwg2xEYl3eUN6M3uIW+tHVBA4v2pWyGW4y7/u89 EAcEKAQ9Vgna01pySF0ogP9Fv7SepHddfT7hIpVT/8u1NJefpeow7EZYhZXo73ty 9LQncWf0/sKTizQw6TFfRlaivRSDWacfMCYqSt8HYsk7OmqKGhp68wh4i5TLnTZF sYWLI5Sj778iNUghwBvJf2pDgOmvKpLtIm6MULv2XGVmBpsv+rx3Yvp6iiSICVvT nckbiftK3wdWj/n2GWQXkKBGiFdxxfjCGRvNWsRqpLd2Y5BJS/vOzTgFN856DMb5 OoG+yyKkYtSl1Di1If/bgVe068DaGTsgz7iHtSXmi1Xn8Pfk7AlkGPn2DquUUPli YnlFEAw3bXa5p7XHll8//u4ZtRp8g0w2UBvQ2ozmtt4E/g9BKefKm5PVsXx9B+fz 3glP+qFlZtYXL16pvU4VIv0/v1n0OvZMxEND2gZ9al09dvNMpJEMmepSEO+ezNYK CuwuQdfA54W3th1MCdq+k3RB6SV/RAvGmBgnDHha3Z3ID3dn/umSiaucu+nloZGs FAb+fLCfIabmejZi0jy7oD4CLnFY1hGAKgNPL9pI4IBA9am30cGb2P7YQmmiY3/l Jisw3eTWdmE57blHpd06 =029Y -----END PGP SIGNATURE----- --tI2AQXpNJluTirvsWwBCITw8D9KkCPapt-- From debbugs-submit-bounces@debbugs.gnu.org Fri Mar 04 16:05:29 2016 Received: (at 22865) by debbugs.gnu.org; 4 Mar 2016 21:05:29 +0000 Received: from localhost ([127.0.0.1]:34131 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1abwuf-00029q-Dz for submit@debbugs.gnu.org; Fri, 04 Mar 2016 16:05:29 -0500 Received: from mail-pa0-f51.google.com ([209.85.220.51]:36176) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1abwud-00029d-Ls for 22865@debbugs.gnu.org; Fri, 04 Mar 2016 16:05:28 -0500 Received: by mail-pa0-f51.google.com with SMTP id fi3so38802083pac.3 for <22865@debbugs.gnu.org>; Fri, 04 Mar 2016 13:05:27 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=from:to:cc:subject:in-reply-to:date:message-id:references :user-agent:reply-to:mime-version:content-transfer-encoding; bh=zRiGg9962/7FWEAQI+MOBQNUx/u33+YLxwNl84fZnGA=; b=j/Ub9Xcbure21q9Fk2dmBUpxxpfUhFlPW4zlN8ABFOTPFnViVog2OAoxgcEDj8C5yV PE8AQkMnE2GMtxb3gZ8alRUFmY3gbkEpaC8YgWeWaCfGOjXwi4wvvyrNkXUHQn+A1Kgb Viook7A/1LVCF0+tjomOuTV8c2EmD608bWTSkyNHKxx4Cpy7L2iiT85emWMlLoH7Uc58 UvVoATl0NDl9lEpR/dPh40epzPM/JkAshWiDQARCLS6sfdLKlRYnK3VsY5LVMLrCQjHs 9t9yvtj+4iLSEqmDsN8LHHpFZhiql7+POWFvH4LwNeWidJatWtRD9QRCOzS1MULUyzgY Nuiw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:from:to:cc:subject:in-reply-to:date:message-id :references:user-agent:reply-to:mime-version :content-transfer-encoding; bh=zRiGg9962/7FWEAQI+MOBQNUx/u33+YLxwNl84fZnGA=; b=ao1t9cfnAq+BEyevx3yoA05q3HVDWRWoVPQRR9MPIoShNZvRffNMlVNgMU/6ZWOcj8 QtGjhMQxcf5y43XakERJcbPQInJ5I7LjxLkqt3X8EsUcgcstREIlc13QjfuHSqZFgKkA +uqXcKk2enU/Qf92ZD3jDcr8/PaPG6d/nbdjT+80CA4LCIYUg3+qyNs2g1/uyYoqPOo5 vidwPa+me8eyb3HysgPKa6PnIS5w+a010ZGcWbilmg3VvP4tElHWBXUHHyNTS1q70X47 L/L/amkSqv9ZIhRewvCnb49xA1Cfwzl4n2aZwZoKEQ07FGZzGXcmiPeck+439f2jiviK S2jA== X-Gm-Message-State: AD7BkJLqffJ3jdwmiO20fKfxJiB71AfYzyLtZ8784L0saZ0+CxBMhCztEPh5rzJwpZLGkg== X-Received: by 10.66.140.14 with SMTP id rc14mr15128174pab.65.1457125522027; Fri, 04 Mar 2016 13:05:22 -0800 (PST) Received: from Vulcan.local (76-234-68-79.lightspeed.frokca.sbcglobal.net. [76.234.68.79]) by smtp.gmail.com with ESMTPSA id x1sm7551118pfi.42.2016.03.04.13.05.21 (version=TLS1 cipher=AES128-SHA bits=128/128); Fri, 04 Mar 2016 13:05:21 -0800 (PST) From: John Wiegley X-Google-Original-From: John Wiegley Received: by Vulcan.local (Postfix, from userid 501) id 8D5B5133F05C9; Fri, 4 Mar 2016 13:05:20 -0800 (PST) To: =?utf-8?Q?Cl=C3=A9ment?= Pit--Claudel Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop In-Reply-To: <56D9EF37.9070602@live.com> (=?utf-8?Q?=22Cl=C3=A9ment?= Pit--Claudel"'s message of "Fri, 4 Mar 2016 15:25:27 -0500") Date: Fri, 04 Mar 2016 13:04:34 -0800 Message-ID: References: <56D9EF37.9070602@live.com> User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/24.5 (darwin) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 22865 Cc: 22865@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: John Wiegley Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.7 (/) >>>>> Cl=C3=A9ment Pit--Claudel writes: > Definitely OS X only; I haven't seen it in over 6 months using of Emacs 25 > w/ PG and Coq. That's good to hear, thanks for that data point. I've posted reproduction instructions to emacs-devel, but they should be repeated here: 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: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html And open the file ImpParser.v, it hangs for me while attempting to evaluate the definition parsePrimaryExp. --=20 John Wiegley GPG fingerprint =3D 4710 CF98 AF9B 327B B80F http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2 From debbugs-submit-bounces@debbugs.gnu.org Sat Mar 05 12:22:38 2016 Received: (at 22865-done) by debbugs.gnu.org; 5 Mar 2016 17:22:38 +0000 Received: from localhost ([127.0.0.1]:35733 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acFuX-0007oN-NK for submit@debbugs.gnu.org; Sat, 05 Mar 2016 12:22:38 -0500 Received: from zimbra.cs.ucla.edu ([131.179.128.68]:58279) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acFuW-0007o8-Kh for 22865-done@debbugs.gnu.org; Sat, 05 Mar 2016 12:22:37 -0500 Received: from localhost (localhost [127.0.0.1]) by zimbra.cs.ucla.edu (Postfix) with ESMTP id C5451160FD0; Sat, 5 Mar 2016 09:22:30 -0800 (PST) Received: from zimbra.cs.ucla.edu ([127.0.0.1]) by localhost (zimbra.cs.ucla.edu [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id bizwbhEm9kUm; Sat, 5 Mar 2016 09:22:29 -0800 (PST) Received: from localhost (localhost [127.0.0.1]) by zimbra.cs.ucla.edu (Postfix) with ESMTP id EF932161009; Sat, 5 Mar 2016 09:22:28 -0800 (PST) X-Virus-Scanned: amavisd-new at zimbra.cs.ucla.edu Received: from zimbra.cs.ucla.edu ([127.0.0.1]) by localhost (zimbra.cs.ucla.edu [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id xSTVX_bjQpNG; Sat, 5 Mar 2016 09:22:28 -0800 (PST) Received: from [192.168.1.9] (pool-100-32-155-148.lsanca.fios.verizon.net [100.32.155.148]) by zimbra.cs.ucla.edu (Postfix) with ESMTPSA id C0CD4160FD0; Sat, 5 Mar 2016 09:22:28 -0800 (PST) Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop To: YAMAMOTO Mitsuharu References: From: Paul Eggert Organization: UCLA Computer Science Department Message-ID: <56DB15D4.8050509@cs.ucla.edu> Date: Sat, 5 Mar 2016 09:22:28 -0800 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 22865-done Cc: John Wiegley , =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= , 22865-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) In YAMAMOTO Mitsuharu wrote: > 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. From debbugs-submit-bounces@debbugs.gnu.org Sat Mar 05 13:19:41 2016 Received: (at 22865-done) by debbugs.gnu.org; 5 Mar 2016 18:19:41 +0000 Received: from localhost ([127.0.0.1]:35776 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acGnl-0000mb-KK for submit@debbugs.gnu.org; Sat, 05 Mar 2016 13:19:41 -0500 Received: from mout.kundenserver.de ([212.227.126.135]:57023) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acGDl-0008Hv-U7 for 22865-done@debbugs.gnu.org; Sat, 05 Mar 2016 12:42:30 -0500 Received: from [18.189.68.195] ([18.189.68.195]) by mrelayeu.kundenserver.de (mreue005) with ESMTPSA (Nemesis) id 0LtjF3-1ZvKnJ3zXB-011EJ7; Sat, 05 Mar 2016 18:42:05 +0100 Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop To: Paul Eggert , YAMAMOTO Mitsuharu References: <56DB15D4.8050509@cs.ucla.edu> From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= Message-ID: <56DB1A67.1040902@csail.mit.edu> Date: Sat, 5 Mar 2016 12:41:59 -0500 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 MIME-Version: 1.0 In-Reply-To: <56DB15D4.8050509@cs.ucla.edu> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit X-Provags-ID: V03:K0:Zp3Qu5XMrgVpclYH7XCjnIN72mggu1OTonorGjBhspbh8dmNXTY NDRmHRUVC3Fpk7LYPjBBKvK1jjIhxPdF9n4FOKxL3GpN/oDzNYb/teq4nV6Hy+QYIY/yLL+ affboOPHhgJcWWY0JRdrCjG3hVvdbjRRw3rS6kfcLtegtyOG+vrQuoJTi5ZTTVkMXVxWH9i WrvBfNrp9cPi2HNQeuvDA== X-UI-Out-Filterresults: notjunk:1;V01:K0:I/v69ItQk1Y=:m2ClERjd0wskuDJV9NSjJe OHQyRiRJFI9hLZNTf6Wfg4cXsI+5PFaslXLr5zp9c/BG5N7goxKuwC4S2YsO/G8umI7KTY4IW jlBRZ15csSvvSV9rX66Q/fC7AhUypyv6WPiw6SZNQY0g2K9Xzbvc4te7u1WXh3lQ6edfKsdQu Z0OXOscTpe8mkQZIpplCRMe+tcenNJ101kIo59xbsvZMlIduWiqFpXxVvYmRH/YUJDSW1yO1Z QT4+PTXF4l0mE5Ax3ql/QUdUWHZgrtz9xNc4fteg/u41tHD20dOUkGzkDZ1hDAnGN1ejYv7lv lMXyF5dFCGa+cI0sM4bRd8lQr6Y1BnkCBrHdPLqAav/r0VJq8KIQwjng3rrN1vz0KkMgZ1NQp WdiGukjM0HV8c5ntg7vjvehsOvMAOIvCBJlQm4YhhPoa6ZrTHRyOM0ospRc4v9jagTFTIi5j2 Rz/7DCU47kc8pMCVvnLQIcFcfFfw2RhfQip84Qvgl064Bo9Lu3JcYUm98Khsk1T3JOExWgPSk 0tPkE0KrTqZPpxDgFkGJLvFGu4Aef/uo6/R8u5Q+NYTk0s1pVXl0RsvVgT8N7kE++hj0EifcC rO4tURP7N37c2PEgKLD3eMnOjOL4/fp8u57IX2PZnd68VzwH2AUV8g6zNcrrcbz93k5/ILTg7 q8VnD//uROn5OV5dSNUbnJmLjjP30SSjfhgo7rl4oOeXja98AJsNsrAppCtOOmeSwogAdvo7j 6xvZxCyJnrOuliCw X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: 22865-done X-Mailman-Approved-At: Sat, 05 Mar 2016 13:19:40 -0500 Cc: John Wiegley , 22865-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) On 03/05/2016 12:22 PM, Paul Eggert wrote: > In YAMAMOTO Mitsuharu wrote: > >> 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. Proof General includes a workaround, but isn't this still a bug? From debbugs-submit-bounces@debbugs.gnu.org Sat Mar 05 14:49:58 2016 Received: (at 22865-done) by debbugs.gnu.org; 5 Mar 2016 19:49:58 +0000 Received: from localhost ([127.0.0.1]:35807 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acID7-0004qT-Vr for submit@debbugs.gnu.org; Sat, 05 Mar 2016 14:49:58 -0500 Received: from zimbra.cs.ucla.edu ([131.179.128.68]:33974) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acID6-0004qF-Op for 22865-done@debbugs.gnu.org; Sat, 05 Mar 2016 14:49:57 -0500 Received: from localhost (localhost [127.0.0.1]) by zimbra.cs.ucla.edu (Postfix) with ESMTP id DB54E160FF5; Sat, 5 Mar 2016 11:49:50 -0800 (PST) Received: from zimbra.cs.ucla.edu ([127.0.0.1]) by localhost (zimbra.cs.ucla.edu [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id GfmPcCRM2iUz; Sat, 5 Mar 2016 11:49:50 -0800 (PST) Received: from localhost (localhost [127.0.0.1]) by zimbra.cs.ucla.edu (Postfix) with ESMTP id 36F0D161009; Sat, 5 Mar 2016 11:49:50 -0800 (PST) X-Virus-Scanned: amavisd-new at zimbra.cs.ucla.edu Received: from zimbra.cs.ucla.edu ([127.0.0.1]) by localhost (zimbra.cs.ucla.edu [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id c9_11KRrVzVf; Sat, 5 Mar 2016 11:49:50 -0800 (PST) Received: from [192.168.1.9] (pool-100-32-155-148.lsanca.fios.verizon.net [100.32.155.148]) by zimbra.cs.ucla.edu (Postfix) with ESMTPSA id 0F6AB160FF5; Sat, 5 Mar 2016 11:49:50 -0800 (PST) Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop To: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= , YAMAMOTO Mitsuharu References: <56DB15D4.8050509@cs.ucla.edu> <56DB1A67.1040902@csail.mit.edu> From: Paul Eggert Organization: UCLA Computer Science Department Message-ID: <56DB385D.50201@cs.ucla.edu> Date: Sat, 5 Mar 2016 11:49:49 -0800 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 MIME-Version: 1.0 In-Reply-To: <56DB1A67.1040902@csail.mit.edu> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 22865-done Cc: John Wiegley , 22865-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) Cl=C3=A9ment Pit--Claudel wrote: > Proof General includes a workaround, but isn't this still a bug? Hmm, I suppose it is, though it's no longer a blocker for the release. I'= ll=20 reopen the bug report. From unknown Sun Aug 17 09:10:54 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: Did not alter fixed versions and reopened. Date: Sat, 05 Mar 2016 19:52:01 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # Did not alter fixed versions and reopened. thanks # This fakemail brought to you by your local debbugs # administrator From debbugs-submit-bounces@debbugs.gnu.org Sat Mar 05 23:57:50 2016 Received: (at 22865-done) by debbugs.gnu.org; 6 Mar 2016 04:57:50 +0000 Received: from localhost ([127.0.0.1]:36025 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acQlK-0006zh-88 for submit@debbugs.gnu.org; Sat, 05 Mar 2016 23:57:50 -0500 Received: from mail-io0-f171.google.com ([209.85.223.171]:35965) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acQlI-0006zV-FR for 22865-done@debbugs.gnu.org; Sat, 05 Mar 2016 23:57:48 -0500 Received: by mail-io0-f171.google.com with SMTP id l127so101231711iof.3 for <22865-done@debbugs.gnu.org>; Sat, 05 Mar 2016 20:57:48 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=from:to:cc:subject:in-reply-to:date:message-id:references :user-agent:reply-to:mime-version; bh=2DReWFosEqgmXDK8lgD1cxsdOXVmSYIXrDfe4ZkKFrI=; b=HK+wqzwFLYAQWuRcy2bjK8anDdhk/IM74zJZFULiOpK8W3i47HX+kNkbG69tLJZzTH BVCiLtprySUrzlkYHAMEydQrbluSKOVGbm1jXrVIz1ldYdFXGth/d8ButlqGM6UdzocQ 4nMJjk2RSSrc4fNP/KFgIy85KcwG6XEZ1fnXC7Iy/cVU/T9HCQ2YGTDdrCt4imGU99it kGuqXz/Zve8E6Cmfr2AcPQ6biFNP2+PIg1UCO4RTEIWIlCA/yO04F8dfMt2sZW+ShsSM Ty6nw8gEiz9k1tQq+SvDuwjf2tG0AcGWHev5Zde8r0UyWfhzfyjJbra/qUbOwXhCH9bp jytA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:from:to:cc:subject:in-reply-to:date:message-id :references:user-agent:reply-to:mime-version; bh=2DReWFosEqgmXDK8lgD1cxsdOXVmSYIXrDfe4ZkKFrI=; b=Hxaebztsv1UbjQIGfMZwKcKJJCh+r8Q2izi06jB0W979akgBN4INlBEHeT773xxACD LaoD2mA6D634nHBfnhYorN/kzYKLUAslwmbOm+65YNQYqLjntDM+PPv3+x5FC//vjEuz wMOQzC0ouU9dbiJmKEVNBCcQpMpUqnzvWVxJflA7kgQLgJW6EnP4PLw4eeyyovE2hVDD bgf/vcSBIOX7hPF8k2JW5bnIzJpKXzGMwE45jxpUWLWr8FmhcjwERpX42HctxRHMw8ZO KjUkA3TD5f9nhvLFdRWVewjH+vYNZg+7y9gCrqfYaBpb+e8RwumHfgF/XDJmhivdEQOR PcKw== X-Gm-Message-State: AD7BkJKvV/pWAm89fgAFaljh16sVOWOOL9dSn0fA89iZKrpk/+fzzafdCY6Au/6RQPiw9Q== X-Received: by 10.107.30.195 with SMTP id e186mr13531154ioe.158.1457240262962; Sat, 05 Mar 2016 20:57:42 -0800 (PST) Received: from Hermes.local (mail.johnwiegley.com. [208.82.103.192]) by smtp.gmail.com with ESMTPSA id d19sm1468750ioj.32.2016.03.05.20.57.41 (version=TLS1 cipher=AES128-SHA bits=128/128); Sat, 05 Mar 2016 20:57:41 -0800 (PST) From: John Wiegley X-Google-Original-From: "John Wiegley" Received: by Hermes.local (Postfix, from userid 501) id C55CB4ED27F0; Sat, 5 Mar 2016 20:53:30 -0800 (PST) To: Paul Eggert Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop In-Reply-To: <56DB385D.50201@cs.ucla.edu> (Paul Eggert's message of "Sat, 5 Mar 2016 11:49:49 -0800") Date: Sat, 05 Mar 2016 20:53:27 -0800 Message-ID: References: <56DB15D4.8050509@cs.ucla.edu> <56DB1A67.1040902@csail.mit.edu> <56DB385D.50201@cs.ucla.edu> User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/24.5 (darwin) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 22865-done Cc: =?utf-8?Q?Cl=C3=A9ment?= Pit--Claudel , 22865-done@debbugs.gnu.org, YAMAMOTO Mitsuharu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-To: John Wiegley Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.7 (/) >>>>> Paul Eggert writes: > Hmm, I suppose it is, though it's no longer a blocker for the release. I'll > reopen the bug report. Thank you, Paul. -- John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2 From debbugs-submit-bounces@debbugs.gnu.org Sun Mar 06 08:03:48 2016 Received: (at 22865-done) by debbugs.gnu.org; 6 Mar 2016 13:03:48 +0000 Received: from localhost ([127.0.0.1]:36191 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acYLc-0005Bb-3i for submit@debbugs.gnu.org; Sun, 06 Mar 2016 08:03:48 -0500 Received: from vie01a-dmta-at50-1.mx.upcmail.net ([62.179.121.136]:55070) by debbugs.gnu.org with esmtp (Exim 4.84) (envelope-from ) id 1acYLa-0005BT-CO for 22865-done@debbugs.gnu.org; Sun, 06 Mar 2016 08:03:46 -0500 Received: from [172.31.216.41] (helo=vie01a-pemc-psmtp-at50) by vie01a-dmta-at50.mx.upcmail.net with esmtp (Exim 4.72) (envelope-from ) id 1acYLX-0005bC-4I for 22865-done@debbugs.gnu.org; Sun, 06 Mar 2016 14:03:43 +0100 Received: from iznogoud.viz ([85.127.217.222]) by vie01a-pemc-psmtp-at50 with SMTP @ mailcloud.upcmail.net id Sd3i1s0044oVEQM0Bd3iKa; Sun, 06 Mar 2016 14:03:43 +0100 X-SourceIP: 85.127.217.222 X-CNFS-Analysis: v=2.1 cv=HobaYRnS c=1 sm=2 tr=0 a=7XkrPdG+4gHUuTtvCpm1Cw==:117 a=7XkrPdG+4gHUuTtvCpm1Cw==:17 a=L9H7d07YOLsA:10 a=9cW_t1CCXrUA:10 a=s5jvgZ67dGcA:10 a=IkcTkHD0fZMA:10 a=7OsogOcEt9IA:10 a=EPNNBBjAHo50fTOIK4IA:9 a=QEXdDO2ut3YA:10 a=lb9U1I6oM3UA:10 Received: from wolfgang by iznogoud.viz with local (Exim 4.86 (FreeBSD)) (envelope-from ) id 1acYLV-0000Ip-S3; Sun, 06 Mar 2016 14:03:41 +0100 From: Wolfgang Jenkner To: =?utf-8?Q?Cl=C3=A9ment?= Pit--Claudel Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop References: <56DB15D4.8050509@cs.ucla.edu> <56DB1A67.1040902@csail.mit.edu> Date: Sun, 06 Mar 2016 14:03:41 +0100 In-Reply-To: <56DB1A67.1040902@csail.mit.edu> (=?utf-8?Q?=22Cl=C3=A9ment?= Pit--Claudel"'s message of "Sat, 5 Mar 2016 12:41:59 -0500") Message-ID: <85egbnwyfm.fsf@iznogoud.viz> User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/25.1.50 (berkeley-unix) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 22865-done Cc: John Wiegley , Paul Eggert , 22865-done@debbugs.gnu.org, YAMAMOTO Mitsuharu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.0 (/) On Sat, Mar 05 2016, Cl=C3=A9ment Pit--Claudel wrote: > Proof General includes a workaround, but isn't this still a bug? The same as bug#6771, I guess. From unknown Sun Aug 17 09:10:54 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Mon, 04 Apr 2016 11:24:03 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator