Merge pull request ocaml#22820 from Deducteam/release-lambdapi-2.3.0

[new release] lambdapi (2.3.0)

Author: kit-ty-kate

packages/lambdapi/lambdapi.2.3.0/opam

@@ -0,0 +1,80 @@
+opam-version: "2.0"
+synopsis: "Proof assistant for the λΠ-calculus modulo rewriting"
+description: """
+This package provides:
+- A lambdapi command for checking .lp or .dk files,
+translating .dk files to .lp files and vice versa,
+or launching an LSP server for editing .lp files.
+- A library of logic definitions and basic definitions and proofs
+on natural numbers and polymorphic lists.
+- A rich Emacs mode based on LSP (available on MELPA too).
+- A basic mode for Vim.
+- OCaml libraries.
+A VSCode extension is also available on the VSCode Marketplace.
+
+Find Lambdapi user manual on https://lambdapi.readthedocs.io/.
+
+Lambdapi provides a rich type system with dependent types.
+In Lambdapi, one can define both type and function symbols
+by using rewriting rules (oriented equations).
+A symbol can be declared associative and commutative.
+Lambdapi supports unicode symbols and infix operators.
+The declaration of symbols and rewriting rules is separated
+so that one can easily define inductive-recursive types.
+
+Lambdapi checks that rules are locally confluent (by checking
+the joinability of critical pairs) and preserve typing.
+Rewrite rules can also be exported to the TRS and XTC formats
+for checking confluence and termination with external tools.
+
+Lambdapi does not come with a pre-defined logic. It is a
+powerful logical framework in which one can easily define
+its own logic and build and check proofs in this logic.
+There exist .lp files defining first or higher-order logic
+and complex type systems like in Coq or Agda.
+
+Lambdapi provides a basic module and package system,
+interactive modes for proving both unification goals
+and typing goals, and tactics for solving them step by step.
+In particular, a rewrite tactic like in SSReflect, and
+a why3 tactic for calling external automated provers through
+the Why3 platform."""
+maintainer: ["[email protected]"]
+authors: ["Deducteam"]
+license: "CECILL-2.1"
+homepage: "https://github.com/Deducteam/lambdapi"
+bug-reports: "https://github.com/Deducteam/lambdapi/issues"
+dev-repo: "git+https://github.com/Deducteam/lambdapi.git"
+depends: [
+  "dune" {>= "2.7"}
+  "ocaml" {>= "4.08.0"}
+  "menhir" {>= "20200624"}
+  "sedlex" {>= "2.2"}
+  "alcotest" {with-test}
+  "dedukti" {with-test & >= "2.7"}
+  "bindlib" {>= "6.0.0"}
+  "timed" {>= "1.0"}
+  "pratter" {>= "2.0.0"}
+  "camlp-streams" {>= "5.0"}
+  "why3" {>= "1.5.0"}
+  "yojson" {>= "1.6.0"}
+  "cmdliner" {>= "1.1.0"}
+  "stdlib-shims" {>= "0.1.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [make]
+]
+install: [
+  [make "install"]
+]
+url {
+  src:
+    "https://github.com/Deducteam/lambdapi/releases/download/2.3.0/lambdapi-2.3.0.tbz"
+  checksum: [
+    "sha256=9b13c3121ef87cf4d3311a8a1db43db4be7f0e5e2a702fdaff04a3b3c432cb31"
+    "sha512=81e0760ca77cb862a5bdb8927aa37faf7141c4e2484a8163dad0a3eaa21cc691acb5f72279c78588c085f53dde4bd35186346378feac0ab55ac06a679cf2e60f"
+  ]
+}
+x-commit-hash: "4939b93c2721c8aa4dc88a7b8190dd43e3badfdc"