Centralise and improve documentation on Coq

Signed-off-by: Ali Caglayan <alizter@gmail.com>

doc/coq.rst

@@ -0,0 +1,379 @@
+.. _coq:
+
+***
+Coq
+***
+
+.. contents:: Table of Contents
+    :depth: 3
+
+Introduction
+------------
+
+Dune is able to build Coq theories and plugins with support for source file
+preprocessing, and extraction.
+
+A *Coq theory* is a collection of ``.v`` files, perhaps in several directories,
+all prefixed by a common Coq module name, following the directory hierarchy for
+module names.
+
+A *Coq plugin* is an OCaml :ref:`library`, that is intended to be depended on
+by a Coq theory, and is typically linked with the Coq OCaml API.
+
+A *Coq project* is a collection of Coq plugins and Coq theories. This notion is
+subsumed by that of a :ref:`dune-project`, and should not be considered a
+technical definition.
+
+.. _coq-theory:
+
+coq.theory
+----------
+
+To enable Coq related stanzas in a Dune project. The Coq language version should
+be selected in the :ref:`dune-project` file. For example:
+
+.. code:: scheme
+
+    (using coq 0.3)
+
+This will allow for the ``coq.theory`` stanza and other ``coq.*`` stanzas to be
+included in the current project. See the :ref:`Dune Coq language
+section<coq-lang>` for more details.
+
+The Coq theory stanza is very similar in form to the OCaml :ref:`library`
+stanza:
+
+.. code:: scheme
+
+    (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 will build all ``.v`` files in the given directory and also all
+subdirs if the :ref:`include-subdirs <include-subdirs-coq>` stanza is present.
+The semantics of 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 will be
+  named as ``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 reasons, Coq lang 1.0 will install 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 will compose these properly.
+
+- The ``modules`` field allows one to constrain the set of modules included in
+  the theory, similarly 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 ``package`` is present, Dune will generate install rules for the ``.vo``
+  files of the theory. ``pkg_name`` must be a valid package name.
+
+  Note that Coq lang 1.0 uses the Coq legacy install setup, where all packages
+  share a common root namespace and install directory,
+  ``lib/coq/user-contrib/<module_prefix>``, as customary in the Make-based Coq
+  package ecosystem.
+
+  For compatibility, we also install under the ``user-contrib`` prefix the
+  ``.cmxs`` files that appear in ``<ocaml_libraries>``,
+
+- ``<coq_flags>`` will be passed to ``coqc`` as command-line options.
+  ``:standard`` is taken from the value set in the ``(coq (flags <flags>))``
+  field in ``env`` profile. See :ref:`dune-env` for more information.
+
+- The path to the ``<ocaml_libraries>`` installed locations will be passed to
+  ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq theory
+  to depend on an ML library, making it a Coq plugin.
+
+- Your Coq theory can depend on other theories by specifying them in the
+  ``<coq_theories>`` field. Dune will then pass to Coq the corresponding flags
+  for everything to compile correctly (this corresponds to the ``-Q`` flag for
+  Coq).
+
+  As of today, we only support composition with libraries defined in the same
+  scope (i.e. under the same :ref:`dune-project` domain). 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 can enable the production of Coq's native compiler object files by setting
+  ``<coq_native_mode>`` to ``native``. This will pass ``-native-compiler on`` to
+  Coq and install the corresponding object files under ``.coq-native``, when in
+  the ``release`` profile. The regular ``dev`` profile will skip 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
+  Coq >= 8.12.1. Furthermore, dependant libraries *must* be built with the
+  ``(mode native)`` enabled. In Addition to that, Coq must be configured to
+  support native compilation. Dune will explicitly disable the generation of
+  native compilation objects when ``(mode vo)`` is enabled, irrespective of the
+  configuration of Coq. This will be improved in the future.
+
+.. _include-subdirs-coq:
+
+Recursive Qualification of Modules
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+If you add:
+
+.. code:: scheme
+
+    (include_subdirs qualified)
+
+to a :ref:`dune file<dune-files>`, Dune will consider 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`` will be module
+``A.b.C``.
+
+Limitations
+~~~~~~~~~~~
+
+- ``.v`` files always depend on the native OCaml version of the Coq binary and
+  its plugins, unless the natively compiled versions are not available.
+
+.. _limitation-mlpack:
+
+- A ``foo.mlpack`` file must the present in directories of locally defined
+  plugins for things to work. This is a limitation of ``coqdep``.
+
+.. _coq-lang:
+
+Coq Language Version
+~~~~~~~~~~~~~~~~~~~~
+
+The Coq lang can be modified by adding the following to a :ref:`dune-project`
+file:
+
+.. code:: scheme
+
+    (using coq 0.3)
+
+The supported Coq language versions (not the version of Coq) 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).
+
+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.
+
+Best Practices
+~~~~~~~~~~~~~~
+
+We recommend the following guidelines:
+
+- A separate directory for the files of each :ref:`coq-theory` stanza defined.
+- A separate directory for source files of a plugin.
+
+.. _coq-extraction:
+
+coq.extraction
+--------------
+
+Coq may be instructed to *extract* OCaml sources as part of the compilation
+process by using the ``coq.extraction`` stanza:
+
+.. code:: scheme
+
+   (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``, ``theories``, and ``libraries``. 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
+:ref:`dune file<dune-files>`.
+
+**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:
+
+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:
+
+.. code:: scheme
+
+    (coq.pp (modules <mlg_list>))
+
+which, for each ``g_mod`` in ``<mlg_list>``, is equivalent to the following
+rule:
+
+.. code:: lisp
+
+    (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 Coq Project
+~~~~~~~~~~~~~~~~~~
+
+Let us start with a simple project. First we make sure we have a
+:ref:`dune-project` file with ``(using coq 0.3)``.(or higher) present.
+
+.. code:: scheme
+
+  (lang dune 3.2)
+  (using coq 0.3)
+
+Next we need a :ref:`dune file<dune-files>` with a :ref:`coq-theory` stanza:
+
+.. code:: scheme
+  
+  (coq.theory
+   (name myTheory))
+
+
+Finally, we need a Coq ``.v`` file which we will name ``A.v``:
+
+
+.. code:: coq
+
+  (** This is my def *)
+  Definition mydef := nat.
+
+Now we run ``dune build``. After this is complete, we will get the following
+files:
+
+.. code::
+
+  .
+  ├── 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:
+
+.. code::
+
+  .
+  ├── A
+  │   ├── AA
+  │   │   └── aa.v
+  │   ├── AB
+  │   │   └── ab.v
+  │   └── dune
+  ├── B
+  │   ├── b.v
+  │   └── dune
+  └── dune-project
+
+Here are the :ref:`dune files<dune-files>`:
+
+.. code:: scheme
+
+  ; 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 :ref:`coq-theory` to depend on
+another. Another thing to note is the inclusion of the :ref:`include_subdirs`
+stanza. This allows our theory to have :ref:`multiple
+subdirectories<include-subdirs-coq>`. 
+
+Here are the contents of the ``.v`` files:
+
+.. code:: coq
+  
+  (* 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.
+
+.. _running-coq-top:
+
+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:
+
+.. code:: bash
+
+   $ dune coq top <file> -- <args>
+
+will run a Coq toplevel (``coqtop`` by default) on the given Coq file
+``<file>``, after having re-compiled 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.