Coq ¶

Introduction ¶

Dune can build Coq theories and plugins with additional support for extraction and .mlg file preprocessing.

A Coq theory is a collection of .v files that define Coq modules whose names share a common prefix. The module names reflect the directory hierarchy.

Coq theories may be defined using coq.theory stanzas, or be auto-detected by Dune by inspecting Coq’s install directories.

A Coq plugin is an OCaml library that Coq can load dynamically at runtime. Plugins are typically linked with the Coq OCaml API.

Since Coq 8.16, plugins need to be “public” libraries in Dune’s terminology, that is to say, they must declare a public_name field.

A Coq project is an informal term for a dune-project containing a collection of Coq theories and plugins.

The .v files of a theory need not be present as source files. They may also be Dune targets of other rules.

To enable Coq support in a Dune project, specify the Coq language version in the dune-project file. For example, adding

(using coq 0.8)

to a dune-project file enables using the coq.theory stanza and other coq.* stanzas. See the Dune Coq language section for more details.

coq.theory ¶

The Coq theory stanza is very similar in form to the OCaml library stanza:

(coq.theory
 (name <module_prefix>)
 (package <package>)
 (synopsis <text>)
 (modules <ordered_set_lang>)
 (plugins <ocaml_plugins>)
 (flags <coq_flags>)
 (coqdoc_flags <coqdoc_flags>)
 (stdlib <stdlib_included>)
 (mode <coq_native_mode>)
 (theories <coq_theories>))

The stanza builds all the .v files in the given directory and its subdirectories if the include-subdirs stanza is present.

For usage of this stanza, see the Examples of Coq Projects.

The semantics of the fields are:

<module_prefix> is a dot-separated list of valid Coq module names and determines the module scope under which the theory is compiled (this corresponds to Coq’s -R option).

For example, if <module_prefix> is foo.Bar, the theory modules are named foo.Bar.module1, foo.Bar.module2, etc. Note that modules in the same theory don’t see the foo.Bar prefix in the same way that OCaml wrapped libraries do.

For compatibility, Coq lang 1.0 installs a theory named foo.Bar under foo/Bar. Also note that Coq supports composing a module path from different theories, thus you can name a theory foo.Bar and a second one foo.Baz, and Dune composes these properly. See an example of a multi-theory Coq project for this.
The modules field allows one to constrain the set of modules included in the theory, similar to its OCaml counterpart. Modules are specified in Coq notation. That is to say, A/b.v is written A.b in this field.
If the package field is present, Dune generates install rules for the .vo files of the theory. pkg_name must be a valid package name.

Note that Coq lang 1.0 will use the Coq legacy install setup, where all packages share a common root namespace and install directory, lib/coq/user-contrib/<module_prefix>, as is customary in the Make-based Coq package ecosystem.

For compatibility, Dune also installs, under the user-contrib prefix, the .cmxs files that appear in <ocaml_plugins>. This will be dropped in future versions.
<coq_flags> are passed to coqc as command-line options. :standard is taken from the value set in the (coq (flags <flags>)) field in env profile. See env for more information.
<coqdoc_flags> are extra user-configurable flags passed to coqdoc. The default value for :standard is --toc. The --html or --latex flags are passed separately depending on which mode is targed. See the section on documentation using coqdoc for more information.
<stdlib_included> can either be yes or no, currently defaulting to yes. When set to no, Coq’s standard library won’t be visible from this theory, which means the Coq prefix won’t be bound, and Coq.Init.Prelude won’t be imported by default.
If the plugins field is present, Dune will pass the corresponding flags to Coq so that coqdep and coqc can find the corresponding OCaml libraries declared in <ocaml_plugins>. This allows a Coq theory to depend on OCaml plugins. Starting with (lang coq 0.6), <ocaml_plugins> must contain public library names.
Your Coq theory can depend on other theories — globally installed or defined in the current workspace — by adding the theories names to the <coq_theories> field. Then, Dune will ensure that the depended theories are present and correctly registered with Coq.

