[bug#58310] [PATCH 12/14] gnu: Add coq-elpi.

[Garek Dyszel]

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 60937af750..313366cb11 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -771,3 +771,75 @@ (define-public coq-mathcomp-bigenough
 purposes as @code{bigenough} will be subsumed by the near tactics.  The
 formalization is based on the Mathematical Components library.")
     (license license:cecill-b)))
+
+(define-public coq-elpi
+  (package
+    (name "coq-elpi")
+    ;; 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.15.4")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/coq-elpi";)
+                    (commit (string-append "v" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                "115ll1g5dyn8z58x7xg6nsliga669875s560j5053flr6cvb8mq1"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:make-flags ,#~(list (string-append "COQBIN="
+                                            #$(this-package-input "coq-core")
+                                            "/bin/")
+                             (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)
+                  ;; --- old phase from version 1.14.0
+                  (add-before 'build 'remove-extra-src-file
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      ;; Remove the useless line "src/META.coq-elpi"
+                      ;; in file _CoqProject. The file
+                      ;; src/META.coq-elpi does not exist in the
+                      ;; repository, so this line inhibits compilation
+                      ;; unnecessarily.
+                      (invoke "sed" "-i" "s|src/META.coq-elpi||g"
+                              "_CoqProject")))
+                  (replace 'check
+                    ;; Error when running the "check" phase:
+                    ;; "make: *** No rule to make target 'check'.
+                    ;; Stop."
+                    ;; Tests run if we invoke "make test" instead.
+                    (lambda* (#:key tests? make-flags #:allow-other-keys)
+                      (when tests?
+                        (apply invoke "make" "test" make-flags)))))))
+    (propagated-inputs (list ocaml
+                             ocaml-stdlib-shims
+                             ocaml-elpi
+                             ocaml-zarith
+                             coq-core
+                             coq-stdlib))
+    (inputs (list python))
+    (home-page "https://github.com/LPCIC/coq-elpi";)
+    (synopsis "Elpi extension language for Coq")
+    (description
+     "Coq-elpi provides a Coq plugin that embeds ELPI, an extension language
+for OCaml that is an implementation of λProlog.  It also provides a way to
+embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach
+and a way to read terms back.  In addition to that it exports to ELPI a set of
+Coq's primitives.  Finally it provides a way to define new vernacular commands
+and new tactics.")
+    (license license:lgpl2.1)))
-- 
2.37.3