From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id 9pdxNvMnUWFWDgAAgWs5BA (envelope-from ) for ; Mon, 27 Sep 2021 04:09:55 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id UD58MfMnUWERVAAAbx9fmQ (envelope-from ) for ; Mon, 27 Sep 2021 02:09:55 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id DAD0AC5E7 for ; Mon, 27 Sep 2021 04:09:54 +0200 (CEST) Received: from localhost ([::1]:32954 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mUg5Y-0002tc-Bm for larch@yhetil.org; Sun, 26 Sep 2021 22:09:52 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:39054) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mUg5K-0002tT-PS for help-guix@gnu.org; Sun, 26 Sep 2021 22:09:38 -0400 Received: from mail1.g12.pair.com ([66.39.4.99]:64559) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mUg5I-0007qx-LF for help-guix@gnu.org; Sun, 26 Sep 2021 22:09:38 -0400 Received: from mail1.g12.pair.com (localhost [127.0.0.1]) by mail1.g12.pair.com (Postfix) with ESMTP id B0AF473115; Sun, 26 Sep 2021 22:09:34 -0400 (EDT) Received: from smtpclient.apple (pw126247013169.14.panda-world.ne.jp [126.247.13.169]) (using TLSv1.3 with cipher TLS_AES_128_GCM_SHA256 (128/128 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mail1.g12.pair.com (Postfix) with ESMTPSA id 7EF64730AF; Sun, 26 Sep 2021 22:09:34 -0400 (EDT) Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable From: Yasuaki Kudo Mime-Version: 1.0 (1.0) Subject: Re: how to use Proof General? Date: Mon, 27 Sep 2021 11:09:32 +0900 Message-Id: References: <20210926230258.27922a8b@riseup.net> In-Reply-To: <20210926230258.27922a8b@riseup.net> To: raingloom X-Mailer: iPhone Mail (18H17) Received-SPF: none client-ip=66.39.4.99; envelope-from=yasu@yasuaki.com; helo=mail1.g12.pair.com X-Spam_score_int: -25 X-Spam_score: -2.6 X-Spam_bar: -- X-Spam_report: (-2.6 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_DNSWL_LOW=-0.7, SPF_HELO_NONE=0.001, SPF_NONE=0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: help-guix@gnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Cc: help-guix@gnu.org Errors-To: help-guix-bounces+larch=yhetil.org@gnu.org Sender: "Help-Guix" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1632708595; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references:list-id:list-help: list-unsubscribe:list-subscribe:list-post; bh=e861tOKm75YEc/Szw51sT/3SOBu+Q6M09E9fZ2oWLgg=; b=EqakzgNZvCAVJg5/hIqYJtGmim9J+0gDvhLrkJDxmyAPGN0GAZFfMiAmgWIoSR8XCEP+GB N7eoUiVpVfLs3Vx3WOCnwPi9EDs91iFfwpz9KCH1izEVoC2s+jfEjegM6uzM8svw6P1yGF rLkO6Qzl1AzTnlkn0Nh0Yh9usyWfH8MrgsBgoS14vwB5j5+NpOpsdXY443v3oNV34GsFCU Lx4OMPLEQ7Nzk5mGjSUXU3dTuhK+xZ78uOHn+LqaVE+765MaOLrFn08LArgCHFPFVO2n63 ug1eYo+xOKt+n+ZrBPXQd3xVYvnq9mfkV1z8G0Tk16UeDcwtcgi5XR1yk1pVcg== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1632708595; a=rsa-sha256; cv=none; b=nsEjKgZjjNv7uCqDZZcUiri6vzK54G5BJCFxcKK+vt+7BZGnzZjbKT/Un8xgHzIR2Li9/w UnEHX0oxeCQM3QP76/oVOtr5HQu8V8vF3V1oBqrhiFrvrR1QjcU8UaoJck75FXrWGPGWvB B04BANPNuiF6rSbveweFLVPbsjw0b3jWvvAwvKf0FZtdS665Db2qF6w3clFu5RlK46djVw 20HrNDeSPc8XW5teoYwnCsU/Nm1jfZ7R/u8/W6GyT5KNcGu/pXgMqXvWJDWes/cPujE5JA GChKrZpcq45fi4Nu+f9bW5VYp8I6lGE1Qtb+9FaUzrmg75zVo9sykKQ7Fbfd0A== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; spf=pass (aspmx1.migadu.com: domain of help-guix-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=help-guix-bounces@gnu.org X-Migadu-Spam-Score: -0.89 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=none; spf=pass (aspmx1.migadu.com: domain of help-guix-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=help-guix-bounces@gnu.org X-Migadu-Queue-Id: DAD0AC5E7 X-Spam-Score: -0.89 X-Migadu-Scanner: scn0.migadu.com X-TUID: igwg2gc0zlb5 Hi! I did this just last night so let me tell you what I did. I installed using guix install command emacs, coq and proof-general but in t= he end I probably could not observe that proof-general was working from the G= uix installation so I followed the standard installation instruction on Proo= f General homepage , which is an instruction of how to do so with MELPA. =F0= =9F=98=84 I didn't spend much time examining whether proof-genetal from Guix was worki= ng or not... -Yasu > On Sep 27, 2021, at 10:07, raingloom wrote: >=20 > =EF=BB=BFHi! >=20 > I'm trying to use Proof General with Emacs, but so far I couldn't > figure out a way to launch it. Running guix environment `--ad-hoc > proof-general emacs coq emacs-company-coq -- emacs scratchpad.v` > results in Verilog mode being started and when I try to manually launch > coq-mode with M-x, it's not even there. >=20 > I'm running packages from a few days ago. >=20 > Given how many Coq packages we have, I assume someone is in fact using > them. Or that at least they worked at some point. >=20 > Am I missing something obvious? I'm not exactly an Emacs or Coq expert, > but so far I haven't had trouble with Emacs modules in ad-hoc > environments and I managed to run Coq IDE before. > Or is there a bug in how proof-general is packaged? >=20