From debbugs-submit-bounces@debbugs.gnu.org Wed Nov 10 14:34:55 2021 Received: (at submit) by debbugs.gnu.org; 10 Nov 2021 19:34:55 +0000 Received: from localhost ([127.0.0.1]:39217 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mktN1-0005h2-A2 for submit@debbugs.gnu.org; Wed, 10 Nov 2021 14:34:55 -0500 Received: from lists.gnu.org ([209.51.188.17]:60594) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mktMz-0005gt-KM for submit@debbugs.gnu.org; Wed, 10 Nov 2021 14:34:54 -0500 Received: from eggs.gnu.org ([209.51.188.92]:45084) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mktMz-0002D0-Ax for guix-patches@gnu.org; Wed, 10 Nov 2021 14:34:53 -0500 Received: from [2a00:1450:4864:20::32b] (port=46854 helo=mail-wm1-x32b.google.com) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mktMx-00067u-5O for guix-patches@gnu.org; Wed, 10 Nov 2021 14:34:52 -0500 Received: by mail-wm1-x32b.google.com with SMTP id b184-20020a1c1bc1000000b0033140bf8dd5so2759885wmb.5 for ; Wed, 10 Nov 2021 11:34:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:date:message-id:mime-version :content-transfer-encoding; bh=mlqJCcLwgzhhMdz/kqZcL1dOG1xH8+YBHnghZFyu9Lo=; b=HYeXkz7rXhntZa5gBdchaDrZoXDfT/KJuUyMkDK9ZpfawSfPASSWi+XbFRkgxF8uBD fWmRjN3DEbclVJso9kzvGE/ytjFnJmWfSHEFTSkT2qr8BfXDhx5lerANQzcwtLGIyQTL hJpBSDmnonFRt/RJPoWdnQcJX0fLCPxfXqlM7cmkXsWFG5q76IadKvCIHya5JwrJUe83 ZlB6A3RmjnxjPxKKaSkACrZOHxiJv2m8EiCpD3Pxp1l17Msroqhcrw58GtlGqtM3m7sM 8V8sNzkLuIrERfudZma16jLRh6O6HIHsKri/3nVum+/XoSUrk5mRHTI4tBdytYUzMYQs T0jg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:date:message-id:mime-version :content-transfer-encoding; bh=mlqJCcLwgzhhMdz/kqZcL1dOG1xH8+YBHnghZFyu9Lo=; b=AkU6DoqdgQk1RojRqNroe7LDr6qe6qK9SsjE+r4pvnTjUsjW1IpATtIoXyrUAiPyBK 3Q1sZf4PCj/TyFB6DHqvsNICt+X+l9G0qeOUaRmRul5WmXdEPqz11mjTfd/C81aysUXa VBHXr2n7JTQNf8fiNRt4x7qpvKQcJOpAEPi+93d9nrSiu4biOHQboJRYib5MJGyKx0S3 6v7CrrJNr43s/Eg0Kpa+WMFXdKnq7xl/PY5lP5f95wxUK7qK5Yz8XUDtM+OehsWNnmSu XIZdoW8S3yX2Uzm7dzXkm0Wly6j+2+o4FqbTHwNlHsM7o1HHTWiQ645QTMAgovjIJLw0 FIoQ== X-Gm-Message-State: AOAM533kArMKAAmRU4yJotzcPtW+yc/TUkUmWcMOOPuMtvh06pCILqwp BcLhESVvWhnazSkAZEDllk4/gd07Xpc= X-Google-Smtp-Source: ABdhPJxPYTlco6HcuXo+4/QPIGPPoTPnI2rx5qhlH8AhR62zqn2/llB1MTZjlXZZxgCRIKtfl5MRow== X-Received: by 2002:a05:600c:4e45:: with SMTP id e5mr5170807wmq.43.1636572392181; Wed, 10 Nov 2021 11:26:32 -0800 (PST) Received: from localhost.localdomain ([193.48.40.117]) by smtp.gmail.com with ESMTPSA id n4sm886919wri.41.2021.11.10.11.26.31 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 10 Nov 2021 11:26:31 -0800 (PST) From: zimoun To: guix-patches@gnu.org Subject: [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq) Date: Wed, 10 Nov 2021 20:26:22 +0100 Message-Id: <20211110192622.368232-1-zimon.toutoune@gmail.com> X-Mailer: git-send-email 2.33.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Host-Lookup-Failed: Reverse DNS lookup failed for 2a00:1450:4864:20::32b (failed) Received-SPF: pass client-ip=2a00:1450:4864:20::32b; envelope-from=zimon.toutoune@gmail.com; helo=mail-wm1-x32b.google.com X-Spam_score_int: -12 X-Spam_score: -1.3 X-Spam_bar: - X-Spam_report: (-1.3 / 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, PDS_HP_HELO_NORDNS=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-Debbugs-Envelope-To: submit Cc: zimoun X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) Hi, This is a follow-up of bug#46016 [1] and I think close it. Now, it is possible to use ProofGeneral as any other Emacs packages. For instance, guix shell emacs proof-general coq emacs foo.v For now, the dependency of 'coq' is removed as with many Emacs packages. Other said, the user has to provide such dependency. IMHO, it is the spirit of such package where the 'prover' is let to the user (several are more or less supported, see doc [2]). Cheers, simon 1: 2: zimoun (1): gnu: proof-general: Adjust autoloads for Emacs. gnu/packages/coq.scm | 85 +++++++++++++++++++++++--------------------- 1 file changed, 45 insertions(+), 40 deletions(-) base-commit: 140b486437670ce95cb24a935b58cba52a9dac31 -- 2.33.1