Subject: [PATCH] gnu: coq: Update to 8.20.0.

From: Antero Mejr <[email-masked]>
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