GNU bug report logs - #27761
Crash while using proof-general/company-coq on OS X

Previous Next

Full log

Message #68 received at 27761 <at> debbugs.gnu.org (full text, mbox):

From: "Charles A. Roelli" <charles <at> aurox.ch>
To: Денис Редозубов
 <denis.redozubov <at> gmail.com>, Eli Zaretskii <eliz <at> gnu.org>
Cc: 27761 <at> debbugs.gnu.org
Subject: Re: bug#27761: Crash while using proof-general/company-coq on OS X
Date: Fri, 21 Jul 2017 20:43:06 +0200

[Message part 1 (text/plain, inline)]

It seems that "nix" is needed to install the dependencies, and
unfortunately the install script for Nix gives this:

/var/folders/WP/WPe0Q1iAGc0J7iI6J50jcU+++TI/-Tmp-/nix-binary-tarball-unpack.XXXXXXXXXX.LkgYaFZk/unpack/nix-1.11.13-x86_64-darwin/install:
macOS 10.6.8 is not supported, upgrade to 10.10 or higher

So maybe it would be better if somebody with a higher version of macOS
could try to reproduce this issue.  If not I can still try it
eventually, but it might have to wait some time.



On 21/07/2017 04:17, Денис Редозубов wrote:
> 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 Денис Редозубов <denis.redozubov <at> gmail.com 
> <mailto:denis.redozubov <at> gmail.com>>:
>
>     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
>     <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 <eliz <at> gnu.org
>     <mailto:eliz <at> gnu.org>>:
>
>         > Cc: 27761 <at> debbugs.gnu.org <mailto:27761 <at> debbugs.gnu.org>, Eli
>         Zaretskii <eliz <at> gnu.org <mailto:eliz <at> gnu.org>>
>         > From: "Charles A. Roelli" <charles <at> aurox.ch
>         <mailto:charles <at> 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?
>
>
>

[Message part 2 (text/html, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.