Skip to content

Latest commit

 

History

History
1667 lines (1525 loc) · 102 KB

README~dev.md

File metadata and controls

1667 lines (1525 loc) · 102 KB

Coq Platform 2023.11.0 providing Coq dev (latest master of all packages)

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.11.0 with Coq dev. The README files for other versions are linked in the main README.

This is the latest development version of Coq and all packages.

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.11.0 with Coq dev "base level"

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

coq.dev (dev) 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 writenmathematical definitions, executable algorithms, and theorems, togethernwith an environment for semi-interactive development of machine-checkednproofs. Typical applications include the certification of properties of programmingnlanguages (e.g., the CompCert compiler certification project and thenBedrock verified low-level programming library), the formalization ofnmathematics (e.g., the full formalization of the Feit-Thompson theoremnand homotopy type theory) and teaching.

Coq Platform 2023.11.0 with Coq dev "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.dev (dev) 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 developmentnof mathematical definitions, executable algorithms, and proofs of theoremsnusing the Coq proof assistant.

Coq Platform 2023.11.0 with Coq dev "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.dev (dev) This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) 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 universally quantifiednequations, modulo associativity and commutativity of some operator.nThe tactics can be applied for custom operators by registering thenoperators and their properties as type class instances. Many commonnoperator instances, such as for Z binary arithmetic and booleans, arenprovided with the plugin.
coq-bignums.dev (dev) 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.dev (dev) 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 contextnof the ForMath EU FP7 project (2009-2013). It has two parts:n- theory, which contains developments in algebra including normal forms of matrices,n and optimized algorithms on MathComp data structures.n- refinements, which is a framework to ease change of data representations during a proof.
coq-coqprime-generator.dev (dev) 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.dev (dev) Certifying prime numbers in Coq
authors
Laurent Théry
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
coq-coquelicot.dev (dev) A Coq formalization of real analysis compatible with the standard library.
authors
Sylvie Boldo <[email protected]> - Catherine Lelay <[email protected]> - Guillaume Melquiond <[email protected]>
license
LGPL 3 - see homepage for details
links
(homepage) (bug reports) (opam package)
description
coq-corn.dev (dev) Constructive Coq Repository at Nijmegen.
authors
Iris Loeb - Rik van Ginneken - Randy Pollack - Mariusz Giero - Dan Synek - Lionel Mamane - Luís Cruz-Filipe - Milad Niqui - Pierre Letouzey - Herman Geuvers - Freek Wiedijk - Henk Barendregt - Dimitri Hendriks - Bart Kirkels - Russell O'Connor - Bas Spitters - Sébastien Hinderer - Nickolay V. Shmyrev - Jan Zwanenburg
license
GPL 2 - see homepage for details
links
(homepage) (opam package)
description
The Constructive Coq Repository at Nijmegen, C-CoRN, aims at buildingna computer based library of constructive mathematics, formalized innthe theorem prover Coq. It includes the following parts:nn* Algebraic Hierarchynno An axiomatic formalization of the most common algebraicnstructures, including setoids, monoids, groups, rings,nfields, ordered fields, rings of polynomials, real andncomplex numbersnn* Model of the Real Numbersnno Construction of a concrete real number structurensatisfying the previously defined axiomsnn* Fundamental Theorem of Algebranno A proof that every non-constant polynomial on the complexnplane has at least one rootnn* Real Calculusnno A collection of elementary results on real analysis,nincluding continuity, differentiability, integration,nTaylor's theorem and the Fundamental Theorem of Calculus
coq-dpdgraph.dev (dev) 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,nand produces files with dependency information. Includes toolsnto visualize dependency graphs and find unused definitions.
coq-elpi.dev (dev) Elpi extension language for Coq
authors
Enrico Tassi
license
LGPL-2.1-or-later
links
(homepage) (opam package)
description
Coq-elpi provides a Coq plugin that embeds ELPI.nIt also provides a way to embed Coq's terms into λProlog usingnthe Higher-Order Abstract Syntax approachnand a way to read terms back. In addition to that it exports to ELPI anset of Coq's primitives, e.g. printing a message, accessing thenenvironment of theorems and data types, defining a new constant and so on.nFor convenience it also provides a quotation and anti-quotation for Coq'snsyntax in λProlog. E.g. `{{nat}}` is expanded to the type name of naturalnnumbers, or `{{A -> B}}` to the representation of a product by unfoldingn the `->` notation. Finally it provides a way to define new vernacular commandsnandnnew tactics.
coq-equations.dev (dev) A function definition package for Coq
authors
Matthieu Sozeau <[email protected]> - Cyprien Mangin <[email protected]>
license
LGPL-2.1-or-later
links
(homepage) (bug reports) (opam package)
description
Equations is a function definition plugin for Coq, that allows thendefinition of functions by dependent pattern-matching and well-founded,nmutual or nested structural recursion and compiles them into corenterms. It automatically derives the clauses equations, the graph of thenfunction and its associated elimination principle.
coq-ext-lib.dev (dev) a library of Coq definitions, theorems, and tactics
authors
Gregory Malecha
license
BSD-2-Clause-FreeBSD
links
(homepage) (bug reports) (opam package)
description
coq-flocq.3.dev (3.dev) A floating-point formalization for the Coq system.
authors
Sylvie Boldo <[email protected]> - Guillaume Melquiond <[email protected]>
license
LGPL 3 - see homepage for details
links
(homepage) (opam package)
description
coq-gappa.dev (dev) A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
authors
Guillaume Melquiond <[email protected]>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-hammer-tactics.dev (dev) Reconstruction tactics for the hammer for Coq
authors
Lukasz Czajka <[email protected]>
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
Collection of tactics that are used by the hammer for Coqnto reconstruct proofs found by automated theorem provers. When the hammernhas been successfully applied to a project, only this package needsnto be installed; the hammer plugin is not required.
coq-hammer.dev (dev) General-purpose automated reasoning hammer tool for Coq
authors
Lukasz Czajka <[email protected]> - Cezary Kaliszyk <[email protected]>
license
LGPL-2.1-only
links
(homepage) (bug reports) (opam package)
description
A general-purpose automated reasoning hammer tool for Coq that combinesnlearning from previous proofs with the translation of problems to thenlogics of automated systems and the reconstruction of successfully found proofs.
coq-hierarchy-builder.dev (dev) 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 thesenhierarchies evolve without breaking user code. The key concepts are the ones of factory, buildernand abbreviation that let the hierarchy developer describe an actual interface for their library.nBehind that interface the developer can provide appropriate code to ensure retro compatibility.
coq-hott.dev (dev) 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:n -noinit -indices-matternnTo use the HoTT library in a project, add the following to _CoqProject:n -arg -noinitn -arg -indices-mattern`
coq-interval.dev (dev) A Coq tactic for proving bounds on real-valued expressions automatically
authors
Guillaume Melquiond <[email protected]> - Érik Martin-Dorel <[email protected]> - Pierre Roux <[email protected]> - Thomas Sibut-Pinote <[email protected]>
license
CECILL-C
links
(homepage) (bug reports) (opam package)
description
coq-iris-heap-lang.dev (dev) 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, andnuses Iris to build a program logic for HeapLang programs.
coq-iris.dev (dev) 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 usingnconcurrent separation logic. It can be used to develop a program logic, forndefining logical relations, and for reasoning about type systems, among othernapplications. This package includes the base logic, Iris Proof Mode (IPM) /nMoSeL, and a general language-independent program logic; see coq-iris-heap-langnfor an instantiation of the program logic to a particular programming language.
coq-libhyps.dev (dev) Hypotheses manipulation library
authors
Pierre Courtieu
license
MIT
links
(homepage) (bug reports) (opam package)
description
This library defines a set of tactics to manipulate hypothesisnindividually or by group. In particular it allows applying a tactic onneach hypothesis of a goal, or only on *new* hypothesis after somentactic. Examples of manipulations: automatic renaming, subst, revert,nor any tactic expecting a hypothesis name as argument.nnIt also provides the especialize tactic to ease forward reasoning byninstantianting one, several or all premisses of a hypothesis.
coq-math-classes.dev (dev) A library of abstract interfaces for mathematical structures in Coq.
authors
Eelis van der Weegen Bas Spitters Robbert Krebbers
license
Public Domain - see homepage for details
links
(homepage) (bug reports) (opam package)
description
We have been working on a new set of foundational interfaces for formalized constructive mathematics in Coq, heavily based on Coq's new type classes, used in a systematic way in order to achieve:n* elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory);n* a very flexible purely predicate-based representation of algebraic structures that makes sharing, multiple inheritance, and derived inheritance, all trivial;n* clean expression terms that neither refer to proofs nor require deeply nested record projections;n* fluent rewriting;n* easy and flexible replacement and specialization of data representations and operations with more efficient versions;n* ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.
coq-mathcomp-algebra.dev (dev) 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 discreten(i.e. with decidable equality) algebraic structures : ring, fields,nordered fields, real fields, modules, algebras, integers, rationalnnumbers, polynomials, matrices, vector spaces...
coq-mathcomp-analysis.dev (dev) 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 fornthe Coq proof-assistant and using the Mathematical Components library.
coq-mathcomp-bigenough.dev (dev) A small library to do epsilon - N reasonning
authors
Cyril Cohen <[email protected]>
license
CECILL-B
links
(homepage) (bug reports) (opam package)
description
The package contains a package to reasoning with big enough objectsn(mostly natural numbers). This package is essentially for backwardncompatibility purposes as `bigenough` will be subsumed by the nearntactics. The formalization is based on the Mathematical Componentsnlibrary.
coq-mathcomp-character.dev (dev) 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 groupnrepresentations, characters and class functions.
coq-mathcomp-field.dev (dev) 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,ngalois theory, algebraic numbers, cyclotomic polynomials...
coq-mathcomp-fingroup.dev (dev) 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,ngroup quotients, group morphisms, group presentation, group action...
coq-mathcomp-finmap.dev (dev) 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 tonsupport finite sets and finite maps on choicetypes (rather that finitentypes). This includes support for functions with finite support andnmultisets. The library also contains a generic order and set libary,nwhich will be used to subsume notations for finite sets, eventually.
coq-mathcomp-multinomials.dev (dev) 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.dev (dev) 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 closednfields, with a construction of the real closure and the algebraicnclosure (including a proof of the fundamental theorem ofnalgebra). It also contains a proof of decidability of the firstnorder theory of real closed field, through quantifier elimination.
coq-mathcomp-solvable.dev (dev) 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.dev (dev) 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 languagenextension and the minimal set of libraries to take advantage of it.nThis includes libraries on lists (seq), boolean and booleannpredicates, natural numbers and types with decidable equality,nfinite types, finite sets, finite functions, finite graphs, basic arithmeticsnand prime numbers, big operators
coq-mathcomp-zify.dev (dev) 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 tactics for goals statednwith the definitions of the Mathematical Components library by extending thenzify tactic.
coq-menhirlib.dev (dev) A support library for verified Coq parsers produced by Menhir
authors
Jacques-Henri Jourdan <[email protected]>
license
LGPL-3.0-or-later
links
(homepage) (bug reports) (opam package)
description
coq-mtac2.dev (dev) Mtac2: Typed Tactics for Coq
authors
Beta Ziliani <[email protected]> - Jan-Oliver Kaiser <[email protected]> - Robbert Krebbers <[email protected]> - Yann Régis-Gianas <[email protected]> - Derek Dreyer <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-paramcoq.dev (dev) Paramcoq
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
The plugin is still in an experimental state. It is not very usernfriendly (lack of good error messages) and still contains bugs. But isnuseable enough to translate a large chunk of standard library.
coq-quickchick.dev (dev) QuickChick is a random property-based testing library for Coq.
authors
Leonidas Lampropoulos - Zoe Paraskevopoulou - Maxime Denes - Catalin Hritcu - Benjamin Pierce - Arthur Azevedo de Amorim - Antal Spector-Zabusky - Li-Yao Xia - Yishuai Li
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-reglang.dev (dev) 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 betweenndifferent representations of regular languages: various forms ofnautomata (deterministic, nondeterministic, one-way, two-way),nregular expressions, and the logic WS1S. It also contains variousndecidability results and closure properties of regular languages.
coq-simple-io.dev (dev) IO monad for Coq
authors
Li-yao Xia
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-stdpp.dev (dev) 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:nn- It provides a great number of definitions and lemmas for common datan structures such as lists, finite maps, finite sets, and finite multisets.n- It uses type classes for common notations (like `∅`, `∪`, and Haskell-stylen monad notations) so that these can be overloaded for different data structures.n- It uses type classes to keep track of common properties of types, like itn having decidable equality or being countable or finite.n- Most data structures are represented in canonical ways so that Leibnizn equality can be used as much as possible (for example, for maps we haven `m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library providesn setoid instances for most types and operations.n- It provides various tactics for common tasks, like an ssreflect inspiredn `done` tactic for finishing trivial goals, a simple breadth-first solvern `naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`n for proving compatibility of functions with respect to relations, and a solvern `set_solver` for goals involving set operations.n- It is entirely dependency- and axiom-free.
coq-unicoq.dev (dev) An enhanced unification algorithm for Coq
authors
Matthieu Sozeau <[email protected]> - Beta Ziliani <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
coq-unimath.dev (dev) Library of Univalent Mathematics
authors
The UniMath Development Team
license
Kind of MIT - see homepage for details
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) (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.
menhir.dev (dev) An LR(1) parser generator
authors
François Pottier <[email protected]> - Yann Régis-Gianas <[email protected]>
license
unknown - please clarify with homepage
links
(homepage) (bug reports) (opam package)
description
ppxlib.0.15.0 (0.15.0) Standard library for ppx rewriters
authors
Jane Street Group, LLC
license
MIT
links
(homepage) (bug reports) (opam package)
description
Ppxlib is the standard library for ppx rewriters and other programsnthat manipulate the in-memory reprensation of OCaml programs, a.k.anthe Parsetree.nnIt also comes bundled with two ppx rewriters that are commonly used tonwrite tools that manipulate and/or generate Parsetree values;n`ppxlib.metaquot` which allows to construct Parsetree values using thenOCaml syntax directly and `ppxlib.traverse` which provides variousnways of automatically traversing values of a given type, in particularnallowing to inject a complex structured value into generated code.
z3_tptp.4.8.13 (4.8.13) TPTP front end for Z3 solver
authors
MSR
license
MIT
links
(homepage) (bug reports) (opam package)
description

Coq Platform 2023.11.0 with Coq dev "optional packages"

The optional packages have the same maturity and maintenance level as the packages in the full level, but either 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.dev (dev) The CompCert C compiler (64 bit)
authors
Xavier Leroy <[email protected]>
license
INRIA Non-Commercial License Agreement - see homepage for details
links
(homepage) (bug reports) (opam package)
description
coq-vst.dev (dev) Verified Software Toolchain
authors
Andrew W. Appel - Lennart Beringer - Sandrine Blazy - Qinxiang Cao - Santiago Cuellar - Robert Dockins - Josiah Dodds - Nick Giannarakis - Samuel Gruetter - Aquinas Hobor - Jean-Marie Madiot - William Mansky
license
link
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.11.0 with Coq dev "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-deriving.dev (dev) 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 forninductive data types. It includes native support for eqType,nchoiceType, countType and finType instances, and it allows users tondefine their own instances for other classes.

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
cairo2.0.6.2 (0.6.2) Binding to Cairo, a 2D Vector Graphics Library
authors
Christophe Troestler <[email protected]> - Pierre Hauweele <[email protected]>
license
LGPL-3.0-only
links
(homepage) (bug reports) (opam package)
description
This is a binding to Cairo, a 2D graphics library with support fornmultiple output devices. Currently supported output targets includenthe X Window System, Quartz, Win32, image buffers, PostScript, PDF,nand SVG file output.
camlp5.7.14 (7.14) Preprocessor-pretty-printer of OCaml
authors
Daniel de Rauglaudre
license
BSD-3-Clause
links
(homepage) (bug reports) (opam package)
description
Camlp5 is a preprocessor and pretty-printer for OCaml programs. It also provides parsing and printing tools.nnAs a preprocessor, it allows to:nnextend the syntax of OCaml,nredefine the whole syntax of the language.nAs a pretty printer, it allows to:nndisplay OCaml programs in an elegant way,nconvert from one syntax to another,ncheck the results of syntax extensions.nCamlp5 also provides some parsing and pretty printing tools:nnextensible grammarsnextensible printersnstream parsers and lexersnpretty print modulenIt works as a shell command and can also be used in the OCaml toplevel.
adwaita-icon-theme.1 (1) 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 commandnis 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.
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.
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 commandnis 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.
perl.2 (2) Virtual package relying on perl
authors
Larry Wall
license
GPL-1.0-or-later
links
(homepage) (bug reports) (opam package)
description
This package can only install if the perl program 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 installednon 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 availablenon the system.nIf a minor version needs to be specified for your operating system, thennpython-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.
cppo.1.6.8 (1.6.8) 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.nIt allows the definition of simple macros and file inclusion.nnCppo is:nn* more OCaml-friendly than cppn* easy to learn without consulting a manualn* reasonably fastn* 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 <[email protected]> - Jane Street Group, LLC - Jeremie Dimino <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
This library provides minimal support for Canonical S-expressionsn[1]. Canonical S-expressions are a binary encoding of S-expressionsnthat is super simple and well suited for communication betweennprograms.nnThis library only provides a few helpers for simple applications. Ifnyou need more advanced support, such as parsing from more fancy inputnsources, you should consider copying the code of this library givennhow simple parsing S-expressions in canonical form is.nnTo avoid a dependency on a particular S-expression library, the onlynmodule of this library is parameterised by the type of S-expressions.nn[1] https://en.wikipedia.org/wiki/Canonical_S-expressions
dune-configurator.2.9.1 (2.9.1) Helper library for gathering system configuration
authors
Jane Street Group, LLC <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
dune-configurator is a small library that helps writing OCaml scripts thatntest features available on the system, in order to generate config.hnfiles for instance.nAmong other things, dune-configurator allows one to:n- test if a C program compilesn- query pkg-confign- import #define from OCaml header filesn- generate config.h file
dune.2.9.1 (2.9.1) Fast, portable, and opinionated build system
authors
Jane Street Group, LLC <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
dune is a build system that was designed to simplify the release ofnJane Street packages. It reads metadata from dune files following anvery simple s-expression syntax.nndune is fast, has very low-overhead, and supports parallel builds onnall platforms. It has no system dependencies; all you need to buildndune or packages using dune is OCaml. You don't need make or bashnas long as the packages themselves don't use bash explicitly.nndune supports multi-package development by simply dropping multiplenrepositories into the same directory.nnIt also supports multi-context builds, such as building againstnseveral opam roots/switches simultaneously. This helps maintainingnpackages across several versions of OCaml and gives cross-compilationnfor free.
elpi.1.13.8 (1.13.8) 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,na programming language well suited to manipulate syntax trees with binders.nnELPI is designed to be embedded into larger applications written in OCaml asnan extension language. It comes with an API to drive the interpreter and nwith an FFI for defining built-in predicates and data types, as well asnquotations and similar goodies that are handy to adapt the language to the hostnapplication.nnThis package provides both a command line interpreter (elpi) and a library tonbe linked in other applications (eg by passing -package elpi to ocamlfind).nnThe ELPI programming language has the following features:nn- Native support for variable binding and substitution, via an Higher Ordern Abstract Syntax (HOAS) embedding of the object language. The programmer needsn not to care about De Bruijn indexes.nn- Native support for hypothetical context. When moving under a binder one cann attach to the bound variable extra information that is collected when then variable gets out of scope. For example when writing a type-checker then programmer needs not to care about managing the typing context.nn- Native support for higher order unification variables, again via HOAS.n Unification variables of the meta-language (λProlog) can be reused ton represent the unification variables of the object language. The programmern does not need to care about the unification-variable assignment map andn cannot assign to a unification variable a term containing variables out ofn scope, or build a circular assignment.nn- Native support for syntactic constraints and their meta-level handling rules.n The generative semantics of Prolog can be disabled by turning a goal into an syntactic constraint (suspended goal). A syntactic constraint is resumed asn soon as relevant variables gets assigned. Syntactic constraints can ben manipulated by constraint handling rules (CHR).nn- Native support for backtracking. To ease implementation of search.nn- The constraint store is extensible. The host application can declaren non-syntactic constraints and use custom constraint solvers to check theirn consistency.nn- Clauses are graftable. The user is free to extend an existing program byn inserting/removing clauses, both at runtime (using implication) and atn compilation time by accumulating files.nnELPI is free software released under the terms of LGPL 2.1 or above.
gappa.dev (dev) 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
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.1 (3.1.1) OCaml interface to GTK+ gtksourceview library
authors
Jacques Garrigue et al., Nagoya University
license
LGPL with linking exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
OCaml interface to GTK+3, gtksourceview3 library.nnSee https://garrigue.github.io/lablgtk/ for more information.
menhirLib.dev (dev) Runtime support library for parsers generated by Menhir
authors
François Pottier <[email protected]> - Yann Régis-Gianas <[email protected]>
license
unknown - please clarify with homepage
links
(homepage) (bug reports) (opam package)
description
menhirSdk.dev (dev) Compile-time library for auxiliary tools related to Menhir
authors
François Pottier <[email protected]> - Yann Régis-Gianas <[email protected]>
license
unknown - please clarify with homepage
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-base-compiler.4.10.2 (4.10.2) Official release 4.10.2
authors
Xavier Leroy and many contributors
license
LGPL-2.1-or-later 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 undernthe toplevel names Ocaml_common, Ocaml_bytecomp, Ocaml_optcomp, ...
ocaml-config.1 (1) OCaml Switch Configuration
authors
Louis Gesbert <[email protected]> - David Allsopp <[email protected]>
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-migrate-parsetree.1.8.0 (1.8.0) Convert OCaml parsetrees between different versions
authors
Frédéric Bour <[email protected]> - Jérémie Dimino <[email protected]>
license
LGPL-2.1-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
Convert OCaml parsetrees between different versionsnnThis library converts parsetrees, outcometree and ast mappers betweenndifferent OCaml versions. High-level functions help making PPXnrewriters independent of a compiler version.
ocaml.4.10.2 (4.10.2) 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,nand polls it to initialise specific variables like `ocaml:native-dynlink`
ocamlbuild.0.14.0 (0.14.0) OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
authors
Nicolas Pouillard Berke Durak
license
LGPL-2.1-only WITH OCaml-LGPL-linking-exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
ocamlfind.1.9.2 (1.9.2) A library manager for OCaml
authors
Gerd Stolpmann <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
Findlib is a library manager for OCaml. It provides a convention hownto store libraries, and a file format (META) to describe thenproperties of libraries. There is also a tool (ocamlfind) forninterpreting the META files, so that it is very easy to use librariesnin 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
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 allownppx_deriving and ppx_type_conv to inter-operate gracefully when linkednas part of the same ocaml-migrate-parsetree driver.
ppx_deriving.5.1 (5.1) Type-driven code generation for OCaml
authors
whitequark <[email protected]>
license
MIT
links
(homepage) (bug reports) (opam package)
description
ppx_deriving provides common infrastructure for generatingncode based on type definitions, and a set of useful pluginsnfor common tasks.
re.1.10.3 (1.10.3) RE is a regular expression library for OCaml
authors
Jerome Vouillon - Thomas Gazagnaire - Anil Madhavapeddy - Rudi Grinberg - Gabriel Radanne
license
LGPL-2.0 with OCaml linking exception - see homepage for details
links
(homepage) (bug reports) (opam package)
description
Pure OCaml regular expressions with:n* Perl-style regular expressions (module Re.Perl)n* Posix extended regular expressions (module Re.Posix)n* Emacs-style regular expressions (module Re.Emacs)n* Shell-style file globbing (module Re.Glob)n* 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.03nwhile staying compatible with older version of OCaml should use thenResult 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
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 librarynThe Core suite of libraries is an industrial strength alternative tonOCaml's standard library that was developed by Jane Street, thenlargest 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
typeof OCaml system - see homepage for details
links
(homepage) (bug reports) (opam package)
description
Backport some of the new stdlib features to older compiler,nsuch as the Stdlib module.nnThis allows projects that require compatibility with older compiler tonuse these new features in their code.
z3.4.8.13 (4.8.13) 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 overnarbitrary-precision integers. It uses GMP to efficiently implementnarithmetic over big integers. Small integers are represented as Camlnunboxed integers, for speed and space economy.