diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/README.md | 27 | ||||
| -rw-r--r-- | doc/dune | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 2 |
3 files changed, 20 insertions, 15 deletions
diff --git a/doc/README.md b/doc/README.md index 3db1261656..c41d269437 100644 --- a/doc/README.md +++ b/doc/README.md @@ -101,18 +101,21 @@ Alternatively, you can use some specific targets: Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. -If you're editing Sphinx documentation, set SPHINXWARNERROR to 0 -to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits -upon detecting the first warning. You can set this on the Sphinx `make` -command line or as an environment variable: - -- `make refman SPHINXWARNERROR=0` - -- ~~~ - export SPHINXWARNERROR=0 - ⋮ - make refman - ~~~ +To build the Sphinx documentation without stopping at the first +warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such: + +``` +SPHINXWARNERROR=0 make refman-html +``` + +To do the same with the Dune build system, change the value of the +`SPHINXWARNOPT` variable (default is `-W`). The following will build +the Sphinx documentation without stopping at the first warning, and +store all the warnings in the file `/tmp/warn.log`: + +``` +SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html +``` Installation ------------ @@ -10,8 +10,10 @@ ; + tools/coqdoc/coqdoc.css (package coq) (source_tree sphinx) - (source_tree tools)) - (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (source_tree tools) + (env_var SPHINXWARNOPT)) + (action + (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1a33a9a46e..8fa631174f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -230,7 +230,7 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Set` is is the universe of *program types* or *specifications*. The +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. |