See Locating Theories for more information on how Coq theories are located by Dune.
If Coq has been configured with -native-compiler yes or ondemand, Dune will always build the cmxs files together with the vo files. This only works on Coq versions after 8.13 in which the option was introduced.

You may override this by specifying (mode native) or (mode vo).

Before Coq lang 0.7, the native mode had to be manually specified, and Coq did not use Coq’s configuration

Versions of Dune < 3.7.0 would disable native compilation if the dev profile was selected.
If the (mode vos) field is present, only Coq compiled interface files .vos will be produced for the theory. This is mainly useful in conjunction with dune coq top, since this makes the compilation of dependencies much faster, at the cost of skipping proof checking. (Appeared in Coq lang 0.8).

When a Coq file a.v depends on another file b.v, Dune is able to build them in the correct order, even if they are in separate theories. Under the hood, Dune asks coqdep how to resolve these dependencies, which is why it is called once per theory.

Coq Documentation ¶

Given a coq.theory stanza with name A, Dune will produce two directory targets, A.html/ and A.tex/. HTML or LaTeX documentation for a Coq theory may then be built by running dune build A.html or dune build A.tex, respectively (if the dune file for the theory is the current directory).

There are also two aliases @doc and @doc-latex that will respectively build the HTML or LaTeX documentation when called. These will determine whether or not Dune passes a --html or --latex flag to coqdoc.

Further flags can also be configured using the (coqdoc_flags) field in the coq.theory stanza. These will be passed to coqdoc and the default value is :standard which is --toc. Extra flags can therefore be passed by writing (coqdoc_flags :standard --body-only) for example.

Recursive Qualification of Modules ¶

If you add:

(include_subdirs qualified)

to a dune file, Dune considers all the modules in the directory and its subdirectories, adding a prefix to the module name in the usual Coq style for subdirectories. For example, file A/b/C.v becomes the module A.b.C.

How Dune Locates and Builds theories ¶

Dune organises it’s knowledge about Coq theories in 3 databases:

Scope database: A Dune scope is a part of the project sharing a single common dune-project file. In a single scope, any theory in the database can depend on any other theory in that database as long as their visibilities are compatible. A public theory for example cannot depend on a private theory.
Public theory database: The set of all scopes that Dune knows about is termed a workspace. Only public theories coming from scopes are added to the database of all public theories in the current workspace.

The public theory database allows theories to depend on theories that are in a different scope. Thus, you can depend on theories belonging to another dune-project as long as they share a common scope under another dune-project file or a dune-workspace file.

Doing so is usually as simple as placing a Coq project within the scope of another. This process is termed composition. See the interproject composition example.

Inter-project composition allows Dune to compute module dependencies using a fine granularity. In practice, this means that Dune will only build the parts of a depended theory that are needed by your project.

Inter-project composition has been available since Coq lang 0.4.
Installed theory database: If a theory cannot be found in the list of workspace-public theories, Dune will try to locate the theory in the list of installed locations Coq knows about.

This list is built using the output of coqc --config in order to infer the COQLIB and COQPATH environment variables. Each path in COQPATH and COQLIB/user-contrib is used to build the database of installed theories.

Note that, for backwards compatibility purposes, installed theories do not have to be installed or built using Dune. Dune tries to infer the name of the theory from the installed layout. This is ambiguous in the sense that a file-system layout of a/b will provide theory names a and a.b.

Resolving this ambiguity in a backwards-compatible way is not possible, but future versions of Dune Coq support will provide a way to improve this.

Coq’s standard library gets a special status in Dune. The location at COQLIB/theories will be assigned a entry with the theory name Coq, and added to the dependency list implicitly. This can be disabled with the (stdlib no) field in the coq.theory stanza.

The Coq prefix can then be used to depend on Coq’s stdlib in a regular, qualified way. We recommend setting (stdlib no) and adding (theories Coq) explicitly.

Composition with installed theories has been available since Coq lang 0.8.

