Coq Platform 2021.09.0 providing Coq 8.13.2 (released Apr 2021) with updated/extended package pick Nov 2021

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

This version of Coq Platform 2021.09.0 includes Coq 8.13.2 from 04/2021. The original Coq Platform package pick for Coq 8.13.2 was from 02/2021. This is a substantially extended package pick with many new and updated packages. This is the latest release version of the Coq Platform and recommended for general application.

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 obtianed 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 2021.09.0 with Coq 8.13.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.13.2 (8.13.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 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 2021.09.0 with Coq 8.13.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.13.2 (8.13.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 developmentnof mathematical definitions, executable algorithms, and proofs of theoremsnusing the Coq proof assistant.

Coq Platform 2021.09.0 with Coq 8.13.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 deatils.

The full level contains the following packages:

coq-aac-tactics.8.13.1 (8.13.1) Coq plugin providing 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.8.13.0 (8.13.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 < 8.6

coq-coqeal.1.0.6 (1.0.6) CoqEAL - The Coq Effective Algebra Library

authors: Guillaume Cano - Cyril Cohen - Maxime Dénès - Anders Mörtberg - Damien Rouhling - 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 and optimized algorithms on mathcomp data structures.n- refinements, which is a framework to ease change of data representations during a proof.

coq-coqprime.1.0.6 (1.0.6) 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:nn- Algebraic Hierarchynn An axiomatic formalization of the most common algebraicn structures, including setoids, monoids, groups, rings,n fields, ordered fields, rings of polynomials, real andn complex numbersnn- Model of the Real Numbersnn Construction of a concrete real number structuren satisfying the previously defined axiomsnn- Fundamental Theorem of Algebrann A proof that every non-constant polynomial on the complexn plane has at least one rootnn- Real Calculusnn A collection of elementary results on real analysis,n including continuity, differentiability, integration,n Taylor's theorem and the Fundamental Theorem of Calculusnn- Exact Real Computationnn Fast verified computation inside Coq. This includes: real numbers, functions,n integrals, graphs of functions, differential equations.

coq-dpdgraph.1.0+8.13 (1.0+8.13) 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.1.11.1 (1.11.1) 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.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.1.2.3+8.13 (1.2.3+8.13) A function definition package for Coq

authors: Matthieu Sozeau <matthieu.sozeau@inria.fr> - Cyprien Mangin <cyprien.mangin@m4x.org>
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.0.11.4 (0.11.4) A library of Coq definitions, theorems, and tactics

authors: Gregory Malecha
license: BSD-2-Clause-FreeBSD
links: (homepage) (bug reports) (opam package)
description: A collection of theories and plugins that may be useful in other Coq developments.

coq-flocq.3.4.2 (3.4.2) 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.0 (1.5.0) 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.13 (1.3.2+8.13) 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 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-hierarchy-builder.1.2.0 (1.2.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 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.8.13 (8.13) 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-matternTo use the HoTT library in a project, add the following to _CoqProject:n -arg -noinitn -arg -indices-matter

coq-interval.4.3.0 (4.3.0) 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.3.4.0 (3.4.0) HeapLang is the canonical example language for Iris

authors: The Iris Team
license: BSD-3-Clause
links: (homepage) (bug reports) (opam package)
description: This package provides the iris.heap_lang Coq module.

coq-iris.3.4.0 (3.4.0) Iris is 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: This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.

coq-libhyps.2.0.3 (2.0.3) 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.8.13.0 (8.13.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 mathematicalnstructures, such as:nn* Algebraic hierarchy (groups, rings, fields, …)n* Relations, orders, …n* Categories, functors, universal algebra, …n* Numbers: N, Z, Q, …n* Operations, (shift, power, abs, …)nnIt is heavily based on Coq’s new type classes in order to provide:nstructure inference, multiple inheritance/sharing, convenientnalgebraic manipulation (e.g. rewriting) and idiomatic use ofnnotations.

coq-mathcomp-algebra.1.12.0 (1.12.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 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.0.3.10 (0.3.10) An analysis library for mathematical components

authors: Reynald Affeldt - Cyril Cohen - Marie Kerjean - Assia Mahboubi - Damien Rouhling - Pierre Roux - Kazuhiko Sakaguchi - 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.1.0.0 (1.0.0) A small library to do epsilon - N reasonning

authors: Cyril Cohen <cyril.cohen@inria.fr>
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.1.12.0 (1.12.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 groupnrepresentations, characters and class functions.

coq-mathcomp-field.1.12.0 (1.12.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,ngalois theory, algebraic numbers, cyclotomic polynomials...

coq-mathcomp-fingroup.1.12.0 (1.12.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,ngroup quotients, group morphisms, group presentation, group action...

coq-mathcomp-finmap.1.5.1 (1.5.1) 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.1.5.4 (1.5.4) 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.2 (1.1.2) 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.1.12.0 (1.12.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.12.0 (1.12.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 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.1.1.0+1.12+8.13 (1.1.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 Coqnfor goals stated with the definitions of the Mathematical Components librarynby extending the zify tactic.

coq-menhirlib.20210419 (20210419) 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.13 (1.4+8.13) 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-paramcoq.1.1.3+coq8.13 (1.1.3+coq8.13) 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.nTypical applications of such statements are in data refinement proofs.nNote that the plugin is still in an experimental state - it is not very usernfriendly (lack of good error messages) and still contains bugs. But itnis usable enough to translate a large chunk of the standard library.

coq-quickchick.1.5.1 (1.5.1) 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.2 (1.1.2) 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.1.6.0 (1.6.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 ansimilar style to Haskell. Facilities for formal verification are not included.nnIO is defined as a parameter with a purely functional interface in Coq,nto be extracted to OCaml. Some wrappers for the basic types and functions innthe OCaml Pervasives module are provided. Users are free to define their ownnAPIs on top of this IO type.

coq-stdpp.1.5.0 (1.5.0) std++ is 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.1.5+8.13 (1.5+8.13) 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

coq-unimath.20210807 (20210807) Library of Univalent Mathematics

authors: The UniMath Development Team
license: Kind of MIT - see homepage for details
links: (homepage) (bug reports) (opam package)
description

gappa.1.4.0 (1.4.0) 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.20210419 (20210419) 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

Coq Platform 2021.09.0 with Coq 8.13.2 "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.3.9 (3.9) 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-vst.2.8 (2.8) 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 2021.09.0 with Coq 8.13.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-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 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.

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 nonconvenient way to update a single field of a record. This library provides angeneric way to update a field by name, where the user only has to implement ansimple typeclass that lists out the record fields.

coq-reduction-effects.0.1.3 (0.1.3) 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-serapi.8.13.0+0.13.0 (8.13.0+0.13.0) 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 thenCoq proof assistant, with particular emphasis on applications in IDEs,ncode analysis tools, and machine learning. SerAPI provides automaticnserialization of Coq's internal OCaml datatypes from/to JSON ornS-expressions (sexps).

Dependecy 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.1 (v0.14.1) 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 OCamlnnBase is a complete and portable alternative to the OCaml standardnlibrary. It provides all standard functionalities one would expectnfrom a language standard library. It uses consistent conventionsnacross all of its module.nnBase aims to be usable in any context. As a result system dependentnfeatures such as I/O are not offered by Base. They are insteadnprovided by companion libraries such as stdio:nn https://github.com/janestreet/stdio

biniou.1.2.1 (1.2.1) Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve

authors: Martin Jambon
license: BSD-3-Clause
links: (homepage) (bug reports) (opam package)
description: Biniou (pronounced be new) is a binary data format designed for speed, safety,nease of use and backward compatibility as protocols evolve. Biniou is vastlynequivalent to JSON in terms of functionality but allows implementations severalntimes faster (4 times faster than yojson), with 25-35% space savings.nnBiniou data can be decoded into human-readable form without knowledge of typendefinitions except for field and variant names which are represented by 31-bitnhashes. A program named bdump is provided for routine visualization of binioundata files.nnThe program atdgen is used to derive OCaml-Biniou serializers and deserializersnfrom type definitions.nnBiniou format specification: mjambon.github.io/atdgen-doc/biniou-format.txt

cairo2.0.6.2 (0.6.2) 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-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.

cmdliner.1.0.4 (1.0.4) Declarative definition of command line interfaces for OCaml

authors: Daniel Bünzli <daniel.buenzl i@erratique.ch>
license: ISC
links: (homepage) (bug reports) (opam package)
description: Cmdliner allows the declarative definition of command line interfacesnfor OCaml.nnIt provides a simple and compositional mechanism to convert commandnline arguments to OCaml values and pass them to your functions. Thenmodule automatically handles syntax errors, help messages and UNIX mannpage generation. It supports programs with single or multiple commandsnand respects most of the [POSIX][1] and [GNU][2] conventions.nnCmdliner has no dependencies and is distributed under the ISC license.nn[1]: http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap12.htmln[2]: http://www.gnu.org/software/libc/manual/html_node/Argument-Syntax.html

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.

gmp.3 (3) 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.

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.1 (1) 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.

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 <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-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 <opensource@janestreet.com>
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 <opensource@janestreet.com>
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.

easy-format.1.3.2 (1.3.2) High-level and functional interface to the Format module of the OCaml standard library

authors: Martin Jambon
license: BSD-3-Clause
links: (homepage) (bug reports) (opam package)
description: This module offers a high-level and functional interface to the Format module ofnthe OCaml standard library. It is a pretty-printing facility, i.e. it takes asninput some code represented as a tree and formats this code into the mostnvisually satisfying result, breaking and indenting lines of code wherenappropriate.nnInput data must be first modelled and converted into a tree using 3 kinds ofnnodes:nn* atomsn* listsn* labelled nodesnnAtoms represent any text that is guaranteed to be printed as-is. Lists can modelnany sequence of items such as arrays of data or lists of definitions that arenlabelled with something like int main, let x = or x:.

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.20210419 (20210419) 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.20210419 (20210419) 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-base-compiler.4.10.0 (4.10.0) Official release 4.10.0

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 <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-migrate-parsetree.1.8.0 (1.8.0) Convert OCaml parsetrees between different versions

authors: Frédéric Bour <frederic.bour@lakaban.net> - Jérémie Dimino <jeremie@dimino.org>
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.0 (4.10.0) 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.1 (1.9.1) 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 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

parsexp.v0.14.1 (v0.14.1) 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 fromnstrings or other medium.nnThe library is focused on performances but still provide full genericnparsers that can be used with strings, bigstrings, lexing buffers,ncharacter streams or any other sources effortlessly.nnIt provides three different class of parsers:n- the normal parsers, producing [Sexp.t] or [Sexp.t list] valuesn- the parsers with positions, building compact position sequences son that one can recover original positions in order to report properlyn located errors at little costn- the Concrete Syntax Tree parsers, produce values of typen [Parsexp.Cst.t] which record the concrete layout of the s-expressionn syntax, including commentsnnThis library is portable and doesn't provide IO functions. To readns-expressions from files or other external sources, you should usenparsexp_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 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 <whitequark@whitequark.org>
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.

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 providesna JSON codec generator.

ppx_import.1.8.0 (1.8.0) 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.1 (v0.14.1) [@@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.

ppx_tools_versioned.5.4.0 (5.4.0) A variant of ppx_tools based on ocaml-migrate-parsetree

authors: Frédéric Bour <frederic.bour@lakaban.net> - Alain Frisch <alain.frisch@lexifi.com>
license: MIT
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.

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

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 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.

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.

yojson.1.7.0 (1.7.0) Yojson is an optimized parsing and printing library for the JSON format

authors: Martin Jambon
license: unknown - please clarify with homepage
links: (homepage) (bug reports) (opam package)
description: Yojson is an optimized parsing and printing library for the JSON format.nnIt addresses a few shortcomings of json-wheel including 2x speedup,npolymorphic variants and optional syntax for tuples and variants.nnydump is a pretty-printing command-line program provided with thenyojson package.nnThe program atdgen can be used to derive OCaml-JSON serializers andndeserializers from type definitions.

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.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

README_2021.09.0_8.13.md

README_2021.09.0_8.13.md

Coq Platform 2021.09.0 providing Coq 8.13.2 (released Apr 2021) with updated/extended package pick Nov 2021

Coq Platform 2021.09.0 with Coq 8.13.2 "base level"

Coq Platform 2021.09.0 with Coq 8.13.2 "IDE level"

Coq Platform 2021.09.0 with Coq 8.13.2 "full level"

Coq Platform 2021.09.0 with Coq 8.13.2 "optional packages"

Coq Platform 2021.09.0 with Coq 8.13.2 "extended level"

Dependecy packages

Files

README_2021.09.0_8.13.md

Latest commit

History

README_2021.09.0_8.13.md

File metadata and controls

Coq Platform 2021.09.0 providing Coq 8.13.2 (released Apr 2021) with updated/extended package pick Nov 2021

Coq Platform 2021.09.0 with Coq 8.13.2 "base level"

Coq Platform 2021.09.0 with Coq 8.13.2 "IDE level"

Coq Platform 2021.09.0 with Coq 8.13.2 "full level"

Coq Platform 2021.09.0 with Coq 8.13.2 "optional packages"

Coq Platform 2021.09.0 with Coq 8.13.2 "extended level"

Dependecy packages