From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id oPvjIG8ZUWHNfwEAgWs5BA (envelope-from ) for ; Mon, 27 Sep 2021 03:07:59 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0 with LMTPS id +DKkHG8ZUWF7AQAA1q6Kng (envelope-from ) for ; Mon, 27 Sep 2021 01:07:59 +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 7ADB932696 for ; Mon, 27 Sep 2021 03:07:58 +0200 (CEST) Received: from localhost ([::1]:52552 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mUf7d-0001xm-Kt for larch@yhetil.org; Sun, 26 Sep 2021 21:07:57 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:57278) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mUf7T-0001xU-3e for help-guix@gnu.org; Sun, 26 Sep 2021 21:07:47 -0400 Received: from mx1.riseup.net ([198.252.153.129]:53240) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mUf7R-0000Qg-0u for help-guix@gnu.org; Sun, 26 Sep 2021 21:07:46 -0400 Received: from fews2.riseup.net (fews2-pn.riseup.net [10.0.1.84]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256 client-signature RSA-PSS (2048 bits) client-digest SHA256) (Client CN "fews2.riseup.net", Issuer "R3" (not verified)) by mx1.riseup.net (Postfix) with ESMTPS id 4HHkyQ6t6czDy5c for ; Sun, 26 Sep 2021 18:07:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak; t=1632704863; bh=WkYhYlwESXAk7ziL3gJPZnBkY9cTNge9xReMK324DaU=; h=Date:From:To:Subject:From; b=C3owyZBXtzyZ9JFiPsQX1qshefL206WpO2f4BjTypKFdUO148byc/HzLXoZjI4uF3 FD09u2KYDqzKjESy6g3scpcBaVzmI/nIIlJBpFaH92gK6wm5px/vSBnLAyGNMh8HUL SzSOzARNa5UWex2Ilqys9Gh2CfQA9Srt0G7rE+xU= X-Riseup-User-ID: C474123C9C080B862A142B1FBAEECA49F0A8393BE4D56A28B00F49BBC2755A98 Received: from [127.0.0.1] (localhost [127.0.0.1]) by fews2.riseup.net (Postfix) with ESMTPSA id 4HHkyQ1k2dz1yVr for ; Sun, 26 Sep 2021 18:07:41 -0700 (PDT) Date: Sun, 26 Sep 2021 23:02:58 +0000 From: raingloom To: "help-guix@gnu.org" Subject: how to use Proof General? Message-ID: <20210926230258.27922a8b@riseup.net> MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Received-SPF: pass client-ip=198.252.153.129; envelope-from=raingloom@riseup.net; helo=mx1.riseup.net X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 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_LOW=-0.7, RCVD_IN_MSPIKE_H3=-0.01, RCVD_IN_MSPIKE_WL=-0.01, SPF_HELO_PASS=-0.001, SPF_PASS=-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: , 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=1632704879; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=WkYhYlwESXAk7ziL3gJPZnBkY9cTNge9xReMK324DaU=; b=RWqwsGbM8y4RmYo4EE3TSGaA0nbL5RDHjKMlwP0hkCUBAVDCy3Fyhrags8jMefL9he599h +5oQZtGkakMTTEHwnyS1tn+kbxryCHOBafJUpYsjGZhZZTY8MmvrRkid+J9YP4AG2zHQ8Y MSye+7nROfDXanMdEkwj4Ms0yfY19GXKCzrPIFtjOJtAF3OUql+cg1X/4YsAPSgIrWdAZr 0U5Ky7+m3+/EdP7N41z6rwNtEm1mPw4xJZl11MV1mzKIBveeo1oKwXeBvX+opDb0j+TBSH C20Yd3OL/wfKzrQXiIZhJrzKsDd+EwdI4XoBeuXUSO7PCTZb4BXbkpBmogzpiA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1632704879; a=rsa-sha256; cv=none; b=jVATxU+v8nnFBfJHOZXh6GUrjGuIjIbc78xLIKeYCPk+QQLSxb5gck4riA9c+Jv/u2EXVy zmQUfImj+BD8FuItliDChRVrEPckqaU+jo7nOChnTYWPHDYd1silpr31rb+U30Wlgy3LvB iiUmYmOvYDPJ1Y/suzcWpyjWuccirV5XnNXsbDANX7pU6F5AITRtinno4eN4YruhV6yW4E j0OekW1kiYxe5Hk5sBC/qkeQwiFO+rpI9aDvxDZoyZSIJsScIaGYzilY188Nu3/dDzfoqC cfE3lVii9ZJ8iKNzwRLR+UqnhHYc6AnWyltPuvBheX7F+0WqH4IjjqE5IVeI6Q== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=riseup.net header.s=squak header.b=C3owyZBX; 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: -2.09 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=riseup.net header.s=squak header.b=C3owyZBX; dmarc=pass (policy=none) header.from=riseup.net; 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: 7ADB932696 X-Spam-Score: -2.09 X-Migadu-Scanner: scn0.migadu.com X-TUID: SSctO1DF71Pz Hi! 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. I'm running packages from a few days ago. Given how many Coq packages we have, I assume someone is in fact using them. Or that at least they worked at some point. 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?