From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: "Charles A. Roelli" Newsgroups: gmane.emacs.bugs Subject: bug#27761: Crash while using proof-general/company-coq on OS X Date: Wed, 26 Jul 2017 21:42:30 +0200 Message-ID: <127db243-cb9b-c89b-ad40-35feb7a513bf@aurox.ch> References: <83y3riapq2.fsf@gnu.org> <94196959-2ede-273d-6bc3-a8f214b128e0@aurox.ch> <83lgnha9kv.fsf@gnu.org> <83pocp7ope.fsf@gnu.org> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1501098195 27985 195.159.176.226 (26 Jul 2017 19:43:15 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Wed, 26 Jul 2017 19:43:15 +0000 (UTC) Cc: 27761@debbugs.gnu.org, denis.redozubov@gmail.com To: Eli Zaretskii , Glenn Morris Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Wed Jul 26 21:43:10 2017 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1daSD6-0006vf-UE for geb-bug-gnu-emacs@m.gmane.org; Wed, 26 Jul 2017 21:43:09 +0200 Original-Received: from localhost ([::1]:39730 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1daSDC-0003kV-OA for geb-bug-gnu-emacs@m.gmane.org; Wed, 26 Jul 2017 15:43:14 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:40450) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1daSD4-0003ih-F4 for bug-gnu-emacs@gnu.org; Wed, 26 Jul 2017 15:43:07 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1daSD0-0000SP-DG for bug-gnu-emacs@gnu.org; Wed, 26 Jul 2017 15:43:06 -0400 Original-Received: from debbugs.gnu.org ([208.118.235.43]:55014) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1daSD0-0000SD-AH for bug-gnu-emacs@gnu.org; Wed, 26 Jul 2017 15:43:02 -0400 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1daSCz-0007PQ-QM for bug-gnu-emacs@gnu.org; Wed, 26 Jul 2017 15:43:01 -0400 X-Loop: help-debbugs@gnu.org Resent-From: "Charles A. Roelli" Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Wed, 26 Jul 2017 19:43:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 27761 X-GNU-PR-Package: emacs X-GNU-PR-Keywords: Original-Received: via spool by 27761-submit@debbugs.gnu.org id=B27761.150109816528458 (code B ref 27761); Wed, 26 Jul 2017 19:43:01 +0000 Original-Received: (at 27761) by debbugs.gnu.org; 26 Jul 2017 19:42:45 +0000 Original-Received: from localhost ([127.0.0.1]:57691 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1daSCi-0007Ow-RO for submit@debbugs.gnu.org; Wed, 26 Jul 2017 15:42:45 -0400 Original-Received: from sinyavsky.aurox.ch ([37.35.109.145]:45646) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1daSCg-0007Oh-6k for 27761@debbugs.gnu.org; Wed, 26 Jul 2017 15:42:42 -0400 Original-Received: from sinyavsky.aurox.ch (sinyavsky.aurox.ch [127.0.0.1]) by sinyavsky.aurox.ch (Postfix) with ESMTP id 26F61224D0 for <27761@debbugs.gnu.org>; Wed, 26 Jul 2017 19:37:11 +0000 (UTC) Authentication-Results: sinyavsky.aurox.ch (amavisd-new); dkim=pass (1024-bit key) reason="pass (just generated, assumed good)" header.d=aurox.ch DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=aurox.ch; h= content-transfer-encoding:content-type:content-type:in-reply-to :mime-version:date:date:message-id:from:from:references:to :subject:subject; s=dkim; t=1501097828; x=1501961829; bh=67LntNG 6Qy5ILvzAAJt6WqoE+VSVAzIBqUsQSUxqhaM=; b=MA1+pvuWjdOc2VI2DfxBY55 8jS8zffrRx/bzZ2ja9fBLOKRwx5Uwo3PWoMDPge9m8FHuIeVd3nCXeidgif9Jw7H as3DboVgDcJy+TEEE1AMXN3nQOOOxcSEPU3N1nN7jIYKhpQAUEcV9H4FNkw3ETuT d7Wrg/JtUSzTx+8pW4q4= X-Virus-Scanned: Debian amavisd-new at test.virtualizor.com Original-Received: from sinyavsky.aurox.ch ([127.0.0.1]) by sinyavsky.aurox.ch (sinyavsky.aurox.ch [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id F2yIGqzwwopA for <27761@debbugs.gnu.org>; Wed, 26 Jul 2017 19:37:08 +0000 (UTC) Original-Received: from Charless-Device.local (125.85.192.178.dynamic.wline.res.cust.swisscom.ch [178.192.85.125]) by sinyavsky.aurox.ch (Postfix) with ESMTPSA id 12805224A1; Wed, 26 Jul 2017 19:37:06 +0000 (UTC) In-Reply-To: <83pocp7ope.fsf@gnu.org> X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 208.118.235.43 X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "bug-gnu-emacs" Xref: news.gmane.org gmane.emacs.bugs:135030 Archived-At: 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 >> Cc: "Charles A. Roelli" , 27761@debbugs.gnu.org, denis.redozubov@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