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

From: "Charles A. Roelli" <[email-masked]>
Date: Fri, 28 Jul 2017 20:48:17 +0200

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 <[email-masked] 
> <mailto:[email-masked]>>:
>
>     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 <[email-masked] <mailto:[email-masked]>>
>     >> Cc: "Charles A. Roelli" <[email-masked]
>     <mailto:[email-masked]>>, [email-masked]
>     <mailto:[email-masked]>, [email-masked]
>     <mailto:[email-masked]>
>     >> 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
>