Skip to content

The bootstrapped plugins

Jump to bottom
Matthieu Sozeau edited this page Oct 12, 2022 · 2 revisions

The CertiCoqC plugin

The CertiCoqC plugin (Require Import CertiCoqC.CertiCoqC) provides the exact same functionality as the CertiCoq Plugin, except that it runs a CertiCoq compiled version of the CertiCoq pipeline, i.e. CertiCoq but in C code rather than ML code.

Commands are simply prefixed with CertiCoqC rather than CertiCoq.

The CertiCoqCheck plugin

This plugin (Require Import CertiCoqCheck.Loader) provides a CertiCoq-compiled version of MetaCoq's safe checker, i.e., a verified type-checker for Coq compiled with a verified compiler.

The plugin provides a single command CertiCoqCheck [global_reference] that typechecks a global reference and all its dependencies and prints its type or an error message.

Clone this wiki locally