[bug#58310] [PATCH 11/14] gnu: Add ocaml-elpi.

[Garek Dyszel]

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index bc876d60a1..641a139e51 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -5007,6 +5007,54 @@ (define-public ocaml-atd
 Definitions language.")
     (license (license:non-copyleft "LICENSE.md"))))
 
+(define-public ocaml-elpi
+  (package
+    (name "ocaml-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.2")
+    (version "1.16.5")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/elpi";)
+                    (commit (string-append "v" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                ;; "0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy")
+                "1l6grpglkvyyj0p01l0q5ih12lp4vizamgj7i63ig82gqpyzk9dl"))))
+    (build-system dune-build-system)
+    (arguments
+     `(#:test-target "tests"))
+    ;; Build currently fails with error (repeated several times):
+    ;; 'Warning 6 [labels-omitted: label argsdepth was omitted in the
+    ;; application of this function.'
+    (propagated-inputs (list ocaml-stdlib-shims
+                             ocaml-ppxlib
+                             ocaml-menhir
+                             ocaml-re
+                             ocaml-ppx-deriving
+                             ocaml-atd
+                             ocaml-camlp-streams
+                             ocaml-biniou
+                             ocaml-yojson))
+    (native-inputs (list ocaml-ansiterminal ocaml-cmdliner time))
+    (home-page "https://github.com/LPCIC/elpi";)
+    (synopsis "ELPI - Embeddable λProlog Interpreter")
+    (description
+     "ELPI is an extension language for OCaml.  It implements a variant of
+λProlog enriched with Constraint Handling Rules, a programming language for
+manipulating syntax trees with binders.
+
+This package provides both a command line interpreter, elpi, and an OCaml
+library with the same name.")
+    (license license:lgpl2.1+)))
+
 (define-public ocaml-timed
   (package
     (name "ocaml-timed")
-- 
2.37.3