[bug#64249] [PATCH ocaml-team v4 5/9] gnu: coq: Update to 8.17.1.

[pukkamustard <pukkamustard@posteo.net>]

* 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
  (coq-core): Remove variable.
  (coq-stdlib): Remove variable.
  (coq-mathcomp-bigenough)[propagated-inputs] Remove coq-core.
---
 gnu/packages/coq.scm | 65 ++++++++++++++++----------------------------
 1 file changed, 24 insertions(+), 41 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index cc914422d4..6f9205cfb0 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -50,10 +50,10 @@ (define-module (gnu packages coq)
   #: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)
@@ -63,7 +63,7 @@ (define-public coq-core
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf"))
+         "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))
        (patches (search-patches "coq-fix-envvars.patch"))))
     (native-search-paths
      (list (search-path-specification
@@ -78,13 +78,29 @@ (define-public coq-core
             (files (list "lib/ocaml/site-lib/coq-core"))
             (separator #f))))
     (build-system dune-build-system)
+    (arguments
+     `(#: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"))
+                    (libdir (string-append out "/lib/ocaml/site-lib")))
+               (invoke "./configure" "-prefix" out
+                       "-libdir" libdir))))
+         (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-core" "coq-stdlib" "coq")))))))
     (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")
@@ -96,39 +112,6 @@ (define-public coq-core
     ;; 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)
@@ -761,7 +744,7 @@ (define-public coq-mathcomp-bigenough
                                             "/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
-- 
2.40.1