The databases above are used to locate a theory dependencies. Note that Dune has a complete global view of every file involved in the compilation of your theory and will therefore rebuild if any changes are detected.

Public and Private Theories ¶

A public theory is a coq.theory stanza that is visible outside the scope of a dune-project file.

A private theory is a coq.theory stanza that is limited to the scope of the dune-project file it is in.

A private theory may depend on both private and public theories; however, a public theory may only depend on other public theories.

By default, all coq.theory stanzas are considered private by Dune. In order to make a private theory into a public theory, the (package ) field must be specified.

(coq.theory
 (name private_theory))

(coq.theory
 (name private_theory)
 (package coq-public-theory))

Limitations ¶

.v files always depend on the native OCaml version of the Coq binary and its plugins, unless the natively compiled versions are missing.

A foo.mlpack file must the present in directories of locally defined plugins for things to work. coqdep, which is used internally by Dune, will recognize a plugin by looking at the existence of an .mlpack file, as it cannot access (for now) Dune’s library database. This is a limitation of coqdep. See the example plugin or the this template.

This limitation will be lifted soon, as newer versions of coqdep can use findlib’s database to check the existence of OCaml libraries.

Coq Language Version ¶

The Coq lang can be modified by adding the following to a dune-project file:

(using coq 0.8)

The supported Coq language versions (not the version of Coq) are:

0.8: Support for composition with installed Coq theories; support for vos builds.

Deprecated experimental Coq language versions are:

0.1: Basic Coq theory support.
0.2: Support for the theories field and composition of theories in the same scope.
0.3: Support for (mode native) requires Coq >= 8.10 (and Dune >= 2.9 for Coq >= 8.14).
0.4: Support for interproject composition of theories.
0.5: (libraries ...) field deprecated in favor of (plugins ...) field.
0.6: Support for (stdlib no).
0.7: (mode ) is automatically detected from the configuration of Coq and (mode native) is deprecated. The dev profile also no longer disables native compilation.

Coq Language Version 1.0 ¶

Guarantees with respect to stability are not yet provided, but we intend that the (0.8) version of the language becomes 1.0. The 1.0 version of Coq lang will commit to a stable set of functionality. All the features below are expected to reach 1.0 unchanged or minimally modified.

coq.extraction ¶

Coq may be instructed to extract OCaml sources as part of the compilation process by using the coq.extraction stanza:

(coq.extraction
 (prelude <name>)
 (extracted_modules <names>)
 <optional-fields>)

(prelude <name>) refers to the Coq source that contains the extraction commands.
(extracted_modules <names>) is an exhaustive list of OCaml modules extracted.
<optional-fields> are flags, stdlib, theories, and plugins. All of these fields have the same meaning as in the coq.theory stanza.

The extracted sources can then be used in executable or library stanzas as any other sources.

Note that the sources are extracted to the directory where the prelude file lives. Thus the common placement for the OCaml stanzas is in the same dune file.

Warning: using Coq’s Cd command to work around problems with the output directory is not allowed when using extraction from Dune. Moreover the Cd command has been deprecated in Coq 8.12.

coq.pp ¶

Authors of Coq plugins often need to write .mlg files to extend the Coq grammar. Such files are preprocessed with the coqpp binary. To help plugin authors avoid writing boilerplate, we provide a (coq.pp ...) stanza:

(coq.pp
 (modules <ordered_set_lang>))

This will run the coqpp binary on all the .mlg files in <ordered_set_lang>.

Examples of Coq Projects ¶

Here we list some examples of some basic Coq project setups in order.

Simple Project ¶

Let us start with a simple project. First, make sure we have a dune-project file with a Coq lang stanza present:

(lang dune 3.12)
(using coq 0.8)

Next we need a dune file with a coq.theory stanza:

(coq.theory
 (name myTheory))

Finally, we need a Coq .v file which we name A.v:

(** This is my def *)
Definition mydef := nat.

Now we run dune build. After this is complete, we get the following files:

.
├── A.v
├── _build
│   ├── default
│   │   ├── A.glob
│   │   ├── A.v
│   │   └── A.vo
│   └── log
├── dune
└── dune-project

