diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 71 |
2 files changed, 60 insertions, 16 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 98d222e317..aa4b6edd7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -227,7 +227,10 @@ and ``coqtop``, unless stated otherwise: type of the option. For flags ``Option Name`` is equivalent to ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. + shell syntax, Coq does not see them. Flags are processed after initialization + of the document. This includes the `Prelude` if loaded and any libraries loaded + through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` + options. :-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 179dff9959..e5ff26520a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -499,40 +499,81 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use (``.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. + <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), 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: +``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 - (coqlib + (coq.theory (name <module_prefix>) - (public_name <package.lib_name>) + (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 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. +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 @@ -565,9 +606,9 @@ of your project. .. code:: scheme - (coqlib + (coq.theory (name Equations) ; -R flag - (public_name equations.Equations) + (package equations) (synopsis "Equations Plugin") (libraries coq.plugins.extraction equations.plugin) (modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build |