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

Previous Next

Full log

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

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

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

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 <at> gnu.org>:

> > Cc: 27761 <at> debbugs.gnu.org, Eli Zaretskii <eliz <at> gnu.org>
> > From: "Charles A. Roelli" <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.