Coq Platform 2023.11.0 providing Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 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 2023.11.0 with Coq 8.13.2. The README files for other versions are linked in the main README.

This version of Coq Platform 2023.11.0 includes Coq 8.13.2 from 04/2021. There are three package picks for Coq 8.13.2: the original from 02/2021, a substantially extended one from 09/2021 and an updated one from 11/2021. This is the original package pick for Coq 8.13 from 02/2021. The 02/2021 and 09/2021 package picks are provided for compatibility and it is recommended to use the 11/2021 pick - or Coq 8.14.0.

The OCaml version used is 4.10.2.

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 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 write
mathematical definitions, executable algorithms, and theorems, together
with an environment for semi-interactive development of machine-checked
proofs. Typical applications include the certification of properties of programming
languages (e.g., the CompCert compiler certification project and the
Bedrock verified low-level programming library), the formalization of
mathematics (e.g., the full formalization of the Feit-Thompson theorem
and homotopy type theory) and teaching.

Coq Platform 2023.11.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 development
of mathematical definitions, executable algorithms, and proofs of theorems
using the Coq proof assistant.

Coq Platform 2023.11.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 details.

The full level contains the following packages:

coq-aac-tactics.8.13.0 (8.13.0) 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 quantified
equations, modulo associativity and commutativity of some operator.
The tactics can be applied for custom operators by registering the
operators and their properties as type class instances. Many common
operator instances, such as for Z binary arithmetic and booleans, are
provided 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

coq-coquelicot.3.1.0 (3.1.0) A Coq formalization of real analysis compatible with the standard library

authors: Sylvie Boldo gt; - Catherine Lelay gt; - Guillaume Melquiond gt;
license: LGPL-3.0-or-later
links: (homepage) (bug reports) (opam package)
description

