Build Status Gitter

MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.

Quick jump

At the center of this project is the Template-Coq quoting library for Coq. The project currently has a single repository extending Template-Coq with additional features:

Template-Coq

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

In addition to this representation of terms, Template Coq includes:

Checker

A partial type-checker for the Calculus of Inductive Constructions, whose extraction to ML is runable as a plugin (using command MetaCoq Check foo). This checker uses fuel, so it must be passed a number of maximal reduction steps to perfom when calling conversion, and is NOT verified.

PCUIC

PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is a cleaned up version of the term language of Coq and its associated type system, equivalent to the one of Coq. This version of the calculus has (partial) proofs of standard metatheoretical results:

Safe Checker

Implementation of a fuel-free and verified reduction machine, conversion checker and type checker for PCUIC. This relies on a postulate of strong normalisation of the reduction relation of PCUIC on well-typed terms. The extracted safe checker is available in Coq through a new vernacular command:

MetaCoq SafeCheck <term>

After importing MetaCoq.SafeChecker.Loader.

To roughly compare the time used to check a definition with Coq’s vanila type-checker, one can use:

MetaCoq CoqCheck <term>

Erasure

An erasure procedure to untyped lambda-calculus accomplishing the same as the Extraction plugin of Coq. The extracted safe erasure is available in Coq through a new vernacular command:

MetaCoq Erase <term>

After importing MetaCoq.Erasure.Loader.

Translations

Examples of translations built on top of this:

Documentation

ident vs. qualid. vs kername

MetaCoq uses three types convertible to string which have a different intended meaning:

Quoting always produce fully qualified names. On the converse, unquoting allow to have only partially qualified names and rely on Coq to resolve them. The commands of the TemplateMonad also allow partially qualified names.

Options

Set / Unset Strict Unquote Universe Mode. When this mode is on, the unquoting of a universe level fails if this level does not exists. Otherwise the level is added to the current context. It is on by default.

There is also an “opaque” universe fresh_universe which is unquoted to a fresh level when Strict Unquote Universe Mode is off.

Papers

Team & Credits

Abhishek Anand Danil Annenkov Simon Boulier
Cyril Cohen Yannick Forster Gregory Malecha
Matthieu Sozeau Nicolas Tabareau Théo Winterhalter
MetaCoq is developed by (left to right) Abhishek Anand, Danil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.
Copyright (c) 2014-2019 Gregory Malecha
Copyright (c) 2015-2019 Abhishek Anand, Matthieu Sozeau
Copyright (c) 2017-2019 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 2018-2019 Danil Annenkov, Yannick Forster, Théo Winterhalter

This software is distributed under the terms of the MIT license. See LICENSE for details.

Bugs

Please report any bugs (or feature requests) on the github issue tracker.

Branches

The coq-8.9 branch is the active development branch. If possible, it’s strongly recommended to use this branch.

The branches coq-8.6, coq-8.7 are frozen. coq-8.8 is also available.

The branch master tracks the current Coq master branch. (Currently not working)

Installation instructions

Installing with OPAM

The easiest way to get all packages is through opam.

To add the Coq repository to available opam packages, use:

# opam repo add coq-released https://coq.inria.fr/opam/released

Then, simply issue:

# opam install coq-metacoq

MetaCoq is split into multiple packages that get all installed using the coq-metacoq meta-package:

The 1.0alpha versions of the package are for Coq 8.8 and Coq 8.9. There are also .dev packages available in the extra-dev repository of Coq, to get those you will need to activate the following repositories:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

Old, deprecated standalone packages template-coq-2.1~beta and template-coq-2.1~beta3 including previous versions of template-coq and parts of the MetaCoq development are for Coq 8.8. Package template-coq-2.0~beta is for Coq 8.7.

Setting up an opam switch

To setup a fresh opam installation, you might want to create a “switch” (an environment of opam packages) for Coq if you don’t have one yet. You need to use opam 2 to obtain the right version of Equations.

# opam switch create coq.8.9.1 4.07.1
# eval $(opam env)

This creates the coq.8.9.1 switch which initially contains only the basic OCaml 4.07.1 compiler, and puts you in the right environment (check with ocamlc -v).

Once in the right switch, you can install Coq and the Equations package using:

# opam pin add coq 8.9.1
# opam pin add coq-equations 1.2+8.9

Pinning the packages prevents opam from trying to upgrade it afterwards, in this switch. If the commands are successful you should have coq available (check with coqc -v). Then simply use:

# opam install coq-metacoq

Installing from GitHub repository (for developers)

To get the source code:

# git clone https://github.com/MetaCoq/metacoq.git
# git checkout -b coq-8.9 origin/coq-8.9
# git status

This checks that you are indeed on the coq-8.9 branch.

You can create a local switch for developing using (in the root directory of the sources):

# opam switch create . 4.07.1

Or use opam switch link foo to link an existing opam switch foo with the sources directory.

Requirements

To compile the library, you need:

When using opam you can get those using opam install --deps-only ..

You can test the installation of the packages locally using

# opam install .

at the root directory.

Compiling from sources

To compile locally without using opam, use ./configure.sh local at the root, then use: