[bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)

[Garek Dyszel]

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

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 0e8e5b2..59f324e 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -26,6 +26,7 @@
 ;;; Copyright © 2021 Sarah Morgensen <iskarian@mgsn.dev>
 ;;; Copyright © 2022 Maxim Cournoyer <maxim.cournoyer@gmail.com>
 ;;; Copyright © 2022 John Kehayias <john.kehayias@protonmail.com>
+;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -8741,3 +8742,104 @@ (define-public ocaml-bibtex2html
     (description "This package allows you to produce, from a set of
 bibliography files in BibTeX format, a bibliography in HTML format.")
     (license license:gpl2)))
+
+(define-public ocaml-elpi
+  (package
+    (name "ocaml-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)
+    ;;
+    ;; The package ocaml-elpi@1.16.5 appears to require a different
+    ;; build process.
+    (version "1.15.2")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/LPCIC/elpi";)
+                    (commit (string-append "v" version))
+                    (recursive? #t)))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32
+                
"0swzqabwrxqb6sz8zpild2lfcnk3l0zxi9fw61dy2g1pzws2j2jy"))))
+    (build-system dune-build-system)
+    (arguments
+     `(;; When running phase 'check', fails with the error:
+       ;; Error: Don't know about directory test specified on the
+       ;; command line!
+       ;;
+       ;; The "make tests" command requires replacing /usr/bin/time
+       ;; with the location of the input package "time".
+       #:tests? #f))
+    (propagated-inputs (list ocaml-stdlib-shims
+                             ocaml-ppxlib
+                             ocaml-menhir
+                             ocaml-re
+                             ocaml-ppx-deriving
+                             ocaml-atdgen
+                             ocaml-atdts
+                             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 implements a variant of λProlog enriched with Constraint
+Handling Rules, a programming language well suited to manipulate
+syntax trees with binders.
+
+ELPI is designed to be embedded into larger applications written in
+OCaml as an extension language.  It comes with an API to drive the
+interpreter and with an FFI for defining built-in predicates and data
+types, as well as quotations and similar goodies that are handy to
+adapt the language to the host application.
+
+This package provides both a command line interpreter (elpi) and a
+library to be linked in other applications (eg by passing -package
+elpi to ocamlfind).
+
+The ELPI programming language has the following features:
+
+- Native support for variable binding and substitution, via an Higher
+Order Abstract Syntax (HOAS) embedding of the object language.  The
+programmer does not need to care about technical devices to handle
+bound variables, like De Bruijn indices.
+
+- Native support for hypothetical context.  When moving under a binder
+one can attach to the bound variable extra information that is
+collected when the variable gets out of scope.  For example when
+writing a type-checker the programmer needs not to care about managing
+the typing context.
+
+- Native support for higher order unification variables, again via
+HOAS.  Unification variables of the meta-language (λProlog) can be
+reused to represent the unification variables of the object language.
+The programmer does not need to care about the unification-variable
+assignment map and cannot assign to a unification variable a term
+containing variables out of scope, or build a circular assignment.
+
+- Native support for syntactic constraints and their meta-level
+handling rules.  The generative semantics of Prolog can be disabled by
+turning a goal into a syntactic constraint (suspended goal).  A
+syntactic constraint is resumed as soon as relevant variables gets
+assigned.  Syntactic constraints can be manipulated by constraint
+handling rules (CHR).
+
+- Native support for backtracking.  To ease implementation of search.
+
+- The constraint store is extensible.  The host application can declare
+non-syntactic constraints and use custom constraint solvers to check
+their consistency.
+
+- Clauses are graftable.  The user is free to extend an existing
+program by inserting/removing clauses, both at runtime (using
+implication) and at \"compilation\" time by accumulating files.
+
+ELPI is free software released under the terms of LGPL 2.1 or above.")
+    (license license:lgpl2.1)))
+
--
2.37.2