Skip to content

Latest commit

 

History

History
2184 lines (2003 loc) · 144 KB

README~8.15~2022.09.md

File metadata and controls

2184 lines (2003 loc) · 144 KB
Raw

Coq Platform 2023.03.0 providing Coq 8.15.2 (released Jun 2022) with an updated package pick from Sep 2022

The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs.

The Coq Platform is a distribution of the Coq interactive prover together with a selection of Coq libraries and plugins.

The Coq Platform supports to install several versions of Coq (also in parallel). This README file is for Coq Platform 2023.03.0 with Coq 8.15.2. The README files for other versions are linked in the main README.

This version of Coq Platform 2023.03.0 includes Coq 8.15.2 from Sep 2022. There are two package picks for Coq 8.15.2: the original from 04/2022, and an updated/extended one from 09/2022. This is the latest package pick for Coq 8.15.2 with some package updates with the goal to make it as compatible as possible to the Coq 8.16.1 package pick.

The OCaml version used is 4.13.1+options ocaml-option-flambda.

The Coq Platform supports four levels of installation extent: base, IDE, full and extended and a few optional packages. The sections below provide a short description of each level and the list of packages included in each level. Packaged versions of the Coq Platform usually contain the extended set with all optional packages.

Note on non-free licenses: The Coq Platform contains software with non-free licenses which do not allow commercial use without purchasing a license, notably the coq-compcert package. Please study the package licenses given below and verify that they are compatible with your intended use in case you plan to use these packages.

Note on license information: The license information given below is obtained from opam. The Coq Platform team does no double check this information.

Note on multiple licenses: In case several licenses are given below, it is not clearly specified what this means. It could mean that parts of the software use one license while other parts use another license. It could also mean that you can choose between the given licenses. Please clarify the details with the homepage of the package.

Note: The package list is also available as CSV.

Note: Click on the triangle to show additional information for a package!


Coq Platform 2023.03.0 with Coq 8.15.2 "base level"

The base level is mostly intended as a basis for custom installations using opam and contains the following package(s):

coq.8.15.2 (8.15.2) Formal proof management system
authors
The Coq development team, INRIA, CNRS, and contributors.
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
The Coq proof assistant provides a formal language to write
mathematical definitions, executable algorithms, and theorems, together
with an environment for semi-interactive development of machine-checked
proofs. Typical applications include the certification of properties of programming
languages (e.g., the CompCert compiler certification project and the
Bedrock verified low-level programming library), the formalization of
mathematics (e.g., the full formalization of the Feit-Thompson theorem
and homotopy type theory) and teaching.
dune-configurator.3.4.1 (3.4.1) Helper library for gathering system configuration
authors
Jane Street Group, LLC <opensource@janestreet.com>
license
MIT
links
(homepage) (bug reports) (opam package)
description
dune-configurator is a small library that helps writing OCaml scripts that
test features available on the system, in order to generate config.h
files for instance.
Among other things, dune-configurator allows one to:
- test if a C program compiles
- query pkg-config
- import #define from OCaml header files
- generate config.h file
dune.3.4.1 (3.4.1) Fast, portable, and opinionated build system
authors
Jane Street Group, LLC <opensource@janestreet.com>
license
MIT
links
(homepage) (bug reports) (opam package)
description
dune is a build system that was designed to simplify the release of
Jane Street packages. It reads metadata from \dune\ files following a
very simple s-expression syntax.

dune is fast, has very low-overhead, and supports parallel builds on
all platforms. It has no system dependencies; all you need to build
dune or packages using dune is OCaml. You don't need make or bash
as long as the packages themselves don't use bash explicitly.

dune supports multi-package development by simply dropping multiple
repositories into the same directory.

It also supports multi-context builds, such as building against
several opam roots/switches simultaneously. This helps maintaining
packages across several versions of OCaml and gives cross-compilation
for free.

Coq Platform 2023.03.0 with Coq 8.15.2 "IDE level"

The IDE level adds an interactive development environment to the base level.

For beginners, e.g. following introductory tutorials, this level is usually sufficient. If you install the IDE level, you can later add additional packages individually via opam install 'package-name' or rerun the Coq Platform installation script and choose the full or extended level.

The IDE level contains the following package(s):

coqide.8.15.2 (8.15.2) IDE of the Coq formal proof management system
authors
The Coq development team, INRIA, CNRS, and contributors.
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
CoqIDE is a graphical user interface for interactive development
of mathematical definitions, executable algorithms, and proofs of theorems
using the Coq proof assistant.

Coq Platform 2023.03.0 with Coq 8.15.2 "full level"

The full level adds many commonly used coq libraries, plug-ins and developments.

The packages in the full level are mature, well maintained and suitable as basis for your own developments. See the Coq Platform charter for details.

The full level contains the following packages:

coq-aac-tactics.8.15.1 (8.15.1) Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
authors
Thomas Braibant Damien Pous Fabian Kunze
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
This Coq plugin provides tactics for rewriting and proving universally
quantified equations modulo associativity and commutativity of some operator,
with idempotent commutative operators enabling additional simplifications.
The tactics can be applied for custom operators by registering the operators and
their properties as type class instances. Instances for many commonly used operators,
such as for binary integer arithmetic and booleans, are provided with the plugin.
coq-bignums.8.15.0 (8.15.0) Bignums, the Coq library of arbitrary large numbers
authors
Laurent Théry - Benjamin Grégoire - Arnaud Spiwack - Evgeny Makarov - Pierre Letouzey
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Provides BigN, BigZ, BigQ that used to be part of Coq standard library
coq-coqeal.1.1.1 (1.1.1) CoqEAL - The Coq Effective Algebra Library
authors
Guillaume Cano - Cyril Cohen - Maxime Dénès - Érik Martin-Dorel - Anders Mörtberg - Damien Rouhling - Pierre Roux - Vincent Siles
license
MIT
links
(homepage) (bug reports) (opam package)
description
This Coq library contains a subset of the work that was developed in the context
of the ForMath EU FP7 project (2009-2013). It has two parts:
- theory, which contains developments in algebra including normal forms of matrices,
and optimized algorithms on MathComp data structures.
- refinements, which is a framework to ease change of data representations during a proof.
coq-coqprime-generator.1.1.1 (1.1.1) Certificate generator for prime numbers in Coq
authors
Laurent Théry
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
coq-coqprime.1.2.0 (1.2.0) Certifying prime numbers in Coq
authors
Laurent Théry
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
coq-coquelicot.3.2.0 (3.2.0) A Coq formalization of real analysis compatible with the standard library
authors
Sylvie Boldo <sylvie.boldo@inria.fr> - Catherine Lelay <catherine.lelay@inria.fr> - Guillaume Melquiond <guillaume.melquiond@inria.fr>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-corn.8.13.0 (8.13.0) The Coq Constructive Repository at Nijmegen
authors
Evgeny Makarov - Robbert Krebbers - Eelis van der Weegen - Bas Spitters - Jelle Herold - Russell O'Connor - Cezary Kaliszyk - Dan Synek - Luís Cruz-Filipe - Milad Niqui - Iris Loeb - Herman Geuvers - Randy Pollack - Freek Wiedijk - Jan Zwanenburg - Dimitri Hendriks - Henk Barendregt - Mariusz Giero - Rik van Ginneken - Dimitri Hendriks - Sébastien Hinderer - Bart Kirkels - Pierre Letouzey - Lionel Mamane - Nickolay Shmyrev - Vincent Semeria
license
GPL-2.0-only
links
(homepage) (bug reports) (opam package)
description
CoRN includes the following parts:

