GNU bug report logs - #75368
[PATCH] gnu: coq: Update to 8.20.0.

Previous Next

To reply to this bug, email your comments to 75368 AT debbugs.gnu.org.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Antero Mejr <mail <at> antr.me>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: coq: Update to 8.20.0.
Date: Sat, 04 Jan 2025 19:55:17 -0500

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 #8 received at 75368 <at> debbugs.gnu.org (full text, mbox):

From: Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
To: Antero Mejr <mail <at> antr.me>
Cc: pukkamustard <at> posteo.net, 75368 <at> debbugs.gnu.org, julien <at> lepiller.eu
Subject: Re: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Date: Thu, 09 Jan 2025 10:37:16 +0100

[Message part 1 (text/plain, inline)]

Hi Antero,

Antero Mejr <mail <at> antr.me> 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:

- some Coq-dependent packages are broken by the update (e.g. stdpp needs
  to be updated to 1.11.0 to compile).  It would be nice to update
  dependent packages if they support 8.20.

- 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]?

- 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,

-- 
Arnaud

[signature.asc (application/pgp-signature, inline)]

Message #11 received at 75368 <at> debbugs.gnu.org (full text, mbox):

From: Antero Mejr <mail <at> antr.me>
To: Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
Cc: pukkamustard <at> posteo.net, 75368 <at> debbugs.gnu.org, julien <at> lepiller.eu
Subject: Re: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Date: Thu, 09 Jan 2025 16:27:44 -0500

Arnaud Daby-Seesaram <ds-ac <at> nanein.fr> 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. stdpp needs
>   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!

Message #14 received at 75368 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Antero Mejr <mail <at> antr.me>
Cc: pukkamustard <at> posteo.net, julien <at> lepiller.eu,
 Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>, 75368 <at> debbugs.gnu.org
Subject: Re: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Date: Wed, 12 Feb 2025 10:57:38 +0100

Hi Antero,

Antero Mejr <mail <at> antr.me> skribis:

> Arnaud Daby-Seesaram <ds-ac <at> nanein.fr> 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. stdpp needs
>>   to be updated to 1.11.0 to compile).  It would be nice to update
>>   dependent packages if they support 8.20.
>
> Yes, definitely.

Could you maybe submit a v2 that includes those package updates in
addition to Coq itself?

Thanks,
Ludo’.

Message #17 received at 75368 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Antero Mejr <mail <at> antr.me>
Cc: pukkamustard <at> posteo.net, julien <at> lepiller.eu, 75368 <at> debbugs.gnu.org,
 Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
Subject: Re: [bug#75368] [PATCH] gnu: coq: Update to 8.20.0.
Date: Fri, 21 Mar 2025 13:45:08 +0100

Hi,

Antero, Arnaud, and the OCaml team: could you take a look at this?

It would be sad to keep an outdated Coq/Rocq.

Ludo’.

Ludovic Courtès <ludo <at> gnu.org> skribis:

> Hi Antero,
>
> Antero Mejr <mail <at> antr.me> skribis:
>
>> Arnaud Daby-Seesaram <ds-ac <at> nanein.fr> 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. stdpp needs
>>>   to be updated to 1.11.0 to compile).  It would be nice to update
>>>   dependent packages if they support 8.20.
>>
>> Yes, definitely.
>
> Could you maybe submit a v2 that includes those package updates in
> addition to Coq itself?
>
> Thanks,
> Ludo’.

Previous Next

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