Coq¶
Table of Contents
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.
A Coq plugin is an OCaml library that Coq can load dynamically at runtime. Plugins are typically linked with the Coq OCaml API.
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.4)
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>)
(libraries <ocaml_libraries>)
(flags <coq_flags>)
(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>
isfoo.Bar
, the theory modules are namedfoo.Bar.module1
,foo.Bar.module2
, etc. Note that modules in the same theory don’t see thefoo.Bar
prefix in the same way that OCamlwrapped
libraries do.For compatibility, Coq lang 1.0 installs a theory named
foo.Bar
underfoo/Bar
. Also note that Coq supports composing a module path from different theories, thus you can name a theoryfoo.Bar
and a second onefoo.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 writtenA.b
in this field.If
package
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_libraries>
.<coq_flags>
are passed tocoqc
as command-line options.:standard
is taken from the value set in the(coq (flags <flags>))
field inenv
profile. See env for more information.The path to the installed locations of the
<ocaml_libraries>
is passed tocoqdep
andcoqc
using Coq’s-I
flag. This allows a Coq theory to depend on an OCaml library.Your Coq theory can depend on other theories by specifying them in the
<coq_theories>
field. Dune then passes to Coq the corresponding flags for everything to compile correctly (this corresponds to the-Q
flag for Coq).You may also 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 can be as simple as placing a Coq project within the scope of another. This process is termed composition. See the interproject composition example.
Interproject composition allows for a fine granularity of dependencies. In practice, this means that Dune will only build the parts of a dependency that are needed. This means that building a project depending on another will not trigger a rebuild of the whole of the latter.
Interproject composition has been available since Coq lang 0.4.
As of today, Dune cannot depend on installed Coq theories. This restriction will be lifted in the future. Note that composition with the Coq standard library is supported, but in this case the
Coq
prefix has been made available in a qualified way, since Coq lang 0.2.You may still use installed libraries in your Coq project, but there is currently no way for Dune to know about it.
You can enable the production of Coq’s native compiler object files by setting
<coq_native_mode>
tonative
. This passes-native-compiler on
to Coq and install the corresponding object files under.coq-native
, when in therelease
profile. The regulardev
profile skips native compilation to make the build faster. This has been available since Coq lang 0.3.Please note: support for
native_compute
is experimental and requires a version of Coq later than 8.12.1. Furthermore, dependent libraries must be built with the(mode native)
enabled. In addition to that, Coq must be configured to support native compilation. Dune explicitly disables the generation of native compilation objects when(mode vo)
is enabled, irrespective of the configuration of Coq. This will be improved in the future.
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
.
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. This is a limitation ofcoqdep
. - Building a theory and a plugin in the same directory can lead to issues with the presence of the META file. We recommend the following: - A separate directory for the files of each coq.theory stanza defined. - A separate directory for source files of a plugin.
Coq Language Version¶
The Coq lang can be modified by adding the following to a dune-project file:
(using coq 0.4)
The supported Coq language versions (not the version of Coq) are:
0.1
: Basic Coq theory support.0.2
: Support for thetheories
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.
Coq Language Version 1.0¶
Guarantees with respect to stability are not yet provided. However, as the
development of features progresses, we hope to reach 1.0
soon. 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>
areflags
,theories
, andlibraries
. All of these fields have the same meaning as in thecoq.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 (coqpp ...)
stanza:
(coq.pp (modules <mlg_list>))
which, for each g_mod
in <mlg_list>
, is equivalent to the following
rule:
(rule
(targets g_mod.ml)
(deps (:mlg-file g_mod.mlg))
(action (run coqpp %{mlg-file})))
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.3)
(using coq 0.4)
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.v.d
│ │ └── 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.
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>
.
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.