From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: "Charles A. Roelli" Newsgroups: gmane.emacs.bugs Subject: bug#27761: Crash while using proof-general/company-coq on OS X Date: Fri, 21 Jul 2017 06:58:18 +0200 Message-ID: References: <83y3riapq2.fsf@gnu.org> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 (1.0) Content-Type: multipart/alternative; boundary=Apple-Mail-DD6BD835-36FB-4FFA-8201-EF8A8BD0237B Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1500613153 21172 195.159.176.226 (21 Jul 2017 04:59:13 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 21 Jul 2017 04:59:13 +0000 (UTC) Cc: 27761@debbugs.gnu.org To: =?UTF-8?Q?=D0=94=D0=B5=D0=BD=D0=B8=D1=81_?= =?UTF-8?Q?=D0=A0=D0=B5=D0=B4=D0=BE=D0=B7=D1=83=D0=B1=D0=BE=D0=B2?= Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Fri Jul 21 06:59:07 2017 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYQ1p-000589-GJ for geb-bug-gnu-emacs@m.gmane.org; Fri, 21 Jul 2017 06:59:06 +0200 Original-Received: from localhost ([::1]:41047 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dYQ1v-00020w-0a for geb-bug-gnu-emacs@m.gmane.org; Fri, 21 Jul 2017 00:59:11 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:59641) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dYQ1p-0001zw-Au for bug-gnu-emacs@gnu.org; Fri, 21 Jul 2017 00:59:06 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dYQ1m-0000la-8n for bug-gnu-emacs@gnu.org; Fri, 21 Jul 2017 00:59:05 -0400 Original-Received: from debbugs.gnu.org ([208.118.235.43]:47585) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dYQ1m-0000lP-5T for bug-gnu-emacs@gnu.org; Fri, 21 Jul 2017 00:59:02 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dYQ1l-0005uN-Tl for bug-gnu-emacs@gnu.org; Fri, 21 Jul 2017 00:59:01 -0400 X-Loop: help-debbugs@gnu.org Resent-From: "Charles A. Roelli" Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Fri, 21 Jul 2017 04:59:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 27761 X-GNU-PR-Package: emacs X-GNU-PR-Keywords: Original-Received: via spool by 27761-submit@debbugs.gnu.org id=B27761.150061311222677 (code B ref 27761); Fri, 21 Jul 2017 04:59:01 +0000 Original-Received: (at 27761) by debbugs.gnu.org; 21 Jul 2017 04:58:32 +0000 Original-Received: from localhost ([127.0.0.1]:50262 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYQ1I-0005tg-2E for submit@debbugs.gnu.org; Fri, 21 Jul 2017 00:58:32 -0400 Original-Received: from sinyavsky.aurox.ch ([37.35.109.145]:41509) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYQ1G-0005tS-F6 for 27761@debbugs.gnu.org; Fri, 21 Jul 2017 00:58:31 -0400 Original-Received: from sinyavsky.aurox.ch (sinyavsky.aurox.ch [127.0.0.1]) by sinyavsky.aurox.ch (Postfix) with ESMTP id 6638B224C5 for <27761@debbugs.gnu.org>; Fri, 21 Jul 2017 04:53:04 +0000 (UTC) Authentication-Results: sinyavsky.aurox.ch (amavisd-new); dkim=pass (1024-bit key) reason="pass (just generated, assumed good)" header.d=aurox.ch DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=aurox.ch; h=to :references:message-id:content-transfer-encoding:date:date :in-reply-to:x-mailer:from:from:subject:subject:mime-version :content-type:content-type; s=dkim; t=1500612781; x=1501476782; bh=GphCZXhRG4KgC68xxu4ohoMbELQYLljLegLwM4B7dls=; b=aU9apIUhkbv/ 3zE5W4uCMY+E+Vu99rr49ZWXZIeqxWW/2B0qKkcWMeOX9CNqqxkOuRLcPzuZD6UK XvP2D5aDj4oZb7HqUFeUYDnu1yBueuiqyM4I/URxfTDQxPJcZ8TEULDqSORRMTCL 58OdNNNosn7iLYzvXyv/7aOeaY+OLZU= X-Virus-Scanned: Debian amavisd-new at test.virtualizor.com Original-Received: from sinyavsky.aurox.ch ([127.0.0.1]) by sinyavsky.aurox.ch (sinyavsky.aurox.ch [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id QjojixAndkkW for <27761@debbugs.gnu.org>; Fri, 21 Jul 2017 04:53:01 +0000 (UTC) Original-Received: from [192.168.1.110] (125.85.192.178.dynamic.wline.res.cust.swisscom.ch [178.192.85.125]) by sinyavsky.aurox.ch (Postfix) with ESMTPSA id 2BF1E224BC; Fri, 21 Jul 2017 04:52:59 +0000 (UTC) X-Mailer: iPhone Mail (14F89) In-Reply-To: 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" Xref: news.gmane.org gmane.emacs.bugs:134813 Archived-At: --Apple-Mail-DD6BD835-36FB-4FFA-8201-EF8A8BD0237B Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable No worries, Denis. I'll give it another try later today. > On 21 Jul 2017, at 04:17, =D0=94=D0=B5=D0=BD=D0=B8=D1=81 =D0=A0=D0=B5=D0=B4= =D0=BE=D0=B7=D1=83=D0=B1=D0=BE=D0=B2 wrote: >=20 > Update: I've tried a few builds of emacs with John and I don't think I'll b= e able to extract any more useful information with lldb. To the best of my u= nderstanding it would be preferable if Charles would try to use instructions= from my previous email to try to reproduce the issue. >=20 > 2017-07-20 16:06 GMT-04:00 =D0=94=D0=B5=D0=BD=D0=B8=D1=81 =D0=A0=D0=B5=D0=B4= =D0=BE=D0=B7=D1=83=D0=B1=D0=BE=D0=B2 : >> That's a mistake on my part. Sorry for that, Charles. To have a proper de= velopment environment you can use this repo: https://github.com/jwiegley/dss= s17 The instructions are in the README file. We were able to determine with J= ohn it is definitely an infinite loop, but that's about it for now. We'll tr= y to provide more info today or tomorrow. >>=20 >> 2017-07-20 15:11 GMT-04:00 Eli Zaretskii : >>> > Cc: 27761@debbugs.gnu.org, Eli Zaretskii >>> > From: "Charles A. Roelli" >>> > Date: Thu, 20 Jul 2017 20:54:38 +0200 >>> > >>> > I can't do C-c C-RET successfully since it gives this error: >>> > >>> > Error: Cannot find library Metalib.Metatheory in loadpath >>> > >>> > and apparently that library requires a higher version of "coq", so >>> > maybe I'm out of luck here. I'm not sure if this was important. >>> > >>> > I still tried typing "intuition" + C-h around EOL line 166, but that >>> > worked fine (popping up the documentation buffer). >>> > >>> > I also tried adding to prettify-symbols-alist as discussed in the >>> > issue (and trying what was discussed there), and it worked OK. >>>=20 >>> Thank you for your efforts. >>>=20 >>> Denis, I guess this means the steps for reproducing need some >>> refinements, specifically more details about where to download the >>> add-on packages? >>=20 >=20 --Apple-Mail-DD6BD835-36FB-4FFA-8201-EF8A8BD0237B Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
No worries, Denis. I'll giv= e it another try later today.


