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: Eli Zaretskii <eliz <at> gnu.org>
To: YAMAMOTO Mitsuharu <mituharu <at> math.s.chiba-u.ac.jp>
Cc: 27761 <at> debbugs.gnu.org, charles <at> aurox.ch, denis.redozubov <at> gmail.com
Subject: bug#27761: Crash while using proof-general/company-coq on OS X
Date: Thu, 03 Aug 2017 19:18:20 +0300

> Date: Thu, 03 Aug 2017 17:36:49 +0900
> From: YAMAMOTO Mitsuharu <mituharu <at> math.s.chiba-u.ac.jp>
> Cc: 27761 <at> debbugs.gnu.org, "Charles A. Roelli" <charles <at> 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).

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.