From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: =?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?= Newsgroups: gmane.emacs.bugs Subject: bug#27761: Crash while using proof-general/company-coq on OS X Date: Thu, 20 Jul 2017 22:17:52 -0400 Message-ID: References: <83y3riapq2.fsf@gnu.org> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary="001a1130c07624e9a50554ca7a7d" X-Trace: blaine.gmane.org 1500603562 334 195.159.176.226 (21 Jul 2017 02:19:22 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 21 Jul 2017 02:19:22 +0000 (UTC) Cc: 27761@debbugs.gnu.org, "Charles A. Roelli" To: Eli Zaretskii Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Fri Jul 21 04:19:14 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 1dYNX7-0007sI-9f for geb-bug-gnu-emacs@m.gmane.org; Fri, 21 Jul 2017 04:19:13 +0200 Original-Received: from localhost ([::1]:40649 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dYNX9-0001Xj-IC for geb-bug-gnu-emacs@m.gmane.org; Thu, 20 Jul 2017 22:19:15 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33711) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dYNWz-0001XS-RP for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 22:19:07 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dYNWw-0003eV-MQ for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 22:19:05 -0400 Original-Received: from debbugs.gnu.org ([208.118.235.43]:47502) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dYNWw-0003e2-IR for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 22:19:02 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dYNWv-00075r-Na for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 22:19:02 -0400 X-Loop: help-debbugs@gnu.org Resent-From: =?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-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Fri, 21 Jul 2017 02:19: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.150060350027220 (code B ref 27761); Fri, 21 Jul 2017 02:19:01 +0000 Original-Received: (at 27761) by debbugs.gnu.org; 21 Jul 2017 02:18:20 +0000 Original-Received: from localhost ([127.0.0.1]:50179 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYNWF-00074x-MC for submit@debbugs.gnu.org; Thu, 20 Jul 2017 22:18:19 -0400 Original-Received: from mail-ua0-f172.google.com ([209.85.217.172]:37076) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYNWE-00074k-Gu for 27761@debbugs.gnu.org; Thu, 20 Jul 2017 22:18:19 -0400 Original-Received: by mail-ua0-f172.google.com with SMTP id f9so36146412uaf.4 for <27761@debbugs.gnu.org>; Thu, 20 Jul 2017 19:18:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=EAjBYt+jwNlIZhEk/h3hPjTKd83G3lD0LW9804uQpaI=; b=WOJZQY25Yyh4TL/XD05Fr5Bg5PSf9KpZmgVMX7R1plkksqYA4jVdG/W/OwBYBybK8S h0paeJkTLZGOO/m11HSUkbmVq92Cthed85YWOBNkIw4TJRrVqET7l4NZFVJsiMnXRAiE +qtja+bAuE5I0AtluyC45AyYvlM22gY2ePqRjMIRT+vxvzcePwtq34Em88jmbiSnV+XV q2DNRvSiDt1PIBDH7/WCDYnfvIWr6kvkv+IwTamkM4pdv6PYsHVG6EriFDS15zCfJZOV jMBw7SJ3CrnrOMqxOGP+PhPq6bs6cXDrbG9whfv3aeGSvJs6AKsTHXNQhkBdK2/dS5lB OXvQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:sender:in-reply-to:references:from :date:message-id:subject:to:cc; bh=EAjBYt+jwNlIZhEk/h3hPjTKd83G3lD0LW9804uQpaI=; b=Dv6P1L191YJHKwIoBZMsb7sVGUId2OgOA0PorVoZfDeNVkY4EBxu/1LgtBKwI1mon1 TpTPvoHeR8+k74lKlVwmdve5AqTFvdlPD4do6la2ZL9YwcsAgkilcToDqCsMK+zonxjg gIY1cdk+I7UbuDx2zVlIDY303TIIs4b5veAtY6anoz7/kMQNivQ3nHkE5WxZRiDAmxl0 O2alDm+wikTPCuGRr8wewyZTL/2R/oXzkS7w2sm2j/Q64upMYeYpby3CJMhKSL28ydjS ztOMnYM8M3CrRdAwR+Twhb9CPOvzQ51cG0ctVSzYldUgHSJq3e38WqWoyiRRJaxg31yz Twqg== X-Gm-Message-State: AIVw113zjb+jfGlDW2VSkDW9Q+EDz8xUhNagIQ6d4gyzgXV0+9T+WMS6 mDnk2xAj3PuuNHGkzecpUFmnBpeyQDET X-Received: by 10.31.33.20 with SMTP id h20mr2665694vkh.190.1500603492917; Thu, 20 Jul 2017 19:18:12 -0700 (PDT) Original-Received: by 10.159.33.150 with HTTP; Thu, 20 Jul 2017 19:17:52 -0700 (PDT) In-Reply-To: X-Google-Sender-Auth: 99lh_lFwk4f1mPe8OtJRYeshO60 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:134806 Archived-At: --001a1130c07624e9a50554ca7a7d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Update: I've tried a few builds of emacs with John and I don'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 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 > development environment you can use this repo: https://github.com/ > jwiegley/dsss17 The instructions are in the README file. We were able to > determine with John it is definitely an infinite loop, but that's about i= t > for now. We'll try to provide more info today or tomorrow. > > 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. >> >> 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? >> > > --001a1130c07624e9a50554ca7a7d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Update: I've tried a few builds of emacs with John and= I don'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 Charle= s would try to use instructions from my previous email to try to reproduce = the issue.

2= 017-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 <denis.redozubov@gmail.com>:
That's= a mistake on my part. Sorry for that, Charles. To have a proper developmen= t environment you can use this repo:=C2=A0https://github.com/jwiegley/dsss17= The instructions are in the README file. We were able to determine with Jo= hn it is definitely an infinite loop, but that's about it for now. We&#= 39;ll try to provide more info today or tomorrow.

2017-07-20 15:11 GMT-04:00 Eli Zaretskii <eliz@gnu.org>:
=
> Cc: 27761@debbugs.gnu.org, Eli 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&quo= t;, 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?


--001a1130c07624e9a50554ca7a7d--