- Algebraic Hierarchy

An axiomatic formalization of the most common algebraic
structures, including setoids, monoids, groups, rings,
fields, ordered fields, rings of polynomials, real and
complex numbers

- Model of the Real Numbers

Construction of a concrete real number structure
satisfying the previously defined axioms

- Fundamental Theorem of Algebra

A proof that every non-constant polynomial on the complex
plane has at least one root

- Real Calculus

A collection of elementary results on real analysis,
including continuity, differentiability, integration,
Taylor's theorem and the Fundamental Theorem of Calculus

- Exact Real Computation

Fast verified computation inside Coq. This includes: real numbers, functions,
integrals, graphs of functions, differential equations.
coq-dpdgraph.1.0+8.15 (1.0+8.15) Compute dependencies between Coq objects (definitions, theorems) and produce graphs
authors
Anne Pacalet Yves Bertot Olivier Pons
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Coq plugin that extracts the dependencies between Coq objects,
and produces files with dependency information. Includes tools
to visualize dependency graphs and find unused definitions.
coq-elpi.1.14.0 (1.14.0) Elpi extension language for Coq
authors
Enrico Tassi
license
LGPL-2.1-or-later
links
(homepage) (bug reports) (opam package)
description
Coq-elpi provides a Coq plugin that embeds ELPI.
It also provides a way to embed Coq's terms into λProlog using
the Higher-Order Abstract Syntax approach
and a way to read terms back. In addition to that it exports to ELPI a
set of Coq's primitives, e.g. printing a message, accessing the
environment of theorems and data types, defining a new constant and so on.
For convenience it also provides a quotation and anti-quotation for Coq's
syntax in λProlog. E.g. `{{nat}}` is expanded to the type name of natural
numbers, or `{{A -> B}}` to the representation of a product by unfolding
the `->` notation. Finally it provides a way to define new vernacular commands
and
new tactics.
coq-equations.1.3+8.15 (1.3+8.15) A function definition package for Coq
authors
Matthieu Sozeau <matthieu.sozeau@inria.fr> - Cyprien Mangin <cyprien.mangin@m4x.org>
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Equations is a function definition plugin for Coq, that allows the
definition of functions by dependent pattern-matching and well-founded,
mutual or nested structural recursion and compiles them into core
terms. It automatically derives the clauses equations, the graph of the
function and its associated elimination principle.
coq-ext-lib.0.11.7 (0.11.7) A library of Coq definitions, theorems, and tactics
authors
Gregory Malecha
license
BSD-2-Clause
links
(homepage) (bug reports) (opam package)
description
A collection of theories and plugins that may be useful in other Coq developments.
coq-flocq.4.1.0 (4.1.0) A formalization of floating-point arithmetic for the Coq system
authors
Sylvie Boldo <sylvie.boldo@inria.fr> - Guillaume Melquiond <guillaume.melquiond@inria.fr>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-gappa.1.5.2 (1.5.2) A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
authors
Guillaume Melquiond <guillaume.melquiond@inria.fr>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-hammer-tactics.1.3.2+8.15 (1.3.2+8.15) Reconstruction tactics for the hammer for Coq
authors
Lukasz Czajka <lukaszcz@mimuw.edu.pl>
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Collection of tactics that are used by the hammer for Coq
to reconstruct proofs found by automated theorem provers. When the hammer
has been successfully applied to a project, only this package needs
to be installed; the hammer plugin is not required.
coq-hammer.1.3.2+8.15 (1.3.2+8.15) General-purpose automated reasoning hammer tool for Coq
authors
Lukasz Czajka <lukaszcz@mimuw.edu.pl> - Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
A general-purpose automated reasoning hammer tool for Coq that combines
learning from previous proofs with the translation of problems to the
logics of automated systems and the reconstruction of successfully found proofs.
coq-hierarchy-builder.1.3.0 (1.3.0) High level commands to declare and evolve a hierarchy based on packed classes
authors
Cyril Cohen Kazuhiko Sakaguchi Enrico Tassi
license
MIT
links
(homepage) (bug reports) (opam package)
description
Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these
hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder
and abbreviation that let the hierarchy developer describe an actual interface for their library.
Behind that interface the developer can provide appropriate code to ensure retro compatibility.
coq-hott.8.15 (8.15) The Homotopy Type Theory library
authors
The Coq-HoTT Development Team
license
BSD-2-Clause
links
(homepage) (bug reports) (opam package)
description
To use the HoTT library, the following flags must be passed to coqc:
-noinit -indices-matter
To use the HoTT library in a project, add the following to _CoqProject:
-arg -noinit
-arg -indices-matter
coq-interval.4.5.2 (4.5.2) A Coq tactic for proving bounds on real-valued expressions automatically
authors
Guillaume Melquiond <guillaume.melquiond@inria.fr> - Érik Martin-Dorel <erik.martin-dorel@irit.fr> - Pierre Roux <pierre.roux@onera.fr> - Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>
license
CECILL-C
links
(homepage) (bug reports) (opam package)
description
coq-iris-heap-lang.4.0.0 (4.0.0) The canonical example language for Iris
authors
The Iris Team
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
This package defines HeapLang, a concurrent lambda calculus with references, and
uses Iris to build a program logic for HeapLang programs.
coq-iris.4.0.0 (4.0.0) A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
authors
The Iris Team
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Iris is a framework for reasoning about the safety of concurrent programs using
concurrent separation logic. It can be used to develop a program logic, for
defining logical relations, and for reasoning about type systems, among other
applications. This package includes the base logic, Iris Proof Mode (IPM) /
MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
for an instantiation of the program logic to a particular programming language.
coq-itauto.8.15.0 (8.15.0) 'itauto' is a reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support
authors
Frédéric Besson
license
MIT
links
(homepage) (bug reports (email), bug reports) (opam package)
description
coq-libhyps.2.0.6 (2.0.6) Hypotheses manipulation library
authors
Pierre Courtieu
license
MIT
links
(homepage) (bug reports) (opam package)
description
This library defines a set of tactics to manipulate hypothesis
individually or by group. In particular it allows applying a tactic on
each hypothesis of a goal, or only on *new* hypothesis after some
tactic. Examples of manipulations: automatic renaming, subst, revert,
or any tactic expecting a hypothesis name as argument.

It also provides the especialize tactic to ease forward reasoning by
instantianting one, several or all premisses of a hypothesis.
coq-math-classes.8.15.0 (8.15.0) A library of abstract interfaces for mathematical structures in Coq
authors
Eelis van der Weegen Bas Spitters Robbert Krebbers
license
MIT
links
(homepage) (bug reports) (opam package)
description
Math classes is a library of abstract interfaces for mathematical
structures, such as:

* Algebraic hierarchy (groups, rings, fields, …)
* Relations, orders, …
* Categories, functors, universal algebra, …
* Numbers: N, Z, Q, …
* Operations, (shift, power, abs, …)

