[bug#58310] [PATCH 13/14] gnu: Add coq-mathcomp-hierarchy-builder.

[Garek Dyszel]

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 313366cb11..184e503dd5 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -843,3 +843,65 @@ (define-public coq-elpi
 Coq's primitives.  Finally it provides a way to define new vernacular commands
 and new tactics.")
     (license license:lgpl2.1)))
+
+(define-public coq-mathcomp-hierarchy-builder
+  (package
+    (name "coq-mathcomp-hierarchy-builder")
+    ;; For more information on which version works with Coq 8.16,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.15.4 + ocaml-elpi 1.16.5 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.16)
+    (version "1.3.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/math-comp/hierarchy-builder";)
+                    (commit (string-append "v" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test-suite"
+       #:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (string-append "COQBININSTALL="
+                                            (assoc-ref %outputs "out") "/bin/")
+                             (string-append "DESTDIR="
+                                            (assoc-ref %outputs "out"))
+                             (string-append "ELPIDIR="
+                                            #$(this-package-input "ocaml-elpi")
+                                            "/lib/ocaml/site-lib/elpi")
+                             (string-append "COQMF_COQLIB="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/ocaml/site-lib/coq")
+                             (string-append "COQLIBINSTALL="
+                                            (assoc-ref %outputs "out")
+                                            "/lib/coq/user-contrib"))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure)
+                  (replace 'build
+                    (lambda* (#:key make-flags #:allow-other-keys)
+                      (apply invoke "make" "build" make-flags))))))
+    (inputs (list coq
+                  coq-core
+                  coq-mathcomp
+                  which
+                  ocaml
+                  coq-elpi
+                  ocaml-elpi))
+    (synopsis "Hierarchy structures for the Coq proof assistant")
+    (description
+     "Hierarchy Builder (HB) provides high level commands to declare a
+hierarchy of interfaces for the Coq system.
+
+Given a structure one can develop its theory, and that theory becomes
+applicable to all examples of the structure.  One can also declare alternative
+interfaces, for convenience or backward compatibility, and provide glue code
+linking these interfaces to the structures part of the hierarchy.")
+    (home-page "https://math-comp.github.io/";)
+    (license license:expat)))
-- 
2.37.3