From unknown Sun Jun 22 07:56:43 2025 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-Spam-Score: 0.9 (/) 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 From unknown Sun Jun 22 07:56:43 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. References: <20211110192622.368232-1-zimon.toutoune@gmail.com> In-Reply-To: <20211110192622.368232-1-zimon.toutoune@gmail.com> Resent-From: zimoun Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 10 Nov 2021 19:38:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 51755@debbugs.gnu.org Cc: zimoun Received: via spool by 51755-submit@debbugs.gnu.org id=B51755.163657307922209 (code B ref 51755); Wed, 10 Nov 2021 19:38:01 +0000 Received: (at 51755) by debbugs.gnu.org; 10 Nov 2021 19:37:59 +0000 Received: from localhost ([127.0.0.1]:39222 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mktPy-0005m9-QU for submit@debbugs.gnu.org; Wed, 10 Nov 2021 14:37:59 -0500 Received: from mail-wr1-f49.google.com ([209.85.221.49]:35834) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mktPw-0005lr-Pk for 51755@debbugs.gnu.org; Wed, 10 Nov 2021 14:37:57 -0500 Received: by mail-wr1-f49.google.com with SMTP id i5so5933168wrb.2 for <51755@debbugs.gnu.org>; Wed, 10 Nov 2021 11:37:56 -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=wjdpagCUF3lYU18RbKLtY+yYfRZnDSuruXLHYUnEBjo=; b=qe53g1Sag//yaNn8SBfKUuYuwMVedof7bsi32eXqgPGnigfqkHAbpWwZUDR99OfKL7 QM6Em1vc78fyhihoSPHf1W3FbPiIh1468l1Hs5WKY63ZMqUBrgaEKHUVORkofa7+nRhy BF+5sJaiizhyXuf89k3Za7Ig5vT4r8jGqfp4qs9Gm+yQQoualp0nEk1vbIBXUaWeEEUW ENWyNeG6TgMiglutqs5OlJkEddEhlzrg7vCXq1LGDEZfx9hsUjTX5+EiHX56HYakkGG9 8YBLQTB3nkyhh75ctWSg84L5BUUuT7wj2Df8iTPnDl368Mrb+FDMWgbKBcB0lDQBaRK1 M3kw== 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=wjdpagCUF3lYU18RbKLtY+yYfRZnDSuruXLHYUnEBjo=; b=OfDCN5RFYH5PRiRfj33Hzvs/62A42p7EdvNMAcw7J3TZEidPq9qgSp4uAO7jXXnHxN kIi/6jHeeilv2BBSy/5HIYc0zM7dCjqr5xrvmFvlRbjZZHeE3Hfoj3iRGa9zRzcIU4tL Ttg9qjhslXkI3TJRewuVaXLvnQZ1GX9B9R3uFc142RZ0dcBX5yV12BFFVkRwpL8q2b+r i/6vBHGLry5I7i0QULgUE7JYEJp1b8cC9baOiL2ObJ6tYOFC8LVBT6XuAVZz9NjSj7KJ hpDuAdvrYXJySPNCw2PihYY3vpKTDQ0GrslpsK62Rn7R9dfbjEpNDpIiJOhnpJGhqGB9 ZABg== X-Gm-Message-State: AOAM533VneYa0pQE3ckfKZFkfo9hDPSu1KgK0oCfw2+0552RQURvyQ3o Ui7smJAfviRATK1NIUs0ajsiSjEQFeM= X-Google-Smtp-Source: ABdhPJwQZ1HcHDUHpHacvzko62Ks64XlTWFIJy+cr5jlByEX41RFLna62F2og7mj9ElKNkggu3C1ww== X-Received: by 2002:a05:6000:1688:: with SMTP id y8mr1862126wrd.420.1636573070864; Wed, 10 Nov 2021 11:37:50 -0800 (PST) Received: from localhost.localdomain ([193.48.40.117]) by smtp.gmail.com with ESMTPSA id w10sm703638wrq.88.2021.11.10.11.37.50 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 10 Nov 2021 11:37:50 -0800 (PST) From: zimoun Date: Wed, 10 Nov 2021 20:37:48 +0100 Message-Id: <20211110193748.368696-1-zimon.toutoune@gmail.com> X-Mailer: git-send-email 2.33.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) 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: -1.0 (-) Fixes . * gnu/packages/coq.scm (proof-general)[native-inputs]: Remove 'which'. [inputs]: Remove 'coq' and 'emacs'. [arguments]<#:make-flags>: Adjust to find 'emacs'. Set 'ELISP' and 'DEST_LISP'. <#:modules, #:imported-modules>: Remove. <#:phases>: Remove call to 'which' in Makefile. Add copy file allowing Emacs autoloads. Clean unnecessary code. --- gnu/packages/coq.scm | 85 +++++++++++++++++++++++--------------------- 1 file changed, 45 insertions(+), 40 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index dccb9bea4c..2cf9d1a602 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -135,50 +135,55 @@ (define-public proof-general "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) (build-system gnu-build-system) (native-inputs - `(("which" ,which) - ("emacs" ,emacs-minimal) + `(("emacs" ,emacs-minimal) ("texinfo" ,texinfo))) (inputs - `(("host-emacs" ,emacs) - ("perl" ,perl) - ("coq" ,coq))) + `(("perl" ,perl))) (arguments - `(#:tests? #f ; no check target - #:make-flags (list (string-append "PREFIX=" %output) - (string-append "DEST_PREFIX=" %output) - (string-append "ELISP_START=" %output - "/share/emacs/site-lisp/ProofGeneral")) - #:modules ((guix build gnu-build-system) - (guix build utils) - (guix build emacs-utils)) - #:imported-modules (,@%gnu-build-system-modules - (guix build emacs-utils)) - #:phases - (modify-phases %standard-phases - (delete 'configure) - (add-after 'unpack 'disable-byte-compile-error-on-warn - (lambda _ - (substitute* "Makefile" - (("\\(setq byte-compile-error-on-warn t\\)") - "(setq byte-compile-error-on-warn nil)")))) - (add-after 'unpack 'patch-hardcoded-paths - (lambda* (#:key inputs outputs #:allow-other-keys) - (let ((out (assoc-ref outputs "out")) - (coq (assoc-ref inputs "coq")) - (emacs (assoc-ref inputs "host-emacs"))) + (let ((base-directory "/share/emacs/site-lisp/ProofGeneral")) + `(#:tests? #f ; no check target + #:make-flags (list (string-append "PREFIX=" %output) + (string-append "EMACS=" (assoc-ref %build-inputs "emacs") + "/bin/emacs") + (string-append "DEST_PREFIX=" %output) + (string-append "ELISP=" %output ,base-directory) + (string-append "DEST_ELISP=" %output ,base-directory) + (string-append "ELISP_START=" %output ,base-directory)) + #:phases + (modify-phases %standard-phases + (delete 'configure) + (add-after 'unpack 'disable-byte-compile-error-on-warn + (lambda _ + (substitute* "Makefile" + (("\\(setq byte-compile-error-on-warn t\\)") + "(setq byte-compile-error-on-warn nil)")))) + (add-after 'unpack 'patch-hardcoded-paths + (lambda _ + (substitute* "Makefile" + (("/sbin/install-info") "install-info")))) + (add-after 'unpack 'remove-which + (lambda _ + (substitute* "Makefile" + (("`which perl`") "perl") + (("`which bash`") "bash")))) + (add-after 'unpack 'clean + (lambda _ + ;; Delete the pre-compiled elc files for Emacs 23. + (invoke "make" "clean"))) + (add-after 'install 'install-doc + (lambda* (#:key make-flags #:allow-other-keys) + ;; XXX FIXME avoid building/installing pdf files, + ;; due to unresolved errors building them. (substitute* "Makefile" - (("/sbin/install-info") "install-info"))))) - (add-after 'unpack 'clean - (lambda _ - ;; Delete the pre-compiled elc files for Emacs 23. - (invoke "make" "clean"))) - (add-after 'install 'install-doc - (lambda* (#:key make-flags #:allow-other-keys) - ;; XXX FIXME avoid building/installing pdf files, - ;; due to unresolved errors building them. - (substitute* "Makefile" - ((" [^ ]*\\.pdf") "")) - (apply invoke "make" "install-doc" make-flags)))))) + ((" [^ ]*\\.pdf") "")) + (apply invoke "make" "install-doc" make-flags))) + (add-after 'install 'allow-subfolders-autoloads + (lambda* (#:key outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out"))) + ;; Make it visible by Emacs + (copy-file "proof-general.el" + (string-append out ,base-directory + "/proof-general-autoloads.el"))))))))) (home-page "https://proofgeneral.github.io/") (synopsis "Generic front-end for proof assistants based on Emacs") (description -- 2.33.1 From unknown Sun Jun 22 07:56:43 2025 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: Fri, 19 Nov 2021 12:28:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 51755@debbugs.gnu.org Cc: Julien Lepiller , Nicolas Goaziou Received: via spool by 51755-submit@debbugs.gnu.org id=B51755.16373248566875 (code B ref 51755); Fri, 19 Nov 2021 12:28:01 +0000 Received: (at 51755) by debbugs.gnu.org; 19 Nov 2021 12:27:36 +0000 Received: from localhost ([127.0.0.1]:38293 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mo2zQ-0001mp-AO for submit@debbugs.gnu.org; Fri, 19 Nov 2021 07:27:36 -0500 Received: from mail-wr1-f47.google.com ([209.85.221.47]:46891) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mo2zO-0001mY-Qt for 51755@debbugs.gnu.org; Fri, 19 Nov 2021 07:27:35 -0500 Received: by mail-wr1-f47.google.com with SMTP id u1so17843615wru.13 for <51755@debbugs.gnu.org>; Fri, 19 Nov 2021 04:27:34 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=NCnxC1Cb71BYxEfTDD5kF1vSSoKPEYmEl17J6vJX9/I=; b=bdm8llFYKPqptfeKdARRconH0N98rfVpb+1hE91CSHvzWtsoQllqsxmWezlQKT7wtz /8bxpbrM2H3dDlFKIsVEkxFyKCjqLM/mUdFq/BuUqBkeZ5VFh0yaYGkwQjr8B6WLCVQC B1sVK8F4kRwM2wlCV5qysJxRgT16tZDXAUaoFGdNqgeXE4Ffwl0OGbsiOdvEGaRa/ARe QQJ0w9eey2YQSN6O9jOesAMd1sOGHRbyrtjqThkJV1T17NdWUKj4gbIkFK+e70m+BZ37 aONWTie+k3c8O72H8RURLtkH48HQLH3lrgjrF1w9VAaVzkiOFfdRMf3M9vvAQEeUBDNC tRfg== 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:references:date:in-reply-to :message-id:user-agent:mime-version; bh=NCnxC1Cb71BYxEfTDD5kF1vSSoKPEYmEl17J6vJX9/I=; b=cSALrq4P3GfzFMLgJ3EVHS/rQYW9x0KxowTlLky2hCfK142KvbXqSpQwIdbIlbW+1p WfRIpgkNMOM8ppbyB6+NPMPil8ZYgCAoaDhWyVmuwy7JQ/SwhnmjL0qJ2Nu107CplEai 1MxCYnnLrSMsL16tfIDmdEvPNSpMpI8EuFt/4RO+dEGstK9gQKt/bTaKi6Vtgs92gn6f EeSVySuev9Z3p921R3SAKXYRI1+7CvSXF3xpPnVANG+V32Zmk2t9sqxfZpw4iSbVep1t CvKR27qhxZdKAjvIkSAvVDhb+SyKD5iF/DED/fYu6RgPKn+qAWgUFGrwJVnlJ0y/uwsO K/NQ== X-Gm-Message-State: AOAM532Emecwt+EWY4PkyUDXKRzQpv8TpO7+6UImmsD3u6aiUjYdpyhp mcOmm5xCqaECpzk3TsbJci8= X-Google-Smtp-Source: ABdhPJxc4LaMHHsN0OD7xpEZOgj1iWNQ4dSiFJNS7banaiE0+XECB8l6tgQm6e884D8hE/ydaw6aGw== X-Received: by 2002:adf:cd06:: with SMTP id w6mr6670329wrm.431.1637324848804; Fri, 19 Nov 2021 04:27:28 -0800 (PST) Received: from lili ([2a01:e0a:59b:9120:65d2:2476:f637:db1e]) by smtp.gmail.com with ESMTPSA id z5sm14678625wmp.26.2021.11.19.04.27.27 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 19 Nov 2021 04:27:28 -0800 (PST) From: zimoun References: <20211110192622.368232-1-zimon.toutoune@gmail.com> Date: Fri, 19 Nov 2021 13:27:13 +0100 In-Reply-To: <20211110192622.368232-1-zimon.toutoune@gmail.com> (zimoun's message of "Wed, 10 Nov 2021 20:26:22 +0100") Message-ID: <86czmwgwke.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.0 (/) 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: -1.0 (-) Hi Coq or Emacs reviewers, On Wed, 10 Nov 2021 at 20:26, zimoun wrote: > 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]). > > 1: > 2: Friendly ping. :-) Cheers, simon From unknown Sun Jun 22 07:56:43 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. Resent-From: Nicolas Goaziou Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 21 Nov 2021 18:42:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: zimoun Cc: 51755@debbugs.gnu.org Received: via spool by 51755-submit@debbugs.gnu.org id=B51755.163752007013011 (code B ref 51755); Sun, 21 Nov 2021 18:42:02 +0000 Received: (at 51755) by debbugs.gnu.org; 21 Nov 2021 18:41:10 +0000 Received: from localhost ([127.0.0.1]:46006 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1morm2-0003Nl-0P for submit@debbugs.gnu.org; Sun, 21 Nov 2021 13:41:10 -0500 Received: from relay4-d.mail.gandi.net ([217.70.183.196]:51919) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1morlw-0003N5-9y for 51755@debbugs.gnu.org; Sun, 21 Nov 2021 13:41:08 -0500 Received: (Authenticated sender: admin@nicolasgoaziou.fr) by relay4-d.mail.gandi.net (Postfix) with ESMTPSA id 8C8ABE0003; Sun, 21 Nov 2021 18:40:57 +0000 (UTC) From: Nicolas Goaziou References: <20211110192622.368232-1-zimon.toutoune@gmail.com> <20211110193748.368696-1-zimon.toutoune@gmail.com> Date: Sun, 21 Nov 2021 19:40:56 +0100 In-Reply-To: <20211110193748.368696-1-zimon.toutoune@gmail.com> (zimoun's message of "Wed, 10 Nov 2021 20:37:48 +0100") Message-ID: <8735npwdvr.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) 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: -1.7 (-) Hello, zimoun writes: > * gnu/packages/coq.scm (proof-general)[native-inputs]: Remove 'which'. > [inputs]: Remove 'coq' and 'emacs'. > [arguments]<#:make-flags>: Adjust to find 'emacs'. > Set 'ELISP' and 'DEST_LISP'. > <#:modules, #:imported-modules>: Remove. > <#:phases>: Remove call to 'which' in Makefile. > Add copy file allowing Emacs autoloads. > Clean unnecessary code. Thanks. > + (add-after 'install 'allow-subfolders-autoloads > + (lambda* (#:key outputs #:allow-other-keys) > + (let ((out (assoc-ref outputs "out"))) > + ;; Make it visible by Emacs > + (copy-file "proof-general.el" > + (string-append out ,base-directory > + "/proof-general-autoloads.el"))))))))) So, IIUC, the above is basically a hack: you disguise the main file into an autoloads file because no autoloads file is generated from the code base? If so, this might deserve a longer comment, IMO. Otherwise, LGTM. Regards, -- Nicolas Goaziou From unknown Sun Jun 22 07:56:43 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 21 Nov 2021 19:08:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Nicolas Goaziou , zimoun Cc: 51755@debbugs.gnu.org Received: via spool by 51755-submit@debbugs.gnu.org id=B51755.163752167815671 (code B ref 51755); Sun, 21 Nov 2021 19:08:01 +0000 Received: (at 51755) by debbugs.gnu.org; 21 Nov 2021 19:07:58 +0000 Received: from localhost ([127.0.0.1]:46039 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mosBx-00044h-SY for submit@debbugs.gnu.org; Sun, 21 Nov 2021 14:07:58 -0500 Received: from mail-wr1-f65.google.com ([209.85.221.65]:43935) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mosBw-00044V-G0 for 51755@debbugs.gnu.org; Sun, 21 Nov 2021 14:07:56 -0500 Received: by mail-wr1-f65.google.com with SMTP id t30so28464621wra.10 for <51755@debbugs.gnu.org>; Sun, 21 Nov 2021 11:07:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=message-id:subject:from:to:cc:date:in-reply-to:references :user-agent:mime-version:content-transfer-encoding; bh=KyBjhcZXZyWSP5FnKaladdz+LJ/xpc7wGeMEGcnoxCk=; b=XyKjrMzT7kyIpMXWjv9uxjJVhK3hiwH51CWfHVXsIGe3qpoSHbZJwMfI9+C5pIKfrB risRoEXVkp8gQ2JRWqxr+JacMF8q8WwC4AVxERn5fuURzqS3+v6Duur817ZXJDuoZf1h t5+2nvSiT7gEZen5EfXbKR2704Id0AKOFLCD2pLWoipweBKW0GrWW9/ixaAEDfupdQN2 a/russ9T7+BJt/xBS3o12GDVklL1DurBtIn2fyt0+EE3z8Wql7HixBaMYp/zMjVryDh3 Y+rPP0VofqXP+9Qk9w1T3RHtNAdW4YfWbW9AglmSTbTD6dvJBxC8r6Xcjj9iBU5ejunr g9Eg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:message-id:subject:from:to:cc:date:in-reply-to :references:user-agent:mime-version:content-transfer-encoding; bh=KyBjhcZXZyWSP5FnKaladdz+LJ/xpc7wGeMEGcnoxCk=; b=FgeziCTEZDWcICwNuOTxQ41fDGvdZV5Asp3QqBmfkE4hagc3dCSRFQDr9o5HIVelG2 2WgWmnBvUQo5t0rkZrYr7miCQJN5XC6LIlAcFwBBN8arW1c0fPglsvIp3dBPK+J8QpKJ KSOshcidZhOsEE0VWwhZv/EPycuFb4T6O+FSwg6tXv/4xmIie3ruNSgffrRBiK7AkKW/ cmcGuh3OBu+ck3wgON31wAHp2iXdJXq8vXW/Ya+O4P2wFdXxpNb2HfBYd7joI4p4eUE5 GypTM0RM6I2TplvwpXSuBsT1NHdb+2Ot3ZpRMbUEbci9gzU20lJQsKxCEvXziLscqazZ S1hQ== X-Gm-Message-State: AOAM532MSHBwFYmCd2ClZQHr5WpTdoiTFF3j2zGFnudgZJYXCcDjZrgA xxD3GOqLeByWJN/BbSPeIHk= X-Google-Smtp-Source: ABdhPJzP8goNF8++oyESpVessyFzuliLXUdv1AU2KfxD0i8zBwxykPNpYSnN5Zmjs5KoRWWcawor7A== X-Received: by 2002:a05:6000:1568:: with SMTP id 8mr30270539wrz.76.1637521670639; Sun, 21 Nov 2021 11:07:50 -0800 (PST) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id 138sm14306066wma.17.2021.11.21.11.07.49 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 21 Nov 2021 11:07:50 -0800 (PST) Message-ID: <6aab24bab9512e0957e33256a3addf1076a9d012.camel@gmail.com> From: Liliana Marie Prikler Date: Sun, 21 Nov 2021 20:07:48 +0100 In-Reply-To: <8735npwdvr.fsf@nicolasgoaziou.fr> References: <20211110192622.368232-1-zimon.toutoune@gmail.com> <20211110193748.368696-1-zimon.toutoune@gmail.com> <8735npwdvr.fsf@nicolasgoaziou.fr> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.34.2 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Spam-Score: 0.0 (/) 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: -1.0 (-) Hi, Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou: > > + (add-after 'install 'allow-subfolders-autoloads > > + (lambda* (#:key outputs #:allow-other-keys) > > + (let ((out (assoc-ref outputs "out"))) > > + ;; Make it visible by Emacs > > + (copy-file "proof-general.el" > > + (string-append out ,base-directory > > + "/proof-general- > > autoloads.el"))))))))) > > So, IIUC, the above is basically a hack: you disguise the main file > into an autoloads file because no autoloads file is generated from > the code base? If so, this might deserve a longer comment, IMO. On a related note, what would be so bad about having to (require 'proof-general) interactively? Alternatively, we could in an after- unpack phase add autoload cookies to the source file or write our own autoloads altogether. WDYT? From unknown Sun Jun 22 07:56:43 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. Resent-From: Nicolas Goaziou Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 21 Nov 2021 20:16:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Liliana Marie Prikler Cc: 51755@debbugs.gnu.org, zimoun Received: via spool by 51755-submit@debbugs.gnu.org id=B51755.163752574322491 (code B ref 51755); Sun, 21 Nov 2021 20:16:01 +0000 Received: (at 51755) by debbugs.gnu.org; 21 Nov 2021 20:15:43 +0000 Received: from localhost ([127.0.0.1]:46105 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1motFW-0005qg-Ol for submit@debbugs.gnu.org; Sun, 21 Nov 2021 15:15:42 -0500 Received: from relay3-d.mail.gandi.net ([217.70.183.195]:45521) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1motFU-0005qQ-96 for 51755@debbugs.gnu.org; Sun, 21 Nov 2021 15:15:41 -0500 Received: (Authenticated sender: admin@nicolasgoaziou.fr) by relay3-d.mail.gandi.net (Postfix) with ESMTPSA id 28CE960007; Sun, 21 Nov 2021 20:15:32 +0000 (UTC) From: Nicolas Goaziou References: <20211110192622.368232-1-zimon.toutoune@gmail.com> <20211110193748.368696-1-zimon.toutoune@gmail.com> <8735npwdvr.fsf@nicolasgoaziou.fr> <6aab24bab9512e0957e33256a3addf1076a9d012.camel@gmail.com> Date: Sun, 21 Nov 2021 21:15:30 +0100 In-Reply-To: <6aab24bab9512e0957e33256a3addf1076a9d012.camel@gmail.com> (Liliana Marie Prikler's message of "Sun, 21 Nov 2021 20:07:48 +0100") Message-ID: <87y25huuxp.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) 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: -1.7 (-) Hello, Liliana Marie Prikler writes: > Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou: >> So, IIUC, the above is basically a hack: you disguise the main file >> into an autoloads file because no autoloads file is generated from >> the code base? If so, this might deserve a longer comment, IMO. Actually, my assumption was wrong. "proof-general.el" is a meta-autoloads file: ;; This file is a thin, package.el-friendly wrapper around generic/proof-site, ;; suitable for execution on Emacs start-up. It serves two purposes: ;; ;; * Setting up the load path when byte-compiling PG. ;; * Loading a minimal PG setup on startup (not all of Proof General, of course; ;; mostly mode hooks and autoloads). > On a related note, what would be so bad about having to (require > 'proof-general) interactively? When not byte compiled, the file only does (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root))) I guess we could also provide a single autoloads file doing just that or, according to the manual, (load "PROOF-GENERAL-HOME/generic/proof-site.el") > Alternatively, we could in an after- > unpack phase add autoload cookies to the source file or write our own > autoloads altogether. WDYT? Autoload cookies are already present in the code base, but in sub-directories. OTOH, I assume the solution proposed by Zimoun, as hackish as it is, works well enough. And it requires less work. IMO, it is acceptable with a good comment. Regards, -- Nicolas Goaziou From unknown Sun Jun 22 07:56:43 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. Resent-From: zimoun Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 21 Nov 2021 21:22:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Nicolas Goaziou , Liliana Marie Prikler Cc: 51755@debbugs.gnu.org Received: via spool by 51755-submit@debbugs.gnu.org id=B51755.163752971329260 (code B ref 51755); Sun, 21 Nov 2021 21:22:02 +0000 Received: (at 51755) by debbugs.gnu.org; 21 Nov 2021 21:21:53 +0000 Received: from localhost ([127.0.0.1]:46230 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mouHY-0007bs-I3 for submit@debbugs.gnu.org; Sun, 21 Nov 2021 16:21:52 -0500 Received: from mail-wm1-f45.google.com ([209.85.128.45]:56301) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mouHX-0007bd-ES for 51755@debbugs.gnu.org; Sun, 21 Nov 2021 16:21:52 -0500 Received: by mail-wm1-f45.google.com with SMTP id p18so13491555wmq.5 for <51755@debbugs.gnu.org>; Sun, 21 Nov 2021 13:21:51 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:in-reply-to:references:date:message-id :mime-version:content-transfer-encoding; bh=h9JJrB7U0P4DSbq2w83dXj0iFO6+eDLJmBXgl80fCGM=; b=jxJWs+HAL3UT1mExroSCU5rd688YpkaGmF1vLakL8HvmxcyQdgCbu73NIvS9jHJZZ8 bhXOHB5ULSFw+f6Hu3diM8iKGBXTitPAvK+NoKbGDdQbm0J9n3hU+b/7+jlkV7xdPkqb UcmLgDVmufvJFMrC/wVmvAzyRrc8Dw361/xYw+nBhOFfd+6MBvf4Qy/YcqXeNsboTBnJ i11OeLm1xf3EwbJopNLz78N96p2OYCfo8Y3zDdNmNubIsXeBR3BSTJ8qOszOAGF0WLL9 Tc2KxrSR70K3NWTmw7iNggDv1myNz5DRUdm/kKvxP/hq6cSBPazTOa4Rg4S3WV71kMo2 ppCA== 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:in-reply-to:references:date :message-id:mime-version:content-transfer-encoding; bh=h9JJrB7U0P4DSbq2w83dXj0iFO6+eDLJmBXgl80fCGM=; b=CCDsj5mZoae3CfXuHfAFQI82KZEuteT+6vCkN0FVDDHiJu0xWTh5txZovQGrQNNkyH LIF9HcWTAZTgYhmDO7E8PhBb/S6bDRD3einxlxn/BzLPhqM0HgtpDqj7QEnv/rEI8ncK dyP2qN8pMwU7jslinU2weiYpr8GcuP8x3Yj3htEgHzG46MuX2/t018EhgLEHbIdZuMAN OsqKtgNp/RWwgzcahHVaf49Pgg28/L/f9ItHyBme1dPCEMfRp4iMKNEWgWLO5UyR/DM5 Bl88lzIX3jBbcUh4/YdWm5fF+zv6dvCUPmE/5H1NDzpyZCfG9n7TbY4GnYxzQZBoG4lC DRbg== X-Gm-Message-State: AOAM530hq7SmJ/UjiGoO9m00HD9D29TvWdnbs0P43TW3nzBRcmSAmaDN 8fJi1gpQoHka2l96T5bkoabEWZz22sg= X-Google-Smtp-Source: ABdhPJy91r+2h0PYEREJewSd8KEF/1FTieamfdojfz2qP+4nDUQbFnxtI3sDdx9viXRNYD1fQVUYPw== X-Received: by 2002:a05:600c:4ec7:: with SMTP id g7mr23415370wmq.138.1637529705401; Sun, 21 Nov 2021 13:21:45 -0800 (PST) Received: from lili (2a01cb04061b8800444bb83f830ae295.ipv6.abo.wanadoo.fr. [2a01:cb04:61b:8800:444b:b83f:830a:e295]) by smtp.gmail.com with ESMTPSA id h13sm6872181wrx.82.2021.11.21.13.21.44 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 21 Nov 2021 13:21:45 -0800 (PST) From: zimoun In-Reply-To: <87y25huuxp.fsf@nicolasgoaziou.fr> References: <20211110192622.368232-1-zimon.toutoune@gmail.com> <20211110193748.368696-1-zimon.toutoune@gmail.com> <8735npwdvr.fsf@nicolasgoaziou.fr> <6aab24bab9512e0957e33256a3addf1076a9d012.camel@gmail.com> <87y25huuxp.fsf@nicolasgoaziou.fr> Date: Sun, 21 Nov 2021 22:11:58 +0100 Message-ID: <86bl2dfc2p.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) 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: -1.0 (-) Hi, Thanks for the review. On Sun, 21 Nov 2021 at 21:15, Nicolas Goaziou wrot= e: > Liliana Marie Prikler writes: >> Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou: >>> So, IIUC, the above is basically a hack: you disguise the main file >>> into an autoloads file because no autoloads file is generated from >>> the code base? If so, this might deserve a longer comment, IMO. > > Actually, my assumption was wrong. "proof-general.el" is > a meta-autoloads file: > > ;; This file is a thin, package.el-friendly wrapper around generic/pr= oof-site, > ;; suitable for execution on Emacs start-up. It serves two purposes: > ;; > ;; * Setting up the load path when byte-compiling PG. > ;; * Loading a minimal PG setup on startup (not all of Proof General,= of course; > ;; mostly mode hooks and autoloads). Yes. Note that =E2=80=99proof-general=E2=80=99 was at one moment in its lo= ng history a standalone package, i.e., running =E2=80=99bin/proofgeneneral=E2=80=99 star= ted Emacs and launched everything. This had been removed long time ago [1] but the current code inherits this long history. 1: >> Alternatively, we could in an after- >> unpack phase add autoload cookies to the source file or write our own >> autoloads altogether. WDYT? > > Autoload cookies are already present in the code base, but in > sub-directories. Yes. The limitation comes from this subdirectory structure. This breaks the usual way of packaging Emacs tools for Guix, IIUC. > OTOH, I assume the solution proposed by Zimoun, as hackish as it is, > works well enough. And it requires less work. IMO, it is acceptable with > a good comment. >From my point of view, my proposed patch appears to me the easiest fix. If something is better, please let me know. :-) About the comment, I thought =C2=AB allow-subfolders-autoloads =C2=BB and = =C2=AB Make it visible by Emacs =C2=BB would have been enough. ;-) --8<---------------cut here---------------start------------->8--- (add-after 'install 'allow-subfolders-autoloads (lambda* (#:key outputs #:allow-other-keys) (let ((out (assoc-ref outputs "out"))) ;; Make it visible by Emacs --8<---------------cut here---------------end--------------->8--- Instead, I propose to extend to: --8<---------------cut here---------------start------------->8--- (add-after 'install 'allow-subfolders-autoloads ;; Autoload cookies are present in sub-directories. A friend= ly ;; wrapper proof-general.el around generic/proof-site.el is ;; provided for execution on Emacs start-up. It serves two ;; purposes: ;; * Setting up the load path when byte-compiling pg. ;; * Loading a minimal PG setup on startup (not all of Proof ;; General, of course;mostly mode hooks and autoloads). ;; The rename to proof-general-autoloads.el is Guix specific. (lambda* (#:key outputs #:allow-other-keys) (let ((out (assoc-ref outputs "out"))) (copy-file "proof-general.el" (string-append out ,base-directory "/proof-general-autoloads.el")= )))))))) --8<---------------cut here---------------end--------------->8--- Is it fine? If yes, I can send* a v2. Or please push directly. :-) Cheers, simon *send v2: for the record, I do not have commit right. ;-) From unknown Sun Jun 22 07:56:43 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: zimoun Subject: bug#51755: closed (Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.) Message-ID: References: <87r1b8t5hs.fsf@nicolasgoaziou.fr> <20211110192622.368232-1-zimon.toutoune@gmail.com> X-Gnu-PR-Message: they-closed 51755 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 51755@debbugs.gnu.org Date: Mon, 22 Nov 2021 18:23:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1637605382-32244-1" This is a multi-part message in MIME format... ------------=_1637605382-32244-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #51755: [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq) which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 51755@debbugs.gnu.org. --=20 51755: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D51755 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1637605382-32244-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 51755-done) by debbugs.gnu.org; 22 Nov 2021 18:22:49 +0000 Received: from localhost ([127.0.0.1]:49089 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mpDxp-0008NZ-8u for submit@debbugs.gnu.org; Mon, 22 Nov 2021 13:22:49 -0500 Received: from relay9-d.mail.gandi.net ([217.70.183.199]:39649) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mpDxn-0008NL-5Z for 51755-done@debbugs.gnu.org; Mon, 22 Nov 2021 13:22:47 -0500 Received: (Authenticated sender: admin@nicolasgoaziou.fr) by relay9-d.mail.gandi.net (Postfix) with ESMTPSA id 61367FF80E; Mon, 22 Nov 2021 18:22:40 +0000 (UTC) From: Nicolas Goaziou To: zimoun Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. References: <20211110192622.368232-1-zimon.toutoune@gmail.com> <20211110193748.368696-1-zimon.toutoune@gmail.com> <8735npwdvr.fsf@nicolasgoaziou.fr> <6aab24bab9512e0957e33256a3addf1076a9d012.camel@gmail.com> <87y25huuxp.fsf@nicolasgoaziou.fr> <86bl2dfc2p.fsf@gmail.com> Date: Mon, 22 Nov 2021 19:22:39 +0100 In-Reply-To: <86bl2dfc2p.fsf@gmail.com> (zimoun's message of "Sun, 21 Nov 2021 22:11:58 +0100") Message-ID: <87r1b8t5hs.fsf@nicolasgoaziou.fr> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 51755-done Cc: 51755-done@debbugs.gnu.org, Liliana Marie Prikler 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: -1.7 (-) Hello, zimoun writes: > Instead, I propose to extend to: > > --8<---------------cut here---------------start------------->8--- > (add-after 'install 'allow-subfolders-autoloads > ;; Autoload cookies are present in sub-directories. A friendly > ;; wrapper proof-general.el around generic/proof-site.el is > ;; provided for execution on Emacs start-up. It serves two > ;; purposes: > ;; * Setting up the load path when byte-compiling pg. > ;; * Loading a minimal PG setup on startup (not all of Proof > ;; General, of course;mostly mode hooks and autoloads). > ;; The rename to proof-general-autoloads.el is Guix specific. > (lambda* (#:key outputs #:allow-other-keys) > (let ((out (assoc-ref outputs "out"))) > (copy-file "proof-general.el" > (string-append out ,base-directory > "/proof-general-autoloads.el"))))))))) > --8<---------------cut here---------------end--------------->8--- > > > Is it fine? If yes, I can send* a v2. Or please push directly. :-) I pushed it directly. Thank you! Regards, -- Nicolas Goaziou ------------=_1637605382-32244-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit 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 ------------=_1637605382-32244-1-- From unknown Sun Jun 22 07:56:43 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs. Resent-From: zimoun Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 22 Nov 2021 21:53:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 51755 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Nicolas Goaziou Cc: 51755-done@debbugs.gnu.org, Liliana Marie Prikler Received: via spool by 51755-done@debbugs.gnu.org id=D51755.163761795814253 (code D ref 51755); Mon, 22 Nov 2021 21:53:01 +0000 Received: (at 51755-done) by debbugs.gnu.org; 22 Nov 2021 21:52:38 +0000 Received: from localhost ([127.0.0.1]:49306 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mpHEr-0003hp-QD for submit@debbugs.gnu.org; Mon, 22 Nov 2021 16:52:37 -0500 Received: from mail-wm1-f51.google.com ([209.85.128.51]:35562) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mpHEp-0003hZ-QP for 51755-done@debbugs.gnu.org; Mon, 22 Nov 2021 16:52:36 -0500 Received: by mail-wm1-f51.google.com with SMTP id 77-20020a1c0450000000b0033123de3425so432848wme.0 for <51755-done@debbugs.gnu.org>; Mon, 22 Nov 2021 13:52:35 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:in-reply-to:references:date:message-id :mime-version; bh=9fCnliaW7xpzMvpEkmvJQbRUCxoSWdAFiMKt3SyqK7I=; b=TFpAyltkzfBemNjgre1xmWSwT0SrdVO+lTAWx+hwpxr3eL+jYzai7emZp4XJYQwRqt IjvoRpPd48pDSReBTG67MJmejNa1/EQSoxNtwXqMKDF8PFmxN+rODOBxWLQeM2RlbJFu 6zYK0qj9+oago4fc/IWJtgfn+3oiL/QQtEyr37qAcIWbKlf1/Q64IvPEd9PzupY/P8+e 8TAKBdX3JmpbLKz+n7ksm1wFMBZCdmrUeLRLAH28Osdke4oVcLcPVr/+IqRBJc0VA0FP 673EUOfD8nY+mc55Fts/0nu8IcAIcWjYW7CccegxnvIHGE/Wchb7qBdedmdc0wgxA7hN 0WGw== 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:in-reply-to:references:date :message-id:mime-version; bh=9fCnliaW7xpzMvpEkmvJQbRUCxoSWdAFiMKt3SyqK7I=; b=Tc6zVFGhhoUGwAx0X3Q7sjcgeVcYgB/HK1+JYuNqIdcjKnrPwQNTIhLfv3RpTpCY1T CL96ify1F1fS69JoiXDBoDdwgatx7BY/57tK1jnS3r5hqzBGlX4rTOEEKE07fTdRMrZ4 e3kHzhZkFHEw09P15rGPWPWEvgFEPudcTZwgnCwZ1CUcSeqiK41SbkfELu6dTM/9hFmb PTIZlgPzbSTbrF1DQ0iRacRBpiF9RthJozIbtl65La8aKimLixTcz9jWVoTVIskJcGtk CYszapfLroufGBiGFt/L9gRuGNXLulZ99LANjS9eQ1dmd+FM5T/6DVm7c46PnHHOjNxb 0cyQ== X-Gm-Message-State: AOAM5306p0o3XITEBXQvwt+xpF6Vyv3XTKVqgkHRy8QLUnaxyuYRr+BF nvfO1HE9dpFJM1zR01A/axhkvJfJrsc= X-Google-Smtp-Source: ABdhPJzrm97T9bieW9BvdXCj9tI/kS5IFMMb4eca1NJ6iijh+7a7wkK4xzvZCr0VtVyIdrbIr6VJdA== X-Received: by 2002:a7b:c155:: with SMTP id z21mr32914510wmi.107.1637617949832; Mon, 22 Nov 2021 13:52:29 -0800 (PST) Received: from lili ([2a01:e0a:59b:9120:65d2:2476:f637:db1e]) by smtp.gmail.com with ESMTPSA id z14sm10302939wrp.70.2021.11.22.13.52.28 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 22 Nov 2021 13:52:29 -0800 (PST) From: zimoun In-Reply-To: <87r1b8t5hs.fsf@nicolasgoaziou.fr> References: <20211110192622.368232-1-zimon.toutoune@gmail.com> <20211110193748.368696-1-zimon.toutoune@gmail.com> <8735npwdvr.fsf@nicolasgoaziou.fr> <6aab24bab9512e0957e33256a3addf1076a9d012.camel@gmail.com> <87y25huuxp.fsf@nicolasgoaziou.fr> <86bl2dfc2p.fsf@gmail.com> <87r1b8t5hs.fsf@nicolasgoaziou.fr> Date: Sun, 21 Nov 2021 23:17:45 +0100 Message-ID: <86ee79xieu.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.8 (/) 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: -0.2 (/) Hi Nicolas, On Mon, 22 Nov 2021 at 19:22, Nicolas Goaziou wrote: > I pushed it directly. Thank you! Thank you. Cheers, simon