coq-elpi.1.8.1 (1.8.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.
It also provides a way to embed Coq'apos;s terms into λProlog using
the Higher-Order Abstract Syntax approach
and a way to read terms back. In addition to that it exports to ELPI a
set of Coq'apos;s primitives, e.g. printing a message, accessing the
environment of theorems and data types, defining a new constant and so on.
For convenience it also provides a quotation and anti-quotation for Coq'apos;s
syntax in λProlog. E.g. `{{nat}}` is expanded to the type name of natural
numbers, or `{{A ->gt; B}}` to the representation of a product by unfolding
the `->gt;` notation. Finally it provides a way to define new vernacular commands
and
new tactics.

coq-equations.1.2.3+8.13 (1.2.3+8.13) A function definition package for Coq

authors: Matthieu Sozeau gt; - Cyprien Mangin gt;
license: LGPL-2.1-only
links: (homepage) (bug reports) (opam package)
description: Equations is a function definition plugin for Coq, that allows the
definition of functions by dependent pattern-matching and well-founded,
mutual or nested structural recursion and compiles them into core
terms. It automatically derives the clauses equations, the graph of the
function and its associated elimination principle.

coq-ext-lib.0.11.3 (0.11.3) 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.3.1 (3.3.1) A formalization of floating-point arithmetic for the Coq system

authors: Sylvie Boldo gt; - Guillaume Melquiond gt;
license: LGPL-3.0-or-later
links: (homepage) (bug reports) (opam package)
description

coq-gappa.1.4.6 (1.4.6) A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover

authors: Guillaume Melquiond gt;
license: LGPL-3.0-or-later
links: (homepage) (bug reports) (opam package)
description

coq-hierarchy-builder.1.0.0 (1.0.0) High level commands to declare and evolve a hierarchy based on packed classes

authors: Cyril Cohen Kazuhiko Sakaguchi Enrico Tassi
license: MIT
links: (homepage) (bug reports) (opam package)
description: Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these
hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder
and abbreviation that let the hierarchy developer describe an actual interface for their library.
Behind that interface the developer can provide appropriate code to ensure retro compatibility.

coq-hott.8.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:
-noinit -indices-matter
To use the HoTT library in a project, add the following to _CoqProject:
-arg -noinit
-arg -indices-matter

coq-interval.4.1.1 (4.1.1) A Coq tactic for proving bounds on real-valued expressions automatically

authors: Guillaume Melquiond gt; - Érik Martin-Dorel gt; - Pierre Roux gt; - Thomas Sibut-Pinote gt;
license: CECILL-C
links: (homepage) (bug reports) (opam package)
description

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'apos;Connor - Laurent Théry - Assia Mahboubi
license: CECILL-B
links: (homepage) (bug reports) (opam package)
description: This library contains definitions and theorems about discrete
(i.e. with decidable equality) algebraic structures : ring, fields,
ordered fields, real fields, modules, algebras, integers, rational
numbers, polynomials, matrices, vector spaces...

coq-mathcomp-bigenough.1.0.0 (1.0.0) A small library to do epsilon - N reasonning

authors: Cyril Cohen gt;
license: CECILL-B
links: (homepage) (bug reports) (opam package)
description: The package contains a package to reasoning with big enough objects
(mostly natural numbers). This package is essentially for backward
compatibility purposes as `bigenough` will be subsumed by the near
tactics. The formalization is based on the Mathematical Components
library.

coq-mathcomp-character.1.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'apos;Connor - Laurent Théry - Assia Mahboubi
license: CECILL-B
links: (homepage) (bug reports) (opam package)
description: This library contains definitions and theorems about group
representations, characters and class functions.

coq-mathcomp-field.1.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'apos;Connor - Laurent Théry - Assia Mahboubi
license: CECILL-B
links: (homepage) (bug reports) (opam package)
description: This library contains definitions and theorems about field extensions,
galois theory, algebraic numbers, cyclotomic polynomials...

coq-mathcomp-fingroup.1.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'apos;Connor - Laurent Théry - Assia Mahboubi
license: CECILL-B
links: (homepage) (bug reports) (opam package)
description: This library contains definitions and theorems about finite groups,
group quotients, group morphisms, group presentation, group action...

coq-mathcomp-finmap.1.5.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 to
support finite sets and finite maps on choicetypes (rather that finite
types). This includes support for functions with finite support and
multisets. The library also contains a generic order and set libary,
which will be used to subsume notations for finite sets, eventually.

coq-mathcomp-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 closed
fields, with a construction of the real closure and the algebraic
closure (including a proof of the fundamental theorem of
algebra). It also contains a proof of decidability of the first
order theory of real closed field, through quantifier elimination.

coq-mathcomp-solvable.1.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'apos;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'apos;Connor - Laurent Théry - Assia Mahboubi
license: CECILL-B
links: (homepage) (bug reports) (opam package)
description: This library includes the small scale reflection proof language
extension and the minimal set of libraries to take advantage of it.
This includes libraries on lists (seq), boolean and boolean
predicates, natural numbers and types with decidable equality,
finite types, finite sets, finite functions, finite graphs, basic arithmetics
and prime numbers, big operators

coq-menhirlib.20200624 (20200624) A support library for verified Coq parsers produced by Menhir

authors: Jacques-Henri Jourdan gt;
license: LGPL-3.0-or-later
links: (homepage) (bug reports (email)) (opam package)
description

coq-mtac2.1.4+8.13 (1.4+8.13) Mtac2: Typed Tactics for Coq

authors: Beta Ziliani gt; - Jan-Oliver Kaiser gt; - Robbert Krebbers gt; - Yann Régis-Gianas gt; - Derek Dreyer gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description

coq-quickchick.1.5.0 (1.5.0) 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-simple-io.1.5.0 (1.5.0) IO monad for Coq

authors: Li-yao Xia
license: MIT
links: (homepage) (bug reports) (opam package)
description: This library provides tools to implement IO programs directly in Coq, in a
similar style to Haskell. Facilities for formal verification are not included.

IO is defined as a parameter with a purely functional interface in Coq,
to be extracted to OCaml. Some wrappers for the basic types and functions in
the OCaml Pervasives module are provided. Users are free to define their own
APIs on top of this IO type.

coq-unicoq.1.5+8.13 (1.5+8.13) An enhanced unification algorithm for Coq

authors: Matthieu Sozeau gt; - Beta Ziliani gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description

gappa.1.3.5 (1.3.5) 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.20200624 (20200624) An LR(1) parser generator

authors: François Pottier gt; - Yann Régis-Gianas gt;
license: unknown - please clarify with homepage
links: (homepage) (bug reports (email)) (opam package)
description

Coq Platform 2023.11.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 take a rather long time to build or have a non open source license or depend on packages with non open source license.

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

The macOS and snap installation bundles always include these packages.

The following packages are optional:

coq-compcert.3.8 (3.8) The CompCert C compiler (64 bit)

authors: Xavier Leroy gt;
license: INRIA Non-Commercial License Agreement - see homepage for details
links: (homepage) (bug reports) (opam package)
description

coq-vst.2.7.1 (2.7.1) 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 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:

Dependency packages

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

base-bigarray.base (base)

authors
license: unknown - please clarify with homepage
links: (opam package)
description: Bigarray library distributed with the OCaml compiler

base-threads.base (base)

authors
license: unknown - please clarify with homepage
links: (opam package)
description: Threads library distributed with the OCaml compiler

base-unix.base (base)

authors
license: unknown - please clarify with homepage
links: (opam package)
description: Unix library distributed with the OCaml compiler

base.v0.15.1 (v0.15.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 OCaml

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

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

https://github.com/janestreet/stdio

cairo2.0.6.4 (0.6.4) Binding to Cairo, a 2D Vector Graphics Library

authors: Christophe Troestler gt; - Pierre Hauweele gt;
license: LGPL-3.0
links: (homepage) (bug reports) (opam package)
description: This is a binding to Cairo, a 2D graphics library with support for
multiple output devices. Currently supported output targets include
the X Window System, Quartz, Win32, image buffers, PostScript, PDF,
and SVG file output.

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.

As a preprocessor, it allows to:

extend the syntax of OCaml,
redefine the whole syntax of the language.
As a pretty printer, it allows to:

display OCaml programs in an elegant way,
convert from one syntax to another,
check the results of syntax extensions.
Camlp5 also provides some parsing and pretty printing tools:

extensible grammars
extensible printers
stream parsers and lexers
pretty print module
It works as a shell command and can also be used in the OCaml toplevel.

adwaita-icon-theme.2 (2) Virtual package relying on adwaita-icon-theme

authors: GNOME devs
license: LGPL-3.0-only CC-BY-SA-3.0
links: (homepage) (bug reports) (opam package)
description: This package can only install if the adwaita-icon-theme package is installed on the system.

autoconf.0.1 (0.1) Virtual package relying on autoconf installation

authors: https://www.gnu.org/software/autoconf/autoconf.html#maintainer
license: GPL-3.0-only
links: (homepage) (bug reports) (opam package)
description: This package can only install if the autoconf command
is available on the system.

automake.1 (1) Virtual package relying on GNU automake

authors: Jim Meyering - David J. MacKenzie - https://git.savannah.gnu.org/cgit/automake.git/tree/THANKS
license: GPL-2.0-or-later
links: (homepage) (bug reports) (opam package)
description: This package can only install if GNU automake is installed on the system.

bison.2 (2) Virtual package relying on GNU bison

authors: Robert Corbett - Richard Stallman - Wilfred Hansen - Akim Demaille - Paul Hilfinger - Joel E. Denny - Paolo Bonzini - Alex Rozenman - Paul Eggert
license: GPL-3.0-or-later
links: (homepage) (bug reports) (opam package)
description: This package can only install if GNU bison is installed on the system.

boost.1 (1) Virtual package relying on boost

authors: Beman Dawes, David Abrahams, et al.
license: MIT
links: (homepage) (bug reports) (opam package)
description: This package can only install if the boost library is installed on the system.

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.4 (4) Virtual package relying on a GMP lib system installation

authors: nbraud
license: GPL-1.0-or-later
links: (homepage) (bug reports) (opam package)
description: This package can only install if the GMP lib is installed on the system.

gtk3.18 (18) Virtual package relying on GTK+ 3

authors: The GTK Toolkit
license: unknown - please clarify with homepage
links: (homepage) (bug reports) (opam package)
description: This package can only install if GTK+ 3 is installed on the system.

gtksourceview3.0+2 (0+2) Virtual package relying on a GtkSourceView-3 system installation

authors: The gtksourceview programmers
license: LGPL-2.1-or-later
links: (homepage) (bug reports) (opam package)
description: This package can only install if libgtksourceview-3.0-dev is installed on the system.

libjpeg.1 (1) Virtual package relying on a libjpeg system installation

authors: Bob Friesenhahn Lee Howard Frank Warmerdam
license: BSD-like - see homepage for details
links: (homepage) (bug reports) (opam package)
description: This package can only install if the libjpeg is installed on the system.

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.3 (3) Check if pkg-config is installed and create an opam switch local pkgconfig folder

authors: Francois Berenger
license: GPL-1.0-or-later
links: (homepage) (bug reports) (opam package)
description: This package can only install if the pkg-config package is installed
on the system.

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.9 (1.6.9) Code preprocessor like cpp for OCaml

authors: Martin Jambon
license: BSD-3-Clause
links: (homepage) (bug reports) (opam package)
description: Cppo is an equivalent of the C preprocessor for OCaml programs.
It allows the definition of simple macros and file inclusion.

Cppo is:

* more OCaml-friendly than cpp
* easy to learn without consulting a manual
* reasonably fast
* simple to install and to maintain

csexp.1.5.2 (1.5.2) Parsing and printing of S-expressions in Canonical form

authors: Quentin Hocquet gt; - Jane Street Group, LLC gt; - Jeremie Dimino gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description: This library provides minimal support for Canonical S-expressions
[1]. Canonical S-expressions are a binary encoding of S-expressions
that is super simple and well suited for communication between
programs.

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

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

[1] https://en.wikipedia.org/wiki/Canonical_S-expressions

dune-configurator.3.12.1 (3.12.1) Helper library for gathering system configuration

authors: Jane Street Group, LLC gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description: dune-configurator is a small library that helps writing OCaml scripts that
test features available on the system, in order to generate config.h
files for instance.
Among other things, dune-configurator allows one to:
- test if a C program compiles
- query pkg-config
- import #define from OCaml header files
- generate config.h file

dune.3.12.1 (3.12.1) Fast, portable, and opinionated build system

authors: Jane Street Group, LLC gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description: Dune is a build system that was designed to simplify the release of
Jane Street packages. It reads metadata from \dune\ files following a
very simple s-expression syntax.

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

Dune is composable; supporting multi-package development by simply
dropping multiple repositories into the same directory.

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

elpi.1.12.0 (1.12.0) ELPI - Embeddable λProlog Interpreter

authors: Claudio Sacerdoti Coen Enrico Tassi
license: LGPL-2.1-or-later
links: (homepage) (bug reports) (opam package)
description: ELPI implements a variant of λProlog enriched with Constraint Handling Rules,
a programming language well suited to manipulate syntax trees with binders.

ELPI is designed to be embedded into larger applications written in OCaml as
an extension language. It comes with an API to drive the interpreter and
with an FFI for defining built-in predicates and data types, as well as
quotations and similar goodies that are handy to adapt the language to the host
application.

This package provides both a command line interpreter (elpi) and a library to
be linked in other applications (eg by passing -package elpi to ocamlfind).

The ELPI programming language has the following features:

- Native support for variable binding and substitution, via an Higher Order
Abstract Syntax (HOAS) embedding of the object language. The programmer needs
not to care about De Bruijn indexes.

- Native support for hypothetical context. When moving under a binder one can
attach to the bound variable extra information that is collected when the
variable gets out of scope. For example when writing a type-checker the
programmer needs not to care about managing the typing context.

- Native support for higher order unification variables, again via HOAS.
Unification variables of the meta-language (λProlog) can be reused to
represent the unification variables of the object language. The programmer
does not need to care about the unification-variable assignment map and
cannot assign to a unification variable a term containing variables out of
scope, or build a circular assignment.

- Native support for syntactic constraints and their meta-level handling rules.
The generative semantics of Prolog can be disabled by turning a goal into a
syntactic constraint (suspended goal). A syntactic constraint is resumed as
soon as relevant variables gets assigned. Syntactic constraints can be
manipulated by constraint handling rules (CHR).

- Native support for backtracking. To ease implementation of search.

- The constraint store is extensible. The host application can declare
non-syntactic constraints and use custom constraint solvers to check their
consistency.

- Clauses are graftable. The user is free to extend an existing program by
inserting/removing clauses, both at runtime (using implication) and at
\compilation\ time by accumulating files.

ELPI is free software released under the terms of LGPL 2.1 or above.

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.

See https://garrigue.github.io/lablgtk/ for more information.

lablgtk3.3.1.1 (3.1.1) OCaml interface to GTK+3

authors: Jacques Garrigue et al., Nagoya University
license: LGPL-2.1-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links: (homepage) (bug reports) (opam package)
description: OCaml interface to GTK+3

See https://garrigue.github.io/lablgtk/ for more information.

menhirLib.20200624 (20200624) Runtime support library for parsers generated by Menhir

authors: François Pottier gt; - Yann Régis-Gianas gt;
license: unknown - please clarify with homepage
links: (homepage) (bug reports (email)) (opam package)
description

menhirSdk.20200624 (20200624) Compile-time library for auxiliary tools related to Menhir

authors: François Pottier gt; - Yann Régis-Gianas gt;
license: unknown - please clarify with homepage
links: (homepage) (bug reports (email)) (opam package)
description

num.1.5 (1.5) 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 under
the toplevel names Ocaml_common, Ocaml_bytecomp, Ocaml_optcomp, ...

ocaml-config.1 (1) OCaml Switch Configuration

authors: Louis Gesbert gt; - David Allsopp gt;
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 gt; - Jérémie Dimino gt;
license: LGPL-2.1-only WITH OCaml-LGPL-linking-exception - see homepage for details
links: (homepage) (bug reports) (opam package)
description: Deprecated. Please, use Ppxlib instead.
More info on https://ocaml.org/changelog/2023-10-23-omp-deprecation

Convert OCaml parsetrees between different versions

This library converts parsetrees, outcometree and ast mappers between
different OCaml versions. High-level functions help making PPX
rewriters 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,
and polls it to initialise specific variables like `ocaml:native-dynlink`

ocamlbuild.0.14.3 (0.14.3) OCamlbuild is a build system with builtin rules to easily build most OCaml projects

authors: Nicolas Pouillard Berke Durak
license: LGPL-2.0-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links: (homepage) (bug reports) (opam package)
description

ocamlfind.1.9.6 (1.9.6) A library manager for OCaml

authors: Gerd Stolpmann gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description: Findlib is a library manager for OCaml. It provides a convention how
to store libraries, and a file format (\META\) to describe the
properties of libraries. There is also a tool (ocamlfind) for
interpreting the META files, so that it is very easy to use libraries
in programs and scripts.

ppx_derivers.1.2.1 (1.2.1) Shared [@@deriving] plugin registry

authors: Jérémie Dimino
license: BSD-3-Clause
links: (homepage) (bug reports) (opam package)
description: Ppx_derivers is a tiny package whose sole purpose is to allow
ppx_deriving and ppx_type_conv to inter-operate gracefully when linked
as part of the same ocaml-migrate-parsetree driver.

ppx_deriving.5.1 (5.1) Type-driven code generation for OCaml

authors: whitequark gt;
license: MIT
links: (homepage) (bug reports) (opam package)
description: ppx_deriving provides common infrastructure for generating
code based on type definitions, and a set of useful plugins
for common tasks.

ppxlib.0.14.0 (0.14.0) Base library and tools for ppx rewriters

authors: Jane Street Group, LLC
license: MIT
links: (homepage) (bug reports) (opam package)
description: A comprehensive toolbox for ppx development. It features:
- a OCaml AST / parser / pretty-printer snapshot,to create a full
frontend independent of the version of OCaml;
- a library for library for ppx rewriters in general, and type-driven
code generators in particular;
- a feature-full driver for OCaml AST transformers;
- a quotation mechanism allowing to write values representing the
OCaml AST in the OCaml syntax;
- a generator of open recursion classes from type definitions.

re.1.11.0 (1.11.0) RE is a regular expression library for OCaml

authors: Jerome Vouillon - Thomas Gazagnaire - Anil Madhavapeddy - Rudi Grinberg - Gabriel Radanne
license: LGPL-2.1-or-later WITH OCaml-LGPL-linking-exception - see homepage for details
links: (homepage) (bug reports) (opam package)
description: Pure OCaml regular expressions with:
* Perl-style regular expressions (module Re.Perl)
* Posix extended regular expressions (module Re.Posix)
* Emacs-style regular expressions (module Re.Emacs)
* Shell-style file globbing (module Re.Glob)
* Compatibility layer for OCaml'apos;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 >gt;= 4.03
while staying compatible with older version of OCaml should use the
Result module defined in this library.

seq.base (base) Compatibility package for OCaml'apos;s standard iterator type starting from 4.07.

authors
license: unknown - please clarify with homepage
links: (homepage) (bug reports) (opam package)
description

sexplib0.v0.15.1 (v0.15.1) 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'apos;s Core library
The Core suite of libraries is an industrial strength alternative to
OCaml'apos;s standard library that was developed by Jane Street, the
largest industrial user of OCaml.

stdio.v0.15.0 (v0.15.0) Standard IO library for OCaml

authors: Jane Street Group, LLC
license: MIT
links: (homepage) (bug reports) (opam package)
description: Stdio implements simple input/output functionalities for OCaml.

It re-exports the input/output functions of the OCaml standard
libraries using a more consistent API.

zarith.1.13 (1.13) Implements arithmetic and logical operations over arbitrary-precision integers

authors: Antoine Miné Xavier Leroy Pascal Cuoq
license: LGPL-2.0-only WITH OCaml-LGPL-linking-exception - see homepage for details
links: (homepage) (bug reports) (opam package)
description: The Zarith library implements arithmetic and logical operations over
arbitrary-precision integers. It uses GMP to efficiently implement
arithmetic over big integers. Small integers are represented as Caml
unboxed integers, for speed and space economy.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

README~8.13~2021.02.md

README~8.13~2021.02.md

Coq Platform 2023.11.0 providing Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021

Coq Platform 2023.11.0 with Coq 8.13.2 "base level"

Coq Platform 2023.11.0 with Coq 8.13.2 "IDE level"

Coq Platform 2023.11.0 with Coq 8.13.2 "full level"

Coq Platform 2023.11.0 with Coq 8.13.2 "optional packages"

Coq Platform 2023.11.0 with Coq 8.13.2 "extended level"

Dependency packages

Files

README~8.13~2021.02.md

Latest commit

History

README~8.13~2021.02.md

File metadata and controls

Coq Platform 2023.11.0 providing Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021

Coq Platform 2023.11.0 with Coq 8.13.2 "base level"

Coq Platform 2023.11.0 with Coq 8.13.2 "IDE level"

Coq Platform 2023.11.0 with Coq 8.13.2 "full level"

Coq Platform 2023.11.0 with Coq 8.13.2 "optional packages"

Coq Platform 2023.11.0 with Coq 8.13.2 "extended level"

Dependency packages