[bug#57540] [PATCH 3/6] gnu: Add coq-elpi.

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

* gnu/packages/coq.scm (coq-elpi)
---
  gnu/packages/coq.scm | 74 ++++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 74 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bbb34df..5a37432 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -685,3 +685,77 @@ (define-public coq-stdpp
  @end itemize")
      (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
      (license license:bsd-3)))
+
+(define-public coq-elpi
+  (package
+    (name "coq-elpi")
+    ;; 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.14.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/coq-elpi")
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"))))
+    (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)
+                  (add-before 'build 'remove-extra-src-file
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      ;; Remove the useless line
+                      ;; "src/META.coq-elpi"
+                      ;; in file _CoqProject.
+                      ;; It does not affect
+                      ;; the success of compliation.
+                      (invoke "sed" "-i" "s|src/META.coq-elpi||g"
+                              "_CoqProject")
+                      #t))
+                  (replace 'check
+                    (lambda* (#:key tests? make-flags 
#:allow-other-keys)
+                      (when tests?
+                        (apply invoke "make" "test" make-flags)))))))
+    (inputs (list python))
+    (propagated-inputs (list ocaml
+                             ocaml-stdlib-shims
+                             ocaml-elpi-1.15
+                             ocaml-zarith
+                             coq-core
+                             coq-stdlib))
+    (home-page "https://github.com/LPCIC/coq-elpi")
+    (synopsis "Elpi extension language for Coq")
+    (description
+     "Coq-elpi provides a Coq plugin that embeds ELPI.  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, e.g.  printing a
+message, accessing the environment of theorems and data types,
+defining a new constant and so on.  For convenience it also provides a
+quotation and anti-quotation for Coq's syntax in λProlog.  E.g.
+`{{nat}}` is expanded to the type name of natural numbers, or `{{A ->
+B}}` to the representation of a product by unfolding the `->`
+notation.  Finally it provides a way to define new vernacular commands
+and new tactics.")
+    (license license:lgpl2.1)))
-- 
2.37.2