[bug#57540] [RFC PATCH v2 04/19] gnu: Add coq-elpi.* gnu/packages/coq.scm (coq-elpi): New variable.

[Garek Dyszel]

* gnu/packages/coq.scm (coq-elpi): New variable.
---
 gnu/packages/coq.scm | 79 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index bbb34df27d..5ae5392db4 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -8,6 +8,7 @@
 ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
 ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
 ;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -685,3 +686,81 @@ (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)
+    (outputs '("out"))
+    (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. 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)))))))
+    (inputs (list python))
+    (propagated-inputs (list ocaml
+                             ocaml-stdlib-shims
+                             ocaml-elpi
+                             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. @code{{{nat}}} is expanded to the type name of natural numbers,
+or @code{{{A -> B}}} to the representation of a product by unfolding
+the @code{->} notation.  Finally it provides a way to define new
+vernacular commands and new tactics.")
+    (license license:lgpl2.1)))
-- 
2.37.2