It is heavily based on Coq’s new type classes in order to provide:
structure inference, multiple inheritance/sharing, convenient
algebraic manipulation (e.g. rewriting) and idiomatic use of
notations.
coq-mathcomp-algebra-tactics.1.0.0 (1.0.0) Ring and field tactics for Mathematical Components
authors
Kazuhiko Sakaguchi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library provides `ring` and `field` tactics for Mathematical Components,
that work with any `comRingType` and `fieldType` instances, respectively.
Their instance resolution is done through canonical structure inference.
Therefore, they work with abstract rings and do not require `Add Ring` and
`Add Field` commands. Another key feature of this library is that they
automatically push down ring morphisms and additive functions to leaves of
ring/field expressions before normalization to the Horner form.
coq-mathcomp-algebra.1.15.0 (1.15.0) Mathematical Components Library on Algebra
authors
Jeremy Avigad - Andrea Asperti - Stephane Le Roux - Yves Bertot - Laurence Rideau - Enrico Tassi - Ioana Pasca - Georges Gonthier - Sidi Ould Biha - Cyril Cohen - Francois Garillot - Alexey Solovyev - Russell O'Connor - Laurent Théry - Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library contains definitions and theorems about discrete
(i.e. with decidable equality) algebraic structures : ring, fields,
ordered fields, real fields, modules, algebras, integers, rational
numbers, polynomials, matrices, vector spaces...
coq-mathcomp-analysis.0.5.4 (0.5.4) An analysis library for mathematical components
authors
Reynald Affeldt - Yves Bertot - Cyril Cohen - Marie Kerjean - Assia Mahboubi - Damien Rouhling - Pierre Roux - Kazuhiko Sakaguchi - Zachary Stone - Pierre-Yves Strub - Laurent Théry
license
CECILL-C
links
(homepage) (bug reports) (opam package)
description
This repository contains an experimental library for real analysis for
the Coq proof-assistant and using the Mathematical Components library.
coq-mathcomp-bigenough.1.0.1 (1.0.1) A small library to do epsilon - N reasoning
authors
Cyril Cohen
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
The package contains a package to reasoning with big enough objects
(mostly natural numbers). This package is essentially for backward
compatibility purposes as `bigenough` will be subsumed by the near
tactics. The formalization is based on the Mathematical Components
library.
coq-mathcomp-character.1.15.0 (1.15.0) Mathematical Components Library on character theory
authors
Jeremy Avigad - Andrea Asperti - Stephane Le Roux - Yves Bertot - Laurence Rideau - Enrico Tassi - Ioana Pasca - Georges Gonthier - Sidi Ould Biha - Cyril Cohen - Francois Garillot - Alexey Solovyev - Russell O'Connor - Laurent Théry - Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library contains definitions and theorems about group
representations, characters and class functions.
coq-mathcomp-field.1.15.0 (1.15.0) Mathematical Components Library on Fields
authors
Jeremy Avigad - Andrea Asperti - Stephane Le Roux - Yves Bertot - Laurence Rideau - Enrico Tassi - Ioana Pasca - Georges Gonthier - Sidi Ould Biha - Cyril Cohen - Francois Garillot - Alexey Solovyev - Russell O'Connor - Laurent Théry - Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library contains definitions and theorems about field extensions,
galois theory, algebraic numbers, cyclotomic polynomials...
coq-mathcomp-fingroup.1.15.0 (1.15.0) Mathematical Components Library on finite groups
authors
Jeremy Avigad - Andrea Asperti - Stephane Le Roux - Yves Bertot - Laurence Rideau - Enrico Tassi - Ioana Pasca - Georges Gonthier - Sidi Ould Biha - Cyril Cohen - Francois Garillot - Alexey Solovyev - Russell O'Connor - Laurent Théry - Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library contains definitions and theorems about finite groups,
group quotients, group morphisms, group presentation, group action...
coq-mathcomp-finmap.1.5.2 (1.5.2) Finite sets, finite maps, finitely supported functions
authors
Cyril Cohen Kazuhiko Sakaguchi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library is an extension of mathematical component in order to
support finite sets and finite maps on choicetypes (rather that finite
types). This includes support for functions with finite support and
multisets. The library also contains a generic order and set libary,
which will be used to subsume notations for finite sets, eventually.
coq-mathcomp-multinomials.1.5.5 (1.5.5) A Multivariate polynomial Library for the Mathematical Components Library
authors
Pierre-Yves Strub
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
coq-mathcomp-real-closed.1.1.3 (1.1.3) Mathematical Components Library on real closed fields
authors
Cyril Cohen Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library contains definitions and theorems about real closed
fields, with a construction of the real closure and the algebraic
closure (including a proof of the fundamental theorem of
algebra). It also contains a proof of decidability of the first
order theory of real closed field, through quantifier elimination.
coq-mathcomp-solvable.1.15.0 (1.15.0) Mathematical Components Library on finite groups (II)
authors
Jeremy Avigad - Andrea Asperti - Stephane Le Roux - Yves Bertot - Laurence Rideau - Enrico Tassi - Ioana Pasca - Georges Gonthier - Sidi Ould Biha - Cyril Cohen - Francois Garillot - Alexey Solovyev - Russell O'Connor - Laurent Théry - Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library contains more definitions and theorems about finite groups.
coq-mathcomp-ssreflect.1.15.0 (1.15.0) Small Scale Reflection
authors
Jeremy Avigad - Andrea Asperti - Stephane Le Roux - Yves Bertot - Laurence Rideau - Enrico Tassi - Ioana Pasca - Georges Gonthier - Sidi Ould Biha - Cyril Cohen - Francois Garillot - Alexey Solovyev - Russell O'Connor - Laurent Théry - Assia Mahboubi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library includes the small scale reflection proof language
extension and the minimal set of libraries to take advantage of it.
This includes libraries on lists (seq), boolean and boolean
predicates, natural numbers and types with decidable equality,
finite types, finite sets, finite functions, finite graphs, basic arithmetics
and prime numbers, big operators
coq-mathcomp-word.1.1 (1.1) Yet Another Coq Library on Machine Words
authors
Pierre-Yves Strub
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-mathcomp-zify.1.2.0+1.12+8.13 (1.2.0+1.12+8.13) Micromega tactics for Mathematical Components
authors
Kazuhiko Sakaguchi
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This small library enables the use of the Micromega arithmetic solvers of Coq
for goals stated with the definitions of the Mathematical Components library
by extending the zify tactic.
coq-menhirlib.20220210 (20220210) A support library for verified Coq parsers produced by Menhir
authors
Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-mtac2.1.4+8.15 (1.4+8.15) Mtac2: Typed Tactics for Coq
authors
Beta Ziliani <beta.ziliani@gmail.com> - Jan-Oliver Kaiser <janno@mpi-sws.org> - Robbert Krebbers <mail@robbertkrebbers.nl> - Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> - Derek Dreyer <dreyer@mpi-sws.org>
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-ott.0.32 (0.32) Auxiliary Coq library for Ott, a tool for writing definitions of programming languages and calculi
authors
Peter Sewell Francesco Zappa Nardelli Scott Owens
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Ott takes as input a definition of a language syntax and semantics, in a concise
and readable ASCII notation that is close to what one would write in informal
mathematics. It can then generate a Coq version of the definition, which requires
this library.
coq-paramcoq.1.1.3+coq8.15 (1.1.3+coq8.15) Plugin for generating parametricity statements to perform refinement proofs
authors
Chantal Keller (Inria, École polytechnique) - Marc Lasson (ÉNS de Lyon) - Abhishek Anand - Pierre Roux - Emilio Jesús Gallego Arias - Cyril Cohen - Matthieu Sozeau
license
MIT
links
(homepage) (bug reports) (opam package)
description
A Coq plugin providing commands for generating parametricity statements.
Typical applications of such statements are in data refinement proofs.
Note that the plugin is still in an experimental state - it is not very user
friendly (lack of good error messages) and still contains bugs. But it
is usable enough to \translate\ a large chunk of the standard library.
coq-quickchick.1.6.4 (1.6.4) Randomized Property-Based Testing Plugin for Coq
authors
Leonidas Lampropoulos - Zoe Paraskevopoulou - Maxime Denes - Catalin Hritcu - Benjamin Pierce - Li-yao Xia - Arthur Azevedo de Amorim - Yishuai Li - Antal Spector-Zabusky
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-reglang.1.1.3 (1.1.3) Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
authors
Christian Doczkal Jan-Oliver Kaiser Gert Smolka
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
This library provides definitions and verified translations between
different representations of regular languages: various forms of
automata (deterministic, nondeterministic, one-way, two-way),
regular expressions, and the logic WS1S. It also contains various
decidability results and closure properties of regular languages.
coq-relation-algebra.1.7.7 (1.7.7) Relation Algebra and KAT in Coq
authors
Damien Pous <Damien.Pous@ens-lyon.fr> - Christian Doczkal <christian.doczkal@ens-lyon.fr>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-simple-io.1.7.0 (1.7.0) IO monad for Coq
authors
Li-yao Xia Yishuai Li
license
MIT
links
(homepage) (bug reports) (opam package)
description
This library provides tools to implement IO programs directly in Coq, in a
similar style to Haskell. Facilities for formal verification are not included.

