Skip to content

Commit

Permalink
[new release] elpi (1.20.0)
Browse files Browse the repository at this point in the history
CHANGES:

Requires Menhir 20211230 and OCaml 4.08 or above.

- Language:
  - attribute `:remove` to remove a clause from the program

- Compiler:
  - Build the index at assembly time, rather than optimization time.
    This makes compilation slower, but startup faster.
  - Adding clauses before the type/mode declaration of a predicate
    is now forbidden, since they are immediately inserted in the index
    and the type/mode declaration can change the index type
  • Loading branch information
gares committed Sep 19, 2024
1 parent 164c8ec commit a18eedb
Showing 1 changed file with 90 additions and 0 deletions.
90 changes: 90 additions & 0 deletions packages/elpi/elpi.1.20.0/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
opam-version: "2.0"
maintainer: "Enrico Tassi <[email protected]>"
authors: [ "Claudio Sacerdoti Coen" "Enrico Tassi" ]
license: "LGPL-2.1-or-later"
homepage: "https://github.com/LPCIC/elpi"
doc: "https://LPCIC.github.io/elpi/"
dev-repo: "git+https://github.com/LPCIC/elpi.git"
bug-reports: "https://github.com/LPCIC/elpi/issues"

build: [
["dune" "subst"] {dev}
["dune" "build" "-p" name "-j" jobs]
[make "tests" "DUNE_OPTS=-p %{name}%" "SKIP=performance_HO" "SKIP+=performance_FO" "SKIP+=elpi_api_performance"] {with-test & os != "macos" & os-distribution != "alpine" & os-distribution != "freebsd"}
]

depends: [
"ocaml" {>= "4.08.0" }
"stdlib-shims"
"ppxlib" {>= "0.12.0" }
"menhir" {>= "20211230" }
"re" {>= "1.7.2"}
"ppx_deriving" {>= "4.3"}
"ANSITerminal" {with-test}
"cmdliner" {with-test}
"fileutils" {with-test}
"dune" {>= "2.8.0"}
"conf-time" {with-test}
"atdgen" {>= "2.10.0"}
"atdts" {>= "2.10.0"}
"odoc" {with-doc}
]
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."""
url {
src:
"https://github.com/LPCIC/elpi/releases/download/v1.20.0/elpi-1.20.0.tbz"
checksum: [
"sha256=95cb590084203a0e5df8b7c82ed5ac05572c7a6577cd36587c97c3942c47b5c0"
"sha512=95c0160d237a5786daff5f4748b9c9c41dc1192fe235c6d60b79febfec56c3673815eb2d7983ea595e54927369a4d60a8a2a6008f7053bc7d7bb1871628f1697"
]
}
x-commit-hash: "eb195c67dad82f4cdf3eaaeff47b71e541f8ee0b"

0 comments on commit a18eedb

Please sign in to comment.