unofficial mirror of guix-patches@gnu.org 
 help / color / mirror / code / Atom feed
* [bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis)
@ 2022-09-02  1:44 Garek Dyszel via Guix-patches via
  2022-09-02 15:20 ` [bug#57540] [PATCH 1/6] gnu: Add ocaml-atd Garek Dyszel via Guix-patches via
                   ` (25 more replies)
  0 siblings, 26 replies; 38+ messages in thread
From: Garek Dyszel via Guix-patches via @ 2022-09-02  1:44 UTC (permalink / raw)
  To: 57540

* 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




^ permalink raw reply related	[flat|nested] 38+ messages in thread

end of thread, other threads:[~2022-10-02 22:27 UTC | newest]

Thread overview: 38+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2022-09-02  1:44 [bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis) Garek Dyszel via Guix-patches via
2022-09-02 15:20 ` [bug#57540] [PATCH 1/6] gnu: Add ocaml-atd Garek Dyszel via Guix-patches via
2022-09-02 15:22 ` [bug#57540] [PATCH 2/6] gnu: Add ocaml-ansiterminal Garek Dyszel via Guix-patches via
2022-09-02 15:23 ` [bug#57540] [PATCH 3/6] gnu: Add coq-elpi Garek Dyszel via Guix-patches via
2022-09-02 15:24 ` [bug#57540] [PATCH 4/6] gnu: Add coq-mathcomp-hierarchy-builder Garek Dyszel via Guix-patches via
2022-09-02 15:24 ` [bug#57540] [PATCH 5/6] gnu: Add coq-mathcomp-finmap Garek Dyszel via Guix-patches via
2022-09-02 15:25 ` [bug#57540] [PATCH 6/6] gnu: Add coq-mathcomp-bigenough and coq-mathcomp-analysis Garek Dyszel via Guix-patches via
2022-09-03 18:40 ` [bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis) Julien Lepiller
2022-09-24 13:05   ` Ludovic Courtès
2022-09-24 18:39     ` Julien Lepiller
2022-09-07 18:31 ` [bug#57540] [RFC PATCH v2 01/19] gnu: Add ocaml-elpi Garek Dyszel via Guix-patches via
2022-09-26 16:52   ` [bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis)) zimoun
2022-09-27 13:04     ` Garek Dyszel via Guix-patches via
2022-09-29 17:13       ` Garek Dyszel via Guix-patches via
2022-09-29 17:39         ` Julien Lepiller
2022-09-30 15:02           ` bug#57540: Splitting into several packages instead Garek Dyszel via Guix-patches via
2022-09-30 15:02           ` [bug#57540] [PATCH] Please rebase (was: Add ocaml-elpi (a dependency of coq-mathcomp-analysis)) Garek Dyszel via Guix-patches via
2022-09-30 12:06         ` zimoun
2022-10-02 20:52           ` Garek Dyszel via Guix-patches via
2022-10-02 22:22             ` zimoun
2022-09-07 18:32 ` [bug#57540] [RFC PATCH v2 02/19] gnu: Add ocaml-atd.* gnu/packages/ocaml.scm (ocaml-atd): New variable Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 03/19] gnu: Add ocaml-ansiterminal.* gnu/packages/ocaml.scm (ocaml-ansiterminal): " Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 04/19] gnu: Add coq-elpi.* gnu/packages/coq.scm (coq-elpi): " Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 05/19] gnu: Add coq-mathcomp-hierarchy-builder.* gnu/packages/coq.scm (coq-mathcomp-hierarchy-builder): " Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 06/19] gnu: Add coq-mathcomp-finmap.* gnu/packages/coq.scm (coq-mathcomp-finmap): " Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 07/19] gnu: Add coq-mathcomp-bigenough.* gnu/packages/coq.scm (coq-mathcomp-bigenough): " Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 08/19] gnu: Add coq-mathcomp-analysis.* gnu/packages/coq.scm (coq-mathcomp-analysis): " Garek Dyszel via Guix-patches via
2022-09-07 18:33 ` [bug#57540] [RFC PATCH v2 09/19] gnu: Add python-version.* gnu/packages/python-xyz.scm (python-version): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 10/19] gnu: Add python-hatchling.* gnu/packages/python-xyz.scm (python-hatchling): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 11/19] gnu: Add python-hatch-vcs.* gnu/packages/python-xyz.scm (python-hatch-vcs): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 12/19] gnu: Add python-hatch-fancy-pypi-readme.* gnu/packages/python-xyz.scm (python-hatch-fancy-pypi-readme): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 13/19] gnu: Add python-pprintpp.* gnu/packages/python-xyz.scm (python-pprintpp): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 14/19] gnu: Add python-icdiff.* gnu/packages/python-xyz.scm (python-icdiff): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 15/19] gnu: Add python-pytest-icdiff.* gnu/packages/python-check.scm (python-pytest-icdiff): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 16/19] gnu: Add python-editables.* gnu/packages/python-build.scm (python-editables): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 17/19] gnu: Add python-pluggy-1.0.* gnu/packages/python-xyz.scm (python-pluggy-1.0): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 18/19] gnu: Add python-setuptools-scm-7.* gnu/packages/python.xyz.scm (python-setuptools-scm-7): " Garek Dyszel via Guix-patches via
2022-09-07 18:34 ` [bug#57540] [RFC PATCH v2 19/19] gnu: Add python-jsonschema-4.15.* gnu/packages/python-xyz.scm (python-jsonschema-4.15): " Garek Dyszel via Guix-patches via

Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/guix.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).