diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 110 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 |
5 files changed, 109 insertions, 14 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index a9d894cab5..dd21ea09bd 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -92,7 +92,7 @@ and use the ``==`` notation on terms of this type. Derived Canonical Structures ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We know how to use ``== `` on base types, like ``nat``, ``bool``, ``Z``. Here we show +We know how to use ``==`` on base types, like ``nat``, ``bool``, ``Z``. Here we show how to deal with type constructors, i.e. how to make the following example work: diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 7c78e1a50f..8346b72cb9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -34,9 +34,16 @@ For example, to statically link |Ltac|, you can just do: 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 @@ -119,7 +126,7 @@ 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. @@ -205,7 +212,7 @@ The following makefile rules can be extended. 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. @@ -385,7 +392,7 @@ line timing data: Reusing/extending the generated Makefile -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++ Including the generated makefile with an include directive is discouraged. The contents of this file, including variable names and @@ -429,7 +436,7 @@ have a generic target for invoking unknown targets. 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``. @@ -452,11 +459,90 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use -Module dependencies --------------------- +Building a |Coq| project with Dune +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. 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. + +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), 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 -In order to compute module dependencies (so to use ``make``), |Coq| comes -with an appropriate tool, ``coqdep``. + (coqlib + (name <module_prefix>) + (public_name <package.lib_name>) + (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 a +``<package.lib_name>`` a ``.install`` file for the library will be +generated; the optional ``<modules>`` field allows you to filter +the list of modules, and ``<libraries>`` allows to 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)) + + (rule + (targets g_equations.ml) + (deps (:pp-file g_equations.mlg)) + (action (run coqpp %{pp-file}))) + + And a Coq-specific part that depends on it via the ``libraries`` field: + + .. code:: scheme + + (coqlib + (name Equations) ; -R flag + (public_name equations.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| and |OCaml| programs, and prints the dependencies on the standard output in a @@ -474,10 +560,8 @@ done approximately and you are advised to use ``ocamldep`` instead for the See the man page of ``coqdep`` for more details and options. -The build infrastructure generated by ``coq_makefile`` uses ``coqdep`` to -automatically compute the dependencies among the files part of the -project. - +Both Dune and ``coq_makefile`` use ``coqdep`` to compute the +dependencies among the files part of a Coq project. .. _coqdoc: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7b395900e9..afb0239be4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3912,6 +3912,8 @@ At Coq startup, only the core database is nonempty and can be used. environment, including those used for ``setoid_rewrite``, from the Classes directory. +:fset: internal database for the implementation of the ``FSets`` library. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e5eb7eb4f5..1e201953b3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1473,6 +1473,10 @@ Numeral notations :n:`@ident__2` to the number will be fully reduced, and universes of the resulting term will be refreshed. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, and + primitive integers) will be considered for printing. + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). When a literal larger than :token:`num` is parsed, a warning @@ -1618,6 +1622,10 @@ String notations :n:`@ident__2` to the string will be fully reduced, and universes of the resulting term will be refreshed. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, and + primitive integers) will be considered for printing. + .. exn:: Cannot interpret this string as a value of type @type The string notation registered for :token:`type` does not support diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b58148ffff..b25104ddb9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -22,6 +22,7 @@ plugins/extraction/Extraction.v plugins/funind/FunInd.v plugins/funind/Recdef.v plugins/ltac/Ltac.v +plugins/micromega/DeclConstant.v plugins/micromega/Env.v plugins/micromega/EnvRing.v plugins/micromega/Fourier.v |