Subject: bug#27761: Crash while using proof-general/company-coq on OS X

From: "Charles A. Roelli" <[email-masked]>
Date: Fri, 21 Jul 2017 20:43:06 +0200

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 Денис Редозубов <[email-masked] 
> <mailto:[email-masked]>>:
>
>     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 <[email-masked]
>     <mailto:[email-masked]>>:
>
>         > Cc: [email-masked] <mailto:[email-masked]>, Eli
>         Zaretskii <[email-masked] <mailto:[email-masked]>>
>         > From: "Charles A. Roelli" <[email-masked]
>         <mailto:[email-masked]>>
>         > 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?
>
>
>