From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id CKDPBfUejGHygAEAgWs5BA (envelope-from ) for ; Wed, 10 Nov 2021 20:35:17 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id CJ9/AfUejGEyaAAAB5/wlQ (envelope-from ) for ; Wed, 10 Nov 2021 19:35:17 +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 3B6B91447B for ; Wed, 10 Nov 2021 20:35:16 +0100 (CET) Received: from localhost ([::1]:58936 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mktNL-0002Eo-Am for larch@yhetil.org; Wed, 10 Nov 2021 14:35:15 -0500 Received: from eggs.gnu.org ([209.51.188.92]:45116) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mktN8-0002Ee-TZ for guix-patches@gnu.org; Wed, 10 Nov 2021 14:35:02 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:55904) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mktN8-00069s-KY for guix-patches@gnu.org; Wed, 10 Nov 2021 14:35:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mktN8-0005hW-EI for guix-patches@gnu.org; Wed, 10 Nov 2021 14:35:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq) Resent-From: zimoun Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 10 Nov 2021 19:35:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 51755@debbugs.gnu.org Cc: zimoun X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.163657289521892 (code B ref -1); Wed, 10 Nov 2021 19:35:02 +0000 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 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1636572916; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=mlqJCcLwgzhhMdz/kqZcL1dOG1xH8+YBHnghZFyu9Lo=; b=gktkFiMzJwFbvyiVCkYdXqT2ZXRTHbs9uAok/ZkSFsYE9ml9VTA6gTffm15oG9jVxDTfyA vWHke1YHcSyq0F+e9vElW8wrY4a/h00shTKU5CBnbKtxEUTWYpCFmNisbE7+fXiLUCTl9D 8wIejtgDtQZu8qYfpo4BM2mb4+n19FS/gKjCv+/QH8m8EUwZ5+KDGXghUz3Zzu1uxjnWJm UlGoLrW29YTvx+1GezGEJt+lxhBnzCUdYuerc37viBBqfUt9T6GIvtUPyq/TDPA2FyHz1C VsVugPfgn7rNU3zWSq45FWKe1lcL3hEx2ADR4LPm2roPK4kpq2ANqbpaKHvnEQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1636572916; a=rsa-sha256; cv=none; b=dQp2G7VTg/fJbZudo0450itO4/HeJ6Ej/woOd72TYx4PDp5e/bppaeOl+2iWdCyzWI+ikK HA46zVai5wwYjnJgp6nRk2vEA0jVKYIbqQBJddJf0N7/o1vOBg+BVe9qNtWzmbmY9FBrdn B7vA0DSnWgh4Sqp9NNHa8xiV/0kXcW/koTuyrP9ZqE6kwQkoogvDsYt0u4A+eD4GElzwMN fB7/siwY8YWl6slq1Rkj1Gi5IWsXPaUPN0jkzmtbjpsXosFF96L5llHGwkuwRFq4/XOqcb qGA/dHc7+Q5x/GFATP+HM3Z/xxNz6+xrAX6js5nRukuWZne4+SPUJ2YBZ5rcVQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=HYeXkz7r; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: 2.68 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=HYeXkz7r; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: 3B6B91447B X-Spam-Score: 2.68 X-Migadu-Scanner: scn0.migadu.com X-TUID: T2MtE/Egezbt 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