From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Philip Kaludercic Newsgroups: gmane.emacs.help Subject: Re: Major mode for coq Date: Sun, 05 May 2024 16:59:24 +0000 Message-ID: <87le4o5h5f.fsf@posteo.net> References: Mime-Version: 1.0 Content-Type: text/plain Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="5823"; mail-complaints-to="usenet@ciao.gmane.io" Cc: Stefan Monnier , help-gnu-emacs@gnu.org To: Heime Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Sun May 05 18:59:57 2024 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1s3fDR-0001HV-C7 for geh-help-gnu-emacs@m.gmane-mx.org; Sun, 05 May 2024 18:59:57 +0200 Original-Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1s3fD1-0006e3-1w; Sun, 05 May 2024 12:59:31 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1s3fCz-0006dr-AI for help-gnu-emacs@gnu.org; Sun, 05 May 2024 12:59:29 -0400 Original-Received: from mout01.posteo.de ([185.67.36.65]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1s3fCx-0007Yf-KI for help-gnu-emacs@gnu.org; Sun, 05 May 2024 12:59:29 -0400 Original-Received: from submission (posteo.de [185.67.36.169]) by mout01.posteo.de (Postfix) with ESMTPS id 97D7B24002B for ; Sun, 5 May 2024 18:59:25 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=posteo.net; s=2017; t=1714928365; bh=8SHEDQ/hSQmv4O1jpyTSfqOtWnFXcQZO46Xyh6WgJWM=; h=From:To:Cc:Subject:Date:Message-ID:MIME-Version:Content-Type: From; b=lc6geK3HCY5wEND7y6ZsFCs6JiAAxr/s2wSSx3SrIDJRY84O71qJRKoC1Ym+x5fj7 aLEa0LfBKRA8DILFmtHfVL3c5xSFNkL5dvi/MXDKy2PxbE9GHLGKMf22hL19VM+me7 REGTMm40mJPitMTqXqeAVppRHc54Dd9df6r3GytMclWZPVGcTm9yIZDIUoGsyyVik+ ZSw/FffLK7ivf56fc9iHPWowvr+7QERcva6RY/nk6xyTJDITYIIXleOfYG5pAlarFC /QApKG5dT5CkRY9PxnKW/UZW30LUZ4acEOGlMSoovE39SUMQ3OVcA97OL4wHMeakxq hYoMIlHaDnq8g== Original-Received: from customer (localhost [127.0.0.1]) by submission (posteo.de) with ESMTPSA id 4VXW3c6R4dz6trs; Sun, 5 May 2024 18:59:24 +0200 (CEST) In-Reply-To: (Heime's message of "Sun, 05 May 2024 16:43:05 +0000") X-Hashcash: 1:20:240505:heimeborgia@protonmail.com::weJ1lPO+llZvDBNK:1HuI X-Hashcash: 1:20:240505:monnier@iro.umontreal.ca::TJDGGjWi3Lmo4gGu:5/SC X-Hashcash: 1:20:240505:help-gnu-emacs@gnu.org::Y9XXU7K9po5LWX76:5bSI Received-SPF: pass client-ip=185.67.36.65; envelope-from=philipk@posteo.net; helo=mout01.posteo.de X-Spam_score_int: -43 X-Spam_score: -4.4 X-Spam_bar: ---- X-Spam_report: (-4.4 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_DNSWL_MED=-2.3, RCVD_IN_MSPIKE_H3=-0.01, RCVD_IN_MSPIKE_WL=-0.01, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Xref: news.gmane.io gmane.emacs.help:146561 Archived-At: Heime writes: > Sent with Proton Mail secure email. > > On Monday, May 6th, 2024 at 1:51 AM, Stefan Monnier via Users list for > the GNU Emacs text editor wrote: > >> > Is there any major mode for coq formal proof management system files ? >> >> >> I don't know what you mean by "system files", but there's a coq-mode as >> part of Proof-General (available in NonGNU ELPA). - Stefan > > Right. But I was hoping to see something that we are all familiar with. > Open the file with a coq-mode without the interface of "Proof General". > Just see some highlighting and some tools for the file type, as one gets > with elisp, c, and fortran. Currently the language highlighting only > gets activated as a proof general feature. It goes much beyond just showing > the contents of the file. Proof-general includes a coq-mode, and there is a user option `coq-use-pg' that can disable integration with Proof General (but usually you don't want that, since having the interaction with the Coq system is what makes working with Coq in Emacs interesting). -- Philip Kaludercic on icterid