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 16:06:55 -0400 Message-ID: References: <83y3riapq2.fsf@gnu.org> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary="f403043c4b248a667b0554c54bbd" X-Trace: blaine.gmane.org 1500581300 18342 195.159.176.226 (20 Jul 2017 20:08:20 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 20 Jul 2017 20:08:20 +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 Thu Jul 20 22:08: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 1dYHk0-0004Ai-BJ for geb-bug-gnu-emacs@m.gmane.org; Thu, 20 Jul 2017 22:08:08 +0200 Original-Received: from localhost ([::1]:39799 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dYHk5-0005jt-OS for geb-bug-gnu-emacs@m.gmane.org; Thu, 20 Jul 2017 16:08:13 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:37336) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dYHjx-0005i0-Er for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 16:08:06 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dYHju-0005dz-8M for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 16:08:05 -0400 Original-Received: from debbugs.gnu.org ([208.118.235.43]:47390) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dYHju-0005dq-4a for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 16:08:02 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dYHjt-0006n5-Of for bug-gnu-emacs@gnu.org; Thu, 20 Jul 2017 16:08:01 -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: Thu, 20 Jul 2017 20:08: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: moreinfo Original-Received: via spool by 27761-submit@debbugs.gnu.org id=B27761.150058124426055 (code B ref 27761); Thu, 20 Jul 2017 20:08:01 +0000 Original-Received: (at 27761) by debbugs.gnu.org; 20 Jul 2017 20:07:24 +0000 Original-Received: from localhost ([127.0.0.1]:50067 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYHjI-0006mA-43 for submit@debbugs.gnu.org; Thu, 20 Jul 2017 16:07:24 -0400 Original-Received: from mail-ua0-f173.google.com ([209.85.217.173]:36992) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dYHjF-0006lx-NK for 27761@debbugs.gnu.org; Thu, 20 Jul 2017 16:07:23 -0400 Original-Received: by mail-ua0-f173.google.com with SMTP id f9so31444549uaf.4 for <27761@debbugs.gnu.org>; Thu, 20 Jul 2017 13:07:21 -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=D5M/a1PBDiJlZ8cQHJYK34icwD8O+7AkBBBlM3OD9Wk=; b=CEicv94EqA6xBZPoULU6KHRrGB/+TqtnaNA1iRk7+oi+fvf0zGoImb1rScG4bwi+us Ii2dleOw04mD2DRDmnvvSeW9jtnwl7aNIsNSMoZOjUDTM6UJhg0UQgSgYpB5Gf44+fPk 24w07LoRoQbNQ5xW/eSlqHFtF3yz2C9nkD/9F5U0jAQjdsPx2uI58Y0FLmKQAZEUDE6n rDNRhHTCaA/LsOobCeuGB0yDrTZqGmP6JDj8/Sh6+xCwmd+5nESqT7ghAPbc6z+UlzLN GsQN4U1I3rvDncV55xNTv2UoXcGGfAgYQzuPUStild/N4OgXjlMaD0JeE9RS4IUQUD6O AIfQ== 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=D5M/a1PBDiJlZ8cQHJYK34icwD8O+7AkBBBlM3OD9Wk=; b=oFY0Yg5jp5JcvM3Zqqzk4Gol3dVl2xWjf+daxBTr9SznAPXcAD0KxVgSNwkQH9nqW4 t0eG63+ukSqdghwht0GeLlASHjXYrGLhu7G2VJ2D85xNW32qg1bOrhqn2LCmdLv7MxhL xK4vgcvGmYXBv7brLfS9kMXU+zFRBC3BR/vfjW0BS9vvBjGRTi1hYULdzxVgblSHMpND OMTeLGH+Xmsedb07CWJ1YGwgI2yILJpWO1rytcFeGlVDaGtmXvCbEQlGkusj/7q0sPCB hSSGJM/w7kSJRk1jKvUGHDiwaIe3tw2tkYIcXPx5SFIH/3y2x4eg57/UjjAih3jYCNBD x0/w== X-Gm-Message-State: AIVw113afI6OioMwoVtofSPxMGYR9vnPn6dXlri08e2UgD/XV+KhwBOS 9LltvO0nTp3+HxJhiN+tGb9z/3iTCQ== X-Received: by 10.176.77.96 with SMTP id k32mr2397045uag.39.1500581236201; Thu, 20 Jul 2017 13:07:16 -0700 (PDT) Original-Received: by 10.159.33.150 with HTTP; Thu, 20 Jul 2017 13:06:55 -0700 (PDT) In-Reply-To: <83y3riapq2.fsf@gnu.org> X-Google-Sender-Auth: jkxTpoQiANf4_Bk5JTKap_RUlp8 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:134798 Archived-At: --f403043c4b248a667b0554c54bbd Content-Type: text/plain; charset="UTF-8" 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 it 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? > --f403043c4b248a667b0554c54bbd Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
That's a mistake on my part. Sorry for that, Charles. = To have a proper development environment you can use this repo:=C2=A0https://github.com/jwiegley/dsss17= The instructions are in the README file. We were able to determine wit= h John it is definitely an infinite loop, but that's about it for now. = We'll try to provide more info today or tomorrow.

2017-07-20 15:11 GMT-04:00 Eli Za= retskii <eliz@gnu.org>:
> Cc= : 27761@debbugs.gnu.org, Eli Z= aretskii <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?

--f403043c4b248a667b0554c54bbd--