Multi-Theory Project ¶

Here is an example of a more complicated setup:

.
├── A
│   ├── AA
│   │   └── aa.v
│   ├── AB
│   │   └── ab.v
│   └── dune
├── B
│   ├── b.v
│   └── dune
└── dune-project

Here are the dune files:

; A/dune
(include_subdirs qualified)
(coq.theory
 (name A))

; B/dune
(coq.theory
 (name B)
 (theories A))

Notice the theories field in B allows one coq.theory to depend on another. Another thing to note is the inclusion of the include_subdirs stanza. This allows our theory to have multiple subdirectories.

Here are the contents of the .v files:

(* A/AA/aa.v is empty *)

(* A/AB/ab.v *)
Require Import AA.aa.

(* B/b.v *)
From A Require Import AB.ab.

This causes a dependency chain b.v -> ab.v -> aa.v. Now we might be interested in building theory B, so all we have to do is run dune build B. Dune will automatically build the theory A since it is a dependency.

Composing Projects ¶

To demonstrate the composition of Coq projects, we can take our previous two examples and put them in project which has a theory that depends on theories in both projects.

.
├── CombinedWork
│   ├── comb.v
│   └── dune
├── DeeperTheory
│   ├── A
│   │   ├── AA
│   │   │   └── aa.v
│   │   ├── AB
│   │   │   └── ab.v
│   │   └── dune
│   ├── B
│   │   ├── b.v
│   │   └── dune
│   ├── Deep.opam
│   └── dune-project
├── dune-project
└── SimpleTheory
    ├── A.v
    ├── dune
    ├── dune-project
    └── Simple.opam

The file comb.v looks like:

(* Files from DeeperTheory *)
From A.AA Require Import aa.
(* In Coq, partial prefixes for theory names are enough *)
From A Require Import ab.
From B Require Import b.

(* Files from SimpleTheory *)
From myTheory Require Import A.

We are referencing Coq modules from all three of our previously defined theories.

Our dune file in CombinedWork looks like:

(coq.theory
 (name Combined)
 (theories myTheory A B))

As you can see, there are dependencies on all the theories we mentioned.

All three of the theories we defined before were private theories. In order to depend on them, we needed to make them public theories. See the section on Public and Private Theories.

Composing With Installed Theories ¶

We can also compose with theories that are installed. If we wanted to have a theory that depends on the Coq theory mathcomp.ssreflect we can add the following to our stanza:

(coq.theory
 (name my_mathcomp_theory)
 (theories mathcomp.ssreflect))

Note that mathcomp on its own would also work, since there would be a matchcomp directory in user-contrib, however it would not compose locally with a coq.theory stanza with the mathcomp.ssreflect name (in case one exists). So it is advisable to use the actual theory name. Dune is not able to validate theory names that have been installed since they do not include their Dune metadata.

Building Documentation ¶

Following from our last example, we might wish to build the HTML documentation for A. We simply do dune build A/A.html/. This will produce the following files:

A
├── AA
│   ├── aa.glob
│   ├── aa.v
│   └── aa.vo
├── AB
│   ├── ab.glob
│   ├── ab.v
│   └── ab.vo
└── A.html
    ├── A.AA.aa.html
    ├── A.AB.ab.html
    ├── coqdoc.css
    ├── index.html
    └── toc.html

We may also want to build the LaTeX documentation of the theory B. For this we can call dune build B/B.tex/. If we want to build all the HTML documentation targets, we can use the @doc alias as in dune build @doc. If we want to build all the LaTeX documentation then we use the @doc-latex alias instead.

Coq Plugin Project ¶

Let us build a simple Coq plugin to demonstrate how Dune can handle this setup.

.
├── dune-project
├── src
│   ├── dune
│   ├── hello_world.ml
│   ├── my_plugin.mlpack
│   └── syntax.mlg
└── theories
    ├── dune
    └── UsingMyPlugin.v

