[bug#57540] [PATCH 4/6] gnu: Add coq-mathcomp-hierarchy-builder.

[Garek Dyszel via Guix-patches via <guix-patches@gnu.org>]

* gnu/packages/coq.scm (coq-mathcomp-hierarchy-builder)
---
  gnu/packages/coq.scm | 75 ++++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 75 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 5a37432..bb4788a 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -759,3 +759,78 @@ (define-public coq-elpi
  notation.  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.15,
+    ;; see the relevant issue:
+    ;; https://github.com/math-comp/hierarchy-builder/issues/297
+    ;; Here we use
+    ;; coq-elpi 1.14.0 + ocaml-elpi 1.15.2 +
+    ;; coq-mathcomp-hierarchy-builder 1.3.0 (Coq 8.15)
+    (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))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#: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)))
+                  (replace 'check
+                    (lambda* (#:key tests? make-flags 
#:allow-other-keys)
+                      (when tests?
+                        (apply invoke "make" "test-suite" 
make-flags)))))))
+    (inputs (list coq
+                  coq-core
+                  coq-mathcomp
+                  which
+                  ocaml
+                  coq-elpi-1.14
+                  ocaml-elpi-1.15))
+    (synopsis "Hierarchy structures for the Coq proof assistant")
+    (description
+     "Hierarchy Builder (HB) provides high level commands to declare a
+hierarchy of algebraic structure (or interfaces if you prefer the
+glossary of computer science) for the Coq system.
+
+Given a structure one can develop its theory, and that theory becomes
+automatically applicable to all the 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.
+
+HB commands compile down to Coq modules, sections, records, coercions,
+canonical structure instances and notations following the packed
+classes discipline which is at the core of the Mathematical Components
+library.  All that complexity is hidden behind a few concepts and a few
+declarative Coq commands.")
+    (home-page "https://math-comp.github.io/")
+    ;; MIT license
+    (license license:expat)))
-- 
2.37.2