09/34: gnu: coq: Update to 8.17.1.

[guix-commits]

roptat pushed a commit to branch master
in repository guix.

commit 4b941ab3d5dea321e1fd96dd21faf346258e2d80
Author: pukkamustard <pukkamustard@posteo.net>
AuthorDate: Wed Jan 10 08:43:10 2024 +0100

    gnu: coq: Update to 8.17.1.
    
    * gnu/packages/coq.scm (coq): Update to 8.17.1 and merge with coq-core and 
coq-stdlib.
      [arguments] Merge with coq-core and coq-stdlib. Add pre-build phases and
      add a custom install phase. Remove unnecessary test-target.
      [source](patches): Remove.
      [native-search-paths]: Remove COQLIBPATH and COQCORELIB.
      (coq-core): Remove variable.
      (coq-stdlib): Remove variable.
      (coq-ide)[propagated-inputs]: Add zlib.
      (coq-mathcomp-bigenough)[propagated-inputs]: Remove coq-core.
      (coq-mathcomp-finmap)[inputs]: Remove coq-stdlib.
      (coq-equations): Update to 1.3-8.17.
    * gnu/packages/patches/coq-fix-envvars.patch: Delete file.
    * gnu/local.mk (dist_patch_DATA): Adjust accordingly.
    
    Co-authored-by: Josselin Poiret <dev@jpoiret.xyz>
    Signed-off-by: Julien Lepiller <julien@lepiller.eu>
    Change-Id: I0a0d9f7a6e06dd19ce1b66051334476d85f4f195
---
 gnu/local.mk                               |  1 -
 gnu/packages/coq.scm                       | 89 +++++++++++-------------------
 gnu/packages/patches/coq-fix-envvars.patch | 53 ------------------
 3 files changed, 32 insertions(+), 111 deletions(-)

diff --git a/gnu/local.mk b/gnu/local.mk
index f7ef95e2f8..168590f778 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1056,7 +1056,6 @@ dist_patch_DATA =                                         
\
   %D%/packages/patches/converseen-hide-non-free-pointers.patch \
   %D%/packages/patches/cool-retro-term-wctype.patch            \
   %D%/packages/patches/coreutils-gnulib-tests.patch            \
-  %D%/packages/patches/coq-fix-envvars.patch                   \
   %D%/packages/patches/cppcheck-disable-char-signedness-test.patch     \
   %D%/packages/patches/cpuinfo-system-libraries.patch          \
   %D%/packages/patches/cpulimit-with-glib-2.32.patch           \
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 57f8489a18..105b942ad3 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -31,6 +31,7 @@
   #:use-module (gnu packages base)
   #:use-module (gnu packages bison)
   #:use-module (gnu packages boost)
+  #:use-module (gnu packages compression)
   #:use-module (gnu packages emacs)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages gawk)
@@ -51,10 +52,10 @@
   #:use-module (guix utils)
   #:use-module ((srfi srfi-1) #:hide (zip)))
 
