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

Previous Next

Full log

View this message in rfc822 format

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

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

Thanks.  In that case, could you please bisect your local configuration
until you find what causes the issue?



On 27.07.17 15:12, Денис Редозубов wrote:
> I don't think you've missed anything, Charles, it sounds exactly like 
> the way to reproduce it on my machine, the expected behavior would be 
> to see the documentation in a separate buffer.
>
>
> ср, 26 июля 2017 г. в 15:42, Charles A. Roelli <charles <at> aurox.ch 
> <mailto:charles <at> aurox.ch>>:
>
>     I have a build environment in macOS Sierra now, so I can try to get it
>     in GDB.
>
>     Denis: I have the requirements for the file installed (Metalib, Stlc).
>     I go to line 166 in Stlc/Lemmas.v, type C-c C-RET, type
>     'intuition', to
>     get this:
>
>     pose proof size_typ_min_mutual as H; intuition eauto.intuition
>
>     And then hit C-h.  I get no crash (no documentation popup shows
>     either, though).  Did I miss a step?
>
>
>
>     On 24.07.17 19:02, Eli Zaretskii wrote:
>     >> From: Glenn Morris <rgm <at> gnu.org <mailto:rgm <at> gnu.org>>
>     >> Cc: "Charles A. Roelli" <charles <at> aurox.ch
>     <mailto:charles <at> aurox.ch>>, 27761 <at> debbugs.gnu.org
>     <mailto:27761 <at> debbugs.gnu.org>, denis.redozubov <at> gmail.com
>     <mailto:denis.redozubov <at> gmail.com>
>     >> Date: Mon, 24 Jul 2017 12:58:49 -0400
>     >>
>     >> Is it impossible to "provide a minimal example starting from
>     emacs -Q"
>     >> for this issue?
>     > I still hope it will be possible.  Alternatively, if someone catches
>     > this in GDB, I can ask a few questions and probably understand
>     what's
>     > going on, the reason cannot be too complicated.
>     >
>     > TIA
>

[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.