On 21 Jul 2017, a= t 04:17, =D0=94=D0=B5=D0=BD=D0=B8=D1=81 =D0=A0=D0=B5=D0=B4=D0=BE=D0=B7=D1=83= =D0=B1=D0=BE=D0=B2 <denis.re= dozubov@gmail.com> wrote:

Update: I've tried a few builds of emacs with John and I d= on't think I'll be able to extract any more useful information with lldb. To= the best of my understanding it would be preferable if Charles would try to= use instructions from my previous email to try to reproduce the issue.

2017-07-20 16:06 G= MT-04:00 =D0=94=D0=B5=D0=BD=D0=B8=D1=81 =D0=A0=D0=B5=D0=B4=D0=BE=D0=B7=D1=83= =D0=B1=D0=BE=D0=B2 <denis.redozubov@gmail.com>:
That's a mistake on my part. Sor= ry for that, Charles. To have a proper development environment you can use t= his repo: https://github.com/jwiegley/dsss17 The instructions are in the R= EADME file. We were able to determine with John it is definitely an infinite= loop, but that's about it for now. We'll try to provide more info today or t= omorrow.

2017-07-20 15:11 GMT-04:00 Eli Zaretskii= <eli= z@gnu.org>:
> Cc: 27761@debbugs.gnu.org, E= li Zaretskii <eliz@gnu.= org>
> From: "Charles A. Roelli" <charles@aurox.ch>
> Date: Thu, 20 Jul 2017 20:54:38 +0200
>
> I can't do C-c C-RET successfully since it gives this error:
>
> Error: Cannot find library Metalib.Metatheory in loadpath
>
> and apparently that library requires a higher version of "coq", so
> maybe I'm out of luck here. I'm not sure if this was important.
>
> I still tried typing "intuition" + C-h around EOL line 166, but that > worked fine (popping up the documentation buffer).
>
> I also tried adding to prettify-symbols-alist as discussed in the
> issue (and trying what was discussed there), and it worked OK.

Thank you for your efforts.

Denis, I guess this means the steps for reproducing need some
refinements, specifically more details about where to download the
add-on packages?


= --Apple-Mail-DD6BD835-36FB-4FFA-8201-EF8A8BD0237B--