-(define-public coq-core
+(define-public coq
   (package
-    (name "coq-core")
-    (version "8.16.1")
+    (name "coq")
+    (version "8.17.1")
     (source
      (origin
        (method git-fetch)
@@ -64,28 +65,35 @@
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf"))
-       (patches (search-patches "coq-fix-envvars.patch"))))
+         "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
-            (files (list "lib/ocaml/site-lib/coq/user-contrib"
-                         "lib/coq/user-contrib")))
-           (search-path-specification
-            (variable "COQLIBPATH")
-            (files (list "lib/ocaml/site-lib/coq")))
-           (search-path-specification
-            (variable "COQCORELIB")
-            (files (list "lib/ocaml/site-lib/coq-core"))
-            (separator #f))))
+            (files (list "lib/coq/user-contrib")))))
     (build-system dune-build-system)
+    (arguments
+     (list
+      #:package "coq-core,coq-stdlib,coq"
+      #:phases
+      #~(modify-phases %standard-phases
+          (add-before 'build 'configure
+            (lambda* (#:key outputs #:allow-other-keys)
+              (let* ((out (assoc-ref outputs "out"))
+                     (coqlib (string-append out "/lib/ocaml/site-lib/coq/")))
+                (invoke "./configure" "-prefix" out
+                        "-libdir" coqlib))))
+          (add-before 'build 'make-dunestrap
+            (lambda _ (invoke "make" "dunestrap")))
+          (replace 'install
+            (lambda* (#:key outputs #:allow-other-keys)
+              (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")))))))
     (inputs
      (list gmp ocaml-zarith))
     (native-inputs
      (list ocaml-ounit2 which))
-    (arguments
-     `(#:package "coq-core"
-       #:test-target "."))
     (properties '((upstream-name . "coq"))) ; also for inherited packages
     (home-page "https://coq.inria.fr";)
     (synopsis "Proof assistant for higher-order logic")
@@ -97,39 +105,6 @@ It is developed using Objective Caml and Camlp5.")
     ;; Some of the documentation is distributed under opl1.0+.
     (license (list license:lgpl2.1 license:opl1.0+))))
 
-(define-public coq-stdlib
-  (package
-    (inherit coq-core)
-    (name "coq-stdlib")
-    (arguments
-     `(#:package "coq-stdlib"
-       #:test-target "."
-       #:phases
-       (modify-phases %standard-phases
-         (add-before 'build 'fix-dune
-           (lambda _
-             (substitute* "user-contrib/Ltac2/dune"
-               (("coq-core.plugins.ltac2")
-                (string-join
-                  (map (lambda (plugin) (string-append "coq-core.plugins." 
plugin))
-                       '("ltac2" "number_string_notation" "tauto" "cc"
-                         "firstorder"))
-                  " "))))))))
-    (inputs
-     (list coq-core gmp ocaml-zarith))
-    (native-inputs '())))
-
-(define-public coq
-  (package
-    (inherit coq-core)
-    (name "coq")
-    (arguments
-     `(#:package "coq"
-       #:test-target "."))
-    (propagated-inputs
-     (list coq-core coq-stdlib))
-    (native-inputs '())))
-
 (define-public coq-ide-server
   (package
     (inherit coq)
@@ -148,7 +123,7 @@ It is developed using Objective Caml and Camlp5.")
      `(#:tests? #f
        #:package "coqide"))
     (propagated-inputs
-     (list coq coq-ide-server))
+     (list coq coq-ide-server zlib))
     (inputs
      (list lablgtk3 ocaml-lablgtk3-sourceview3))))
 
@@ -582,16 +557,16 @@ uses Ltac to synthesize the substitution operation.")
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.3")
+    (version "1.3-8.17")
     (source (origin
               (method git-fetch)
               (uri (git-reference
                     (url "https://github.com/mattam82/Coq-Equations";)
-                    (commit (string-append "v" version "-8.16"))))
+                    (commit (string-append "v" version))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "08f756vgdd1wklkarg0b93j4n5mhkqm5ixxrhyb23dcv2dwhc8yg"))))
+                "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
     (build-system gnu-build-system)
     (native-inputs
      (list ocaml coq camlp5))
@@ -743,7 +718,7 @@ for goals involving set operations.
                                          "/lib/coq/user-contrib"))
        #:phases (modify-phases %standard-phases
                   (delete 'configure))))
-    (inputs (list coq coq-stdlib coq-mathcomp which))
+    (inputs (list coq coq coq-mathcomp which))
     (synopsis "Finite sets and finite types for coq-mathcomp")
     (description
      "This library is an extension of coq-mathcomp which supports finite sets
@@ -774,7 +749,7 @@ subsume notations for finite sets.")
        ;; by the packaged project in the future.
        #:tests? #f
        #:make-flags ,#~(list (string-append "COQBIN="
-                                            #$(this-package-input "coq-core")
+                                            #$(this-package-input "coq")
                                             "/bin/")
                              (string-append "COQMF_COQLIB="
                                             (assoc-ref %outputs "out")
@@ -784,7 +759,7 @@ subsume notations for finite sets.")
                                             "/lib/coq/user-contrib"))
        #:phases (modify-phases %standard-phases
                   (delete 'configure))))
-    (propagated-inputs (list coq coq-core coq-mathcomp which))
+    (propagated-inputs (list coq coq-mathcomp which))
     (home-page "https://math-comp.github.io/";)
     (synopsis "Small library to do epsilon - N reasoning")
     (description
diff --git a/gnu/packages/patches/coq-fix-envvars.patch 
b/gnu/packages/patches/coq-fix-envvars.patch
deleted file mode 100644
index 6c48224c64..0000000000
--- a/gnu/packages/patches/coq-fix-envvars.patch
+++ /dev/null
@@ -1,53 +0,0 @@
-From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001
-From: Julien Lepiller <julien@lepiller.eu>
-Date: Thu, 10 Feb 2022 16:44:10 +0100
-Subject: [PATCH] Fix environment variable usage.
-
----
- boot/env.ml | 26 +++++++++++++++++++-------
- 1 file changed, 19 insertions(+), 7 deletions(-)
-
-diff --git a/boot/env.ml b/boot/env.ml
-index e8521e7..d834a3a 100644
---- a/boot/env.ml
-+++ b/boot/env.ml
-@@ -32,17 +32,29 @@ let fail_msg =
- 
- let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1
- 
-+let path_to_list p =
-+  let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
-+    String.split_on_char sep p
-+
- (* This code needs to be refactored, for now it is just what used to be in 
envvars  *)
- let guess_coqlib () =
-   Util.getenv_else "COQLIB" (fun () ->
-   let prelude = "theories/Init/Prelude.vo" in
--  Util.check_file_else
--    ~dir:Coq_config.coqlibsuffix
--    ~file:prelude
--    (fun () ->
--      if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
--      then Coq_config.coqlib
--      else fail ()))
-+  let coqlibpath = Util.getenv_else "COQLIBPATH" (fun () -> 
Coq_config.coqlibsuffix) in
-+  let paths = path_to_list coqlibpath in
-+  let valid_paths =
-+    List.filter
-+      (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> 
"")) <> "")
-+      paths in
-+  match valid_paths with
-+  | [] ->
-+    if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
-+    then Coq_config.coqlib
-+    else
-+      fail "cannot guess a path for Coq libraries; please use -coqlib option \
-+            or ensure you have installed the package containing Coq's stdlib 
(coq-stdlib in OPAM) \
-+            If you intend to use Coq without a standard library, the -boot 
-noinit options must be used."
-+  | p::_ -> p)
- 
- (* Build layout uses coqlib = coqcorelib *)
- let guess_coqcorelib lib =
--- 
-2.34.0
-