From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id wPuXGp6xUWHQIwEAgWs5BA (envelope-from ) for ; Mon, 27 Sep 2021 13:57:18 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id MGA7Fp6xUWEgIQAAB5/wlQ (envelope-from ) for ; Mon, 27 Sep 2021 11:57:18 +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 AF79F15FDB for ; Mon, 27 Sep 2021 13:57:17 +0200 (CEST) Received: from localhost ([::1]:36200 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mUpFy-0004pI-Th for larch@yhetil.org; Mon, 27 Sep 2021 07:57:15 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:55886) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mUpFd-0004p7-Mj for help-guix@gnu.org; Mon, 27 Sep 2021 07:56:54 -0400 Received: from mail-qv1-xf33.google.com ([2607:f8b0:4864:20::f33]:40619) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mUpFY-0001VU-SX for help-guix@gnu.org; Mon, 27 Sep 2021 07:56:50 -0400 Received: by mail-qv1-xf33.google.com with SMTP id n6so2698262qvp.7 for ; Mon, 27 Sep 2021 04:56:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=D2tO6QDdTFoidzvVTs6+QWlMn/Ezx07IRS85XnCGzvw=; b=hj88JInUyNyiUzsRP3EPH2foLK50yO8zF2NQlw0KIwV4Dff7dy7Ru2J/uEv406+msO rptEC4hBLvZTVRgqhLLq7mm6w8d3yzyOUNb8ganoPiqxkfyS/ZT8U7Ej0a/FZctXaBNq oZDl1ntYjjFK8iJGfhhWmMfNint6WfSfebyyaXMDiVbfaHV5TkK++D22MfJj9WLwA/h3 I1PRVq8ia8FskuSNwGZ/CxHD32MOO7lJh6MDdSBmWjlJb7WqDjM3XbRdfkL/3vPOaxH6 DFP6YlXBEAzFBm3zq3In9bqugnePTpwiHQO/w5XOJbUXwZh+7Wcezipf/W9PtuKa52CQ guEQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=D2tO6QDdTFoidzvVTs6+QWlMn/Ezx07IRS85XnCGzvw=; b=03dMdw9oswXmHBNvPPPN6ohvG2JAFnSTqtdRPz/F6tRAN/F3YVsqZDiO/W/4q42unY TFCfFpqKeO75CMTHrCrZKOh1z00VNhfI2G++9qcsBPMZxi8tE6GPlO8doZBaUJ7xp3nI bWdevpCP1eOvwia4HOnnW7PIwmWL9uhW2kWTN0mCK/Smzpvj3uW3jIN99JOPtcmubHPn xZBsTXXSHcknB6E0+kAfT9AcFZkmY0kJPKNfdipI4HvXMO03wIRMSodA4y0nRtdlj4c1 aune8ypWVIxiijY/x0pXlk35My0KBIJQX9Gl8GgCQNB8cdrNaRk0ej8MA6lv+CsRo3iY CTOg== X-Gm-Message-State: AOAM5319eFFYwEKKkMlR4QqO3PCuFfCKWg19nm7Bnq4KgPIQlfXuNEYj Ben/BEi5yXHi2hexi0jTB/4e/zQUEvL45tEvpkE= X-Google-Smtp-Source: ABdhPJybKfRl67ibffhYmHFDjZA6Z1KyB49JeQroPaKaco32aPoyEXmJI68iKYRFW2CleLZwMzzjMl5VogOzTeytU84= X-Received: by 2002:a05:6214:1425:: with SMTP id o5mr23291103qvx.5.1632743807446; Mon, 27 Sep 2021 04:56:47 -0700 (PDT) MIME-Version: 1.0 References: <20210926230258.27922a8b@riseup.net> In-Reply-To: <20210926230258.27922a8b@riseup.net> From: zimoun Date: Mon, 27 Sep 2021 13:56:36 +0200 Message-ID: Subject: Re: how to use Proof General? To: raingloom Content-Type: text/plain; charset="UTF-8" Received-SPF: pass client-ip=2607:f8b0:4864:20::f33; envelope-from=zimon.toutoune@gmail.com; helo=mail-qv1-xf33.google.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 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, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=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: , 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=1632743837; 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:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=D2tO6QDdTFoidzvVTs6+QWlMn/Ezx07IRS85XnCGzvw=; b=KIrygJraxSfaUv7yTFWOGWpksfheLpmgvHfxF1kt2nuLOsyr+Zzlgapxl+a5ik5nT6r4NE cOhPSyxRSp+jvi7PQm31KMjpMWhTUpX6d0Ur3prGJ2rrlV3SXYn++8P5Zy5tyje66waruP Y9eVwATyD8NgGyZjgdGJQQRgklWfGdkTe3eYVfBmHMiSavna1+E36nkjLek05/SmOu9GP1 hrEv9Hn+LdpWSLvOrvW0ZntItsCALkqw23M0ps6F0v4W5oK+/WzjW9Tv1GpYhhUKI2Ml+2 LD4q8ajSiw4eHqM88IV0a9uqmNcx5v/q63gJ/jVI29qO7BlSGPpl21e+wbvWkw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1632743837; a=rsa-sha256; cv=none; b=m+s49lHbRmgmfmojz5+oG/KeudM+HJnzRHt1cXGWvGN3WCS9F5ef3lVGUsj26PIyZc3gNm zpJSQ3L2sMyv8Bvv+/Gx/OE/7MXrQ9kiGk9wlQaKgFOmza/lZUltcyDmmT9I6GsnDgql3S qGYimqUWSiFGbp3eJNl0qVlTyNLclo0xX1thBAfddYq0Va7lmget/k276Agb33EDwmqGKo e3tMtPDnHe5ApmR/F6K8FiFEF7wi6eFQziYpfz4oA0UYUF8kdfFWwE2h+LulAkQo5G7xR0 /Ebzp1z2nEUJPMPCSbYk0cCEHSCX0C3ORGq7iPAhWAwGopa6T2SnCX0vY0sb+Q== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b=hj88JInU; dmarc=pass (policy=none) header.from=gmail.com; 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=gmail.com header.s=20210112 header.b=hj88JInU; dmarc=pass (policy=none) header.from=gmail.com; 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: AF79F15FDB X-Spam-Score: -2.09 X-Migadu-Scanner: scn0.migadu.com X-TUID: FSQz2m6kx8uX Hi, On Mon, 27 Sept 2021 at 03:08, raingloom wrote: > > 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? You might be interested by: explaining that there is a bug in the default config of the Emacs front-end of ProofGeneral. All the best, simon