From unknown Sat Aug 16 11:41:45 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#48947 <48947@debbugs.gnu.org> To: bug#48947 <48947@debbugs.gnu.org> Subject: Status: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. Reply-To: bug#48947 <48947@debbugs.gnu.org> Date: Sat, 16 Aug 2025 18:41:45 +0000 retitle 48947 [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. reassign 48947 guix-patches submitter 48947 Xinglu Chen severity 48947 normal tag 48947 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Thu Jun 10 09:30:25 2021 Received: (at submit) by debbugs.gnu.org; 10 Jun 2021 13:30:25 +0000 Received: from localhost ([127.0.0.1]:35819 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrKlJ-0006f6-BQ for submit@debbugs.gnu.org; Thu, 10 Jun 2021 09:30:25 -0400 Received: from lists.gnu.org ([209.51.188.17]:52856) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrKlG-0006ex-U6 for submit@debbugs.gnu.org; Thu, 10 Jun 2021 09:30:19 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:46042) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lrKlG-0004VF-Kq for guix-patches@gnu.org; Thu, 10 Jun 2021 09:30:18 -0400 Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:55100 helo=mail.yoctocell.xyz) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lrKlD-0001kO-QC for guix-patches@gnu.org; Thu, 10 Jun 2021 09:30:18 -0400 From: Xinglu Chen DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz; s=mail; t=1623331808; bh=5IxzRa5ASZzHFAV/lFxoX8Bo6OPSI1cxGkrgUGUuuqk=; h=From:To:Subject:Date; b=lTZI7SF7t6Fv+JJCzBHjtb+OWSln5KmJN5Be4ULaWI/YKd+lMewKLf/IO6vwu9Xt/ g2Y+OB8YKB9k9gm3rSxo9Q2BimOSlp3lvvGnz+a7MgOLIKnFczvqYm760Y/HeUZaWx n2yHPT+5TwEN4ivTIosYYR/Wi2heFgAn1CN+IxfE= To: guix-patches@gnu.org Subject: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. Message-Id: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> Date: Thu, 10 Jun 2021 15:30:06 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Received-SPF: pass client-ip=87.96.130.155; envelope-from=public@yoctocell.xyz; helo=mail.yoctocell.xyz X-Spam_score_int: 30 X-Spam_score: 3.0 X-Spam_bar: +++ X-Spam_report: (3.0 / 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, FROM_SUSPICIOUS_NTLD=0.499, FROM_SUSPICIOUS_NTLD_FP=1.596, PDS_OTHER_BAD_TLD=1.997, RDNS_DYNAMIC=0.982, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-Spam-Score: 3.5 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: There hasn’t been a new release since 2016 and there has been more than 450 new commits since then. * gnu/packages/coq.scm (proof-general): Update to 4.4-0.bc86736. [arguments]<#:make-flags>: Set ELISP_START. <#:phases>: Remove ‘coq-prog’ procedure which was unused; don’t run ‘substitute*’ [...] Content analysis details: (3.5 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -2.3 RCVD_IN_DNSWL_MED RBL: Sender listed at https://www.dnswl.org/, medium trust [209.51.188.17 listed in list.dnswl.org] 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: yoctocell.xyz (xyz)] 1.0 SPF_SOFTFAIL SPF: sender does not match SPF record (softfail) -0.0 SPF_HELO_PASS SPF: HELO matches SPF record 0.1 URIBL_SBL_A Contains URL's A record listed in the Spamhaus SBL blocklist [URIs: proofgeneral.github.io] 0.6 URIBL_SBL Contains an URL's NS IP listed in the Spamhaus SBL blocklist [URIs: proofgeneral.github.io] 0.0 RCVD_IN_MSPIKE_H4 RBL: Very Good reputation (+4) [209.51.188.17 listed in wl.mailspike.net] 1.6 FROM_SUSPICIOUS_NTLD_FP From abused NTLD 0.0 RCVD_IN_MSPIKE_WL Mailspike good senders 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD X-Debbugs-Envelope-To: submit 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.9 (/) There hasn=E2=80=99t been a new release since 2016 and there has been more = than 450 new commits since then. * gnu/packages/coq.scm (proof-general): Update to 4.4-0.bc86736. [arguments]<#:make-flags>: Set ELISP_START. <#:phases>: Remove =E2=80=98coq-prog=E2=80=99 procedure which was unused; d= on=E2=80=99t run =E2=80=98substitute*=E2=80=99 on bin/proofgeneral since it no longer exists= . Don=E2=80=99t end phases with #t, this will be unnecessary once the =E2=80=98core-updates=E2=80=99 b= ranch is merged. [home-page]: Remove trailing whitesapce. --- gnu/packages/coq.scm | 140 +++++++++++++++++++++---------------------- 1 file changed, 69 insertions(+), 71 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index fb6a899b48..fa1f4078b8 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -6,6 +6,7 @@ ;;; Copyright =C2=A9 2020 Bj=C3=B6rn H=C3=B6fling ;;; Copyright =C2=A9 2020 raingloom ;;; Copyright =C2=A9 2020 Robin Green +;;; Copyright =C2=A9 2021 Xinglu Chen ;;; ;;; This file is part of GNU Guix. ;;; @@ -142,79 +143,76 @@ It is developed using Objective Caml and Camlp5.") (license (list license:lgpl2.1 license:opl1.0+)))) =20 (define-public proof-general - (package - (name "proof-general") - (version "4.4") - (source (origin - (method git-fetch) - (uri (git-reference - (url (string-append - "https://github.com/ProofGeneral/PG")) - (commit (string-append "v" version)))) - (file-name (git-file-name name version)) - (sha256 - (base32 - "0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8")))) - (build-system gnu-build-system) - (native-inputs - `(("which" ,which) - ("emacs" ,emacs-minimal) - ("texinfo" ,texinfo))) - (inputs - `(("host-emacs" ,emacs) - ("perl" ,perl) - ("coq" ,coq))) - (arguments - `(#:tests? #f ; no check target - #:make-flags (list (string-append "PREFIX=3D" %output) - (string-append "DEST_PREFIX=3D" %output)) - #: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)")) - #t)) - (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"))) - (define (coq-prog name) - (string-append coq "/bin/" name)) - (substitute* "Makefile" - (("/sbin/install-info") "install-info")) - (substitute* "bin/proofgeneral" - (("^PGHOMEDEFAULT=3D.*" all) - (string-append all - "PGHOME=3D$PGHOMEDEFAULT\n" - "EMACS=3D" emacs "/bin/emacs"))) - #t))) - (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)))))) - (home-page "https://proofgeneral.github.io/ ") - (synopsis "Generic front-end for proof assistants based on Emacs") - (description - "Proof General is a major mode to turn Emacs into an interactive proof + ;; The latest release is from 2016 and there has been more than 450 comm= its + ;; since then. + ;; Commit from 2021-06-07. + (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a") + (revision "0")) + (package + (name "proof-general") + (version (git-version "4.4" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/ProofGeneral/PG") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))= )) + (build-system gnu-build-system) + (native-inputs + `(("which" ,which) + ("emacs" ,emacs-minimal) + ("texinfo" ,texinfo))) + (inputs + `(("host-emacs" ,emacs) + ("perl" ,perl) + ("coq" ,coq))) + (arguments + `(#:tests? #f ; no check target + #:make-flags (list (string-append "PREFIX=3D" %output) + (string-append "DEST_PREFIX=3D" %output) + (string-append "ELISP_START=3D" %output + "/share/emacs/site-lisp/ProofGe= neral")) + #: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"))) + (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)))))) + (home-page "https://proofgeneral.github.io/") + (synopsis "Generic front-end for proof assistants based on Emacs") + (description + "Proof General is a major mode to turn Emacs into an interactive pr= oof assistant to write formal mathematical proofs using a variety of theorem provers.") - (license license:gpl2+))) + (license license:gpl2+)))) =20 (define-public coq-flocq (package base-commit: ac886034020b11b647f893116824f7d7b998ce82 --=20 2.32.0 From debbugs-submit-bounces@debbugs.gnu.org Thu Jun 10 12:07:21 2021 Received: (at 48947) by debbugs.gnu.org; 10 Jun 2021 16:07:22 +0000 Received: from localhost ([127.0.0.1]:37637 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrNDF-0004iP-OP for submit@debbugs.gnu.org; Thu, 10 Jun 2021 12:07:21 -0400 Received: from mail-qt1-f179.google.com ([209.85.160.179]:40507) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrNDE-0004iD-52 for 48947@debbugs.gnu.org; Thu, 10 Jun 2021 12:07:21 -0400 Received: by mail-qt1-f179.google.com with SMTP id t9so207293qtw.7 for <48947@debbugs.gnu.org>; Thu, 10 Jun 2021 09:07:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=cUYaEg8NDpVDXV4z52wBjLLeABWg4wnTZBW6H/Xb8mg=; b=fjyGJm9gjSE/j+QsIKEsxeiCdd7u0bxxnVavKKEHT+SBppsv2t0Fz1JFPAZwleXmMW 5QhMBNPx+ozICMAk87Vmx7B8SRHQ/bgHwAefocF11vn1Kl354lNTYVRpHWBeyyULCf/l toN516tZYHNbWLuK14qCatOBzzpAGL8cpaL/bZ84Xrk1nLQXmy7Iy4IQUrPvrmDiq+4o MLmMaKVa0EcUP0cle8tMiXnO+URMmtcqWh9EXE4iEBJvdYUXWVQ35wKYSytawbxJ3IPz lF4rOXBj9zYtHBkjoj+g37gr9QP53GnG/fmVg7hqTDoGMOvF0tPMevYvnmnDHgrdmnta 1TrQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=cUYaEg8NDpVDXV4z52wBjLLeABWg4wnTZBW6H/Xb8mg=; b=bnoB9C2UC/YFWqSVJ/StivWf8OnsebVDyu5XA6j5EJJu0UorjgSX1AL72FrnJFTQfT b8YJ39slS8KAfSscPgiuSKWdMPnZTyYlXmqffjCaFOe81xJBM9ehPZMW66NuE+SuqAkW mVzBcuZ+ymtZZxgKWvnOkd9+sLH5KLAMXLdjiG+Bz01DCkWF5+eoqReMC8F12gVpIh27 eNPwZtxrhRuzvj5t0XOtygKT5xLzvDrXR9H3YaGAAawcsld8wZXcDMahEu1gTv+af5Y5 k5ymT9zmVvLZ8rxjL/Swx6T0bqJfSnNGilcG/2M2lbYZY6rAYKSfQ8ZwUVtGBwwWSVz0 jy6w== X-Gm-Message-State: AOAM533tPcWaVY0UaqlxNpvOJ5uJCeKcyUiPybvht0+V0WGbZBiLTdRH j1khlc5tAkA8lKavgIpkBcTRybpsOJ+E7wXcWgAnXGS3h6c= X-Google-Smtp-Source: ABdhPJzcHyBmCbILRSiVlRKOZ5fKZajc+DPSwfuR5+5nmlrbaGNROddBJk1wsYJtX72HevV0J1yZILEwcbQDKUtPSLI= X-Received: by 2002:ac8:718b:: with SMTP id w11mr350577qto.354.1623341234665; Thu, 10 Jun 2021 09:07:14 -0700 (PDT) MIME-Version: 1.0 References: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> In-Reply-To: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> From: zimoun Date: Thu, 10 Jun 2021 18:07:03 +0200 Message-ID: Subject: Re: [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. To: Xinglu Chen Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: 2.0 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Hi, On Thu, 10 Jun 2021 at 15:31, Xinglu Chen wrote: > > There hasn’t been a new release since 2016 and there has been more than 450 > new commits since then. Cool! Content analysis details: (2.0 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: yoctocell.xyz (xyz)] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at https://www.dnswl.org/, no trust [209.85.160.179 listed in list.dnswl.org] 0.0 RCVD_IN_MSPIKE_H3 RBL: Good reputation (+3) [209.85.160.179 listed in wl.mailspike.net] 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (zimon.toutoune[at]gmail.com) -0.0 SPF_PASS SPF: sender matches SPF record 0.0 RCVD_IN_MSPIKE_WL Mailspike good senders X-Debbugs-Envelope-To: 48947 Cc: 48947@debbugs.gnu.org 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, On Thu, 10 Jun 2021 at 15:31, Xinglu Chen wrote: > > There hasn=E2=80=99t been a new release since 2016 and there has been mor= e than 450 > new commits since then. Cool! Does this patch fix the bug#46016? All the best, simon From debbugs-submit-bounces@debbugs.gnu.org Fri Jun 11 05:05:35 2021 Received: (at 48947) by debbugs.gnu.org; 11 Jun 2021 09:05:35 +0000 Received: from localhost ([127.0.0.1]:38133 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrd6c-0003eK-UH for submit@debbugs.gnu.org; Fri, 11 Jun 2021 05:05:35 -0400 Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:59116 helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrd6Z-0003e3-73 for 48947@debbugs.gnu.org; Fri, 11 Jun 2021 05:05:33 -0400 From: Xinglu Chen DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz; s=mail; t=1623402323; bh=JORdAIrE6GH2Be8Ee2beXr0DI1FzfJH1awUnE2MAqEA=; h=From:To:Cc:Subject:In-Reply-To:References:Date; b=UCGAfbXbBoCMIUHH56ex2liiO0nOe/yC1AOJOfP7YNKpy7EHFdiRNksY51drOdTsC 0IOJ34h1T+IalmZnbC7ytgIymEftYhWvUi2LbwxVq0lWkCMWKBQ/WRLpblAtbmD51E 8ZgU5byqv+fUj9Gqtz6dGTW+KisVi71F27Mxad4A= To: zimoun Subject: Re: [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. In-Reply-To: References: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> Date: Fri, 11 Jun 2021 11:05:02 +0200 Message-ID: <87pmwsbwld.fsf@yoctocell.xyz> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" X-Spam-Score: 2.9 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: On Thu, Jun 10 2021, zimoun wrote: > Hi, > > On Thu, 10 Jun 2021 at 15:31, Xinglu Chen wrote: >> >> There hasn’t been a new release since 2016 and there has been more than 450 >> new commits since then. > > Coo [...] Content analysis details: (2.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: yoctocell.xyz (xyz)] -0.0 SPF_PASS SPF: sender matches SPF record 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD X-Debbugs-Envelope-To: 48947 Cc: 48947@debbugs.gnu.org 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.9 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: On Thu, Jun 10 2021, zimoun wrote: > Hi, > > On Thu, 10 Jun 2021 at 15:31, Xinglu Chen wrote: >> >> There hasn’t been a new release since 2016 and there has been more than 450 >> new commits since then. > > Coo [...] Content analysis details: (2.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: yoctocell.xyz (xyz)] -0.0 SPF_PASS SPF: sender matches SPF record 1.0 BULK_RE_SUSP_NTLD Precedence bulk and RE: from a suspicious TLD 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD -1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list manager --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On Thu, Jun 10 2021, zimoun wrote: > Hi, > > On Thu, 10 Jun 2021 at 15:31, Xinglu Chen wrote: >> >> There hasn=E2=80=99t been a new release since 2016 and there has been mo= re than 450 >> new commits since then. > > Cool! > > Does this patch fix the bug#46016? > > I didn=E2=80=99t know about this bug report, but I did notice that Emacs wa= sn=E2=80=99t able to load the Elisp files (M-x coq-mode didn=E2=80=99t work). Proof General generates a pg-init.el file in /path/to/guix-profile/share/emacs/site-lisp/ProofGeneral/site-start.d, Emacs isn=E2=80=99t able to find that file, so doing (require 'proof-site) doesn=E2=80=99t work. Relevant part of the Makefile =2D-8<---------------cut here---------------start------------->8--- ELISPP=3Dshare/${EMACS}/site-lisp/ProofGeneral ELISP_START=3D${PREFIX}/share/${EMACS}/site-lisp/site-start.d [...] install-init: mkdir -p ${ELISP_START} echo ';;; pg-init.el --- setup for Proof General' > ${ELISP_START}/pg-init= .el echo "(setq load-path (append load-path '(\"${DEST_ELISP}/generic\")))" >>= ${ELISP_START}/pg-init.el echo "(require 'proof-site)" >> ${ELISP_START}/pg-init.el =2D-8<---------------cut here---------------end--------------->8--- With this patch, I set the ELISP_START variable to the same value os ELISPP, now the pg-init.el file ends up in the ProofGeneral directory, and Emacs is now able to find it. Doing (require 'proof-site) worked, and M-x coq-mode created a splash screen, so it seems to work (I just starting looking into Coq). --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQJJBAEBCAAzFiEEAVhh4yyK5+SEykIzrPUJmaL7XHkFAmDDJz4VHHB1YmxpY0B5 b2N0b2NlbGwueHl6AAoJEKz1CZmi+1x5ThsP/inqkyFcjhjKnOpf+l2XQ7hKmUfM 42jvKCIcnlHsxpK0zpsc+aTIX/1o9XFDoBkPfvISG65GqAujiiJgI++pVHH5ebfD pX42arbu785xD024XWdKIcR5mNG45Ct/wotRDiQuMUkgzmnWyA8KD+jLB7wqRha4 KLt+IUKzHmc6k1qG1JNiPM+knQ6LYs08kRIWwXDK+sIa19A3oUNGBPGF3KVW1Dyr j1y8RGJaFzV6kRFj8yzkmCbRD24MXSJGX9qdbbi4lNAgXIOpcctGU2keUCGtsl9G ZAUdU0eqca8gNHfactPX25tEFrSHrsEp02dMmG4ZYX1v3psO0r28iOCrRTTNCHVv qUWQlPYVHre6XGLvwlSAi0e5KV/0SAIewsdNcVr/k4ZTfJ4BipJZmSQqETibMlhC AgygFXzsgFUtaPtGw0HbzGbu9PWgLgRyuuFPEhx7i2KfPYU4jyXKIvWTX+fJ2wtQ i8c9Us65a6MKPPkFNrQhdEGPJUU6/PTjCfHGVNL1iFoWgJ5OE/W6GTgcuFeT0rei WFcxFGqiPBuktEwphpYPajh5jnBQnnnJ/iROXggarHMoC7yRbzE70HP90fXplAXZ M0qcuvG2MIJZl1QmdYG1YNVY65w3WebXU/SOusSt99DyItx+3eQjlL+SRX2+fDZG DQtILkOvyAHi2qiG =Gf/G -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sun Jun 13 16:41:16 2021 Received: (at 48947-done) by debbugs.gnu.org; 13 Jun 2021 20:41:16 +0000 Received: from localhost ([127.0.0.1]:44443 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lsWuy-0002Fd-7x for submit@debbugs.gnu.org; Sun, 13 Jun 2021 16:41:16 -0400 Received: from eggs.gnu.org ([209.51.188.92]:59322) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lsWuw-0002FO-Md for 48947-done@debbugs.gnu.org; Sun, 13 Jun 2021 16:41:15 -0400 Received: from fencepost.gnu.org ([2001:470:142:3::e]:52460) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lsWuq-0003mT-KU; Sun, 13 Jun 2021 16:41:08 -0400 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=57650 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lsWuq-0000eC-Cs; Sun, 13 Jun 2021 16:41:08 -0400 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Xinglu Chen Subject: Re: bug#48947: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. References: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> Date: Sun, 13 Jun 2021 22:41:06 +0200 In-Reply-To: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> (Xinglu Chen's message of "Thu, 10 Jun 2021 15:30:06 +0200") Message-ID: <87k0mxzee5.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.3 (/) X-Debbugs-Envelope-To: 48947-done Cc: 48947-done@debbugs.gnu.org, 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: -1.3 (-) Hi, Xinglu Chen skribis: > There hasn=E2=80=99t been a new release since 2016 and there has been mor= e than 450 > new commits since then. > > * gnu/packages/coq.scm (proof-general): Update to 4.4-0.bc86736. > [arguments]<#:make-flags>: Set ELISP_START. > <#:phases>: Remove =E2=80=98coq-prog=E2=80=99 procedure which was unused;= don=E2=80=99t run > =E2=80=98substitute*=E2=80=99 on bin/proofgeneral since it no longer exis= ts. Don=E2=80=99t end phases > with #t, this will be unnecessary once the =E2=80=98core-updates=E2=80=99= branch is merged. > [home-page]: Remove trailing whitesapce. Applied, thanks! I let you check whether the issue zimoun refers to can be closed. Ludo=E2=80=99. From unknown Sat Aug 16 11:41:45 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Mon, 12 Jul 2021 11:24:08 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator