MetaCoq

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

• Installing
• Documentation
• Papers
• Team

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:

• Reification of the environment structures, for constant and inductive declarations.

• Denotation of terms and global declarations

• A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MTac.

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:

• Weakening for global declarations, weakening and substitution for local contexts.

• Confluence of reduction using a notion of parallel reduction

• Validity, Subject Reduction and Principality.

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:

• a parametricity plugin in translations/param_original.v
• a plugin to negate funext in translations/times_bool_fun.v

Documentation

• You may want to start with a demo
• The 8.9 branch documentation (as light coqdoc files).
• An example Coq plugin built on the Template Monad, which can be used to add a constructor to any inductive type is in test-suite/add_constructor.v
• The test-suite files test-suite/erasure_test.v and test-suite/safechecker_test.v show example uses (and current limitations of) the verified checker and erasure.

ident vs. qualid. vs kername

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

• ident is the type of identifiers, they should not contains any dot. E.g. nat

• qualid is the type of partially qualified names. E.g. Datatypes.nat

• kername is the type of fully qualified names. E.g. Coq.Init.Datatypes.nat

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

• "Coq Coq Codet! Towards a Verified Toolchain for Coq in MetaCoq" Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. Abstract and presentation given at the Coq Workshop 2019, September 2019.

• "Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq". Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. Submitted, July 2019.

• A certifying extraction with time bounds from Coq to call-by-value λ-calculus. Yannick Forster and Fabian Kunze. ITP 2019. Example

• "The MetaCoq Project" Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau and Théo Winterhalter. Extended version of the ITP 2018 paper. Submitted, March 2019.

  This includes a full documentation of the Template Monad.

• "Towards Certified Meta-Programming with Typed Template-Coq" Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau. ITP 2018.

• The system was presented at Coq'PL 2018

Team & Credits

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.

Install from GitHub repository

To get the source code:

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

Check that you are indeed on the coq-8.8 branch.

Requirements

To compile the library, you need:

• Coq 8.8.2 (older versions of 8.8 might also work)
• OCaml (tested with 4.04.1, beware that OCaml 4.06.0 can produce linking errors on some platforms)
• Equations 1.2

Requirements through opam

The easiest way to get all packages is through opam:

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.8.2 4.04.1
# eval $(opam env)

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

You can also create a local switch for developing using:

# opam switch create . 4.04.1

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

# opam pin add coq 8.8.2
# opam pin add coq-equations 1.2+8.8

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

You can test the installation of the packages locally using opam install . at the root directory.

Compile

Once in the right environment, run ./configure.sh for a global build or ./configure.sh local for a local build. Then use:

• make to compile the template-coq plugin, the checker, the pcuic development and the erasure plugin. You can also selectively build each target.

• make translations to compile the translation plugins ======= 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:

• coq-metacoq-template for the Template Monad and quoting plugin
• coq-metacoq-checker for the UNverified checker of template-coq terms
• coq-metacoq-pcuic for the PCUIC development and proof of the Template-Coq -> PCUIC translation
• coq-metacoq-safechecker for the verified checker on PCUIC terms
• coq-metacoq-erasure for the verifed erasure from PCUIC to untyped lambda-calculus.
• coq-metacoq-translations for example translations from type theory to type theory: e.g. variants of parametricity.

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:

• Coq 8.9.1 (for the coq-8.9 branch) or Coq 8.8.2 (for the coq-8.8 branch). Older versions of 8.9 or 8.8 might also work.
• OCaml (tested with 4.06.1 and 4.07.1, beware that OCaml 4.06.0 can produce linking errors on some platforms)
• Equations 1.2

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:

• make to compile the template-coq plugin, the checker, the pcuic development and the safechecker and erasure plugins. You can also selectively build each target.

• make translations to compile the translation plugins

• make test-suite to compile the test suite

• make install to install the plugin in Coq's user-contrib local library. Then the MetaCoq namespace can be used for Require Import statements, e.g. From MetaCoq.Template Require Import All..