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

[Eli Zaretskii]

> Date: Thu, 03 Aug 2017 17:36:49 +0900
> From: YAMAMOTO Mitsuharu <mituharu@math.s.chiba-u.ac.jp>
> Cc: 27761@debbugs.gnu.org, "Charles A. Roelli" <charles@aurox.ch>
> 
> Finally, I could reproduce the crash by this example with my own
> installation of Coq, Proof General, and Company-Coq on macOS 10.12.

Great, thanks for trying.

> The recent post on gdb session implies it has something to do with the
> string " 163" and overlays.  The key point to reproduce it was to turn
> on linum-mode.  Without linum-mode, the above procedure did not crash.

Yes, I guess 163 is the line number?

The problem has to do with something that prevents the display engine
to pop the iterator state from the stack when it reaches the end of a
Lisp string (" 163") which it needs to display.  I'm trying to
understand why this happens, my guess is that some condition somewhere
is not working as expected, perhaps because the display of the string
specifies padding with blanks (or so it seems).