[bug#57540] [RFC PATCH v2 01/19] gnu: Add ocaml-elpi.

[Garek Dyszel]

Hi Julien,

Thank you for your thoughtful suggestions! All patches are now split such that 
each package has its own patch.

* Quickies
> And then I wonder why you need that at all, if it doesn't change
> compilation result?
The file src/META.coq-elpi does not exist in the source tree. I changed the 
comment; hopefully it's less ambiguous now.

> Please don't use #t at the end of phases anymore.
Thanks for catching this! It's removed.

>  Instead of replacing this phase, maybe try #:test-target "test-suite"
This worked, thanks!

> If that means that future versions will have tests (for instance if
> master has tests), maybe this should say it more explicitely.
It looks like coq-mathcomp-analysis has no tests and no plans to include any 
tests in the traditional sense. I changed the comment to reflect that.

* Other changes
For all the ocaml packages, using #:test-target as suggested with the 
appropriate directory worked. There still remain three packages without tests, 
but tests were not supplied with those three.

I had to add about 10 python packages in order to get the tests for ocaml-atd 
to pass.

Some packages (python-pluggy-1.0, python-jsonschema-4.15, 
python-setuptools-scm-7) are present already in the Guix tree  were required by 
the ocaml-atd tests.

Is there a better way to include those packages without sending this patch 
through core-updates?

Lists should now be formatted with @itemize (assuming I didn't miss any!).

We now use git-references for most packages. In cases where git-references were 
not used, they were python packages. The tests with the PyPi versions passed, 
but using the git repository for the same package yielded failing tests. 

* Remaining issues
This set of patches still is not ready to be merged; python-hatchling breaks 
Guix. The upstream hash differed this afternoon from a "guix hash -rx ." run 
from this morning, though the commit we are building from hasn't changed. The 
command "pytest -vv" in phase "check" fails with: "ERROR Missing dependencies: 
pluggy>=1.0.0". It seems that python-pluggy-1.0 built correctly, so maybe it is 
just not specified correctly in the inputs for python-hatchling?

What do you think?

Thanks again for the help!
Garek

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

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 2fd519ca41..c4fa05b934 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.
 ;;;
@@ -8774,3 +8775,98 @@ (define-public ocaml-guile
      "The OCaml guile library provides high-level OCaml bindings to GNU Guile
 3.0, supporting easy interop between OCaml and GNU Guile Scheme.")
     (license license:gpl3+)))
+
+(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
+     `(#:test-target "tests"))
+    (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 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:
+
+@itemize
+@item 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.
+
+@item 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.
+
+@item 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.
+
+@item 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).
+
+@item Native support for backtracking.  To ease implementation of search.
+
+@item The constraint store is extensible.  The host application can declare
+non-syntactic constraints and use custom constraint solvers to check
+their consistency.
+
+@item 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.
+@end itemize
+
+ELPI is free software released under the terms of LGPL 2.1 or above.")
+    (license license:lgpl2.1)))
-- 
2.37.2