Prepare split of section about coqdoc.

1 files changed, 0 insertions, 665 deletions

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e5ff26520a..cada680895 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -1,642 +1,3 @@
-.. _utilities:
-
----------------------
- Utilities
----------------------
-
-The distribution provides utilities to simplify some tedious works
-beside proof development, tactics writing or documentation.
-
-
-Using Coq as a library
-----------------------
-
-In previous versions, ``coqmktop`` was used to build custom
-toplevels - for example for better debugging or custom static
-linking. Nowadays, the preferred method is to use ``ocamlfind``.
-
-The most basic custom toplevel is built using:
-
-::
-
-   % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
-                 -package coq.toplevel \
-                 topbin/coqtop_bin.ml -o my_toplevel.native
-
-
-For example, to statically link |Ltac|, you can just do:
-
-::
-
-   % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
-                 -package coq.toplevel,coq.plugins.ltac \
-                 topbin/coqtop_bin.ml -o my_toplevel.native
-
-and similarly for other plugins.
-
-Building a |Coq| project
-------------------------
-
-As of today it is possible to build Coq projects using two tools:
-
-- coq_makefile, which is distributed by Coq and is based on generating a makefile,
-- Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries.
-
-Building a |Coq| project with coq_makefile
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The majority of |Coq| projects are very similar: a collection of ``.v``
-files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
-metadata needed in order to build the project are the command line
-options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command
-line options <command-line-options>`). Collecting the list of files
-and options is the job of the ``_CoqProject`` file.
-
-A simple example of a ``_CoqProject`` file follows:
-
-::
-
-    -R theories/ MyCode
-    -arg -w
-    -arg all
-    theories/foo.v
-    theories/bar.v
-    -I src/
-    src/baz.mlg
-    src/bazaux.ml
-    src/qux_plugin.mlpack
-
-where options ``-R``, ``-Q`` and ``-I`` are natively recognized, as well as
-file names. The lines of the form ``-arg foo`` are used in order to tell
-to literally pass an argument ``foo`` to ``coqc``: in the
-example, this allows to pass the two-word option ``-w all`` (see
-:ref:`command line options <command-line-options>`).
-
-Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``)
-understand ``_CoqProject`` files and invoke |Coq| with the desired options.
-
-The ``coq_makefile`` utility can be used to set up a build infrastructure
-for the |Coq| project based on makefiles. The recommended way of
-invoking ``coq_makefile`` is the following one:
-
-::
-
-    coq_makefile -f _CoqProject -o CoqMakefile
-
-
-Such command generates the following files:
-
-CoqMakefile
-  is a generic makefile for ``GNU Make`` that provides
-  targets to build the project (both ``.v`` and ``.ml*`` files), to install it
-  system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed)
-  as well as to invoke coqdoc to generate HTML documentation.
-
-CoqMakefile.conf
-  contains make variables assignments that reflect
-  the contents of the ``_CoqProject`` file as well as the path relevant to
-  |Coq|.
-
-
-An optional file ``CoqMakefile.local`` can be provided by the user in order to
-extend ``CoqMakefile``. In particular one can declare custom actions to be
-performed before or after the build process. Similarly one can customize the
-install target or even provide new targets. Extension points are documented in
-paragraph :ref:`coqmakefilelocal`.
-
-The extensions of the files listed in ``_CoqProject`` is used in order to
-decide how to build them. In particular:
-
-
-+ |Coq| files must use the ``.v`` extension
-+ |OCaml| files must use the ``.ml`` or ``.mli`` extension
-+ |OCaml| files that require pre processing for syntax
-  extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension
-+ In order to generate a plugin one has to list all |OCaml|
-  modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib``
-  file).
-
-
-The use of ``.mlpack`` files has to be preferred over ``.mllib`` files,
-since it results in a “packed” plugin: All auxiliary modules (as
-``Baz`` and ``Bazaux``) are hidden inside the plugin’s "namespace"
-(``Qux_plugin``). This reduces the chances of begin unable to load two
-distinct plugins because of a clash in their auxiliary module names.
-
-.. _coqmakefilelocal:
-
-CoqMakefile.local
-+++++++++++++++++
-
-The optional file ``CoqMakefile.local`` is included by the generated
-file ``CoqMakefile``. It can contain two kinds of directives.
-
-**Variable assignment**
-
-The variable must belong to the variables listed in the ``Parameters``
-section of the generated makefile.
-Here we describe only few of them.
-
-:CAMLPKGS:
-   can be used to specify third party findlib packages, and is
-   passed to the OCaml compiler on building or linking of modules. Eg:
-   ``-package yojson``.
-:CAMLFLAGS:
-   can be used to specify additional flags to the |OCaml|
-   compiler, like ``-bin-annot`` or ``-w``....
-:OCAMLWARN:
-   it contains a default of ``-warn-error +a-3``, useful to modify
-   this setting; beware this is not recommended for projects in
-   Coq's CI.
-:COQC, COQDEP, COQDOC:
-   can be set in order to use alternative binaries
-   (e.g. wrappers)
-:COQ_SRC_SUBDIRS:
-   can be extended by including other paths in which ``*.cm*`` files
-   are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq``
-   lets you build a plugin containing OCaml code that depends on the
-   OCaml code of ``Unicoq``
-:COQFLAGS:
-   override the flags passed to ``coqc``. By default ``-q``.
-:COQEXTRAFLAGS:
-   extend the flags passed to ``coqc``
-:COQCHKFLAGS:
-   override the flags passed to ``coqchk``.  By default ``-silent -o``.
-:COQCHKEXTRAFLAGS:
-   extend the flags passed to ``coqchk``
-:COQDOCFLAGS:
-   override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``.
-:COQDOCEXTRAFLAGS:
-   extend the flags passed to ``coqdoc``
-
-**Rule extension**
-
-The following makefile rules can be extended.
-
-.. example::
-
-    ::
-
-        pre-all::
-                echo "This line is print before making the all target"
-        install-extra::
-                cp ThisExtraFile /there/it/goes
-
-``pre-all::``
-  run before the ``all`` target. One can use this to configure
-  the project, or initialize sub modules or check dependencies are met.
-
-``post-all::``
-  run after the ``all`` target. One can use this to run a test
-  suite, or compile extracted code.
-
-``install-extra::``
-  run after ``install``. One can use this to install extra files.
-
-``install-doc::``
-  One can use this to install extra doc.
-
-``uninstall::``
-  \
-
-``uninstall-doc::``
-  \
-
-``clean::``
-  \
-
-``cleanall::``
-  \
-
-``archclean::``
-  \
-
-``merlin-hook::``
-  One can append lines to the generated ``.merlin`` file extending this
-  target.
-
-Timing targets and performance testing
-++++++++++++++++++++++++++++++++++++++
-
-The generated ``Makefile`` supports the generation of two kinds of timing
-data: per-file build-times, and per-line times for an individual file.
-
-The following targets and Makefile variables allow collection of per-
-file timing data:
-
-
-+ ``TIMED=1``
-    passing this variable will cause ``make`` to emit a line
-    describing the user-space build-time and peak memory usage for each
-    file built.
-
-    .. note::
-      On ``Mac OS``, this works best if you’ve installed ``gnu-time``.
-
-    .. example::
-
-       For example, the output of ``make TIMED=1`` may look like
-       this:
-
-       ::
-
-          COQDEP Fast.v
-          COQDEP Slow.v
-          COQC Slow.v
-          Slow (user: 0.34 mem: 395448 ko)
-          COQC Fast.v
-          Fast (user: 0.01 mem: 45184 ko)
-
-+ ``pretty-timed``
-    this target stores the output of ``make TIMED=1`` into
-    ``time-of-build.log``, and displays a table of the times, sorted from
-    slowest to fastest, which is also stored in ``time-of-build-pretty.log``.
-    If you want to construct the ``log`` for targets other than the default
-    one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed
-    TGTS="a.vo b.vo"``.
-
-    .. note::
-       This target requires ``python`` to build the table.
-
-    .. note::
-       This target will *append* to the timing log; if you want a
-       fresh start, you must remove the file ``time-of-build.log`` or
-       ``run make cleanall``.
-
-    .. note::
-       By default the table displays user times.  If the build log
-       contains real times (which it does by default), passing
-       ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times
-       rather than user times in the table.
-
-    .. example::
-
-      For example, the output of ``make pretty-timed`` may look like this:
-
-      ::
-
-        COQDEP Fast.v
-        COQDEP Slow.v
-        COQC Slow.v
-        Slow (user: 0.36 mem: 393912 ko)
-        COQC Fast.v
-        Fast (user: 0.05 mem: 45992 ko)
-        Time     | File Name
-        --------------------
-        0m00.41s | Total
-        --------------------
-        0m00.36s | Slow
-        0m00.05s | Fast
-
-
-+ ``print-pretty-timed-diff``
-    this target builds a table of timing changes between two compilations; run
-    ``make make-pretty-timed-before`` to build the log of the “before” times,
-    and run ``make make-pretty-timed-after`` to build the log of the “after”
-    times. The table is printed on the command line, and stored in
-    ``time-of-build-both.log``. This target is most useful for profiling the
-    difference between two commits in a repository.
-
-    .. note::
-       This target requires ``python`` to build the table.
-
-    .. note::
-       The ``make-pretty-timed-before`` and ``make-pretty-timed-after`` targets will
-       *append* to the timing log; if you want a fresh start, you must remove
-       the files ``time-of-build-before.log`` and ``time-of-build-after.log`` or run
-       ``make cleanall`` *before* building either the “before” or “after”
-       targets.
-
-    .. note::
-       The table will be sorted first by absolute time
-       differences rounded towards zero to a whole-number of seconds, then by
-       times in the “after” column, and finally lexicographically by file
-       name. This will put the biggest changes in either direction first, and
-       will prefer sorting by build-time over subsecond changes in build time
-       (which are frequently noise); lexicographic sorting forces an order on
-       files which take effectively no time to compile.
-
-       If you prefer a different sorting order, you can pass
-       ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or
-       ``TIMING_SORT_BY=diff`` to sort by the signed difference in
-       time.
-
-    .. note::
-       Just like ``pretty-timed``, this table defaults to using user
-       times.  Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead.
-
-    .. example::
-
-        For example, the output table from
-        ``make print-pretty-timed-diff`` may look like this:
-
-        ::
-
-          After    | File Name | Before   || Change    | % Change
-          --------------------------------------------------------
-          0m00.39s | Total     | 0m00.35s || +0m00.03s | +11.42%
-          --------------------------------------------------------
-          0m00.37s | Slow      | 0m00.01s || +0m00.36s | +3600.00%
-          0m00.02s | Fast      | 0m00.34s || -0m00.32s | -94.11%
-
-
-The following targets and ``Makefile`` variables allow collection of per-
-line timing data:
-
-
-+ ``TIMING=1``
-    passing this variable will cause ``make`` to use ``coqc -time`` to
-    write to a ``.v.timing`` file for each ``.v`` file compiled, which contains
-    line-by-line timing information.
-
-    .. example::
-
-       For example, running ``make all TIMING=1`` may result in a file like this:
-
-       ::
-
-          Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s)
-          Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s)
-          Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s)
-          Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s)
-
-+ ``print-pretty-single-time-diff``
-
-    ::
-
-       print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing
-
-    this target will make a sorted table of the per-line timing differences
-    between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and
-    save it to the file specified by the ``TIME_OF_PRETTY_BUILD_FILE`` variable,
-    which defaults to ``time-of-build-pretty.log``.
-    To generate the ``.v.before-timing`` or ``.v.after-timing`` files, you should
-    pass  ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``.
-
-    .. note::
-       The sorting used here is the same as in the ``print-pretty-timed-diff`` target.
-
-    .. note::
-       This target requires python to build the table.
-
-    .. note::
-       This target follows the same sorting order as the
-       ``print-pretty-timed-diff`` target, and supports the same
-       options for the ``TIMING_SORT_BY`` variable.
-
-    .. note::
-       By default, two lines are only considered the same if the
-       character offsets and initial code strings are identical.  Passing
-       ``TIMING_FUZZ=N`` relaxes this constraint by allowing the
-       character locations to differ by up to ``N``, as long
-       as the total number of characters and initial code strings
-       continue to match.  This is useful when there are small changes
-       to a file, and you want to match later lines that have not
-       changed even though the character offsets have changed.
-
-    .. note::
-       By default the table picks up real times, under the assumption
-       that when comparing line-by-line, the real time is a more
-       accurate representation as it includes disk time and time spent
-       in the native compiler.  Passing ``TIMING_REAL=0`` to ``make``
-       will use user times rather than real times in the table.
-
-    .. example::
-
-       For example, running  ``print-pretty-single-time-diff`` might give a table like this:
-
-       ::
-
-          After     | Code                                                | Before    || Change    | % Change
-          ---------------------------------------------------------------------------------------------------
-          0m00.50s  | Total                                               | 0m04.17s  || -0m03.66s | -87.96%
-          ---------------------------------------------------------------------------------------------------
-          0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47%
-          0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.]        | 0m00.143s || -0m00.01s | -11.88%
-             N/A    | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s    || +0m00.00s | N/A
-          0m00.s    | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] |    N/A    || +0m00.00s | N/A
-          0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
-
-
-+ ``all.timing.diff``, ``path/to/file.v.timing.diff``
-    The ``path/to/file.v.timing.diff`` target will make a ``.v.timing.diff`` file for
-    the corresponding ``.v`` file, with a table as would be generated by
-    the ``print-pretty-single-time-diff`` target; it depends on having already
-    made the corresponding ``.v.before-timing`` and ``.v.after-timing`` files,
-    which can be made by passing ``TIMING=before`` and ``TIMING=after``.
-    The  ``all.timing.diff`` target will make such timing difference files for
-    all of the ``.v`` files that the ``Makefile`` knows about. It will fail if
-    some ``.v.before-timing`` or ``.v.after-timing`` files don’t exist.
-
-    .. note::
-      This target requires python to build the table.
-
-
-Reusing/extending the generated Makefile
-++++++++++++++++++++++++++++++++++++++++
-
-Including the generated makefile with an include directive is
-discouraged. The contents of this file, including variable names and
-status of rules shall change in the future. Users are advised to
-include ``Makefile.conf`` or call a target of the generated Makefile as in
-``make -f Makefile target`` from another Makefile.
-
-One way to get access to all targets of the generated ``CoqMakefile`` is to
-have a generic target for invoking unknown targets.
-
-.. example::
-
-  ::
-
-      # KNOWNTARGETS will not be passed along to CoqMakefile
-      KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2
-      # KNOWNFILES will not get implicit targets from the final rule, and so
-      # depending on them won't invoke the submake
-      # Warning: These files get declared as PHONY, so any targets depending
-      # on them always get rebuilt
-      KNOWNFILES   := Makefile _CoqProject
-
-      .DEFAULT_GOAL := invoke-coqmakefile
-
-      CoqMakefile: Makefile _CoqProject
-              $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile
-
-      invoke-coqmakefile: CoqMakefile
-              $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
-
-      .PHONY: invoke-coqmakefile $(KNOWNFILES)
-
-      ####################################################################
-      ##                      Your targets here                         ##
-      ####################################################################
-
-      # This should be the last rule, to handle any targets not declared above
-      %: invoke-coqmakefile
-              @true
-
-
-
-Building a subset of the targets with ``-j``
-++++++++++++++++++++++++++++++++++++++++++++
-
-To build, say, two targets foo.vo and bar.vo in parallel one can use
-``make only TGTS="foo.vo bar.vo" -j``.
-
-.. note::
-
-  ``make foo.vo bar.vo -j`` has a different meaning for the make
-  utility, in particular it may build a shared prerequisite twice.
-
-
-.. note::
-
-  For users of coq_makefile with version < 8.7
-
-  + Support for "subdirectory" is deprecated. To perform actions before
-    or after the build (like invoking ``make`` on a subdirectory) one can hook
-    in pre-all and post-all extension points.
-  + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target
-    (``.PHONY`` or not) please use ``CoqMakefile.local``.
-
-
-Precompiling for ``native_compute``
-+++++++++++++++++++++++++++++++++++
-
-To compile files for ``native_compute``, one can use the
-``-native-compiler yes`` option of |Coq|, for instance by putting the
-following in a :ref:`coqmakefilelocal` file:
-
-::
-
-    COQEXTRAFLAGS += -native-compiler yes
-
-The generated ``CoqMakefile`` installation target will then take care
-of installing the extra ``.coq-native`` directories.
-
-.. note::
-
-   As an alternative to modifying any file, one can set the
-   environment variable when calling ``make``:
-
-   ::
-
-      COQEXTRAFLAGS="-native-compiler yes" make
-
-   This can be useful when files cannot be modified, for instance when
-   installing via OPAM a package built with ``coq_makefile``:
-
-   ::
-
-      COQEXTRAFLAGS="-native-compiler yes" opam install coq-package
-
-.. note::
-
-   This requires all dependencies to be themselves compiled with
-   ``-native-compiler yes``.
-
-Building a |Coq| project with Dune
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. note::
-
-   Dune's Coq support is still experimental; we strongly recommend
-   using Dune 2.3 or later.
-
-.. note::
-
-   The canonical documentation for the Coq Dune extension is
-   maintained upstream; please refer to the `Dune manual
-   <https://dune.readthedocs.io/>`_ for up-to-date information. This
-   documentation is up to date for Dune 2.3.
-
-Building a Coq project with Dune requires setting up a Dune project
-for your files. This involves adding a ``dune-project`` and
-``pkg.opam`` file to the root (``pkg.opam`` can be empty or generated
-by Dune itself), and then providing ``dune`` files in the directories
-your ``.v`` files are placed. For the experimental version "0.1" of
-the Coq Dune language, |Coq| library stanzas look like:
-
-.. code:: scheme
-
-    (coq.theory
-     (name <module_prefix>)
-     (package <opam_package>)
-     (synopsis <text>)
-     (modules <ordered_set_lang>)
-     (libraries <ocaml_libraries>)
-     (flags <coq_flags>))
-
-This stanza will build all `.v` files in the given directory, wrapping
-the library under ``<module_prefix>``. If you declare an
-``<opam_package>``, an ``.install`` file for the library will be
-generated; the optional ``(modules <ordered_set_lang>)`` field allows
-you to filter the list of modules, and ``(libraries
-<ocaml_libraries>)`` allows the Coq theory depend on ML plugins. For
-the moment, Dune relies on Coq's standard mechanisms (such as
-``COQPATH``) to locate installed Coq libraries.
-
-By default Dune will skip ``.v`` files present in subdirectories. In
-order to enable the usual recursive organization of Coq projects add
-
-.. code:: scheme
-
-    (include_subdirs qualified)
-
-to you ``dune`` file.
-
-Once your project is set up, `dune build` will generate the
-`pkg.install` files and all the files necessary for the installation
-of your project.
-
-.. example::
-
-   A typical stanza for a Coq plugin is split into two parts. An OCaml build directive, which is standard Dune:
-
-   .. code:: scheme
-
-       (library
-        (name equations_plugin)
-        (public_name equations.plugin)
-        (flags :standard -warn-error -3-9-27-32-33-50)
-        (libraries coq.plugins.cc coq.plugins.extraction))
-
-       (coq.pp (modules g_equations))
-
-   And a Coq-specific part that depends on it via the ``libraries`` field:
-
-   .. code:: scheme
-
-       (coq.theory
-        (name Equations) ; -R flag
-        (package equations)
-        (synopsis "Equations Plugin")
-        (libraries coq.plugins.extraction equations.plugin)
-        (modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build
-
-       (include_subdirs qualified)
-
-.. _coqdep:
-
-Computing Module dependencies
------------------------------
-
-In order to compute module dependencies (to be used by ``make`` or
-``dune``), |Coq| provides the ``coqdep`` tool.
-
-``coqdep`` computes inter-module dependencies for |Coq|
-programs, and prints the dependencies on the standard output in a
-format readable by make. When a directory is given as argument, it is
-recursively looked at.
-
-Dependencies of |Coq| modules are computed by looking at ``Require``
-commands (``Require``, ``Require Export``, ``Require Import``), but also at the
-command ``Declare ML Module``.
-
-See the man page of ``coqdep`` for more details and options.
-
-Both Dune and ``coq_makefile`` use ``coqdep`` to compute the
-dependencies among the files part of a Coq project.
-
 .. _coqdoc:
 
 Documenting |Coq| files with coqdoc
@@ -1100,29 +461,3 @@ macros:
       \newcommand{\coqdocmodule}[1]{\section*{Module #1}}
 
   and you may redefine it using ``\renewcommand``.
-
-Embedded Coq phrases inside |Latex| documents
----------------------------------------------
-
-When writing documentation about a proof development, one may want
-to insert |Coq| phrases inside a |Latex| document, possibly together
-with the corresponding answers of the system. We provide a mechanical
-way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex``
-filter. This filter extracts |Coq| phrases embedded in |Latex| files,
-evaluates them, and insert the outcome of the evaluation after each
-phrase.
-
-Starting with a file ``file.tex`` containing |Coq| phrases, the ``coq-tex``
-filter produces a file named ``file.v.tex`` with the Coq outcome.
-
-There are options to produce the |Coq| parts in smaller font, italic,
-between horizontal rules, etc. See the man page of ``coq-tex`` for more
-details.
-
-
-Man pages
----------
-
-There are man pages for the commands ``coqdep`` and ``coq-tex``. Man
-pages are installed at installation time (see installation
-instructions in file ``INSTALL``, step 6).