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

[Charles A. Roelli]

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@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 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@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", 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?