From 35495a4ee89988dffba301e69940d6b7ce7c16f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 22 Jul 2024 13:09:25 +0200 Subject: [PATCH 1/2] prepare release 2.5.1 --- CHANGES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index f19b8f32d..0bf4aa14e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,7 +3,7 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/). -## Unreleased +## 2.5.1 (2024-07-22) ### Added From 0f204a05c8295e2a31cd3d49284d855e03970b80 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 27 Jul 2024 16:29:17 +0200 Subject: [PATCH 2/2] wip --- dune-project | 43 ++++++++++------------------------------- lambdapi.opam | 53 +++++++++++++-------------------------------------- 2 files changed, 23 insertions(+), 73 deletions(-) diff --git a/dune-project b/dune-project index 882bfcb77..8f51cba77 100644 --- a/dune-project +++ b/dune-project @@ -14,41 +14,18 @@ (name lambdapi) (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 available on the VSCode Marketplace. -Find Lambdapi user manual on https://lambdapi.readthedocs.io/. +"Lambdapi is an interactive proof assistant for the λΠ-calculus modulo +rewriting. It can call external automated theorem provers via Why3. +The user manual is on https://lambdapi.readthedocs.io/. +A standard library and other developments are available on +https://github.com/Deducteam/opam-lambdapi-repository/. An extension +for Emacs is available on MELPA. An extension for VSCode is available +on the VSCode Marketplace. Lambdapi can read Dedukti files. It +includes checkers for local confluence and subject reduction. It also +provides commands to export Lambdapi files to other formats or +systems: Dedukti, Coq, HRS, CPF.") -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). The declaration -of symbols and rewriting rules is separated so that one can -easily define inductive-recursive types for instance. -Rewrite rules can be exported to the TRS and XTC formats -for checking confluence and termination with external tools. -A symbol can be declared associative and commutative. -Lambdapi supports unicode symbols and infix operators. - -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.") (depends (ocaml (>= 4.08.0)) (menhir (>= 20200624)) diff --git a/lambdapi.opam b/lambdapi.opam index 154ad7a5c..43bbf5a5c 100644 --- a/lambdapi.opam +++ b/lambdapi.opam @@ -1,45 +1,17 @@ -# This file is generated by dune, edit dune-project instead 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.""" +Lambdapi is an interactive proof assistant for the λΠ-calculus modulo +rewriting. It can call external automated theorem provers via Why3. +The user manual is on https://lambdapi.readthedocs.io/. +A standard library and other developments are available on +https://github.com/Deducteam/opam-lambdapi-repository/. An extension +for Emacs is available on MELPA. An extension for VSCode is available +on the VSCode Marketplace. Lambdapi can read Dedukti files. It +includes checkers for local confluence and subject reduction. It also +provides commands to export Lambdapi files to other formats or +systems: Dedukti, Coq, HRS, CPF. +""" maintainer: ["dedukti-dev@inria.fr"] authors: ["Deducteam"] license: "CECILL-2.1" @@ -79,4 +51,5 @@ build: [ "@doc" {with-doc} ] ] -available: arch != "ppc64" +conflicts: [ "ocaml-option-bytecode-only" ] +