Our dune-project will need to have a package for the plugin to sit in, otherwise Coq will not be able to find it.

(lang dune 3.12)
(using coq 0.8)

(package
 (name my-coq-plugin)
 (synopsis "My Coq Plugin")
 (depends coq-core))

Now we have two directories, src/ and theories/ each with their own dune file. Let us begin with the plugin dune file:

(library
 (name my_plugin)
 (public_name my-coq-plugin.plugin)
 (synopsis "My Coq Plugin")
 (flags :standard -rectypes -w -27)
 (libraries coq-core.vernac))

(coq.pp
 (modules syntax))

Here we define a library using the library stanza. Importantly, we declared which external libraries we rely on and gave the library a public_name, as starting with Coq 8.16, Coq will identify plugins using their corresponding findlib public name.

The coq.pp stanza allows src/syntax.mlg to be preprocessed, which for reference looks like:

DECLARE PLUGIN "my-coq-plugin.plugin"

VERNAC COMMAND EXTEND CallToC CLASSIFIED AS QUERY
| [ "Hello" ] -> { Feedback.msg_notice Pp.(str Hello_world.hello_world) }
END

Together with hello_world.ml:

let hello_world = "hello world!"

They make up the plugin. There is one more important ingredient here and that is the my_plugin.mlpack file, needed to signal coqdep the existence of my_plugin in this directory. An empty file suffices. See this note on .mlpack files.

The file for theories/ is a standard coq.theory stanza with an included libraries field allowing Dune to see my-coq-plugin.plugin as a dependency.

(coq.theory
 (name MyPlugin)
 (package my-coq-plugin)
 (plugins my-coq-plugin.plugin))

Finally, our .v file will look something like this:

(* For Coq < 8.16 *)
Declare ML Module "my_plugin".

(* For Coq = 8.16 *)
Declare ML Module "my_plugin:my-coq-plugin.plugin".

(* At some point Coq 8.17 or 8.18 will transition to the syntax below, check Coq's manual *)
Declare ML Module "my-coq-plugin.plugin".

Hello.

Running dune build will build everything correctly.

Running a Coq Toplevel ¶

Dune supports running a Coq toplevel binary such as coqtop, which is typically used by editors such as CoqIDE or Proof General to interact with Coq.

The following command:

$ dune coq top <file> -- <args>

runs a Coq toplevel (coqtop by default) on the given Coq file <file>, after having recompiled its dependencies as necessary. The given arguments <args> are forwarded to the invoked command. For example, this can be used to pass a -emacs flag to coqtop.

A different toplevel can be chosen with dune coq top --toplevel CMD <file>. Note that using --toplevel echo is one way to observe what options are actually passed to the toplevel. These options are computed based on the options that would be passed to the Coq compiler if it was invoked on the Coq file <file>.

In certain situations, it is desirable to not rebuild dependencies for a .v files but still pass the correct flags to the toplevel. For this reason, a --no-build flag can be passed to dune coq top which will skip any building of dependencies.

Limitations ¶

Only files that are part of a stanza can be loaded in a Coq toplevel.
When a file is created, it must be written to the file system before the Coq toplevel is started.
When new dependencies are added to a file (via a Coq Require vernacular command), it is in principle required to save the file and restart to Coq toplevel process.

Coq-Specific Variables ¶

There are some special variables that can be used to access data about the Coq configuration. These are:

%{coq:version} the version of Coq.
%{coq:version.major} the major version of Coq (e.g., 8.15.2 gives 8).
%{coq:version.minor} the minor version of Coq (e.g., 8.15.2 gives 15).
%{coq:version.suffix} the suffix version of Coq (e.g., 8.15.2 gives .2 and 8.15+rc1 gives +rc1).
%{coq:ocaml-version} the version of OCaml used to compile Coq.
%{coq:coqlib} the output of COQLIB from coqc -config.
%{coq:coq_native_compiler_default} the output of COQ_NATIVE_COMPILER_DEFAULT from coqc -config.

See Variables for more information on variables supported by Dune.