Coq¶
Dune is also able to build Coq developments. A Coq project is a mix of
Coq .v
files and (optionally) OCaml libraries linking to the Coq
API (in which case we say the project is a Coq plugin). To enable
Coq support in a dune project, the language version should be selected
in the dune-project
file. For example:
(using coq 0.1)
This will enable support for the coq.theory
stanza in the current project. If the
language version is absent, dune will automatically add this line with the
latest Coq version to the project file once a (coq.theory ...)
stanza is used anywhere.
Basic Usage¶
The basic form for defining Coq libraries is very similar to the OCaml form:
(coq.theory
(name <module_prefix>)
(public_name <package.lib_name>)
(synopsis <text>)
(modules <ordered_set_lang>)
(libraries <ocaml_libraries>)
(flags <coq_flags>))
The stanza will build all .v files on the given directory. The semantics of fields is:
<module_prefix>>
will be used as the default Coq library prefix-R
,- the
modules
field does allow to constraint the set of modules included in the library, similarly to its OCaml counterpart, public_name
will make Dune generate install rules for the .vo files; files will be installed inlib/coq/user-contrib/<module_prefix>
, as customary in the make-based Coq package eco-system. For compatibility, we also installs the .cmxs files appearing in <ocaml-librarie> under the user-contrib prefix.<coq_flags>
will be passed tocoqc
,- the path to installed locations of
<ocaml_libraries>
will be passed tocoqdep
andcoqc
using Coq’s-I
flag; this allows for a Coq library to depend on a ML plugin.
Preprocessing with coqpp
¶
Coq plugin writers usually need to write .mlg
files to extend Coq
grammar. Such files are pre-processed with coqpp; to help plugin
writers avoid boilerplate we provide a (coqpp …) stanza:
(coq.pp (modules <mlg_list>))
which for each g_mod
in ``<mlg_list>```is equivalent to:
(rule
(targets g_mod.ml)
(deps (:mlg-file g_mod.mlg))
(action (run coqpp %{mlg-file})))
Recursive Qualification of Modules¶
If you add:
(include_subdirs qualified)
to a dune
file, Dune will to consider that all the modules in
their directory and sub-directories, adding a prefix to the module
name in the usual Coq style for sub-directories. For example, file A/b/C.v
will be module A.b.C
.
Limitations¶
- composition and scoping of Coq libraries is still not possible. For now, libraries are located using Coq’s built-in library management,
- .v always depend on the native version of a plugin,
- a
foo.mlpack
file must the present for locally defined plugins to work, this is a limitation of coqdep,