GNU logs - #75368, boring messages

Message sent to julien@HIDDEN, pukkamustard@HIDDEN, guix-patches@HIDDEN:

Subject: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: julien@HIDDEN, pukkamustard@HIDDEN, guix-patches@HIDDEN
Resent-Date: Sun, 05 Jan 2025 00:56:02 +0000
Resent-Message-ID: <handler.75368.B.173603854026322 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: 75368 <at> debbugs.gnu.org
Cc: julien@HIDDEN, pukkamustard@HIDDEN
From: Antero Mejr <mail@HIDDEN>
Date: Sat, 04 Jan 2025 19:55:17 -0500
Message-ID: <87zfk62i6i.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
Received-SPF: pass client-ip=136.143.188.15; envelope-from=mail@HIDDEN;
 helo=sender4-op-o15.zoho.com
X-Spam_score_int: -19
X-Spam_score: -2.0
X-Spam_bar: --
X-Spam_report: (-2.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,
 RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_MSPIKE_H2=-0.001,
 RCVD_IN_VALIDITY_RPBL_BLOCKED=0.001, RCVD_IN_VALIDITY_SAFE_BLOCKED=0.001,
 SPF_HELO_NONE=0.001, SPF_PASS=-0.001,
 URIBL_SBL_A=0.1 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: 1.7 (+)
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:  Deprecates coq-ide-server, which is now part of the main coq
 package. * gnu/packages/coq.scm (coq): Update to 8.20.0. [native-inputs]:
 Add python, rsync. [arguments]: Patch tests, build coqide-server, symlink
 `coqidetop`. (coq-ide-server): Deprecate package. (coq-ide)[p [...] 
 Content analysis details:   (1.7 points, 10.0 required)
 pts rule name              description
 ---- ---------------------- --------------------------------------------------
 -0.0 RCVD_IN_DNSWL_NONE     RBL: Sender listed at https://www.dnswl.org/,
 no trust [2001:470:142:0:0:0:0:17 listed in] [list.dnswl.org]
 0.1 URIBL_SBL_A Contains URL's A record listed in the Spamhaus SBL
 blocklist [URIs: antr.me]
 0.6 URIBL_SBL Contains an URL's NS IP listed in the Spamhaus SBL
 blocklist [URIs: antr.me]
 -0.0 SPF_HELO_PASS          SPF: HELO matches SPF record
 1.0 SPF_SOFTFAIL           SPF: sender does not match SPF record (softfail)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 0.7 (/)


Deprecates coq-ide-server, which is now part of the main coq package.

* gnu/packages/coq.scm (coq): Update to 8.20.0.
[native-inputs]: Add python, rsync.
[arguments]: Patch tests, build coqide-server, symlink `coqidetop`.
(coq-ide-server): Deprecate package.
(coq-ide)[propagated-inputs]: Remove coq-ide-server.
(coq-for-coqtail): Remove hidden package.
* gnu/packages/coq.scm (vim-coqtail)[native-inputs]: Remove
coq-for-coqtail.
[native-inputs]: Add coq.

Change-Id: Ic9c3985b76938f78352b8735fb832c7a78519172
---
 gnu/packages/coq.scm | 74 ++++++++++++++++++++------------------------
 gnu/packages/vim.scm |  2 +-
 2 files changed, 35 insertions(+), 41 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 3ef91ad78a..71b14e0dd8 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -57,7 +57,7 @@ (define-module (gnu packages coq)
 (define-public coq
   (package
     (name "coq")
-    (version "8.18.0")
+    (version "8.20.0")
     (source
      (origin
        (method git-fetch)
@@ -67,7 +67,7 @@ (define-public coq
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m"))))
+         "0pf3sfq61w9h7r418pl28cvqidf9iwdn9zzkfbsb9afvj584slkp"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
@@ -75,9 +75,31 @@ (define-public coq
     (build-system dune-build-system)
     (arguments
      (list
-      #:package "coq-core,coq-stdlib,coq"
+      #:package "coq-core,coq-stdlib,coq,coqide-server"
       #:phases
       #~(modify-phases %standard-phases
+          (add-after 'unpack 'fix-tests
+            (lambda _
+              ;; In 8.20, the test Makefile incorrectly assumes installation
+              ;; occurs before tests. Fixing it here.
+              (substitute* "test-suite/Makefile"
+                ;; Disable IDE tests (not available in this package)
+                ((" ide ide ")
+                 " ")
+                ;; Disable tests with incorrect paths
+                ;; TODO: Maybe fixable upstream in a future release?
+                ((" coq-makefile precomputed-time-tests ")
+                 " ")
+                ((" \\$\\(VSUBSYSTEMS\\) misc ")
+                 " $(VSUBSYSTEMS) ")
+                ((" coqdoc ssr ")
+                 " ssr ")
+                ;; Set COQLIB to correct path
+                (("COQLIB\\?=")
+                 "COQLIB=../../install/default/lib/coq")
+                ;; Override incorrect bin directory
+                (("BIN:=\\$\\(COQPREFIX\\)/bin/")
+                 "BIN=../../install/default/bin/"))))
           (add-before 'build 'configure
             (lambda* (#:key outputs #:allow-other-keys)
               (let* ((out (assoc-ref outputs "out"))
@@ -91,13 +113,18 @@ (define-public coq
               (let* ((out (assoc-ref outputs "out"))
                      (libdir (string-append out "/lib/ocaml/site-lib")))
                 (invoke "dune" "install" "--prefix" out
-                        "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
+                        "--libdir" libdir "coq" "coq-core" "coq-stdlib"
+                        "coqide-server")
+                ;; coqide searches for coqidetop on $PATH, but it is installed
+                ;; as coqidetop.opt
+                (symlink (string-append #$output "/bin/coqidetop.opt")
+                         (string-append #$output "/bin/coqidetop"))))))))
     (propagated-inputs
      (list ocaml-zarith))
     (inputs
      (list gmp))
     (native-inputs
-     (list ocaml-ounit2 which))
+     (list ocaml-ounit2 python rsync which))
     (properties '((upstream-name . "coq"))) ; also for inherited packages
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
@@ -110,14 +137,7 @@ (define-public coq
     (license (list license:lgpl2.1 license:opl1.0+))))
 
 (define-public coq-ide-server
-  (package
-    (inherit coq)
-    (name "coq-ide-server")
-    (arguments
-     `(#:tests? #f
-       #:package "coqide-server"))
-    (inputs
-     (list coq gmp))))
+  (deprecated-package "coq-ide-server" coq))
 
 (define-public coq-ide
   (package
@@ -127,7 +147,7 @@ (define-public coq-ide
      `(#:tests? #f
        #:package "coqide"))
     (propagated-inputs
-     (list coq coq-ide-server zlib))
+     (list coq zlib))
     (inputs
      (list lablgtk3 ocaml-lablgtk3-sourceview3))))
 
@@ -255,32 +275,6 @@ (define-public coq-flocq
 inside Coq.")
     (license license:lgpl3+)))
 
-;; Union of coq and coq-ide-server as vim-coqtail expects coqc and coqidetop
-;; to be in the same bin folder, when vim-coqtail is installed coqc and
-;; coqidetop will be in the "same" bin folder in the profile, so this is only
-;; required for testing the package.
-;;
-;; This is deeply ingrained in the internals of vim-coqtail so this is why
-;; it's necessary.
-(define-public coq-for-coqtail
-  (hidden-package
-    (package
-      (inherit coq)
-      (name "coq-for-coqtail")
-      (source #f)
-      (build-system trivial-build-system)
-      (arguments
-       '(#:modules ((guix build union))
-         #:builder
-         (begin
-           (use-modules (ice-9 match)
-                        (guix build union))
-           (match %build-inputs
-             (((names . directories) ...)
-              (union-build (assoc-ref %outputs "out")
-                           directories))))))
-      (inputs (list coq coq-ide-server)))))
-
 (define-public coq-gappa
   (package
     (name "coq-gappa")
diff --git a/gnu/packages/vim.scm b/gnu/packages/vim.scm
index e77578cf18..01b53d5d92 100644
--- a/gnu/packages/vim.scm
+++ b/gnu/packages/vim.scm
@@ -515,7 +515,7 @@ (define-public vim-coqtail
                  ;; they don't get installed.
                  (delete-file-recursively "python/__pycache__")))))))
       (native-inputs
-       (list coq-for-coqtail
+       (list coq
              python-pytest
              vim-vader))
       (propagated-inputs (list coq coq-ide-server))

base-commit: b8858d8b1344525d0d7ac78d8fb9dc1a577b85d3
-- 
2.46.0

Message sent:

Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
MIME-Version: 1.0
X-Mailer: MIME-tools 5.505 (Entity 5.505)
Content-Type: text/plain; charset=utf-8
X-Loop: help-debbugs@HIDDEN
From: help-debbugs@HIDDEN (GNU bug Tracking System)
To: Antero Mejr <mail@HIDDEN>
Subject: bug#75368: Acknowledgement ([PATCH] gnu: coq: Update to 8.20.0.)
Message-ID: <handler.75368.B.173603854026322.ack <at> debbugs.gnu.org>
References: <87zfk62i6i.fsf@HIDDEN>
X-Gnu-PR-Message: ack 75368
X-Gnu-PR-Package: guix-patches
X-Gnu-PR-Keywords: patch
Reply-To: 75368 <at> debbugs.gnu.org
Date: Sun, 05 Jan 2025 00:56:03 +0000

Thank you for filing a new bug report with debbugs.gnu.org.

This is an automatically generated reply to let you know your message
has been received.

Your message is being forwarded to the package maintainers and other
interested parties for their attention; they will reply in due course.

As you requested using X-Debbugs-CC, your message was also forwarded to
  julien@HIDDEN, pukkamustard@HIDDEN
(after having been given a bug report number, if it did not have one).

Your message has been sent to the package maintainer(s):
 guix-patches@HIDDEN

If you wish to submit further information on this problem, please
send it to 75368 <at> debbugs.gnu.org.

Please do not send mail to help-debbugs@HIDDEN unless you wish
to report a problem with the Bug-tracking system.

--=20
75368: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D75368
GNU Bug Tracking System
Contact help-debbugs@HIDDEN with problems

Message sent to guix-patches@HIDDEN:

Subject: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Resent-From: Arnaud Daby-Seesaram <ds-ac@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Thu, 09 Jan 2025 09:38:01 +0000
Resent-Message-ID: <handler.75368.B75368.173641545119060 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: Antero Mejr <mail@HIDDEN>
Cc: pukkamustard@HIDDEN, 75368 <at> debbugs.gnu.org, julien@HIDDEN
From: Arnaud Daby-Seesaram <ds-ac@HIDDEN>
In-Reply-To: <87zfk62i6i.fsf@HIDDEN> (Antero Mejr's message of "Sat, 04 Jan
 2025 19:55:17 -0500")
References: <87zfk62i6i.fsf@HIDDEN>
User-Agent: mu4e 1.12.7; emacs 29.4
Date: Thu, 09 Jan 2025 10:37:16 +0100
Message-ID: <87msg0s4z7.fsf@HIDDEN>
MIME-Version: 1.0
Content-Type: multipart/signed; boundary="=-=-=";
 micalg=pgp-sha512; protocol="application/pgp-signature"
Precedence: list
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>

--=-=-=
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable

Hi Antero,

Antero Mejr <mail@HIDDEN> writes:
> Deprecates coq-ide-server, which is now part of the main coq package.
>
> * gnu/packages/coq.scm (coq): Update to 8.20.0.
> [native-inputs]: Add python, rsync.
> [arguments]: Patch tests, build coqide-server, symlink `coqidetop`.
> (coq-ide-server): Deprecate package.
> (coq-ide)[propagated-inputs]: Remove coq-ide-server.
> (coq-for-coqtail): Remove hidden package.
> * gnu/packages/coq.scm (vim-coqtail)[native-inputs]: Remove
> coq-for-coqtail.
> [native-inputs]: Add coq.

Thank you for your patch.  I have not had the time to look at it in
detail yet, but here are a few questions/remarks that probably call for
a V2:

=2D some Coq-dependent packages are broken by the update (e.g.=C2=A0stdpp n=
eeds
  to be updated to 1.11.0 to compile).  It would be nice to update
  dependent packages if they support 8.20.

=2D If all Coq packages are updated to support 8.20 (I do not know if it
  is possible), would it be worth renaming Coq into Rocq[0]?

=2D I understand the addition of python in the inputs, as Coq uses python
  scripts.  However, I do not understand why rsync is added as an input.
  Could you say a few words about this?

[0] https://rocq-prover.org/

Best regards,

=2D-=20
Arnaud

--=-=-=
Content-Type: application/pgp-signature; name="signature.asc"

-----BEGIN PGP SIGNATURE-----

iQJEBAEBCgAuFiEEMgqfJ4U0fby1t860ojLKXoMTiAwFAmd/mMwQHGRzLWFjQG5h
bmVpbi5mcgAKCRCiMspegxOIDJLfD/9qyWnClngrsHfOWSKE39Js9OoNR/MJIoeR
2G9mEiAhW0vblUh7JNdQi0EQ17DplOEots1Yw5mXmqsR8lSyyPweN03iKzFGyF5l
JkzZqV/+sqTb9p0McdzL7dKYTVUdQZvHDWz5S1YXq2AgI27/A7LxRKylZTKGvD/S
tZ3sUBnD/dWmrsh9Akx0RfCFreN4KAoPIT9gQd66TBEOXYc3hLWObYzu6OhgnC3F
HvXsfYJBCLOoaFfaSBbnf9N7h6bY4XAV3ADe/4F+wqk5MjwZjZFJTdg2RBvgVM3O
HClLd14WOceMBF+5gdAFeWE6JdfWQ8JJEDS+d4WXEbEXen3A6QwGRuAXDdHIJuw+
pXL3Ug9/SD/mBC0gK18cO124SNCr9Kvp3Kk6ifY68dpj874Qm3ZRZmn4uVskI7ZX
DNvHhqziJkJrXbpoKxk2575R9uInIOrUkiToWizKPMWHPs4zimT1f1VA61FO83i+
3JHUKEzuSjlJ1s3J18/ooULrUlryaBH+r0ohzCZMAOVNxE52lQFsSDDqxi7+nTmk
sf1Tn/I2dm8Kxk+WfNKL3RtgOt86z/Ti6fY/qm3pJnRToeUF6DID+EUOVZM6Gkbs
9xZT1itAgamnpdLYMNYQn9aqL0cPnDE5GMe4KAe+H6BYTgOkoODkRXWr2MohMkmB
sSFcoIRYkg==
=cyOE
-----END PGP SIGNATURE-----
--=-=-=--

Message sent to guix-patches@HIDDEN:

Subject: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Resent-From: Antero Mejr <mail@HIDDEN>
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Thu, 09 Jan 2025 21:28:01 +0000
Resent-Message-ID: <handler.75368.B75368.173645807924603 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
To: Arnaud Daby-Seesaram <ds-ac@HIDDEN>
Cc: pukkamustard@HIDDEN, 75368 <at> debbugs.gnu.org, julien@HIDDEN
From: Antero Mejr <mail@HIDDEN>
In-Reply-To: <87msg0s4z7.fsf@HIDDEN> (Arnaud Daby-Seesaram's message of
 "Thu, 09 Jan 2025 10:37:16 +0100")
References: <87zfk62i6i.fsf@HIDDEN> <87msg0s4z7.fsf@HIDDEN>
Date: Thu, 09 Jan 2025 16:27:44 -0500
Message-ID: <87cygv65kf.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Precedence: list
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>

Arnaud Daby-Seesaram <ds-ac@HIDDEN> writes:

> Thank you for your patch.  I have not had the time to look at it in
> detail yet, but here are a few questions/remarks that probably call for
> a V2:
>
> - some Coq-dependent packages are broken by the update (e.g.=C2=A0stdpp n=
eeds
>   to be updated to 1.11.0 to compile).  It would be nice to update
>   dependent packages if they support 8.20.

Yes, definitely.

Lately I've been wondering if a coq-build-system would be helpful, since
it seems there's a lot of commonality/boilerplate in the coq- packages.

> - If all Coq packages are updated to support 8.20 (I do not know if it
>   is possible), would it be worth renaming Coq into Rocq[0]?

AFAIK the rename is planned for the 9.0 release, which is still another
release away (after 8.21). The rename is going to be a mess. It appears
that the packaging system will be changing again, and also we'll have to
deprecate all the coq- packages if we want to maintain naming
consistency.

> - I understand the addition of python in the inputs, as Coq uses python
>   scripts.  However, I do not understand why rsync is added as an input.
>   Could you say a few words about this?

One of the test scripts uses rsync instead of mv to move a file. I chose
to add the dependency instead of patching it out. Maybe submitting a
patch upstream to fix that would be better.

Thanks for the review!

Last modified: Sun, 12 Jan 2025 05:45:02 UTC

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997 nCipher Corporation Ltd, 1994-97 Ian Jackson.