IO is defined as a parameter with a purely functional interface in Coq,
to be extracted to OCaml. Some wrappers for the basic types and functions in
the OCaml Pervasives module are provided. Users are free to define their own
APIs on top of this IO type.
coq-stdpp.1.8.0 (1.8.0) An extended \Standard Library\ for Coq
authors
The std++ team
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
The key features of this library are as follows:

- It provides a great number of definitions and lemmas for common data
structures such as lists, finite maps, finite sets, and finite multisets.
- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
monad notations) so that these can be overloaded for different data structures.
- It uses type classes to keep track of common properties of types, like it
having decidable equality or being countable or finite.
- Most data structures are represented in canonical ways so that Leibniz
equality can be used as much as possible (for example, for maps we have
`m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
setoid instances for most types and operations.
- It provides various tactics for common tasks, like an ssreflect inspired
`done` tactic for finishing trivial goals, a simple breadth-first solver
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely dependency- and axiom-free.
coq-unicoq.1.6+8.15 (1.6+8.15) An enhanced unification algorithm for Coq
authors
Matthieu Sozeau <matthieu.sozeau@inria.fr> - Beta Ziliani <beta@mpi-sws.org>
license
MIT
links
(homepage) (bug reports) (opam package)
description
eprover.2.6 (2.6) E Theorem Prover
authors
Stephan Schulz - Simon Cruanes - Petar Vukmirovic - Mohamed Bassem - Martin Moehrmann
license
LGPL-2.1-or-later GPL-2.0-or-later
links
(homepage) (bug reports: Stephan Schulz (see homepage for email)) (opam package)
description
E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms.
gappa.1.4.1 (1.4.1) Tool intended for formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic
authors
Guillaume Melquiond
license
CECILL - see homepage for details
links
(homepage) (bug reports) (opam package)
description
menhir.20220210 (20220210) An LR(1) parser generator
authors
François Pottier <francois.pottier@inria.fr> - Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>
license
LGPL-2.0-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
ott.0.32 (0.32) A tool for writing definitions of programming languages and calculi
authors
Peter Sewell Francesco Zappa Nardelli Scott Owens
license
BSD-3-Clause LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Ott takes as input a definition of a language syntax and semantics, in a
concise and readable ASCII notation that is close to what one would write in
informal mathematics. It generates output:
- a LaTeX source file that defines commands to build a typeset version of the definition;
- a Coq version of the definition;
- a HOL version of the definition;
- an Isabelle/HOL version of the definition;
- a Lem version of the definition;
- an OCaml version of the syntax of the definition.
Additionally, it can be run as a filter, taking a
LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file
with embedded (symbolic) terms of the defined language, parsing them and
replacing them by typeset terms.
ppxlib.0.25.1 (0.25.1) Standard library for ppx rewriters
authors
Jane Street Group, LLC <opensource@janestreet.com>
license
MIT
links
(homepage) (bug reports) (opam package)
description
Ppxlib is the standard library for ppx rewriters and other programs
that manipulate the in-memory reprensation of OCaml programs, a.k.a
the \Parsetree\.

It also comes bundled with two ppx rewriters that are commonly used to
write tools that manipulate and/or generate Parsetree values;
`ppxlib.metaquot` which allows to construct Parsetree values using the
OCaml syntax directly and `ppxlib.traverse` which provides various
ways of automatically traversing values of a given type, in particular
allowing to inject a complex structured value into generated code.
sexplib0.v0.14.0 (v0.14.0) Library containing the definition of S-expressions and some base converters
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
Part of Jane Street's Core library
The Core suite of libraries is an industrial strength alternative to
OCaml's standard library that was developed by Jane Street, the
largest industrial user of OCaml.
z3_tptp.4.11.0 (4.11.0) TPTP front end for Z3 solver
authors
MSR
license
MIT
links
(homepage) (bug reports) (opam package)
description

Coq Platform 2023.03.0 with Coq 8.15.2 "optional packages"

The optional packages have the same maturity and maintenance level as the packages in the full level, but either take a rather long time to build or have a non open source license or depend on packages with non open source license.

The interactive installation script and the Windows installer explicitly ask if you want to install these packages.

The macOS and snap installation bundles always include these packages.

The following packages are optional:

coq-compcert.3.11 (3.11) The CompCert C compiler (64 bit)
authors
Xavier Leroy <xavier.leroy@inria.fr>
license
INRIA Non-Commercial License Agreement - see homepage for details
links
(homepage) (bug reports) (opam package)
description
coq-unimath.20220816 (20220816) Library of Univalent Mathematics
authors
The UniMath Development Team
license
Kind of MIT - see homepage for details
links
(homepage) (bug reports) (opam package)
description
coq-vst.2.11.1 (2.11.1) Verified Software Toolchain
authors
Andrew W. Appel - Lennart Beringer - Josiah Dodds - Qinxiang Cao - Aquinas Hobor - Gordon Stewart - Qinshi Wang - Sandrine Blazy - Santiago Cuellar - Robert Dockins - Nick Giannarakis - Samuel Gruetter - Jean-Marie Madiot
license
BSD-2-Clause
links
(homepage) (bug reports) (opam package)
description
The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context.

Coq Platform 2023.03.0 with Coq 8.15.2 "extended level"

The extended level contains packages which are in a beta stage or otherwise don't yet have the level of maturity or support required for inclusion in the full level, but there are plans to move them to the full level in a future release of Coq Platform. The main point of the extended level is advertisement: users are important to bring a development from a beta to a release state.

The interactive installation script explicitly asks if you want to install these packages. The macOS and snap installation bundles always include these packages. The Windows installer also includes them, and they are selected by default.

The extended level contains the following packages:

coq-bedrock2-compiler.0.0.4 (0.0.4) A work-in-progress language and compiler for verified low-level programming (compiler part)
authors
Massachusetts Institute of Technology Kevix SiFive
license
MIT
links
(homepage) (bug reports) (opam package)
description
bedrock2 is a low-level systems programming language. This language is
equipped with a simple program logic for proving correctness of the
programs. This package includes a verified compiler targeting RISC-V
from this language.

The project has similar goals as bedrock, but uses a different design.
No code is shared between bedrock and bedrock2.
coq-bedrock2.0.0.4 (0.0.4) A work-in-progress language and compiler for verified low-level programming
authors
Massachusetts Institute of Technology Kevix SiFive
license
MIT
links
(homepage) (bug reports) (opam package)
description
bedrock2 is a low-level systems programming language. This language is
equipped with a simple program logic for proving correctness of the
programs. A verified compiler targeting RISC-V from this language
exists in the coq-bedrock2-compiler package on opam.

The project has similar goals as bedrock, but uses a different design.
No code is shared between bedrock and bedrock2.
coq-coqutil.0.0.2 (0.0.2) Coq library for tactics, basic definitions, sets, maps
authors
Massachusetts Institute of Technology
license
MIT
links
(homepage) (bug reports) (opam package)
description
### coqutil -- Various Coq Utilities

Contents:
* [Datatypes](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Datatypes): Some utilities for existing datatypes, and new datatypes.
* [Decidable](https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Decidable.v): `BoolSpec`-based decidability typeclasses. Allows one to write `if MyType_eqb a b then ... else ...` where `MyType_eqb a b` returns a `bool`, instead of writing `if MyType_eq_dec a b then ... else ...` where `MyType_eq_dec a b` returns a `sumbool`, while still getting `a = b` and `a <> b` as hypotheses (as opposed to `MyType_eqb a b = true` and `MyType_eqb a b = false`) after destructing the `if` (need to use [`destr`](https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/destr.v) instead of `destruct`). So one gets the benefits of `Sumbool` without getting its disadvantage of having to carry around proof terms, which can cause a blow-up under reduction if one is not careful.
* [Map](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Map): A typeclass based map library allowing one to abstract over the concrete implementation of maps. The implementations have to be extensional, which excludes certain efficient implementations, but simplifies proofs, because one can `replace mapA with mapB` if one can prove that `mapA` and `mapB` have the same contents. Comes with a [solver](https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Map/Solver.v) which works reasonably fast on most map goals we have encountered so far.
* [Tactics](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Tactics): A collection of useful general-purpose tactics.
* [Word](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Word): Fixed width words for any width, in the same typeclass based style as the map library. Designed for the case where all words have the same (potentially abstract) bit width. Therefore, it does not provide functions to concatenate and split words, which is better addressed by [bbv](https://github.com/mit-plv/bbv/).
* [Z](https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Z): Utilities to work with the `Z` type from Coq's standard library, including a tactic to prove `Z` equalities by splitting the equality into equalities on bit index ranges, a tactic to make `lia` capable of reasoning about goals with division and modulo, and a tactic to simplify expressions containing nested occurrences of `mod`, and more misc utilities.
* Various macros, notations, and desirable default settings.

Each feature is intended to be as minimal and as independent of the other features as possible, so that users can pick just what they need.
coq-deriving.0.1.0 (0.1.0) Generic instances of MathComp classes
authors
Arthur Azevedo de Amorim
license
MIT
links
(homepage) (bug reports) (opam package)
description
Deriving provides generic instances of MathComp classes for
inductive data types. It includes native support for eqType,
choiceType, countType and finType instances, and it allows users to
define their own instances for other classes.
coq-extructures.0.3.1 (0.3.1) Finite sets, maps, and other data structures with extensional reasoning
authors
Arthur Azevedo de Amorim
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-fiat-crypto.0.0.17 (0.0.17) Cryptographic Primitive Code Generation by Fiat
authors
Andres Erbsen <andreser@mit.edu> - Google Inc. - Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com> - Massachusetts Institute of Technology - Zoe Paraskevopoulou <zoe.paraskevopoulou@gmail.com>
license
MIT OR Apache-2.0 OR BSD-1-Clause - see homepage for details
links
(homepage) (bug reports) (opam package)
description
Coq code and proofs for a command-line binary that can synthesize proven-correct
big-integer modular field arithmetic operations for cryptography.
Target languages include C, Rust, Zig, Go, and bedrock2.
coq-metacoq.1.1+8.15 (1.1+8.15) A meta-programming framework for Coq
authors
Abhishek Anand <aa755@cs.cornell.edu> - Danil Annenkov <danil.v.annenkov@gmail.com> - Simon Boulier <simon.boulier@inria.fr> - Cyril Cohen <cyril.cohen@inria.fr> - Yannick Forster <forster@ps.uni-saarland.de> - Fabian Kunze <fkunze@fakusb.de> - Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr> - Kenji Maillard <kenji.maillard@inria.fr> - Gregory Malecha <gmalecha@gmail.com> - Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> - Matthieu Sozeau <matthieu.sozeau@inria.fr> - Nicolas Tabareau <nicolas.tabareau@inria.fr> - Théo Winterhalter <theo.winterhalter@inria.fr>
license
MIT
links
(homepage) (bug reports) (opam package)
description
MetaCoq is a meta-programming framework for Coq.

The meta-package includes the template-coq library,
the PCUIC development including a verified equivalence between Coq and PCUIC,
a safe type checker and verified erasure for PCUIC and example translations.

See individual packages for more detailed descriptions.
coq-record-update.0.3.0 (0.3.0) Generic support for updating record fields in Coq
authors
Tej Chajed
license
MIT
links
(homepage) (bug reports) (opam package)
description
While Coq provides projections for each field of a record, it has no
convenient way to update a single field of a record. This library provides a
generic way to update a field by name, where the user only has to implement a
simple typeclass that lists out the record fields.
coq-reduction-effects.0.1.4 (0.1.4) A Coq plugin to add reduction side effects to some Coq reduction strategies
authors
Hugo Herbelin
license
MPL-2.0
links
(homepage) (bug reports) (opam package)
description
coq-rewriter.0.0.6 (0.0.6) Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography
authors
Google Inc. Massachusetts Institute of Technology
license
MIT OR Apache-2.0 OR BSD-1-Clause - see homepage for details
links
(homepage) (bug reports) (opam package)
description
coq-riscv.0.0.3 (0.0.3) RISC-V Specification in Coq, somewhat experimental
authors
Massachusetts Institute of Technology
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
coq-rupicola.0.0.6 (0.0.6) Gallina to imperative code compilation, currently in design phase
authors
Clément Pit-Claudel <clement.pitclaudel@live.com> - Jade Philipoom - Dustin Jamner - Andres Erbsen - Adam Chlipala
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-serapi.8.15.0+0.15.2 (8.15.0+0.15.2) Serialization library and protocol for machine interaction with the Coq proof assistant
authors
Emilio Jesús Gallego Arias - Karl Palmskog - Clément Pit-Claudel - Kaiyu Yang
license
GPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
SerAPI is a library for machine-to-machine interaction with the
Coq proof assistant, with particular emphasis on applications in IDEs,
code analysis tools, and machine learning. SerAPI provides automatic
serialization of Coq's internal OCaml datatypes from/to JSON or
S-expressions (sexps).

Dependency packages

In addition the dependencies listed below are partially or fully included or required during build time. Please note, that the version numbers given are the versions of opam packages, which do not always match with the version of the supplied packages. E.g. some opam packages just refer to latest packages e.g. installed by MacPorts, Homebrew or Linux system package managers. Please refer to the linked opam package and/or your system package manager for details on what software version is used.

base-bigarray.base (base)
authors
license
unknown - please clarify with homepage
links
(opam package)
description
Bigarray library distributed with the OCaml compiler
base-threads.base (base)
authors
license
unknown - please clarify with homepage
links
(opam package)
description
Threads library distributed with the OCaml compiler
base-unix.base (base)
authors
license
unknown - please clarify with homepage
links
(opam package)
description
Unix library distributed with the OCaml compiler
base.v0.14.3 (v0.14.3) Full standard library replacement for OCaml
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
Full standard library replacement for OCaml

Base is a complete and portable alternative to the OCaml standard
library. It provides all standard functionalities one would expect
from a language standard library. It uses consistent conventions
across all of its module.

Base aims to be usable in any context. As a result system dependent
features such as I/O are not offered by Base. They are instead
provided by companion libraries such as stdio:

https://github.com/janestreet/stdio
cairo2.0.6.4 (0.6.4) Binding to Cairo, a 2D Vector Graphics Library
authors
Christophe Troestler <Christophe.Troestler@umons.ac.be> - Pierre Hauweele <pierre@hauweele.net>
license
LGPL-3.0
links
(homepage) (bug reports) (opam package)
description
This is a binding to Cairo, a 2D graphics library with support for
multiple output devices. Currently supported output targets include
the X Window System, Quartz, Win32, image buffers, PostScript, PDF,
and SVG file output.
camlp-streams.5.0.1 (5.0.1) The Stream and Genlex libraries for use with Camlp4 and Camlp5
authors
Daniel de Rauglaudre Xavier Leroy
license
LGPL-2.1-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
This package provides two library modules:
- Stream: imperative streams, with in-place update and memoization
of the latest element produced.
- Genlex: a small parameterized lexical analyzer producing streams
of tokens from streams of characters.

The two modules are designed for use with Camlp4 and Camlp5:
- The stream patterns and stream expressions of Camlp4/Camlp5 consume
and produce data of type 'a Stream.t.
- The Genlex tokenizer can be used as a simple lexical analyzer for
Camlp4/Camlp5-generated parsers.

The Stream module can also be used by hand-written recursive-descent
parsers, but is not very convenient for this purpose.

The Stream and Genlex modules have been part of the OCaml standard library
for a long time, and have been distributed as part of the core OCaml system.
They will be removed from the OCaml standard library at some future point,
but will be maintained and distributed separately in this camlpstreams package.
cmdliner.1.1.1 (1.1.1) Declarative definition of command line interfaces for OCaml
authors
The cmdliner programmers
license
ISC
links
(homepage) (bug reports) (opam package)
description
Cmdliner allows the declarative definition of command line interfaces
for OCaml.

It provides a simple and compositional mechanism to convert command
line arguments to OCaml values and pass them to your functions. The
module automatically handles syntax errors, help messages and UNIX man
page generation. It supports programs with single or multiple commands
and respects most of the [POSIX][1] and [GNU][2] conventions.

Cmdliner has no dependencies and is distributed under the ISC license.

[1]: http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap12.html
[2]: http://www.gnu.org/software/libc/manual/html_node/Argument-Syntax.html

Home page: http://erratique.ch/software/cmdliner
adwaita-icon-theme.2 (2) Virtual package relying on adwaita-icon-theme
authors
GNOME devs
license
LGPL-3.0-only CC-BY-SA-3.0
links
(homepage) (bug reports) (opam package)
description
This package can only install if the adwaita-icon-theme package is installed on the system.
autoconf.0.1 (0.1) Virtual package relying on autoconf installation
authors
https://www.gnu.org/software/autoconf/autoconf.html#maintainer
license
GPL-3.0-only
links
(homepage) (bug reports) (opam package)
description
This package can only install if the autoconf command
is available on the system.
automake.1 (1) Virtual package relying on GNU automake
authors
Jim Meyering - David J. MacKenzie - https://git.savannah.gnu.org/cgit/automake.git/tree/THANKS
license
GPL-2.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if GNU automake is installed on the system.
bison.2 (2) Virtual package relying on GNU bison
authors
Robert Corbett - Richard Stallman - Wilfred Hansen - Akim Demaille - Paul Hilfinger - Joel E. Denny - Paolo Bonzini - Alex Rozenman - Paul Eggert
license
GPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if GNU bison is installed on the system.
boost.1 (1) Virtual package relying on boost
authors
Beman Dawes, David Abrahams, et al.
license
MIT
links
(homepage) (bug reports) (opam package)
description
This package can only install if the boost library is installed on the system.
c++.1.0 (1.0) Virtual package relying on the c++ compiler
authors
C++ compiler developers
license
GPL-2.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the c++ compiler is installed on the system.
cairo.1 (1) Virtual package relying on a Cairo system installation
authors
Keith Packard Carl Worth Behdad Esfahbod
license
LGPL-2.1-only MPL-1.1
links
(homepage) (bug reports) (opam package)
description
This package can only install if the cairo lib is installed on the system.
findutils.1 (1) Virtual package relying on findutils
authors
GNU Project
license
GPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the findutils binary is installed on the system.
flex.2 (2) Virtual package relying on GNU flex
authors
The Flex Project
license
link
links
(homepage) (bug reports) (opam package)
description
This package can only install if GNU flex is installed on the system.
g++.1.0 (1.0) Virtual package relying on the g++ compiler (for C++)
authors
Francois Berenger
license
GPL-2.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the g++ compiler is installed on the system.
gcc.1.0 (1.0) Virtual package relying on the gcc compiler (for C)
authors
Francois Berenger Francois Bobot
license
GPL-2.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the gcc compiler is installed on the system.
gmp.4 (4) Virtual package relying on a GMP lib system installation
authors
nbraud
license
GPL-1.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the GMP lib is installed on the system.
gtk3.18 (18) Virtual package relying on GTK+ 3
authors
The GTK Toolkit
license
unknown - please clarify with homepage
links
(homepage) (bug reports) (opam package)
description
This package can only install if GTK+ 3 is installed on the system.
gtksourceview3.0+2 (0+2) Virtual package relying on a GtkSourceView-3 system installation
authors
The gtksourceview programmers
license
LGPL-2.1-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if libgtksourceview-3.0-dev is installed on the system.
libjpeg.1 (1) Virtual package relying on a libjpeg system installation
authors
Bob Friesenhahn Lee Howard Frank Warmerdam
license
BSD-like - see homepage for details
links
(homepage) (bug reports) (opam package)
description
This package can only install if the libjpeg is installed on the system.
libtool.1 (1) Virtual package relying on libtool installation
authors
https://www.gnu.org/software/libtool/libtool.html#maintainer
license
GPL-3.0-only
links
(homepage) (bug reports) (opam package)
description
This package can only install if the libtool command
is available on the system.
mpfr.3 (3) Virtual package relying on library MPFR installation
authors
http://www.mpfr.org/credit.html
license
LGPL-2.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the MPFR library is installed on the system.
pkg-config.2 (2) Check if pkg-config is installed and create an opam switch local pkgconfig folder
authors
Francois Berenger
license
GPL-1.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the pkg-config package is installed
on the system.
python-3.9.0.0 (9.0.0) Virtual package relying on Python-3 installation
authors
Python Software Foundation
license
PSF - see homepage for details
links
(homepage) (bug reports) (opam package)
description
This package can only install if a Python-3 interpreter is available
on the system.
If a minor version needs to be specified for your operating system, then
python-3.9 will be used.
which.1 (1) Virtual package relying on which
authors
Carlo Wood
license
GPL-2.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the which program is installed on the system.
coq-metacoq-erasure.1.1+8.15 (1.1+8.15) Implementation and verification of an erasure procedure for Coq
authors
Abhishek Anand <aa755@cs.cornell.edu> - Danil Annenkov <danil.v.annenkov@gmail.com> - Simon Boulier <simon.boulier@inria.fr> - Cyril Cohen <cyril.cohen@inria.fr> - Yannick Forster <forster@ps.uni-saarland.de> - Fabian Kunze <fkunze@fakusb.de> - Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr> - Kenji Maillard <kenji.maillard@inria.fr> - Gregory Malecha <gmalecha@gmail.com> - Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> - Matthieu Sozeau <matthieu.sozeau@inria.fr> - Nicolas Tabareau <nicolas.tabareau@inria.fr> - Théo Winterhalter <theo.winterhalter@inria.fr>
license
MIT
links
(homepage) (bug reports) (opam package)
description
MetaCoq is a meta-programming framework for Coq.

The Erasure module provides a complete specification of Coq's so-called
\extraction\ procedure, starting from the PCUIC calculus and targeting
untyped call-by-value lambda-calculus.

The `erasure` function translates types and proofs in well-typed terms
into a dummy `tBox` constructor, following closely P. Letouzey's PhD
thesis.
coq-metacoq-pcuic.1.1+8.15 (1.1+8.15) A type system equivalent to Coq's and its metatheory
authors
Abhishek Anand <aa755@cs.cornell.edu> - Danil Annenkov <danil.v.annenkov@gmail.com> - Simon Boulier <simon.boulier@inria.fr> - Cyril Cohen <cyril.cohen@inria.fr> - Yannick Forster <forster@ps.uni-saarland.de> - Fabian Kunze <fkunze@fakusb.de> - Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr> - Kenji Maillard <kenji.maillard@inria.fr> - Gregory Malecha <gmalecha@gmail.com> - Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> - Matthieu Sozeau <matthieu.sozeau@inria.fr> - Nicolas Tabareau <nicolas.tabareau@inria.fr> - Théo Winterhalter <theo.winterhalter@inria.fr>
license
MIT
links
(homepage) (bug reports) (opam package)
description
MetaCoq is a meta-programming framework for Coq.

The PCUIC module provides a cleaned-up specification of Coq's typing algorithm along
with a certified typechecker for it. This module includes the standard metatheory of
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
coq-metacoq-safechecker.1.1+8.15 (1.1+8.15) Implementation and verification of safe conversion and typechecking algorithms for Coq
authors
Abhishek Anand <aa755@cs.cornell.edu> - Danil Annenkov <danil.v.annenkov@gmail.com> - Simon Boulier <simon.boulier@inria.fr> - Cyril Cohen <cyril.cohen@inria.fr> - Yannick Forster <forster@ps.uni-saarland.de> - Fabian Kunze <fkunze@fakusb.de> - Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr> - Kenji Maillard <kenji.maillard@inria.fr> - Gregory Malecha <gmalecha@gmail.com> - Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> - Matthieu Sozeau <matthieu.sozeau@inria.fr> - Nicolas Tabareau <nicolas.tabareau@inria.fr> - Théo Winterhalter <theo.winterhalter@inria.fr>
license
MIT
links
(homepage) (bug reports) (opam package)
description
MetaCoq is a meta-programming framework for Coq.

The SafeChecker modules provides a correct implementation of
weak-head reduction, conversion and typechecking of Coq definitions and global environments.
coq-metacoq-template.1.1+8.15 (1.1+8.15) A quoting and unquoting library for Coq in Coq
authors
Abhishek Anand <aa755@cs.cornell.edu> - Danil Annenkov <danil.v.annenkov@gmail.com> - Simon Boulier <simon.boulier@inria.fr> - Cyril Cohen <cyril.cohen@inria.fr> - Yannick Forster <forster@ps.uni-saarland.de> - Fabian Kunze <fkunze@fakusb.de> - Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr> - Kenji Maillard <kenji.maillard@inria.fr> - Gregory Malecha <gmalecha@gmail.com> - Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> - Matthieu Sozeau <matthieu.sozeau@inria.fr> - Nicolas Tabareau <nicolas.tabareau@inria.fr> - Théo Winterhalter <theo.winterhalter@inria.fr>
license
MIT
links
(homepage) (bug reports) (opam package)
description
MetaCoq is a meta-programming framework for Coq.

Template Coq is a quoting library for Coq. It takes Coq terms and
constructs a representation of their syntax tree as a Coq inductive data
type. The representation is based on the kernel's term representation.

In addition to a complete reification and denotation of CIC terms,
Template Coq includes:

- Reification of the environment structures, for constant and inductive declarations.
- Denotation of terms and global declarations
- A monad for manipulating global declarations, calling the type
checker, and inserting them in the global environment, in the style of
MetaCoq/MTac.
coq-metacoq-translations.1.1+8.15 (1.1+8.15) Translations built on top of MetaCoq
authors
Abhishek Anand <aa755@cs.cornell.edu> - Danil Annenkov <danil.v.annenkov@gmail.com> - Simon Boulier <simon.boulier@inria.fr> - Cyril Cohen <cyril.cohen@inria.fr> - Yannick Forster <forster@ps.uni-saarland.de> - Fabian Kunze <fkunze@fakusb.de> - Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr> - Kenji Maillard <kenji.maillard@inria.fr> - Gregory Malecha <gmalecha@gmail.com> - Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com> - Matthieu Sozeau <matthieu.sozeau@inria.fr> - Nicolas Tabareau <nicolas.tabareau@inria.fr> - Théo Winterhalter <theo.winterhalter@inria.fr>
license
MIT
links
(homepage) (bug reports) (opam package)
description
MetaCoq is a meta-programming framework for Coq.

The Translations modules provides implementation of standard translations
from type theory to type theory, e.g. parametricity and the `cross-bool`
translation that invalidates functional extensionality.
coq-vst-zlist.2.11 (2.11) A list library indexed by Z type, with a powerful automatic solver
authors
Qinshi Wang Andrew W. Appel
license
BSD-2-Clause
links
(homepage) (bug reports) (opam package)
description
cppo.1.6.9 (1.6.9) Code preprocessor like cpp for OCaml
authors
Martin Jambon
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Cppo is an equivalent of the C preprocessor for OCaml programs.
It allows the definition of simple macros and file inclusion.

Cppo is:

* more OCaml-friendly than cpp
* easy to learn without consulting a manual
* reasonably fast
* simple to install and to maintain
csexp.1.5.1 (1.5.1) Parsing and printing of S-expressions in Canonical form
authors
Quentin Hocquet <mefyl@gruntech.org> - Jane Street Group, LLC - Jeremie Dimino <jeremie@dimino.org>
license
MIT
links
(homepage) (bug reports) (opam package)
description
This library provides minimal support for Canonical S-expressions
[1]. Canonical S-expressions are a binary encoding of S-expressions
that is super simple and well suited for communication between
programs.

This library only provides a few helpers for simple applications. If
you need more advanced support, such as parsing from more fancy input
sources, you should consider copying the code of this library given
how simple parsing S-expressions in canonical form is.

To avoid a dependency on a particular S-expression library, the only
module of this library is parameterised by the type of S-expressions.

[1] https://en.wikipedia.org/wiki/Canonical_S-expressions
elpi.1.15.2 (1.15.2) ELPI - Embeddable λProlog Interpreter
authors
Claudio Sacerdoti Coen Enrico Tassi
license
LGPL-2.1-or-later
links
(homepage) (bug reports) (opam package)
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.
gmp-ecm.7.0.3 (7.0.3) GMP-ECM library for the Elliptic Curve Method (ECM) for integer factorization
authors
Cyril Bouvier - David Cleaver - Pierrick Gaudry - Brian Gladman - Jim Fougeron - Laurent Fousse - Alexander Kruppa - Francois Morain - Dave Newman - Jason S. Papadopoulos - Paul Zimmermann
license
GPL-3.0 LGPL-3.0
links
(homepage) (bug reports) (opam package)
description
lablgtk3-sourceview3.3.1.3 (3.1.3) OCaml interface to GTK+ gtksourceview library
authors
Jacques Garrigue et al., Nagoya University
license
LGPL-2.1-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
OCaml interface to GTK+3, gtksourceview3 library.

See https://garrigue.github.io/lablgtk/ for more information.
lablgtk3.3.1.3 (3.1.3) OCaml interface to GTK+3
authors
Jacques Garrigue et al., Nagoya University
license
LGPL-2.1-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
OCaml interface to GTK+3

See https://garrigue.github.io/lablgtk/ for more information.
menhirLib.20220210 (20220210) Runtime support library for parsers generated by Menhir
authors
François Pottier <francois.pottier@inria.fr> - Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>
license
LGPL-2.0-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
menhirSdk.20220210 (20220210) Compile-time library for auxiliary tools related to Menhir
authors
François Pottier <francois.pottier@inria.fr> - Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>
license
LGPL-2.0-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
num.1.4 (1.4) The legacy Num library for arbitrary-precision integer and rational arithmetic
authors
Valérie Ménissier-Morain Pierre Weis Xavier Leroy
license
LGPL-2.1-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
ocaml-compiler-libs.v0.12.4 (v0.12.4) OCaml compiler libraries repackaged
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
This packages exposes the OCaml compiler libraries repackages under
the toplevel names Ocaml_common, Ocaml_bytecomp, Ocaml_optcomp, ...
ocaml-config.2 (2) OCaml Switch Configuration
authors
Louis Gesbert <louis.gesbert@ocamlpro.com> - David Allsopp <david.allsopp@metastack.com>
license
unknown - please clarify with homepage
links
(homepage) (bug reports) (opam package)
description
This package is used by the OCaml package to set-up its variables.
ocaml-option-flambda.1 (1) Set OCaml to be compiled with flambda activated
authors
license
unknown - please clarify with homepage
links
(opam package)
description
ocaml-variants.4.13.1+options (4.13.1+options) Official release of OCaml 4.13.1
authors
Xavier Leroy - Damien Doligez - Alain Frisch - Jacques Garrigue - Didier Rémy - Jérôme Vouillon
license
LGPL-2.1-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
ocaml.4.13.1 (4.13.1) The OCaml compiler (virtual package)
authors
Xavier Leroy - Damien Doligez - Alain Frisch - Jacques Garrigue - Didier Rémy - Jérôme Vouillon
license
LGPL-2.1-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
This package requires a matching implementation of OCaml,
and polls it to initialise specific variables like `ocaml:native-dynlink`
ocamlbuild.0.14.2 (0.14.2) OCamlbuild is a build system with builtin rules to easily build most OCaml projects
authors
Nicolas Pouillard Berke Durak
license
LGPL-2.0-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
ocamlfind.1.9.5~relocatable (1.9.5~relocatable) A library manager for OCaml
authors
Gerd Stolpmann <gerd@gerd-stolpmann.de>
license
MIT
links
(homepage) (bug reports) (opam package)
description
Findlib is a library manager for OCaml. It provides a convention how
to store libraries, and a file format (\META\) to describe the
properties of libraries. There is also a tool (ocamlfind) for
interpreting the META files, so that it is very easy to use libraries
in programs and scripts.
ocamlgraph.2.0.0 (2.0.0) A generic graph library for OCaml
authors
Sylvain Conchon Jean-Christophe Filliâtre Julien Signoles
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Provides both graph data structures and graph algorithms
parsexp.v0.14.2 (v0.14.2) S-expression parsing library
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
This library provides generic parsers for parsing S-expressions from
strings or other medium.

The library is focused on performances but still provide full generic
parsers that can be used with strings, bigstrings, lexing buffers,
character streams or any other sources effortlessly.

It provides three different class of parsers:
- the normal parsers, producing [Sexp.t] or [Sexp.t list] values
- the parsers with positions, building compact position sequences so
that one can recover original positions in order to report properly
located errors at little cost
- the Concrete Syntax Tree parsers, produce values of type
[Parsexp.Cst.t] which record the concrete layout of the s-expression
syntax, including comments

This library is portable and doesn't provide IO functions. To read
s-expressions from files or other external sources, you should use
parsexp_io.
ppx_derivers.1.2.1 (1.2.1) Shared [@@deriving] plugin registry
authors
Jérémie Dimino
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Ppx_derivers is a tiny package whose sole purpose is to allow
ppx_deriving and ppx_type_conv to inter-operate gracefully when linked
as part of the same ocaml-migrate-parsetree driver.
ppx_deriving.5.2.1 (5.2.1) Type-driven code generation for OCaml
authors
whitequark <whitequark@whitequark.org>
license
MIT
links
(homepage) (bug reports) (opam package)
description
ppx_deriving provides common infrastructure for generating
code based on type definitions, and a set of useful plugins
for common tasks.
ppx_deriving_yojson.3.6.1 (3.6.1) JSON codec generator for OCaml
authors
whitequark <whitequark@whitequark.org>
license
MIT
links
(homepage) (bug reports) (opam package)
description
ppx_deriving_yojson is a ppx_deriving plugin that provides
a JSON codec generator.
ppx_import.1.9.1 (1.9.1) A syntax extension for importing declarations from interface files
authors
whitequark <whitequark@whitequark.org>
license
MIT
links
(homepage) (bug reports) (opam package)
description
ppx_sexp_conv.v0.14.3 (v0.14.3) [@@deriving] plugin to generate S-expression conversion functions
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
Part of the Jane Street's PPX rewriters collection.
re.1.10.4 (1.10.4) RE is a regular expression library for OCaml
authors
Jerome Vouillon - Thomas Gazagnaire - Anil Madhavapeddy - Rudi Grinberg - Gabriel Radanne
license
LGPL-2.0-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
Pure OCaml regular expressions with:
* Perl-style regular expressions (module Re.Perl)
* Posix extended regular expressions (module Re.Posix)
* Emacs-style regular expressions (module Re.Emacs)
* Shell-style file globbing (module Re.Glob)
* Compatibility layer for OCaml's built-in Str module (module Re.Str)
result.1.5 (1.5) Compatibility Result module
authors
Jane Street Group, LLC
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Projects that want to use the new result type defined in OCaml >= 4.03
while staying compatible with older version of OCaml should use the
Result module defined in this library.
seq.base (base) Compatibility package for OCaml's standard iterator type starting from 4.07.
authors
license
unknown - please clarify with homepage
links
(homepage) (bug reports) (opam package)
description
sexplib.v0.14.0 (v0.14.0) Library for serializing OCaml values to and from S-expressions
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
Part of Jane Street's Core library
The Core suite of libraries is an industrial strength alternative to
OCaml's standard library that was developed by Jane Street, the
largest industrial user of OCaml.
stdlib-shims.0.3.0 (0.3.0) Backport some of the new stdlib features to older compiler
authors
The stdlib-shims programmers
license
LGPL-2.1-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
Backport some of the new stdlib features to older compiler,
such as the Stdlib module.

This allows projects that require compatibility with older compiler to
use these new features in their code.
yojson.2.0.2 (2.0.2) Yojson is an optimized parsing and printing library for the JSON format
authors
Martin Jambon
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Yojson is an optimized parsing and printing library for the JSON format.

ydump is a pretty-printing command-line program provided with the
yojson package.
z3.4.11.0 (4.11.0) Z3 solver
authors
MSR
license
MIT
links
(homepage) (bug reports) (opam package)
description
zarith.1.12 (1.12) Implements arithmetic and logical operations over arbitrary-precision integers
authors
Antoine Miné Xavier Leroy Pascal Cuoq
license
unknown - please clarify with homepage
links
(homepage) (bug reports) (opam package)
description
The Zarith library implements arithmetic and logical operations over
arbitrary-precision integers. It uses GMP to efficiently implement
arithmetic over big integers. Small integers are represented as Caml
unboxed integers, for speed and space economy.