diff options
101 files changed, 1938 insertions, 1054 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 9009c798f2..267da478d7 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -151,9 +151,8 @@ /plugins/ltac/ @ppedrot # Secondary maintainer @herbelin -/plugins/micromega/ @fajb -/test-suite/micromega/ @fajb -# Secondary maintainer @bgregoir +/plugins/micromega/ @coq/micromega-maintainers +/test-suite/micromega/ @coq/micromega-maintainers /plugins/nsatz/ @thery # Secondary maintainer @ppedrot diff --git a/.gitignore b/.gitignore index 8fc3c802ad..582a8f43c7 100644 --- a/.gitignore +++ b/.gitignore @@ -99,6 +99,9 @@ doc/faq/axioms.eps doc/faq/axioms.eps_t doc/faq/axioms.pdf_t doc/faq/axioms.png +doc/sphinx/index.rst +doc/sphinx/zebibliography.rst +doc/sphinx/credits-wrapper.rst doc/stdlib/Library.out doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0115ac9eff..039c02c4b9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-09-05-V1" + CACHEKEY: "bionic_coq-V2018-09-21-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/.travis.yml b/.travis.yml index dd28410bec..1a2c909c7d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -105,8 +105,8 @@ matrix: # Full Coq test-suite with two compilers - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" - - EXTRA_CONF="-coqide opt -with-doc yes" + - TEST_TARGET="doc-html test-suite" + - EXTRA_CONF="-coqide opt" - EXTRA_OPAM="${LABLGTK} ounit" before_install: &sphinx-install - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex @@ -119,26 +119,17 @@ matrix: - aspcud - libgtk2.0-dev - libgtksourceview2.0-dev - - texlive-latex-base - - texlive-latex-recommended - - texlive-latex-extra - - texlive-math-extra - - texlive-fonts-recommended - - texlive-fonts-extra - - latex-xcolor - - ghostscript - - tipa - python3 - python3-pip - python3-setuptools - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" + - TEST_TARGET="doc-html test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -with-doc yes" + - EXTRA_CONF="-coqide opt" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: @@ -150,11 +141,11 @@ matrix: # Full test-suite with flambda - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" + - TEST_TARGET="doc-html test-suite" - COMPILER="${COMPILER_BE}+flambda" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" + - EXTRA_CONF="-coqide opt -flambda-opts -O3" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: @@ -175,7 +166,9 @@ matrix: before_install: - brew update - brew unlink python - - brew install opam gnu-time + - brew install gnu-time + # only way to continue using OPAM 1.2 + - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb - if: NOT (type = pull_request) os: osx @@ -192,7 +185,9 @@ matrix: before_install: - brew update - brew unlink python - - brew install opam gnu-time gtk+ expat gtksourceview gdk-pixbuf + - brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf + # only way to continue using OPAM 1.2 + - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb - brew unlink python@2 - brew install python3 - pip3 install macpack @@ -215,6 +215,10 @@ Notations Changes from 8.8.1 to 8.8.2 =========================== +Documentation + +- A PDF version of the reference manual is available once again. + Tools - The coq-makefile targets `print-pretty-timed`, `print-pretty-timed-diff`, @@ -227,6 +231,14 @@ Kernel polymorphic universe binders, fixing a soundness break (triggered only through custom plugins) +Windows installer + +- The Windows installer now includes many more external packages that can be +individually selected for installation. + +Many other bug fixes and lots of documentation improvements (for details, +see the 8.8.2 milestone at https://github.com/coq/coq/milestone/15?closed=1). + Changes from 8.8.0 to 8.8.1 =========================== diff --git a/Makefile.doc b/Makefile.doc index 0dcf9daf27..788e4e61e7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -58,17 +58,24 @@ ifndef QUICK SPHINX_DEPS := coq endif +# sphinx-html and sphinx-latex +sphinx-%: $(SPHINX_DEPS) + $(SHOW)'SPHINXBUILD doc/sphinx ($*)' + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ + $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* + +sphinx-pdf: sphinx-latex + +$(MAKE) -C $(SPHINXBUILDDIR)/latex + sphinx: $(SPHINX_DEPS) - $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html - @echo - @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." + +$(MAKE) sphinx-html + +$(MAKE) sphinx-pdf doc-html:\ - doc/stdlib/html/index.html sphinx + doc/stdlib/html/index.html sphinx-html doc-pdf:\ - doc/stdlib/Library.pdf + doc/stdlib/Library.pdf sphinx-pdf doc-ps:\ doc/stdlib/Library.ps @@ -181,7 +188,7 @@ install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: install-doc-stdlib-html install-doc-sphinx +install-doc-html: install-doc-stdlib-html install-doc-sphinx-html install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib @@ -192,7 +199,7 @@ install-doc-printable: $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps -install-doc-sphinx: +install-doc-sphinx-html: $(MKDIR) $(FULLDOCDIR)/sphinx (for f in `cd doc/sphinx/_build; find . -type f`; do \ $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ diff --git a/Makefile.dune b/Makefile.dune index e04982650f..cac1bdd6a1 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -7,11 +7,15 @@ # DUNEOPT=--display=short BUILD_CONTEXT=_build/default +COQ_CONFIGURE_PREFIX?=_build/install/default + +export COQ_CONFIGURE_PREFIX help: @echo "Welcome to Coq's Dune-based build system. Targets are:" @echo " - states: build a minimal functional coqtop" @echo " - world: build all binaries and libraries" + @echo " - watch: build all binaries and libraries [continuous build]" @echo " - release: build Coq in release mode" @echo " - apidoc: build ML API documentation" @echo " - clean: remove build directory and autogenerated files" @@ -27,6 +31,9 @@ states: voboot world: voboot dune build $(DUNEOPT) @install +watch: voboot + dune build $(DUNEOPT) @install -w + release: voboot dune build $(DUNEOPT) -p coq diff --git a/config/dune b/config/dune index 30faf1233e..cf2bc71363 100644 --- a/config/dune +++ b/config/dune @@ -9,5 +9,5 @@ (rule (targets coq_config.ml) (mode fallback) - (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run) - (action (chdir %{project_root} (run %{ocaml} configure.ml -local -warn-error yes -native-compiler yes)))) + (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) + (action (chdir %{project_root} (run %{ocaml} configure.ml -native-compiler no)))) diff --git a/configure.ml b/configure.ml index 00ec559a1b..1c2edefc5c 100644 --- a/configure.ml +++ b/configure.ml @@ -1038,7 +1038,16 @@ let find_suffix prefix path = match prefix with let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) = let dir,suffix = if !prefs.local then (use_suffix coqtop locallayout,locallayout) - else match uservalue, !prefs.prefix with + else + let env_prefix = + match !prefs.prefix with + | None -> + begin + try Some (Sys.getenv "COQ_CONFIGURE_PREFIX") + with Not_found -> None + end + | p -> p + in match uservalue, env_prefix with | Some d, p -> d,find_suffix p d | _, Some p -> let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in @@ -15,8 +15,12 @@ depends: [ "camlp5" ] +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] + build: [ [ "dune" "build" "@vodeps" ] [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ] - [ "dune" "build" "-p" package "-j" jobs ] + [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/default.nix b/default.nix index 6f759f41d1..88992a30a3 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz"; - sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc"; + url = "https://github.com/NixOS/nixpkgs/archive/947ae71dcec680b5075ece14e38eae64831b9819.tar.gz"; + sha256 = "15nryymfch4fzxk6nacli4gw4cyicpdjwzai5v3bc0azaslww2x5"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -38,18 +38,6 @@ with pkgs; with stdenv.lib; -let dune = - overrideDerivation jbuilder (o: { - name = "dune-1.1.1"; - src = fetchFromGitHub { - owner = "ocaml"; - repo = "dune"; - rev = "1.1.1"; - sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw"; - }; - }); -in - stdenv.mkDerivation rec { name = "coq"; diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8a49b97dac..2a29b0d3b6 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -878,7 +878,7 @@ function make_num { function make_findlib { make_ocaml - if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then + if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8b26294d8f..d943795258 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-05-V1" +# CACHEKEY: "bionic_coq-V2018-09-21-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -7,13 +7,19 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ + # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib opam \ + # Dependencies of lablgtk (for CoqIDE) libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-science tipa \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ - python3-setuptools python3-wheel python3-pip + # Dependencies of stdlib and sphinx doc + texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ + xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + # Dependencies of source-doc and coq-makefile + texlive-science tipa -RUN pip3 install antlr4-python3-runtime +# More dependencies of the sphinx doc +RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # Basic OPAM setup ENV NJOBS="2" \ @@ -28,7 +34,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml. # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. diff --git a/doc/README.md b/doc/README.md index 47507de52d..1461fa2e2c 100644 --- a/doc/README.md +++ b/doc/README.md @@ -28,18 +28,18 @@ To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + - sphinx >= 1.7.8 + - sphinx_rtd_theme >= 0.2.5b2 + - beautifulsoup4 >= 4.0.6 + - antlr4-python3-runtime >= 4.7.1 + - pexpect >= 4.2.1 + - sphinxcontrib-bibtex >= 0.4.0 -You can install them using `pip3 install` or using your distribution's package -manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", -Ubuntu 18.04, ...) you can use: +To install them, you should first install pip and setuptools (for instance, +with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: - apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ - python3-bs4 python3-sphinxcontrib.bibtex python3-pip - -Then, install the missing Python3 Antlr4 package: - - pip3 install antlr4-python3-runtime + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \ + pexpect sphinxcontrib-bibtex Nix users should get the correct development environment to build the HTML documentation from Coq's [`default.nix`](../default.nix) (note this @@ -54,10 +54,19 @@ additional tools are required: - pdflatex - dvips - makeindex + - xelatex + - latexmk + - xindy + +All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu, +install them with: + + apt install texlive-full -Install them using your package manager. E.g. on Debian / Ubuntu: +Or if you want to use less disk space: - apt install texlive-latex-extra texlive-fonts-recommended + apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ + latexmk xindy Compilation ----------- @@ -80,7 +89,7 @@ Alternatively, you can use some specific targets: to produce all HTML documents - `make sphinx` - to produce the HTML version of the reference manual + to produce the HTML and PDF versions of the reference manual - `make stdlib` to produce all formats of the Coq standard library @@ -94,7 +103,7 @@ 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 sphinx SPINXWARNERROR=0` +- `make sphinx SPHINXWARNERROR=0` - ~~~ export SPHINXWARNERROR=0 diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4673107e3d..c1f3f7b4d0 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -114,15 +114,33 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Raised if :n:`@tactic` does not fully solve the goal. -``.. opt::`` :black_nib: A Coq option. +``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting). Example:: - .. opt:: Nonrecursive Elimination Schemes + .. flag:: Nonrecursive Elimination Schemes This option controls whether types declared with the keywords :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. +``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options) + Example:: + + .. opt:: Printing Width @num + :name: Printing Width + + This command sets which left-aligned part of the width of the screen is used + for display. At the time of writing this documentation, the default value + is 78. + +``.. table::`` :black_nib: A Coq table (i.e a setting whose value is a set). + Example:: + + .. table:: Search Blacklist @string + :name: Search Blacklist + + This table controls ... + ``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists @@ -260,8 +278,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo .. inference:: name - newline-separated premisses - ------------------------ + newline-separated premises + -------------------------- conclusion Example:: @@ -274,14 +292,12 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo ----------------------------- \WTEG{\forall~x:T,U}{\Prop} -``.. preamble::`` A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. - - Example:: +``.. preamble::`` A reST directive to include a TeX file. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. - .. preamble:: + Usage:: - \newcommand{\paren}[#1]{\left(#1\right)} + .. preamble:: preamble.tex Coq roles ========= @@ -364,6 +380,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -377,6 +419,86 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DON'T + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + +Overusing the ``example`` directive +----------------------------------- + +DO + .. code:: + + Here is a useful axiom: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + +DO + .. code:: + + .. example:: Using proof-irrelevance + + If you assume the axiom above, … + +DON'T + .. code:: + + Here is a useful axiom: + + .. example:: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + Tips and tricks =============== @@ -398,7 +520,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index c333d6e9d5..86914a71df 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -140,6 +140,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -153,6 +179,86 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DON'T + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + +Overusing the ``example`` directive +----------------------------------- + +DO + .. code:: + + Here is a useful axiom: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + +DO + .. code:: + + .. example:: Using proof-irrelevance + + If you assume the axiom above, … + +DON'T + .. code:: + + Here is a useful axiom: + + .. example:: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + Tips and tricks =============== @@ -174,7 +280,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 2cc1f95c08..3e414a714c 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _canonicalstructures: Canonical Structures diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e507a224c6..cb267576b2 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -1,15 +1,13 @@ -.. include:: ../replaces.rst - .. _extendedpatternmatching: -Extended pattern-matching +Extended pattern matching ========================= :Authors: Cristina Cornes and Hugo Herbelin .. TODO links to figures -This section describes the full form of pattern-matching in |Coq| terms. +This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -38,7 +36,7 @@ same values as ``pattern`` does and ``identifier`` is bound to the matched value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A list of patterns separated with commas is also considered as a pattern and is called *multiple pattern*. However multiple patterns can only -occur at the root of pattern-matching equations. Disjunctions of +occur at the root of pattern matching equations. Disjunctions of *multiple patterns* are allowed though. Since extended ``match`` expressions are compiled into the primitive ones, @@ -46,7 +44,7 @@ the expressiveness of the theory remains the same. Once parsing has finished only simple patterns remain. The original nesting of the ``match`` expressions is recovered at printing time. An easy way to see the result of the expansion is to toggle off the nesting performed at printing -(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print` +(use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print` if the term is a constant, or using the command :cmd:`Check`. The extended ``match`` still accepts an optional *elimination predicate* @@ -88,7 +86,7 @@ Using multiple patterns in the definition of ``max`` lets us write: which will be compiled into the previous form. -The pattern-matching compilation strategy examines patterns from left +The pattern matching compilation strategy examines patterns from left to right. A match expression is generated **only** when there is at least one constructor in the column of patterns. E.g. the following example does not build a match expression. @@ -262,9 +260,9 @@ When we use parameters in patterns there is an error message: | cons A _ l' => l' end). -.. opt:: Asymmetric Patterns +.. flag:: Asymmetric Patterns -This option (off by default) removes parameters from constructors in patterns: + This flag (off by default) removes parameters from constructors in patterns: .. coqtop:: all @@ -597,7 +595,7 @@ situation: incorrect (because constructors are not applied to the correct number of the arguments, because they are not linear or they are wrongly typed). -.. exn:: Non exhaustive pattern-matching. +.. exn:: Non exhaustive pattern matching. The pattern matching is not exhaustive. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e3d25cf5cf..3d58f522dd 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extraction: Extraction of programs in |OCaml| and Haskell @@ -131,14 +129,14 @@ order to produce more readable code. The type-preserving optimizations are controlled by the following |Coq| options: -.. opt:: Extraction Optimize +.. flag:: Extraction Optimize Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Turn this option off if you want a ML term as close as possible to the Coq term. -.. opt:: Extraction Conservative Types +.. flag:: Extraction Conservative Types Default is off. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy @@ -146,7 +144,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. -.. opt:: Extraction KeepSingleton +.. flag:: Extraction KeepSingleton Default is off. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and @@ -155,7 +153,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: The typical example is ``sig``. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -.. opt:: Extraction AutoInline +.. flag:: Extraction AutoInline Default is on. The extraction mechanism inlines the bodies of some defined constants, according to some heuristics @@ -227,7 +225,7 @@ When an actual extraction takes place, an error is normally raised if the if any of the implicit arguments still occurs in the final code. This behavior can be relaxed via the following option: -.. opt:: Extraction SafeImplicits +.. flag:: Extraction SafeImplicits Default is on. When this option is off, a warning is emitted instead of an error if some implicit arguments still occur in the @@ -319,15 +317,15 @@ native boolean type instead of the |Coq| one. The syntax is the following: extractions for the type itself (first `string`) and all its constructors (all the `string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native - pattern-matching of the language will be used. + pattern matching of the language will be used. .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra `string` that indicates how to - perform pattern-matching over this inductive type. In this form, + perform pattern matching over this inductive type. In this form, the ML extraction could be an arbitrary type. For an inductive type with `k` constructors, the function used to - emulate the pattern-matching should expect `(k+1)` arguments, first the `k` + emulate the pattern matching should expect `(k+1)` arguments, first the `k` branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no @@ -344,7 +342,7 @@ native boolean type instead of the |Coq| one. The syntax is the following: * Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an - ad-hoc pattern-matching) will often **not** be fully rigorously + ad-hoc pattern matching) will often **not** be fully rigorously correct. For instance, when extracting ``nat`` to |OCaml| ``int``, it is theoretically possible to build ``nat`` values that are larger than |OCaml| ``max_int``. It is the user's responsibility to diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e0babb6c4e..403b163196 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _generalizedrewriting: Generalized rewriting @@ -126,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. coqtop:: in - forall (A : Type) (S1 S1’ S2 S2’ : list A), - set_eq A S1 S1’ -> - set_eq A S2 S2’ -> - set_eq A (union A S1 S2) (union A S1’ S2’). + forall (A: Type) (S1 S1' S2 S2': list A), + set_eq A S1 S1' -> + set_eq A S2 S2' -> + set_eq A (union A S1 S2) (union A S1' S2'). The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` for all ``A``. @@ -451,7 +448,7 @@ various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration: -.. coqtop:: in +.. coqdoc:: Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] @@ -462,7 +459,7 @@ hint database. For example, the declaration: is equivalent to an instance declaration: -.. coqtop:: in +.. coqdoc:: Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 23cbd76eda..fc5a366caf 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _implicitcoercions: Implicit Coercions @@ -256,19 +254,16 @@ Displaying Available Coercions Activating the Printing of Coercions ------------------------------------- -.. opt:: Printing Coercions +.. flag:: Printing Coercions When on, this option forces all the coercions to be printed. By default, coercions are not printed. -.. cmd:: Add Printing Coercion @qualid - - This command forces coercion denoted by :n:`@qualid` to be printed. - By default, a coercion is never printed. - -.. cmd:: Remove Printing Coercion @qualid +.. table:: Printing Coercion @qualid + :name: Printing Coercion - Use this command, to skip the printing of coercion :n:`@qualid`. + Specifies a set of qualids for which coercions are always displayed. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. .. _coercions-classes-as-records: @@ -315,7 +310,7 @@ are also forgotten. Coercions and Modules --------------------- -.. opt:: Automatic Coercions Import +.. flag:: Automatic Coercions Import Since |Coq| version 8.3, the coercions present in a module are activated only when the module is explicitly imported. Formerly, the coercions diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 0f2d35d044..2cde65dcdc 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _miscellaneousextensions: Miscellaneous extensions diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 9adeca46fc..e7a8c238ac 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,5 +1,3 @@ -.. include:: ../preamble.rst - .. _nsatz_chapter: Nsatz: tactics for proving equalities in integral domains diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index f7a431ef29..828505b850 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -116,23 +116,23 @@ loaded by Options ------- -.. opt:: Stable Omega +.. flag:: Stable Omega .. deprecated:: 8.5 This deprecated option (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. -.. opt:: Omega UseLocalDefs +.. flag:: Omega UseLocalDefs This option (on by default) allows :tacn:`omega` to use the bodies of local variables. -.. opt:: Omega System +.. flag:: Omega System This option (off by default) activate the printing of debug information -.. opt:: Omega Action +.. flag:: Omega Action This option (off by default) activate the printing of debug information diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8ee8f52227..8b7214e2ab 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _asynchronousandparallelproofprocessing: Asynchronous and Parallel Proof Processing @@ -60,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index d6895f5fe5..fad45995d2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. this should be just "_program", but refs to it don't work .. _programs: @@ -45,7 +42,7 @@ be considered as an object of type :g:`{x : T | P}` for any well-formed will generate an obligation for every such coercion. In the other direction, Russell will automatically insert a projection. -Another distinction is the treatment of pattern-matching. Apart from +Another distinction is the treatment of pattern matching. Apart from the following differences, it is equivalent to the standard match operation (see :ref:`extendedpatternmatching`). @@ -84,15 +81,15 @@ operation (see :ref:`extendedpatternmatching`). There are options to control the generation of equalities and coercions. -.. opt:: Program Cases +.. flag:: Program Cases - This controls the special treatment of pattern-matching generating equalities + This controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. -.. opt:: Program Generalized Coercion +.. flag:: Program Generalized Coercion This controls the coercion of general inductive types when using |Program| (the option is on by default). Coercion of subset types and pairs is still @@ -105,7 +102,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern-matching if a return or in clause is specified. Likewise, the +pattern matching if a return or in clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -213,7 +210,7 @@ with mutually recursive definitions too. end. Here we have one obligation for each branch (branches for :g:`0` and -``(S 0)`` are automatically generated by the pattern-matching +``(S 0)`` are automatically generated by the pattern matching compilation algorithm). .. coqtop:: all @@ -320,19 +317,19 @@ optional tactic is replaced by the default one if not specified. Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging. -.. opt:: Transparent Obligations +.. flag:: Transparent Obligations Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. -.. opt:: Hide Obligations +.. flag:: Hide Obligations Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation. -.. opt:: Shrink Obligations +.. flag:: Shrink Obligations *Deprecated since 8.7* @@ -378,6 +375,3 @@ Frequently Asked Questions using lazy evaluation; #. Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible. - -.. bibliography:: ../biblio.bib - :keyprefix: p- diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 8cb86e2267..58617916c0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,11 +1,9 @@ -.. include:: ../replaces.rst .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` - .. _theringandfieldtacticfamilies: The ring and field tactic families diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ab4b4a9824..369dae0ead 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _typeclasses: Type Classes @@ -458,7 +456,7 @@ This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. Options ~~~~~~~ -.. opt:: Typeclasses Dependency Order +.. flag:: Typeclasses Dependency Order This option (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend @@ -467,7 +465,7 @@ Options quite different performance behaviors of proof search. -.. opt:: Typeclasses Filtered Unification +.. flag:: Typeclasses Filtered Unification This option, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a @@ -481,7 +479,7 @@ Options where there is a hole in that place. -.. opt:: Typeclasses Limit Intros +.. flag:: Typeclasses Limit Intros This option (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It @@ -495,7 +493,7 @@ Options status of the product introduction rule, resulting in potentially more expensive proof-search (i.e. more useless backtracking). -.. opt:: Typeclass Resolution For Conversion +.. flag:: Typeclass Resolution For Conversion This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type @@ -503,7 +501,7 @@ Options resolution is tried before launching unification once again. -.. opt:: Typeclasses Strict Resolution +.. flag:: Typeclasses Strict Resolution Typeclass declarations introduced when this option is set have a stricter resolution behavior (the option is off by default). When @@ -513,28 +511,33 @@ Options instantiated. -.. opt:: Typeclasses Unique Solutions +.. flag:: Typeclasses Unique Solutions When a typeclass resolution is launched we ensure that it has a single solution or fail. This ensures that the resolution is canonical, but can make proof search much more expensive. -.. opt:: Typeclasses Unique Instances +.. flag:: Typeclasses Unique Instances Typeclass declarations introduced when this option is set have a more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. -.. opt:: Typeclasses Debug {? Verbosity @num} +.. flag:: Typeclasses Debug + + Controls whether typeclass resolution steps are shown during search. Setting this flag + also sets :opt:`Typeclasses Debug Verbosity` to 1. + +.. opt:: Typeclasses Debug Verbosity @num + :name: Typeclasses Debug Verbosity - These options allow to see the resolution steps of typeclasses that are - performed during search. The ``Debug`` option is synonymous to ``Debug - Verbosity 1``, and ``Debug Verbosity 2`` provides more information - (tried tactics, shelving of goals, etc…). + Determines how much information is shown for typeclass resolution steps during search. + 1 is the default level. 2 shows additional information such as tried tactics and shelving + of goals. Setting this option also sets :flag:`Typeclasses Debug`. -.. opt:: Refine Instance Mode +.. flag:: Refine Instance Mode This option allows to switch the behavior of instance declarations made through the Instance command. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e77dea457..41afe3c312 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _polymorphicuniverses: Polymorphic Universes @@ -59,7 +57,7 @@ so: Definition selfpid := pidentity (@pidentity). Of course, the two instances of :g:`pidentity` in this definition are -different. This can be seen when the :opt:`Printing Universes` option is on: +different. This can be seen when the :flag:`Printing Universes` flag is on: .. coqtop:: none @@ -79,7 +77,7 @@ levels. When printing :g:`pidentity`, we can see the universes it binds in the annotation :g:`@{Top.2}`. Additionally, when -:opt:`Printing Universes` is on we print the "universe context" of +:flag:`Printing Universes` is on we print the "universe context" of :g:`pidentity` consisting of the bound universes and the constraints they must verify (for :g:`pidentity` there are no constraints). @@ -129,14 +127,14 @@ Polymorphic, Monomorphic As shown in the examples, polymorphic definitions and inductives can be declared using the ``Polymorphic`` prefix. -.. opt:: Universe Polymorphism +.. flag:: Universe Polymorphism Once enabled, this option will implicitly prepend ``Polymorphic`` to any definition of the user. .. cmd:: Monomorphic @definition - When the :opt:`Universe Polymorphism` option is set, to make a definition + When the :flag:`Universe Polymorphism` option is set, to make a definition producing global universe constraints, one can use the ``Monomorphic`` prefix. Many other commands support the ``Polymorphic`` flag, including: @@ -169,7 +167,7 @@ declared cumulative using the :g:`Cumulative` prefix. Declares the inductive as cumulative -Alternatively, there is an option :opt:`Polymorphic Inductive +Alternatively, there is a flag :flag:`Polymorphic Inductive Cumulativity` which when set, makes all subsequent *polymorphic* inductive definitions cumulative. When set, inductive types and the like can be enforced to be non-cumulative using the :g:`NonCumulative` @@ -179,7 +177,7 @@ prefix. Declares the inductive as non-cumulative -.. opt:: Polymorphic Inductive Cumulativity +.. flag:: Polymorphic Inductive Cumulativity When this option is on, it sets all following polymorphic inductive types as cumulative (it is off by default). @@ -229,7 +227,7 @@ Cumulative inductive types, coninductive types, variants and records only make sense when they are universe polymorphic. Therefore, an error is issued whenever the user uses the :g:`Cumulative` or :g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`. +Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`. That is, this option, when set, makes all subsequent *polymorphic* inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) but has no effect on *monomorphic* inductive declarations. @@ -277,18 +275,18 @@ An example of a proof using cumulativity Cumulativity Weak Constraints ----------------------------- -.. opt:: Cumulativity Weak Constraints +.. flag:: Cumulativity Weak Constraints -This option, on by default, causes "weak" constraints to be produced -when comparing universes in an irrelevant position. Processing weak -constraints is delayed until minimization time. A weak constraint -between `u` and `v` when neither is smaller than the other and -one is flexible causes them to be unified. Otherwise the constraint is -silently discarded. + When set, which is the default, causes "weak" constraints to be produced + when comparing universes in an irrelevant position. Processing weak + constraints is delayed until minimization time. A weak constraint + between `u` and `v` when neither is smaller than the other and + one is flexible causes them to be unified. Otherwise the constraint is + silently discarded. -This heuristic is experimental and may change in future versions. -Disabling weak constraints is more predictable but may produce -arbitrary numbers of universes. + This heuristic is experimental and may change in future versions. + Disabling weak constraints is more predictable but may produce + arbitrary numbers of universes. Global and local universes @@ -354,9 +352,9 @@ This minimization process is applied only to fresh universe variables. It simply adds an equation between the variable and its lower bound if it is an atomic universe (i.e. not an algebraic max() universe). -.. opt:: Universe Minimization ToSet +.. flag:: Universe Minimization ToSet - Turning this option off (it is on by default) disallows minimization + Turning this flag off (it is on by default) disallows minimization to the sort :g:`Set` and only collapses floating universes between themselves. @@ -436,7 +434,7 @@ underscore or by omitting the annotation to a polymorphic definition. Check le@{k _}. Check le. -.. opt:: Strict Universe Declaration. +.. flag:: Strict Universe Declaration Turning this option off allows one to freely use identifiers for universes without declaring them first, with the diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index c74d8f540c..aa8537c92d 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -121,7 +121,7 @@ s}, volume = {7998}, editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, series = {LNCS }, - doi = {10.1007/978-3-642-39634-2\_5 }, + doi = {10.1007/978-3-642-39634-2_5}, year = {2013}, } @@ -136,7 +136,7 @@ s}, pages = {85--95}, month = {November}, year = {2000}, - url = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf} + url = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf} } @Article{Dyc92, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 8127d3df3f..b43d5fb6f0 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -24,6 +24,8 @@ import sys import os +from shutil import copyfile +import sphinx # Increase recursion limit for sphinx sys.setrecursionlimit(1500) @@ -36,6 +38,12 @@ sys.path.append(os.path.abspath('../../config/')) import coq_config +# -- Prolog --------------------------------------------------------------- + +# Include substitution definitions in all files +with open("refman-preamble.rst") as s: + rst_prolog = s.read() + # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. @@ -66,11 +74,39 @@ source_suffix = '.rst' # The encoding of source files. #source_encoding = 'utf-8-sig' +# Add extra cases here to support more formats + +SUPPORTED_FORMATS = ["html", "latex"] + +def readbin(fname): + try: + with open(fname, mode="rb") as f: + return f.read() + except FileNotFoundError: + return None + +def copy_formatspecific_files(app): + ext = ".{}.rst".format(app.builder.name) + for fname in sorted(os.listdir(app.srcdir)): + if fname.endswith(ext): + src = os.path.join(app.srcdir, fname) + dst = os.path.join(app.srcdir, fname[:-len(ext)] + ".rst") + logger = sphinx.util.logging.getLogger(__name__) + if readbin(src) == readbin(dst): + logger.info("Skipping {}: {} is up to date".format(src, dst)) + else: + logger.info("Copying {} to {}".format(src, dst)) + copyfile(src, dst) + +def setup(app): + app.connect('builder-inited', copy_formatspecific_files) + # The master toctree document. -master_doc = 'index' +# We create this file in `copy_master_doc` above. +master_doc = "index" # General information about the project. -project = 'Coq' +project = 'The Coq Reference Manual' copyright = '1999-2018, Inria' author = 'The Coq Development Team' @@ -104,9 +140,10 @@ exclude_patterns = [ 'Thumbs.db', '.DS_Store', 'introduction.rst', + 'refman-preamble.rst', 'README.rst', 'README.template.rst' -] +] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS] # The reST default role (used for this markup: `text`) to use for all # documents. @@ -129,6 +166,7 @@ primary_domain = 'coq' # The name of the Pygments (syntax highlighting) style to use. pygments_style = 'sphinx' highlight_language = 'text' +suppress_warnings = ["misc.highlighting_failure"] # A list of ignored prefixes for module index sorting. #modindex_common_prefix = [] @@ -257,57 +295,57 @@ smartquotes = False ########################### # Set things up for XeTeX # ########################### + latex_elements = { 'babel': '', 'fontenc': '', 'inputenc': '', 'utf8extra': '', 'cmappkg': '', - # https://www.topbug.net/blog/2015/12/10/a-collection-of-issues-about-the-latex-output-in-sphinx-and-the-solutions/ 'papersize': 'letterpaper', 'classoptions': ',openany', # No blank pages - 'polyglossia' : '\\usepackage{polyglossia}', - 'unicode-math' : '\\usepackage{unicode-math}', - 'microtype' : '\\usepackage{microtype}', - "preamble": r"\usepackage{coqnotations}" + 'polyglossia': '\\usepackage{polyglossia}', + 'sphinxsetup': 'verbatimwithframe=false', + 'preamble': r""" + \usepackage{unicode-math} + \usepackage{microtype} + + % Macro definitions + \usepackage{refman-preamble} + + % Style definitions for notations + \usepackage{coqnotations} + + % Style tweaks + \newcssclass{sigannot}{\textrm{#1:}} + + % Silence 'LaTeX Warning: Command \nobreakspace invalid in math mode' + \everymath{\def\nobreakspace{\ }} + """ } -from sphinx.builders.latex import LaTeXBuilder +latex_engine = "xelatex" ######## # done # ######## -latex_additional_files = ["_static/coqnotations.sty"] +latex_additional_files = [ + "refman-preamble.sty", + "_static/coqnotations.sty" +] -# Grouping the document tree into LaTeX files. List of tuples -# (source start file, target name, title, -# author, documentclass [howto, manual, or own class]). -# latex_documents = [ -# (master_doc, 'CoqRefMan.tex', 'Coq Documentation', -# 'The Coq Development Team', 'manual'), -#] +latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')] # The name of an image file (relative to this directory) to place at the top of # the title page. -#latex_logo = None - -# For "manual" documents, if this is true, then toplevel headings are parts, -# not chapters. -#latex_use_parts = False +# latex_logo = "../../ide/coq.png" # If true, show page references after internal links. #latex_show_pagerefs = False # If true, show URL addresses after external links. -#latex_show_urls = False - -# Documents to append as an appendix to all manuals. -#latex_appendices = [] - -# If false, no module index is generated. -#latex_domain_indices = True - +latex_show_urls = 'footnote' # -- Options for manual page output --------------------------------------- diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst index 7df6cb36c5..fd0b342ae4 100644 --- a/doc/sphinx/coq-cmdindex.rst +++ b/doc/sphinx/coq-cmdindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----------------- diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst index 100c57b085..fc55e91eee 100644 --- a/doc/sphinx/coq-exnindex.rst +++ b/doc/sphinx/coq-exnindex.rst @@ -1,5 +1,7 @@ +:orphan: + .. hack to get index in TOC ----------------------- -Errors, warnings index ----------------------- +------------------------- +Errors and warnings index +------------------------- diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst index f8046a800b..0961bea61f 100644 --- a/doc/sphinx/coq-optindex.rst +++ b/doc/sphinx/coq-optindex.rst @@ -1,5 +1,7 @@ +:orphan: + .. hack to get index in TOC ------------------ -Option index ------------------ +------------------------------- +Flags, options and tables index +------------------------------- diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst index 588104f465..31b2f7f8cb 100644 --- a/doc/sphinx/coq-tacindex.rst +++ b/doc/sphinx/coq-tacindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ------------- diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits-wrapper.html.rst new file mode 100644 index 0000000000..2d35a12dc2 --- /dev/null +++ b/doc/sphinx/credits-wrapper.html.rst @@ -0,0 +1,7 @@ +.. _credits: + +------- +Credits +------- + +.. include:: credits.rst diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst new file mode 100644 index 0000000000..9f7dd49af8 --- /dev/null +++ b/doc/sphinx/credits-wrapper.latex.rst @@ -0,0 +1,3 @@ +.. _credits: + +.. include:: credits.rst diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index be0b5d5f12..212f0a65b0 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1,12 +1,3 @@ -.. include:: preamble.rst -.. include:: replaces.rst - -.. _credits: - -------------------------------------------- -Credits -------------------------------------------- - Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal specification. It is the result of about ten years of research of the @@ -205,7 +196,7 @@ between sorts. The new version provides powerful tools for easier developments. Cristina Cornes designed an extension of the |Coq| syntax to allow -definition of terms using a powerful pattern-matching analysis in the +definition of terms using a powerful pattern matching analysis in the style of ML programs. Amokrane Saïbi wrote a mechanism to simulate inheritance between types @@ -249,7 +240,7 @@ names to Caml functions corresponding to |Coq| tactic names. Bruno Barras wrote new, more efficient reduction functions. Hugo Herbelin introduced more uniform notations in the |Coq| specification -language: the definitions by fixpoints and pattern-matching have a more +language: the definitions by fixpoints and pattern matching have a more readable syntax. Patrick Loiseleur introduced user-friendly notations for arithmetic expressions. @@ -326,14 +317,14 @@ modules and also to get closer to a certified kernel. Hugo Herbelin introduced a new structure of terms with local definitions. He introduced “qualified” names, wrote a new -pattern-matching compilation algorithm and designed a more compact +pattern matching compilation algorithm and designed a more compact algorithm for checking the logical consistency of universes. He contributed to the simplification of |Coq| internal structures and the optimisation of the system. He added basic tactics for forward reasoning and coercions in patterns. David Delahaye introduced a new language for tactics. General tactics -using pattern-matching on goals and context can directly be written from +using pattern matching on goals and context can directly be written from the |Coq| toplevel. He also provided primitives for the design of user-defined tactics in Caml. @@ -624,8 +615,8 @@ with the library of integers he developed. Beside the libraries, various improvements were contributed to provide a more comfortable end-user language and more expressive tactic language. Hugo -Herbelin and Matthieu Sozeau improved the pattern-matching compilation -algorithm (detection of impossible clauses in pattern-matching, +Herbelin and Matthieu Sozeau improved the pattern matching compilation +algorithm (detection of impossible clauses in pattern matching, automatic inference of the return type). Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau contributed various new convenient syntactic constructs and new tactics or tactic features: more inference of @@ -801,7 +792,7 @@ through :math:`\beta`-redexes that are blocked by the “match” construction (blocked commutative cuts). Relying on the added permissiveness of the guard condition, Hugo -Herbelin could extend the pattern-matching compilation algorithm so that +Herbelin could extend the pattern matching compilation algorithm so that matching over a sequence of terms involving dependencies of a term or of the indices of the type of a term in the type of other terms is systematically supported. @@ -979,7 +970,7 @@ principle than the previously added :math:`\eta`-conversion for function types, based on formulations of the Calculus of Inductive Constructions with typed equality. Primitive projections, which do not carry the parameters of the record and are rigid names (not defined as a -pattern-matching construct), make working with nested records more +pattern matching construct), make working with nested records more manageable in terms of time and space consumption. This extension and universe polymorphism were carried out partly while Matthieu Sozeau was working at the IAS in Princeton. diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index a991c7f9f8..29f792b3aa 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----- diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.html.rst index baf2e0d981..9d90857061 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.html.rst @@ -1,11 +1,16 @@ -.. include:: preamble.rst -.. include:: replaces.rst +========================== + The Coq Reference Manual +========================== + +.. _introduction: + +Introduction +------------ .. include:: introduction.rst ------------------- Table of contents ------------------- +----------------- .. toctree:: :caption: Indexes @@ -23,7 +28,7 @@ Table of contents :caption: Preamble self - credits + credits-wrapper .. toctree:: :caption: The language @@ -80,12 +85,7 @@ Table of contents zebibliography -This material (the Coq Reference Manual) may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 or later -(the latest version is presently available at -http://www.opencontent.org/openpub). Options A and B are not elected. +License +------- -.. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). +.. include:: license.rst diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst new file mode 100644 index 0000000000..0f2f7b4897 --- /dev/null +++ b/doc/sphinx/index.latex.rst @@ -0,0 +1,81 @@ +========================== + The Coq Reference Manual +========================== + +Introduction +------------ + +.. include:: introduction.rst + +Credits +------- + +.. include:: credits-wrapper.rst + +License +------- + +.. include:: license.rst + +The language +------------ + +.. toctree:: + + language/gallina-specification-language + language/gallina-extensions + language/coq-library + language/cic + language/module-system + +The proof engine +---------------- + +.. toctree:: + + proof-engine/vernacular-commands + proof-engine/proof-handling + proof-engine/tactics + proof-engine/ltac + proof-engine/detailed-tactic-examples + proof-engine/ssreflect-proof-language + +User extensions +--------------- + +.. toctree:: + + user-extensions/syntax-extensions + user-extensions/proof-schemes + +Practical tools +--------------- + +.. toctree:: + + practical-tools/coq-commands + practical-tools/utilities + practical-tools/coqide + +Addendum +-------- + +.. toctree:: + + addendum/extended-pattern-matching + addendum/implicit-coercions + addendum/canonical-structures + addendum/type-classes + addendum/omega + addendum/micromega + addendum/extraction + addendum/program + addendum/ring + addendum/nsatz + addendum/generalized-rewriting + addendum/parallel-proof-processing + addendum/miscellaneous-extensions + addendum/universe-polymorphism + +.. toctree:: + zebibliography diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index b57e4b209c..b8d2f6b6dc 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,9 +1,3 @@ -.. _introduction: - ------------------------- -Introduction ------------------------- - This document is the Reference Manual of the |Coq| proof assistant. To start using Coq, it is advised to first read a tutorial. Links to several tutorials can be found at @@ -41,6 +35,11 @@ are processed from a file. The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. + .. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). + - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index ac0f0f8ea6..381f8bb661 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _calculusofinductiveconstructions: @@ -1010,7 +1007,7 @@ the Type hierarchy. It is possible to declare the same inductive definition in the universe :math:`\Type`. The :g:`exType` inductive definition has type - :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` + :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}` has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. .. coqtop:: all @@ -1028,21 +1025,21 @@ Template polymorphism Inductive types can be made polymorphic over their arguments in :math:`\Type`. -.. opt:: Auto Template Polymorphism +.. flag:: Auto Template Polymorphism - This option, enabled by default, makes every inductive type declared - at level :math:`Type` (without annotations or hiding it behind a - definition) template polymorphic. + This option, enabled by default, makes every inductive type declared + at level :math:`Type` (without annotations or hiding it behind a + definition) template polymorphic. - This can be prevented using the ``notemplate`` attribute. + This can be prevented using the ``notemplate`` attribute. - An inductive type can be forced to be template polymorphic using the - ``template`` attribute. + An inductive type can be forced to be template polymorphic using the + ``template`` attribute. - Template polymorphism and universe polymorphism (see Chapter - :ref:`polymorphicuniverses`) are incompatible, so if the later is - enabled it will prevail over automatic template polymorphism and - cause an error when using the ``template`` attribute. + Template polymorphism and universe polymorphism (see Chapter + :ref:`polymorphicuniverses`) are incompatible, so if the later is + enabled it will prevail over automatic template polymorphism and + cause an error when using the ``template`` attribute. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. @@ -1123,7 +1120,7 @@ and otherwise in the Type hierarchy. Note that the side-condition about allowed elimination sorts in the rule **Ind-Family** is just to avoid to recompute the allowed elimination -sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). As +sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As an example, let us consider the following definition: .. example:: @@ -1247,7 +1244,7 @@ primitive recursion over the structure. But this operator is rather tedious to implement and use. We choose in this version of |Coq| to factorize the operator for primitive recursion into two more primitive operations as was first suggested by Th. -Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The +Coquand in :cite:`Coq92`. One is the definition by pattern matching. The second one is a definition by guarded fixpoints. @@ -1264,14 +1261,14 @@ The |Coq| term for this proof will be written: .. math:: - \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \endkw + \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend In this expression, if :math:`m` eventually happens to evaluate to :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the :math:`u_1 … u_{p_i}` according to the ι-reduction. -Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need +Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need to know the predicate P to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` @@ -1285,7 +1282,7 @@ using the syntax: .. math:: \Match~m~\as~x~\In~I~\_~a~\return~P~\with~ (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … - | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\endkw + | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend The :math:`\as` part can be omitted if either the result type does not depend on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m` @@ -1471,6 +1468,8 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: where .. math:: + :nowrap: + \begin{eqnarray*} P & = & \lambda~l~.~P^\prime\\ f_1 & = & t_1\\ @@ -1711,13 +1710,15 @@ for primitive recursive operators. The following reductions are now possible: .. math:: - \def\plus{\mathsf{plus}} - \def\tri{\triangleright_\iota} - \begin{eqnarray*} - \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ - & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ - & \tri & \nS~(\nS~(\nS~\nO))\\ - \end{eqnarray*} + :nowrap: + + {\def\plus{\mathsf{plus}} + \def\tri{\triangleright_\iota} + \begin{eqnarray*} + \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ + & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ + & \tri & \nS~(\nS~(\nS~\nO))\\ + \end{eqnarray*}} .. _Mutual-induction: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 9de30e2190..85474a3e98 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqlibrary: The |Coq| library @@ -620,7 +618,7 @@ Finally, it gives the definition of the usual orderings ``le``, Properties of these relations are not initially known, but may be required by the user from modules ``Le`` and ``Lt``. Finally, -``Peano`` gives some lemmas allowing pattern-matching, and a double +``Peano`` gives some lemmas allowing pattern matching, and a double induction principle. .. index:: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 0fbe7ac70b..636144e0c8 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extensionsofgallina: Extensions of |Gallina| @@ -22,7 +20,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: - .. productionlist:: `sentence` + .. productionlist:: sentence record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. @@ -82,11 +80,13 @@ To build an object of type :n:`@ident`, one should provide the constructor Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record-named-fields-grammar: .. productionlist:: - term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `term` + record_term : {| [`field_def` ; … ; `field_def`] |} + field_def : name [binders] := `record_term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have @@ -100,19 +100,25 @@ to be all present if the missing ones can be inferred or prompted for Rat_bottom_cond := O_S 1; Rat_irred_cond := one_two_irred |}. -This syntax can be disabled globally for printing by +The following settings let you control the display format for types: + +.. flag:: Printing Records -.. cmd:: Unset Printing Records + If set, use the record syntax (shown above) as the default display format. -For a given type, one can override this using either +You can override the display format for specified types by adding entries to these tables: -.. cmd:: Add Printing Record @ident +.. table:: Printing Record @qualid + :name: Printing Record -to get record syntax or + Specifies a set of qualids which are displayed as records. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. -.. cmd:: Add Printing Constructor @ident +.. table:: Printing Constructor @qualid + :name: Printing Constructor -to get constructor syntax. + Specifies a set of qualids which are displayed as constructors. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. This syntax can also be used for pattern matching. @@ -145,7 +151,7 @@ available: It can be activated for printing with -.. opt:: Printing Projections +.. flag:: Printing Projections .. example:: @@ -154,12 +160,14 @@ It can be activated for printing with Set Printing Projections. Check top half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record_projections_grammar: .. productionlist:: terms - term : term `.` ( qualid ) - : | term `.` ( qualid arg … arg ) - : | term `.` ( @`qualid` `term` … `term` ) + projection : projection `.` ( `qualid` ) + : | projection `.` ( `qualid` `arg` … `arg` ) + : | projection `.` ( @`qualid` `term` … `term` ) Syntax of Record projections @@ -219,35 +227,35 @@ the errors of inductive definitions, as described in Section Primitive Projections ~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Primitive Projections +.. flag:: Primitive Projections -Turns on the use of primitive -projections when defining subsequent records (even through the ``Inductive`` -and ``CoInductive`` commands). Primitive projections -extended the Calculus of Inductive Constructions with a new binary -term constructor `r.(p)` representing a primitive projection `p` applied -to a record object `r` (i.e., primitive projections are always applied). -Even if the record type has parameters, these do not appear at -applications of the projection, considerably reducing the sizes of -terms when manipulating parameterized records and type checking time. -On the user level, primitive projections can be used as a replacement -for the usual defined ones, although there are a few notable differences. + Turns on the use of primitive + projections when defining subsequent records (even through the ``Inductive`` + and ``CoInductive`` commands). Primitive projections + extended the Calculus of Inductive Constructions with a new binary + term constructor `r.(p)` representing a primitive projection `p` applied + to a record object `r` (i.e., primitive projections are always applied). + Even if the record type has parameters, these do not appear at + applications of the projection, considerably reducing the sizes of + terms when manipulating parameterized records and type checking time. + On the user level, primitive projections can be used as a replacement + for the usual defined ones, although there are a few notable differences. -.. opt:: Printing Primitive Projection Parameters +.. flag:: Printing Primitive Projection Parameters -This compatibility option reconstructs internally omitted parameters at -printing time (even though they are absent in the actual AST manipulated -by the kernel). + This compatibility option reconstructs internally omitted parameters at + printing time (even though they are absent in the actual AST manipulated + by the kernel). -.. opt:: Printing Primitive Projection Compatibility +.. flag:: Printing Primitive Projection Compatibility -This compatibility option (on by default) governs the -printing of pattern-matching over primitive records. + This compatibility option (on by default) governs the + printing of pattern matching over primitive records. Primitive Record Types ++++++++++++++++++++++ -When the :opt:`Primitive Projections` option is on, definitions of +When the :flag:`Primitive Projections` option is on, definitions of record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. @@ -257,9 +265,9 @@ To eliminate the (co-)inductive type, one must use its defined primitive project For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the -``Printing Primitive Projection Parameters`` flag. Further compatibility +:flag:`Printing Primitive Projection Parameters` flag. Further compatibility printing can be deactivated thanks to the ``Printing Primitive Projection -Compatibility`` option which governs the printing of pattern-matching +Compatibility`` option which governs the printing of pattern matching over primitive records. There are currently two ways to introduce primitive records types: @@ -289,7 +297,7 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the ``Printing Primitive Projection Compatibility`` +user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` to display unfolded primitive projections as matches and distinguish them from folded ones. @@ -302,7 +310,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the ``Printing Primitive Projection Parameters`` option +projection if the :flag`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -316,17 +324,17 @@ Variants and extensions of :g:`match` .. _mult-match: -Multiple and nested pattern-matching +Multiple and nested pattern matching ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The basic version of :g:`match` allows pattern-matching on simple +The basic version of :g:`match` allows pattern matching on simple patterns. As an extension, multiple nested patterns or disjunction of patterns are allowed, as in ML-like languages. The extension just acts as a macro that is expanded during parsing into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed -under its expanded form (see :opt:`Printing Matching`). +under its expanded form (see :flag:`Printing Matching`). .. seealso:: :ref:`extendedpatternmatching`. @@ -335,7 +343,7 @@ under its expanded form (see :opt:`Printing Matching`). Pattern-matching on boolean values: the if expression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For inductive types with exactly two constructors and for pattern-matching +For inductive types with exactly two constructors and for pattern matching expressions that do not depend on the arguments of the constructors, it is possible to use a ``if … then … else`` notation. For instance, the definition @@ -474,123 +482,93 @@ of :g:`match` expressions. Printing nested patterns +++++++++++++++++++++++++ -.. opt:: Printing Matching +.. flag:: Printing Matching -The Calculus of Inductive Constructions knows pattern-matching only -over simple patterns. It is however convenient to re-factorize nested -pattern-matching into a single pattern-matching over a nested -pattern. + The Calculus of Inductive Constructions knows pattern matching only + over simple patterns. It is however convenient to re-factorize nested + pattern matching into a single pattern matching over a nested + pattern. -When this option is on (default), |Coq|’s printer tries to do such -limited re-factorization. -Turning it off tells |Coq| to print only simple pattern-matching problems -in the same way as the |Coq| kernel handles them. + When this option is on (default), |Coq|’s printer tries to do such + limited re-factorization. + Turning it off tells |Coq| to print only simple pattern matching problems + in the same way as the |Coq| kernel handles them. Factorization of clauses with same right-hand side ++++++++++++++++++++++++++++++++++++++++++++++++++ -.. opt:: Printing Factorizable Match Patterns +.. flag:: Printing Factorizable Match Patterns -When several patterns share the same right-hand side, it is additionally -possible to share the clauses using disjunctive patterns. Assuming that the -printing matching mode is on, this option (on by default) tells |Coq|'s -printer to try to do this kind of factorization. + When several patterns share the same right-hand side, it is additionally + possible to share the clauses using disjunctive patterns. Assuming that the + printing matching mode is on, this option (on by default) tells |Coq|'s + printer to try to do this kind of factorization. Use of a default clause +++++++++++++++++++++++ -.. opt:: Printing Allow Default Clause +.. flag:: Printing Allow Match Default Clause -When several patterns share the same right-hand side which do not depend on the -arguments of the patterns, yet an extra factorization is possible: the -disjunction of patterns can be replaced with a `_` default clause. Assuming that -the printing matching mode and the factorization mode are on, this option (on by -default) tells |Coq|'s printer to use a default clause when relevant. + When several patterns share the same right-hand side which do not depend on the + arguments of the patterns, yet an extra factorization is possible: the + disjunction of patterns can be replaced with a `_` default clause. Assuming that + the printing matching mode and the factorization mode are on, this option (on by + default) tells |Coq|'s printer to use a default clause when relevant. Printing of wildcard patterns ++++++++++++++++++++++++++++++ -.. opt:: Printing Wildcard +.. flag:: Printing Wildcard -Some variables in a pattern may not occur in the right-hand side of -the pattern-matching clause. When this option is on (default), the -variables having no occurrences in the right-hand side of the -pattern-matching clause are just printed using the wildcard symbol -“_”. + Some variables in a pattern may not occur in the right-hand side of + the pattern matching clause. When this option is on (default), the + variables having no occurrences in the right-hand side of the + pattern matching clause are just printed using the wildcard symbol + “_”. Printing of the elimination predicate +++++++++++++++++++++++++++++++++++++ -.. opt:: Printing Synth +.. flag:: Printing Synth -In most of the cases, the type of the result of a matched term is -mechanically synthesizable. Especially, if the result type does not -depend of the matched term. When this option is on (default), -the result type is not printed when |Coq| knows that it can re- -synthesize it. + In most of the cases, the type of the result of a matched term is + mechanically synthesizable. Especially, if the result type does not + depend of the matched term. When this option is on (default), + the result type is not printed when |Coq| knows that it can re- + synthesize it. Printing matching on irrefutable patterns ++++++++++++++++++++++++++++++++++++++++++ -If an inductive type has just one constructor, pattern-matching can be +If an inductive type has just one constructor, pattern matching can be written using the first destructuring let syntax. -.. cmd:: Add Printing Let @ident - - This adds `ident` to the list of inductive types for which pattern-matching - is written using a let expression. - -.. cmd:: Remove Printing Let @ident - - This removes ident from this list. Note that removing an inductive - type from this list has an impact only for pattern-matching written - using :g:`match`. Pattern-matching explicitly written using a destructuring - :g:`let` are not impacted. - -.. cmd:: Test Printing Let for @ident - - This tells if `ident` belongs to the list. - -.. cmd:: Print Table Printing Let +.. table:: Printing Let @qualid + :name: Printing Let - This prints the list of inductive types for which pattern-matching is - written using a let expression. - - The list of inductive types for which pattern-matching is written - using a :g:`let` expression is managed synchronously. This means that it is - sensitive to the command ``Reset``. + Specifies a set of qualids for which pattern matching is displayed using a let expression. + Note that this only applies to pattern matching instances entered with :g:`match`. + It doesn't affect pattern matching explicitly entered with a destructuring + :g:`let`. + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. Printing matching on booleans +++++++++++++++++++++++++++++ -If an inductive type is isomorphic to the boolean type, pattern-matching -can be written using ``if`` … ``then`` … ``else`` …: - -.. cmd:: Add Printing If @ident - - This adds ident to the list of inductive types for which pattern-matching is - written using an if expression. - -.. cmd:: Remove Printing If @ident - - This removes ident from this list. +If an inductive type is isomorphic to the boolean type, pattern matching +can be written using ``if`` … ``then`` … ``else`` …. This table controls +which types are written this way: -.. cmd:: Test Printing If for @ident +.. table:: Printing If @qualid + :name: Printing If - This tells if ident belongs to the list. - -.. cmd:: Print Table Printing If - - This prints the list of inductive types for which pattern-matching is - written using an if expression. - -The list of inductive types for which pattern-matching is written -using an ``if`` expression is managed synchronously. This means that it is -sensitive to the command ``Reset``. + Specifies a set of qualids for which pattern matching is displayed using + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` + commands to update this set. This example emphasizes what the printing options offer. @@ -672,7 +650,7 @@ than like this: *Limitations* -|term_0| must be built as a *pure pattern-matching tree* (:g:`match … with`) +|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being @@ -700,7 +678,7 @@ terminating functions. - the definition uses pattern matching on dependent types, which ``Function`` cannot deal with yet. - - the definition is not a *pattern-matching tree* as explained above. + - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. @@ -1238,7 +1216,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. Prints the module type corresponding to :n:`@ident`. -.. opt:: Short Module Printing +.. flag:: Short Module Printing This option (off by default) disables the printing of the types of fields, leaving only their names, for the commands :cmd:`Print Module` and @@ -1513,7 +1491,7 @@ says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. +:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` option. .. seealso:: :ref:`displaying-implicit-args`. @@ -1745,65 +1723,65 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Implicit Arguments +.. flag:: Implicit Arguments -This option (off by default) allows to systematically declare implicit -the arguments detectable as such. Auto-detection of implicit arguments is -governed by options controlling whether strict and contextual implicit -arguments have to be considered or not. + This option (off by default) allows to systematically declare implicit + the arguments detectable as such. Auto-detection of implicit arguments is + governed by options controlling whether strict and contextual implicit + arguments have to be considered or not. .. _controlling-strict-implicit-args: Controlling strict implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Strict Implicit +.. flag:: Strict Implicit -When the mode for automatic declaration of implicit arguments is on, -the default is to automatically set implicit only the strict implicit -arguments plus, for historical reasons, a small subset of the non-strict -implicit arguments. To relax this constraint and to set -implicit all non strict implicit arguments by default, you can turn this -option off. + When the mode for automatic declaration of implicit arguments is on, + the default is to automatically set implicit only the strict implicit + arguments plus, for historical reasons, a small subset of the non-strict + implicit arguments. To relax this constraint and to set + implicit all non strict implicit arguments by default, you can turn this + option off. -.. opt:: Strongly Strict Implicit +.. flag:: Strongly Strict Implicit -Use this option (off by default) to capture exactly the strict implicit -arguments and no more than the strict implicit arguments. + Use this option (off by default) to capture exactly the strict implicit + arguments and no more than the strict implicit arguments. .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Contextual Implicit +.. flag:: Contextual Implicit -By default, |Coq| does not automatically set implicit the contextual -implicit arguments. You can turn this option on to tell |Coq| to also -infer contextual implicit argument. + By default, |Coq| does not automatically set implicit the contextual + implicit arguments. You can turn this option on to tell |Coq| to also + infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Reversible Pattern Implicit +.. flag:: Reversible Pattern Implicit -By default, |Coq| does not automatically set implicit the reversible-pattern -implicit arguments. You can turn this option on to tell |Coq| to also infer -reversible-pattern implicit argument. + By default, |Coq| does not automatically set implicit the reversible-pattern + implicit arguments. You can turn this option on to tell |Coq| to also infer + reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Maximal Implicit Insertion +.. flag:: Maximal Implicit Insertion -Assuming the implicit argument mode is on, this option (off by default) -declares implicit arguments to be automatically inserted when a -function is partially applied and the next argument of the function is -an implicit one. + Assuming the implicit argument mode is on, this option (off by default) + declares implicit arguments to be automatically inserted when a + function is partially applied and the next argument of the function is + an implicit one. .. _explicit-applications: @@ -1875,20 +1853,20 @@ if each of them is to be used maximally or not, use the command Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Implicit +.. flag:: Printing Implicit -By default, the basic pretty-printing rules hide the inferable implicit -arguments of an application. Turn this option on to force printing all -implicit arguments. + By default, the basic pretty-printing rules hide the inferable implicit + arguments of an application. Turn this option on to force printing all + implicit arguments. -.. opt:: Printing Implicit Defensive +.. flag:: Printing Implicit Defensive -By default, the basic pretty-printing rules display the implicit -arguments that are not detected as strict implicit arguments. This -“defensive” mode can quickly make the display cumbersome so this can -be deactivated by turning this option off. + By default, the basic pretty-printing rules display the implicit + arguments that are not detected as strict implicit arguments. This + “defensive” mode can quickly make the display cumbersome so this can + be deactivated by turning this option off. -.. seealso:: :opt:`Printing All`. +.. seealso:: :flag:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1913,14 +1891,14 @@ but succeeds in Deactivation of implicit arguments for parsing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Parsing Explicit +.. flag:: Parsing Explicit -Turning this option on (it is off by default) deactivates the use of implicit arguments. + Turning this option on (it is off by default) deactivates the use of implicit arguments. -In this case, all arguments of constants, inductive types, -constructors, etc, including the arguments declared as implicit, have -to be given as if no arguments were implicit. By symmetry, this also -affects printing. + In this case, all arguments of constants, inductive types, + constructors, etc, including the arguments declared as implicit, have + to be given as if no arguments were implicit. By symmetry, this also + affects printing. Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -2132,32 +2110,32 @@ to coercions are provided in :ref:`implicitcoercions`. Printing constructions in full ------------------------------ -.. opt:: Printing All +.. flag:: Printing All -Coercions, implicit arguments, the type of pattern-matching, but also -notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some -tactics (typically the tactics applying to occurrences of subterms are -sensitive to the implicit arguments). Turning this option on -deactivates all high-level printing features such as coercions, -implicit arguments, returned type of pattern-matching, notations and -various syntactic sugar for pattern-matching or record projections. -Otherwise said, :opt:`Printing All` includes the effects of the options -:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`, -:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate -the high-level printing features, use the command ``Unset Printing All``. + Coercions, implicit arguments, the type of pattern matching, but also + notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some + tactics (typically the tactics applying to occurrences of subterms are + sensitive to the implicit arguments). Turning this option on + deactivates all high-level printing features such as coercions, + implicit arguments, returned type of pattern matching, notations and + various syntactic sugar for pattern matching or record projections. + Otherwise said, :flag:`Printing All` includes the effects of the options + :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`, + :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate + the high-level printing features, use the command ``Unset Printing All``. .. _printing-universes: Printing universes ------------------ -.. opt:: Printing Universes +.. flag:: Printing Universes -Turn this option on to activate the display of the actual level of each -occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in -combination with :opt:`Printing All` can help to diagnose failures to unify -terms apparently identical but internally different in the Calculus of Inductive -Constructions. + Turn this option on to activate the display of the actual level of each + occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in + combination with :flag:`Printing All` can help to diagnose failures to unify + terms apparently identical but internally different in the Calculus of Inductive + Constructions. The constraints on the internal level of the occurrences of Type (see :ref:`Sorts`) can be printed using the command @@ -2219,7 +2197,7 @@ form is appending to its name, indicating how the variables of its defining context are instantiated. The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the flag ``Printing Existential Instances`` +instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an existential variable used in the same context as its context of definition is written with no instance. @@ -2241,11 +2219,11 @@ with a named-goal selector, see :ref:`goal-selectors`). Explicit displaying of existential instances for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Existential Instances +.. flag:: Printing Existential Instances -This option (off by default) activates the full display of how the -context of an existential variable is instantiated at each of the -occurrences of the existential variable. + This option (off by default) activates the full display of how the + context of an existential variable is instantiated at each of the + occurrences of the existential variable. .. _tactics-in-terms: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 075235a8e2..daf34500bf 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -216,6 +216,11 @@ numbers (see :ref:`datatypes`). Negative integers are not at the same level as :token:`num`, for this would make precedence unnatural. +.. index:: + single: Set (sort) + single: Prop + single: Type + Sorts ----- @@ -262,6 +267,8 @@ fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). +.. index:: fun ... => ... + Abstractions ------------ @@ -282,6 +289,8 @@ a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). +.. index:: forall + Products -------- @@ -320,6 +329,11 @@ The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see Section :ref:`explicit-applications`). +.. index:: + single: ... : ... (type cast) + single: ... <: ... + single: ... <<: ... + Type cast --------- @@ -329,6 +343,11 @@ the type of :token:`term` to be :token:`type`. :n:`@term <: @type` locally sets up the virtual machine for checking that :token:`term` has type :token:`type`. +:n:`@term <<: @type` uses native compilation for checking that :token:`term` +has type :token:`type`. + +.. index:: _ + Inferable subterms ------------------ @@ -336,6 +355,8 @@ Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will guess the missing piece of information. +.. index:: let ... := ... (term) + .. _let-in: Let-in definitions @@ -347,17 +368,19 @@ denotes the local binding of :token:`term` to the variable definition of functions: :n:`let @ident {+ @binder} := @term in @term’` stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. +.. index:: match ... with ... + Definition by case analysis --------------------------- Objects of inductive types can be destructurated by a case-analysis -construction called *pattern-matching* expression. A pattern-matching +construction called *pattern matching* expression. A pattern matching expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly. -This paragraph describes the basic form of pattern-matching. See +This paragraph describes the basic form of pattern matching. See Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description -of the general form. The basic form of pattern-matching is characterized +of the general form. The basic form of pattern matching is characterized by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form :n:`@qualid {* @ident}`. @@ -365,9 +388,9 @@ single :token:`pattern` and :token:`pattern` restricted to the form The expression match ":token:`term`:math:`_0` :token:`return_type` with :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|` :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a -*pattern-matching* over the term :token:`term`:math:`_0` (expected to be +*pattern matching* over the term :token:`term`:math:`_0` (expected to be of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\ -:token:`term`:math:`_n` are the *branches* of the pattern-matching +:token:`term`:math:`_n` are the *branches* of the pattern matching expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` :token:`ident` where :token:`qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. @@ -380,7 +403,7 @@ inferred from the type of the branches [2]_. In the *dependent* case, there are three subcases. In the first subcase, the type in each branch may depend on the exact value being matched in -the branch. In this case, the whole pattern-matching itself depends on +the branch. In this case, the whole pattern matching itself depends on the term being matched. This dependency of the term being matched in the return type is expressed with an “as :token:`ident`” clause where :token:`ident` is dependent in the return type. For instance, in the following example: @@ -401,7 +424,7 @@ is dependent in the return type. For instance, in the following example: the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" and ":g:`or (eq bool false true) (eq bool false false)`" while the whole -pattern-matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", the identifier :g:`b` being used to represent the dependency. .. note:: @@ -424,7 +447,7 @@ as the equality predicate (see Section :ref:`coq-equality`), the order predicate on natural numbers or the type of lists of a given length (see Section :ref:`matching-dependent`). In this configuration, the type of each branch can depend on the type dependencies specific to the -branch and the whole pattern-matching expression has a type determined +branch and the whole pattern matching expression has a type determined by the specific dependencies in the type of the term being matched. This dependency of the return type in the annotations of the inductive type is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` … @@ -453,13 +476,13 @@ For instance, in the following example: the type of the branch is :g:`eq A x x` because the third argument of :g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the -type of the whole pattern-matching expression has type :g:`eq A y x` because the +type of the whole pattern matching expression has type :g:`eq A y x` because the third argument of eq is y in the type of H. This dependency of the case analysis in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the return type. Finally, the third subcase is a combination of the first and second -subcase. In particular, it only applies to pattern-matching on terms in +subcase. In particular, it only applies to pattern matching on terms in a type with annotations. For this third subcase, both the clauses ``as`` and ``in`` are available. @@ -467,6 +490,10 @@ There are specific notations for case analysis on types with one or two constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). +.. index:: + single: fix + single: cofix + Recursive functions ------------------- @@ -916,7 +943,7 @@ Parametrized inductive types sort for the inductive definition and will produce a less convenient rule for case elimination. -.. opt:: Uniform Inductive Parameters +.. flag:: Uniform Inductive Parameters When this option is set (it is off by default), inductive definitions are abstracted over their parameters @@ -953,7 +980,7 @@ Variants The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except that it disallows recursive definition of types (for instance, lists cannot be defined using :cmd:`Variant`). No induction scheme is generated for - this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on. + this variant, unless option :flag:`Nonrecursive Elimination Schemes` is on. .. exn:: The @num th argument of @ident must be @ident in @type. :undocumented: @@ -1099,7 +1126,7 @@ constructions. .. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term - This command allows defining functions by pattern-matching over inductive + This command allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :token:`ident` a recursive function with arguments specified by the :token:`binders` such that :token:`ident` applied to arguments @@ -1302,7 +1329,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. - To activate it, turn option :opt:`Nested Proofs Allowed` on. + To activate it, turn option :flag:`Nested Proofs Allowed` on. .. cmdv:: Lemma @ident {? @binders } : @type Remark @ident {? @binders } : @type @@ -1376,7 +1403,7 @@ using the keyword :cmd:`Qed`. .. note:: #. Several statements can be simultaneously asserted provided option - :opt:`Nested Proofs Allowed` was turned on. + :flag:`Nested Proofs Allowed` was turned on. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst index e6a6736654..15fee91245 100644 --- a/doc/sphinx/language/module-system.rst +++ b/doc/sphinx/language/module-system.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _themodulesystem: The Module System diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst new file mode 100644 index 0000000000..232b04211c --- /dev/null +++ b/doc/sphinx/license.rst @@ -0,0 +1,4 @@ +This material (the Coq Reference Manual) may be distributed only subject to the +terms and conditions set forth in the Open Publication License, v1.0 or later +(the latest version is presently available at +http://www.opencontent.org/openpub). Options A and B are not elected. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9498f37c7e..343ca9ed7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqcommands: The |Coq| commands diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index bc6a074a27..9455228e7d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment @@ -263,7 +261,7 @@ for the ∀ symbol. A list of symbol codes is available at An alternative method which does not require to know the hexadecimal code of the character is to use an Input Method Editor. On POSIX systems (Linux distributions, BSD variants and MacOS X), you can -use `uim` version 1.6 or later which provides a :math:`\LaTeX`-style input +use `uim` version 1.6 or later which provides a LaTeX-style input method. To configure uim, execute uim-pref-gtk as your regular user. In the diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index b9a4d2a7bd..5d300c3d6d 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _utilities: --------------------- diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst deleted file mode 100644 index 395f558a85..0000000000 --- a/doc/sphinx/preamble.rst +++ /dev/null @@ -1,92 +0,0 @@ -.. preamble:: - - \[ - \newcommand{\alors}{\textsf{then}} - \newcommand{\alter}{\textsf{alter}} - \newcommand{\as}{\kw{as}} - \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} - \newcommand{\bool}{\textsf{bool}} - \newcommand{\case}{\kw{case}} - \newcommand{\conc}{\textsf{conc}} - \newcommand{\cons}{\textsf{cons}} - \newcommand{\consf}{\textsf{consf}} - \newcommand{\conshl}{\textsf{cons\_hl}} - \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} - \newcommand{\emptyf}{\textsf{emptyf}} - \newcommand{\End}{\kw{End}} - \newcommand{\endkw}{\kw{end}} - \newcommand{\EqSt}{\textsf{EqSt}} - \newcommand{\even}{\textsf{even}} - \newcommand{\evenO}{\textsf{even_O}} - \newcommand{\evenS}{\textsf{even_S}} - \newcommand{\false}{\textsf{false}} - \newcommand{\filter}{\textsf{filter}} - \newcommand{\Fix}{\kw{Fix}} - \newcommand{\fix}{\kw{fix}} - \newcommand{\for}{\textsf{for}} - \newcommand{\forest}{\textsf{forest}} - \newcommand{\from}{\textsf{from}} - \newcommand{\Functor}{\kw{Functor}} - \newcommand{\haslength}{\textsf{has\_length}} - \newcommand{\hd}{\textsf{hd}} - \newcommand{\ident}{\textsf{ident}} - \newcommand{\In}{\kw{in}} - \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} - \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} - \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} - \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} - \newcommand{\injective}{\kw{injective}} - \newcommand{\kw}[1]{\textsf{#1}} - \newcommand{\lb}{\lambda} - \newcommand{\length}{\textsf{length}} - \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} - \newcommand{\List}{\textsf{list}} - \newcommand{\lra}{\longrightarrow} - \newcommand{\Match}{\kw{match}} - \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} - \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} - \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} - \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} - \newcommand{\mto}{.\;} - \newcommand{\Nat}{\mathbb{N}} - \newcommand{\nat}{\textsf{nat}} - \newcommand{\Nil}{\textsf{nil}} - \newcommand{\nilhl}{\textsf{nil\_hl}} - \newcommand{\nO}{\textsf{O}} - \newcommand{\node}{\textsf{node}} - \newcommand{\nS}{\textsf{S}} - \newcommand{\odd}{\textsf{odd}} - \newcommand{\oddS}{\textsf{odd_S}} - \newcommand{\ovl}[1]{\overline{#1}} - \newcommand{\Pair}{\textsf{pair}} - \newcommand{\Prod}{\textsf{prod}} - \newcommand{\Prop}{\textsf{Prop}} - \newcommand{\return}{\kw{return}} - \newcommand{\Set}{\textsf{Set}} - \newcommand{\si}{\textsf{if}} - \newcommand{\sinon}{\textsf{else}} - \newcommand{\Sort}{\cal S} - \newcommand{\Str}{\textsf{Stream}} - \newcommand{\Struct}{\kw{Struct}} - \newcommand{\subst}[3]{#1\{#2/#3\}} - \newcommand{\tl}{\textsf{tl}} - \newcommand{\tree}{\textsf{tree}} - \newcommand{\true}{\textsf{true}} - \newcommand{\Type}{\textsf{Type}} - \newcommand{\unfold}{\textsf{unfold}} - \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} - \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} - \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} - \newcommand{\WFE}[1]{\WF{E}{#1}} - \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} - \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} - \newcommand{\with}{\kw{with}} - \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} - \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} - \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} - \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} - \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} - \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} - \newcommand{\zeroone}[1]{[{#1}]} - \newcommand{\zeros}{\textsf{zeros}} - \] diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 70d46e034a..edd83b7cee 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _ltac: The tactic language @@ -27,14 +24,14 @@ represent respectively the natural and integer numbers, the authorized identificators and qualified names, Coq terms and patterns and all the atomic tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is the same as that of terms, but it is extended with pattern matching -metavariables. In :token:`cpattern`, a pattern-matching metavariable is +metavariables. In :token:`cpattern`, a pattern matching metavariable is represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The notation :g:`_` can also be used to denote metavariable whose instance is irrelevant. In the notation :g:`?id`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not -interested in what will be matched. On the right hand side of pattern-matching +interested in what will be matched. On the right hand side of pattern matching clauses, the named metavariables are used without the question mark prefix. There -is also a special notation for second-order pattern-matching problems: in an +is also a special notation for second-order pattern matching problems: in an applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any complex expression with (possible) dependencies in the variables :g:`id1 … idn` and returns a functional term of the form :g:`fun id1 … idn => term`. @@ -717,6 +714,7 @@ Local definitions Local definitions can be done as follows: .. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr + :name: let ... := ... each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for @@ -835,7 +833,7 @@ We can carry out pattern matching on terms with: matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to right (with respect to the raw printing obtained by setting option - :opt:`Printing All`). + :flag:`Printing All`). .. example:: @@ -1189,6 +1187,7 @@ Info trace not printed. .. opt:: Info Level @num + :name: Info Level This option is an alternative to the :cmd:`Info` command. @@ -1199,7 +1198,7 @@ Info trace Interactive debugger ~~~~~~~~~~~~~~~~~~~~ -.. opt:: Ltac Debug +.. flag:: Ltac Debug This option governs the step-by-step debugger that comes with the |Ltac| interpreter @@ -1227,7 +1226,7 @@ following: A non-interactive mode for the debugger is available via the option: -.. opt:: Ltac Batch Debug +.. flag:: Ltac Batch Debug This option has the effect of presenting a newline at every prompt, when the debugger is on. The debug log thus created, which does not require @@ -1248,7 +1247,7 @@ indicates the time spent in a tactic depending on its calling context. Thus it allows to locate the part of a tactic definition that contains the performance issue. -.. opt:: Ltac Profiling +.. flag:: Ltac Profiling This option enables and disables the profiler. @@ -1334,7 +1333,7 @@ performance issue. benchmarking purposes. You can also pass the ``-profile-ltac`` command line option to ``coqc``, which -turns the :opt:`Ltac Profiling` option on at the beginning of each document, +turns the :flag:`Ltac Profiling` option on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. .. warning:: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b1e769c571..4b1b7719c5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _proofhandling: ------------------- @@ -113,7 +112,7 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). - .. seealso:: :opt:`Nested Proofs Allowed` + .. seealso:: :flag:`Nested Proofs Allowed` .. cmdv:: Abort All @@ -201,13 +200,14 @@ The following options modify the behavior of ``Proof using``. .. opt:: Default Proof Using "@expression" + :name: Default Proof Using Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. -.. opt:: Suggest Proof Using +.. flag:: Suggest Proof Using When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not provide one. @@ -442,13 +442,19 @@ The following example script illustrates all these features: You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is mandatory here. -.. exn:: No such goal. Try unfocusing with %{. +.. FIXME: the :noindex: below works around a Sphinx issue. + (https://github.com/sphinx-doc/sphinx/issues/4979) + It should be removed once that issue is fixed. + +.. exn:: No such goal. Try unfocusing with %}. + :noindex: You just finished a goal focused by ``{``, you must unfocus it with ``}``. Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) + :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -581,6 +587,7 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num + :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable @@ -589,7 +596,7 @@ Controlling the effect of proof editing commands available hypotheses. -.. opt:: Automatic Introduction +.. flag:: Automatic Introduction This option controls the way binders are handled in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the @@ -601,7 +608,7 @@ Controlling the effect of proof editing commands has to be used to move the assumptions to the local context. -.. opt:: Nested Proofs Allowed +.. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested proofs: a new assertion command can be inserted before the current proof is diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8656e5eb3e..52609546d5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thessreflectprooflanguage: ------------------------------ @@ -104,8 +102,8 @@ this corresponds to working in the following context: Unset Printing Implicit Defensive. .. seealso:: - :opt:`Implicit Arguments`, :opt:`Strict Implicit`, - :opt:`Printing Implicit Defensive` + :flag:`Implicit Arguments`, :flag:`Strict Implicit`, + :flag:`Printing Implicit Defensive` .. _compatibility_issues_ssr: @@ -2703,7 +2701,7 @@ typeclass inference. No inference for ``t``. Unresolved instances are quantified in the (inferred) type of ``t`` and abstracted in ``t``. -.. opt:: SsrHave NoTCResolution +.. flag:: SsrHave NoTCResolution This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). @@ -3867,7 +3865,7 @@ duplication of function arguments. These copies usually end up in types hidden by the implicit arguments machinery or by user-defined notations. In these situations computing the right occurrence numbers is very tedious because they must be counted on the goal as printed -after setting the Printing All flag. Moreover the resulting script is +after setting the :flag:`Printing All` flag. Moreover the resulting script is not really informative for the reader, since it refers to occurrence numbers he cannot easily see. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fb121c82ec..f99c539251 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _tactics: Tactics @@ -51,7 +48,8 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. opt:: Default Goal Selector @toplevel_selector +.. opt:: Default Goal Selector "@toplevel_selector" + :name: Default Goal Selector This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the @@ -127,7 +125,7 @@ that occurrences have to be selected in the hypotheses named :token:`ident`. If no numbers are given for hypothesis :token:`ident`, then all the occurrences of :token:`term` in the hypothesis are selected. If numbers are given, they refer to occurrences of :token:`term` when the term is printed -using option :opt:`Printing All`, counting from left to right. In particular, +using option :flag:`Printing All`, counting from left to right. In particular, occurrences of :token:`term` in implicit arguments (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. @@ -451,7 +449,7 @@ Applying theorems ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: -.. opt:: Universal Lemma Under Conjunction +.. flag:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). @@ -476,7 +474,7 @@ Applying theorems :token:`ident`. Tuples are decomposed in a width-first left-to-right order (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2` - into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern-matching + into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching with dependent types. .. exn:: Statement without assumptions. @@ -855,7 +853,7 @@ Managing the local context so that all the arguments of the i-th constructors of the corresponding inductive type are introduced can be controlled with the following option: - .. opt:: Bracketing Last Introduction Pattern + .. flag:: Bracketing Last Introduction Pattern Force completion, if needed, when the last introduction pattern is a disjunctive or conjunctive pattern (on by default). @@ -1298,7 +1296,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :opt:`Printing All`). + expression printed using option :flag:`Printing All`). .. tacv:: generalize @term as @ident @@ -2041,14 +2039,14 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. - .. opt:: Structural Injection + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving :n:`injection @term as` (with an empty list of names). This option is off by default. - .. opt:: Keep Proof Equalities + .. flag:: Keep Proof Equalities By default, :tacn:`injection` only creates new equalities between :n:`@terms` whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special @@ -2080,7 +2078,7 @@ and an explanation of the underlying technique. being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort :g:`Prop`). This behavior can be turned off by using the option - :opt`Keep Proof Equalities`. + :flag`Keep Proof Equalities`. .. tacv:: inversion @num @@ -2590,7 +2588,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. - .. opt:: Regular Subst Tactic + .. flag:: Regular Subst Tactic This option controls the behavior of :tacn:`subst`. When it is activated (it is by default), :tacn:`subst` also deals with the following corner cases: @@ -2725,7 +2723,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :math:`\beta` (reduction of functional application), :math:`\delta` (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), :math:`\iota` (reduction of - pattern-matching over a constructed term, and unfolding of :g:`fix` and + pattern matching over a constructed term, and unfolding of :g:`fix` and :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` @@ -2808,12 +2806,13 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. - .. opt:: NativeCompute Profiling + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes it possible to profile ``native_compute`` evaluations. - .. opt:: NativeCompute Profile Filename + .. opt:: NativeCompute Profile Filename @string + :name: NativeCompute Profile Filename This option specifies the profile output; the default is ``native_compute_profile.data``. The actual filename used @@ -2824,7 +2823,7 @@ the conversion in hypotheses :n:`{+ @ident}`. on the profile file to see the results. Consult the ``perf`` documentation for more details. -.. opt:: Debug Cbv +.. flag:: Debug Cbv This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it @@ -2991,7 +2990,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). -.. opt:: Debug RAKAM +.. flag:: Debug RAKAM This option makes :tacn:`cbn` print various debugging information. ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. @@ -3198,10 +3197,11 @@ hints of the database named core. The following options enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics: -.. opt:: Info Auto -.. opt:: Debug Auto -.. opt:: Info Trivial -.. opt:: Debug Trivial +.. flag:: Info Auto + Debug Auto + Info Trivial + Debug Trivial + :undocumented: .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` @@ -3231,8 +3231,9 @@ Note that ``ex_intro`` should be declared as a hint. :tacn:`eauto` also obeys the following options: -.. opt:: Info Eauto -.. opt:: Debug Eauto +.. flag:: Info Eauto + Debug Eauto + :undocumented: .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` @@ -3566,7 +3567,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: - One can use an ``Extern`` hint with no pattern to do pattern-matching on + One can use an ``Extern`` hint with no pattern to do pattern matching on hypotheses using ``match goal`` with inside the tactic. @@ -3862,7 +3863,7 @@ some incompatibilities. ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive types with one constructor and no indices, i.e. record-style connectives. -.. opt:: Intuition Negation Unfolding +.. flag:: Intuition Negation Unfolding Controls whether :tacn:`intuition` unfolds inner negations which do not need to be unfolded. This option is on by default. @@ -3891,6 +3892,7 @@ usual logical connectives but instead may reason about any first-order class inductive definition. .. opt:: Firstorder Solver @tactic + :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto with *`, it can be reset locally or globally using this option. @@ -3919,6 +3921,7 @@ inductive definition. This combines the effects of the different variants of :tacn:`firstorder`. .. opt:: Firstorder Depth @num + :name: Firstorder Depth This option controls the proof-search depth bound. @@ -3981,7 +3984,7 @@ match against it. additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the :tacn:`congruence with` variant described above. -.. opt:: Congruence Verbose +.. flag:: Congruence Verbose This option makes :tacn:`congruence` print debug information. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 584193b9c6..837d3f10a2 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _vernacularcommands: Vernacular commands @@ -78,145 +75,106 @@ Displaying Flags, Options and Tables ----------------------------- -|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options -(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The -names of flags, options and tables are made of non-empty sequences of -identifiers (conventionally with capital initial letter). The general commands -handling flags, options and tables are given below. - -.. TODO : flag is not a syntax entry - -.. cmd:: Set @flag - - This command switches :n:`@flag` on. The original state of :n:`@flag` - is restored when the current module ends. - - .. cmdv:: Local Set @flag - - This command switches :n:`@flag` on. The original state - of :n:`@flag` is restored when the current *section* ends. - - .. cmdv:: Global Set @flag - - This command switches :n:`@flag` on. The original state - of :n:`@flag` is *not* restored at the end of the module. Additionally, if - set in a file, :n:`@flag` is switched on when the file is `Require`-d. +Coq has many settings to control its behavior. Setting types include flags, options +and tables: - .. cmdv:: Export Set @flag +* A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`. +* An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A :production:`table` contains a set of strings or qualids. +* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`. - This command switches :n:`@flag` on. The original state - of :n:`@flag` is restored at the end of the current module, but :n:`@flag` - is switched on when this module is imported. +.. FIXME Convert `Extraction Language OCaml` to an option. +Flags, options and tables are identified by a series of identifiers, each with an initial +capital letter. -.. cmd:: Unset @flag +.. cmd:: {? Local | Global | Export } Set @flag + :name: Set - This command switches :n:`@flag` off. The original state of - :n:`@flag` is restored when the current module ends. + Sets :token:`flag` on. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - .. cmdv:: Local Unset @flag - - This command switches :n:`@flag` off. The original - state of :n:`@flag` is restored when the current *section* ends. - - .. cmdv:: Global Unset @flag - - This command switches :n:`@flag` off. The original - state of :n:`@flag` is *not* restored at the end of the module. Additionally, - if set in a file, :n:`@flag` is switched off when the file is `Require`-d. - - .. cmdv:: Export Unset @flag - - This command switches :n:`@flag` off. The original state - of :n:`@flag` is restored at the end of the current module, but :n:`@flag` - is switched off when this module is imported. +.. cmd:: {? Local | Global | Export } Unset @flag + :name: Unset + Sets :token:`flag` off. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. .. cmd:: Test @flag - This command prints whether :n:`@flag` is on or off. - - -.. cmd:: Set @option @value + Prints the current value of :token:`flag`. - This command sets :n:`@option` to :n:`@value`. The original value of ` option` is - restored when the current module ends. - .. TODO : option and value are not syntax entries +.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) + :name: Set @option - .. cmdv:: Local Set @option @value + Sets :token:`option` to the specified value. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - This command sets :n:`@option` to :n:`@value`. The - original value of :n:`@option` is restored at the end of the module. +.. cmd:: {? Local | Global | Export } Unset @option + :name: Unset @option - .. cmdv:: Global Set @option @value + Sets :token:`option` to its default value. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - This command sets :n:`@option` to :n:`@value`. The - original value of :n:`@option` is *not* restored at the end of the module. - Additionally, if set in a file, :n:`@option` is set to value when the file - is `Require`-d. - - .. cmdv:: Export Set @option - - This command set :n:`@option` to :n:`@value`. The original state - of :n:`@option` is restored at the end of the current module, but :n:`@option` - is set to :n:`@value` when this module is imported. - - -.. cmd:: Unset @option - - This command turns off :n:`@option`. - - .. cmdv:: Local Unset @option +.. cmd:: Test @option - This command turns off :n:`@option`. The original state of :n:`@option` - is restored when the current *section* ends. + Prints the current value of :token:`option`. - .. cmdv:: Global Unset @option +.. cmd:: Print Options - This command turns off :n:`@option`. The original state of :n:`@option` - is *not* restored at the end of the module. Additionally, if unset in a file, - :n:`@option` is reset to its default value when the file is `Require`-d. + Prints the current value of all flags and options, and the names of all tables. - .. cmdv:: Export Unset @option - This command turns off :n:`@option`. The original state of :n:`@option` - is restored at the end of the current module, but :n:`@option` is set to - its default value when this module is imported. +.. cmd:: Add @table ( @string | @qualid ) + :name: Add @table + Adds the specified value to :token:`table`. -.. cmd:: Test @option +.. cmd:: Remove @table ( @string | @qualid ) + :name: Remove @table - This command prints the current value of :n:`@option`. + Removes the specified value from :token:`table`. +.. cmd:: Test @table for ( @string | @qualid ) + :name: Test @table for -.. TODO : table is not a syntax entry + Reports whether :token:`table` contains the specified value. -.. cmd:: Add @table @value - :name: Add `table` `value` +.. cmd:: Print Table @table + :name: Print Table @table -.. cmd:: Remove @table @value - :name: Remove `table` `value` + Prints the values in :token:`table`. -.. cmd:: Test @table @value - :name: Test `table` `value` +.. cmd:: Test @table -.. cmd:: Test @table for @value - :name: Test `table` for `value` + A synonym for :cmd:`Print Table @table`. -.. cmd:: Print Table @table +.. cmd:: Print Tables -These are general commands for tables. + A synonym for :cmd:`Print Options`. +.. _set_unset_scope_qualifiers: -.. cmd:: Print Options +Scope qualifiers for :cmd:`Set` and :cmd:`Unset` +````````````````````````````````````````````````` - This command lists all available flags, options and tables. +:n:`{? Local | Global | Export }` - .. cmdv:: Print Tables +Flag and option settings can be global in scope or local to nested scopes created by +:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - This is a synonymous of :cmd:`Print Options`. +* no qualifier: the original setting is *not* restored at the end of the current module or section. +* **Local**: the setting is applied within the current scope. The original value of the option + or flag is restored at the end of the current module or section. +* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current + module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing + the file sets the option. +* **Export**: similar to **Local**, the original value of the option or flag is restored at the + end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing + the file sets the option. +Newly opened scopes inherit the current settings. .. _requests-to-the-environment: @@ -502,19 +460,16 @@ Requests to the environment .. note:: - .. cmd:: Add Search Blacklist @string + .. table:: Search Blacklist @string - For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite`` - queries, it is possible to globally filter the search results using this - command. A lemma whose fully-qualified name - contains any of the declared strings will be removed from the - search results. The default blacklisted substrings are ``_subproof`` and + Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, + :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + fully-qualified name contains any of the strings will be excluded from the + search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and ``Private_``. - .. cmd:: Remove Search Blacklist @string - - This command allows expunging this blacklist. - + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of + blacklisted strings. .. cmd:: Locate @qualid @@ -979,6 +934,7 @@ Quitting and debugging displayed. .. opt:: Default Timeout @num + :name: Default Timeout This option controls a default timeout for subsequent commands, as if they were passed to a :cmd:`Timeout` command. Commands already starting by a @@ -1003,11 +959,12 @@ Quitting and debugging Controlling display ----------------------- -.. opt:: Silent +.. flag:: Silent This option controls the normal displaying. .. opt:: Warnings "{+, {? %( - %| + %) } @ident }" + :name: Warnings This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -1017,7 +974,7 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. -.. opt:: Search Output Name Only +.. flag:: Search Output Name Only This option restricts the output of search commands to identifier names; turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, @@ -1038,7 +995,7 @@ Controlling display printing. Beyond this depth, display of subterms is replaced by dots. At the time of writing this documentation, the default value is 50. -.. opt:: Printing Compact Contexts +.. flag:: Printing Compact Contexts This option controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting @@ -1046,13 +1003,13 @@ Controlling display does not exceed the printing width (see :opt:`Printing Width`). At the time of writing this documentation, it is off by default. -.. opt:: Printing Unfocused +.. flag:: Printing Unfocused This option controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets (see :ref:`bullets` or :ref:`curly braces <curly-braces>`). It is off by default. -.. opt:: Printing Dependent Evars Line +.. flag:: Printing Dependent Evars Line This option controls the printing of the “(dependent evars: …)” line when ``-emacs`` is passed. diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/refman-preamble.rst index 28a04f90ce..c662028773 100644 --- a/doc/sphinx/replaces.rst +++ b/doc/sphinx/refman-preamble.rst @@ -1,4 +1,13 @@ -.. some handy replacements for common items +.. This file is automatically prepended to all other files using the ``rst_prolog`` option. + +.. only:: html + + .. This is included once per page in the HTML build, and a single time (in the + document's preamble) in the LaTeX one. + + .. preamble:: /refman-preamble.sty + +.. Some handy replacements for common items .. role:: smallcaps @@ -21,7 +30,7 @@ .. |class_2| replace:: `class`\ :math:`_{2}` .. |Coq| replace:: :smallcaps:`Coq` .. |CoqIDE| replace:: :smallcaps:`CoqIDE` -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` .. |ident_0| replace:: `ident`\ :math:`_{0}` .. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty new file mode 100644 index 0000000000..b4fc608e47 --- /dev/null +++ b/doc/sphinx/refman-preamble.sty @@ -0,0 +1,88 @@ +\newcommand{\alors}{\textsf{then}} +\newcommand{\alter}{\textsf{alter}} +\newcommand{\as}{\kw{as}} +\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} +\newcommand{\bool}{\textsf{bool}} +\newcommand{\case}{\kw{case}} +\newcommand{\conc}{\textsf{conc}} +\newcommand{\cons}{\textsf{cons}} +\newcommand{\consf}{\textsf{consf}} +\newcommand{\conshl}{\textsf{cons\_hl}} +\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} +\newcommand{\emptyf}{\textsf{emptyf}} +\newcommand{\End}{\kw{End}} +\newcommand{\kwend}{\kw{end}} +\newcommand{\EqSt}{\textsf{EqSt}} +\newcommand{\even}{\textsf{even}} +\newcommand{\evenO}{\textsf{even}_\textsf{O}} +\newcommand{\evenS}{\textsf{even}_\textsf{S}} +\newcommand{\false}{\textsf{false}} +\newcommand{\filter}{\textsf{filter}} +\newcommand{\Fix}{\kw{Fix}} +\newcommand{\fix}{\kw{fix}} +\newcommand{\for}{\textsf{for}} +\newcommand{\forest}{\textsf{forest}} +\newcommand{\from}{\textsf{from}} +\newcommand{\Functor}{\kw{Functor}} +\newcommand{\haslength}{\textsf{has\_length}} +\newcommand{\hd}{\textsf{hd}} +\newcommand{\ident}{\textsf{ident}} +\newcommand{\In}{\kw{in}} +\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} +\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} +\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} +\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} +\newcommand{\injective}{\kw{injective}} +\newcommand{\kw}[1]{\textsf{#1}} +\newcommand{\lb}{\lambda} +\newcommand{\length}{\textsf{length}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} +\newcommand{\List}{\textsf{list}} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Match}{\kw{match}} +\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} +\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} +\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} +\newcommand{\mto}{.\;} +\newcommand{\Nat}{\mathbb{N}} +\newcommand{\nat}{\textsf{nat}} +\newcommand{\Nil}{\textsf{nil}} +\newcommand{\nilhl}{\textsf{nil\_hl}} +\newcommand{\nO}{\textsf{O}} +\newcommand{\node}{\textsf{node}} +\newcommand{\nS}{\textsf{S}} +\newcommand{\odd}{\textsf{odd}} +\newcommand{\oddS}{\textsf{odd}_\textsf{S}} +\newcommand{\ovl}[1]{\overline{#1}} +\newcommand{\Pair}{\textsf{pair}} +\newcommand{\Prod}{\textsf{prod}} +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\return}{\kw{return}} +\newcommand{\Set}{\textsf{Set}} +\newcommand{\si}{\textsf{if}} +\newcommand{\sinon}{\textsf{else}} +\newcommand{\Sort}{\cal S} +\newcommand{\Str}{\textsf{Stream}} +\newcommand{\Struct}{\kw{Struct}} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\tl}{\textsf{tl}} +\newcommand{\tree}{\textsf{tree}} +\newcommand{\true}{\textsf{true}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\unfold}{\textsf{unfold}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} +\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} +\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} +\newcommand{\with}{\kw{with}} +\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\zeroone}[1]{[{#1}]} +\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index ab1edc0b27..59cad3bea2 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -103,26 +103,23 @@ induction for objects in type `identᵢ`. Automatic declaration of schemes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Elimination Schemes +.. flag:: Elimination Schemes - It is possible to deactivate the automatic declaration of the - induction principles when defining a new inductive type with the - ``Unset Elimination Schemes`` command. It may be reactivated at any time with - ``Set Elimination Schemes``. + Enables automatic declaration of induction principles when defining a new + inductive type. Defaults to on. -.. opt:: Nonrecursive Elimination Schemes +.. flag:: Nonrecursive Elimination Schemes - This option controls whether types declared with the keywords :cmd:`Variant` and - :cmd:`Record` get an automatic declaration of the induction principles. + Enables automatic declaration of induction principles for types declared with the :cmd:`Variant` and + :cmd:`Record` commands. Defaults to off. -.. opt:: Case Analysis Schemes +.. flag:: Case Analysis Schemes This flag governs the generation of case analysis lemmas for inductive types, - i.e. corresponding to the pattern-matching term alone and without fixpoint. + i.e. corresponding to the pattern matching term alone and without fixpoint. -.. opt:: Boolean Equality Schemes - -.. opt:: Decidable Equality Schemes +.. flag:: Boolean Equality Schemes + Decidable Equality Schemes These flags control the automatic declaration of those Boolean equalities (see the second variant of ``Scheme``). @@ -132,7 +129,7 @@ Automatic declaration of schemes You have to be careful with this option since Coq may now reject well-defined inductive types because it cannot compute a Boolean equality for them. -.. opt:: Rewriting Schemes +.. flag:: Rewriting Schemes This flag governs generation of equality-related schemes such as congruence. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4c0e85bdd4..705d67e6c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _syntaxextensionsandinterpretationscopes: Syntax extensions and interpretation scopes @@ -378,17 +376,14 @@ for records. Here are examples: Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Notations - - To deactivate the printing of all notations, use the command - ``Unset Printing Notations``. To reactivate it, use the command - ``Set Printing Notations``. +.. flag:: Printing Notations - The default is to use notations for printing terms wherever possible. + Controls whether to use notations for printing terms wherever possible. + Default is on. .. seealso:: - :opt:`Printing All` + :flag:`Printing All` To disable other elements in addition to notations. .. _locating-notations: diff --git a/doc/sphinx/zebibliography.html.rst b/doc/sphinx/zebibliography.html.rst new file mode 100644 index 0000000000..756edd5482 --- /dev/null +++ b/doc/sphinx/zebibliography.html.rst @@ -0,0 +1,17 @@ +.. There are multiple issues with sphinxcontrib-bibtex that we have to work around: + - The list of cited entries is computed right after encountering + `.. bibliography`, so the file containing that command has to come last + alphabetically: + https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#unresolved-citations-across-documents + - `.. bibliography::` puts the bibliography on its own page with its own + title in LaTeX, but includes it inline without a title in HTML: + https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends + +.. _bibliography: + +============== + Bibliography +============== + +.. bibliography:: biblio.bib + :cited: diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.latex.rst index 0000caa301..2c0396f1c9 100644 --- a/doc/sphinx/zebibliography.rst +++ b/doc/sphinx/zebibliography.latex.rst @@ -1,8 +1,6 @@ -.. _bibliography: +.. See zebibliography.html.rst for details -============ -Bibliography -============ +.. _bibliography: .. bibliography:: biblio.bib :cited: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 40554c3ca3..7992c10abb 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -34,7 +34,7 @@ from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs -from sphinx.ext.mathbase import MathDirective, displaymath +from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors @@ -58,6 +58,15 @@ def make_target(objtype, targetid): """Create a target to an object of type objtype and id targetid""" return "coq:{}.{}".format(objtype, targetid) +def make_math_node(latex, docname, nowrap): + node = mathbase.displaymath() + node['latex'] = latex + node['label'] = None # Otherwise equations are numbered + node['nowrap'] = nowrap + node['docname'] = docname + node['number'] = None + return node + class CoqObject(ObjectDescription): """A generic Coq object for Sphinx; all Coq objects are subclasses of this. @@ -101,7 +110,9 @@ class CoqObject(ObjectDescription): # Explicit object naming 'name': directives.unchanged, # Silence warnings produced by report_undocumented_coq_objects - 'undocumented': directives.flag + 'undocumented': directives.flag, + # noindex omits this object from its index + 'noindex': directives.flag } def subdomain_data(self): @@ -138,6 +149,13 @@ class CoqObject(ObjectDescription): msg = MSG.format(name, self.env.doc2path(objects[name][0])) self.state_machine.reporter.warning(msg, line=self.lineno) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -165,13 +183,16 @@ class CoqObject(ObjectDescription): """Add `name` (pointing to `target`) to the main index.""" assert isinstance(name, str) if not name.startswith("_"): - index_text = name + # remove trailing . , found in commands, but not ... (ellipsis) + trim = name.endswith(".") and not name.endswith("...") + index_text = name[:-1] if trim else name if self.index_suffix: index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) def add_target_and_index(self, name, _, signode): - """Attach a link target to `signode` and an index entry for `name`.""" + """Attach a link target to `signode` and an index entry for `name`. + This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified.""" if name: target = self._add_target(signode, name) self._add_index_entry(name, target) @@ -316,11 +337,10 @@ class OptionObject(NotationObject): Example:: - .. opt:: Nonrecursive Elimination Schemes + .. opt:: Hyps Limit @num - This option controls whether types declared with the keywords - :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the - induction principles. + This option controls the maximum number of hypotheses displayed in goals after + the application of a tactic. """ subdomain = "opt" index_suffix = "(opt)" @@ -329,6 +349,42 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) + +class FlagObject(NotationObject): + """A Coq flag, i.e. a boolean Option. + + Example:: + + .. flag:: Nonrecursive Elimination Schemes + + This flag controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + """ + subdomain = "flag" + index_suffix = "(flag)" + annotation = "Flag" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + + +class TableObject(NotationObject): + """A Coq table, i.e. a setting that is a set of values. + + Example:: + + .. table:: Search Blacklist + + This table controls ... + """ + subdomain = "table" + index_suffix = "(table)" + annotation = "Table" + + def _name_from_signature(self, signature): + return stringify_with_ellipses(signature) + class ProductionObject(CoqObject): r"""A grammar production. @@ -487,7 +543,7 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): CoqCodeRole = coq_code_role class CoqtopDirective(Directive): - """A reST directive to describe interactions with Coqtop. + r"""A reST directive to describe interactions with Coqtop. Usage:: @@ -525,16 +581,17 @@ class CoqtopDirective(Directive): required_arguments = 0 optional_arguments = 1 final_argument_whitespace = True + option_spec = { 'name': directives.unchanged } directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable # Pygments-based post-processing (we could also set rawsource to '') content = '\n'.join(self.content) - options = self.arguments[0].split() if self.arguments else ['in'] - if 'all' in options: - options.extend(['in', 'out']) - node = nodes.container(content, coqtop_options = list(set(options)), + args = self.arguments[0].split() if self.arguments else ['in'] + if 'all' in args: + args.extend(['in', 'out']) + node = nodes.container(content, coqtop_options = list(set(args)), classes=['coqtop', 'literal-block']) self.add_name(node) return [node] @@ -559,6 +616,7 @@ class CoqdocDirective(Directive): required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + option_spec = { 'name': directives.unchanged } directive_name = "coqdoc" def run(self): @@ -567,6 +625,7 @@ class CoqdocDirective(Directive): content = '\n'.join(self.content) node = nodes.inline(content, '', *highlight_using_coqdoc(content)) wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block']) + self.add_name(wrapper) return [wrapper] class ExampleDirective(BaseAdmonition): @@ -602,24 +661,39 @@ class ExampleDirective(BaseAdmonition): self.options['classes'] = ['admonition', 'note'] return super().run() -class PreambleDirective(MathDirective): - r"""A reST directive for hidden math. +class PreambleDirective(Directive): + r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. - Example:: - - .. preamble:: + Usage:: - \newcommand{\paren}[#1]{\left(#1\right)} + .. preamble:: preamble.tex """ - + has_content = False + required_arguments = 1 + optional_arguments = 0 + final_argument_whitespace = True + option_spec = {} directive_name = "preamble" def run(self): - self.options['nowrap'] = True - [node] = super().run() + document = self.state.document + env = document.settings.env + + if not document.settings.file_insertion_enabled: + msg = 'File insertion disabled' + return [document.reporter.warning(msg, line=self.lineno)] + + rel_fname, abs_fname = env.relfn2path(self.arguments[0]) + env.note_dependency(rel_fname) + + with open(abs_fname, encoding="utf-8") as ltx: + latex = ltx.read() + + node = make_math_node(latex, env.docname, nowrap=True) node['classes'] = ["math-preamble"] + set_source_info(self, node) return [node] class InferenceDirective(Directive): @@ -632,8 +706,8 @@ class InferenceDirective(Directive): .. inference:: name - newline-separated premisses - ------------------------ + newline-separated premises + -------------------------- conclusion Example:: @@ -652,15 +726,6 @@ class InferenceDirective(Directive): final_argument_whitespace = True directive_name = "inference" - def make_math_node(self, latex): - node = displaymath() - node['latex'] = latex - node['label'] = None # Otherwise equations are numbered - node['nowrap'] = False - node['docname'] = self.state.document.settings.env.docname - node['number'] = None - return node - @staticmethod def prepare_latex_operand(op): # TODO: Could use a fancier inference class in LaTeX @@ -680,7 +745,8 @@ class InferenceDirective(Directive): title = self.arguments[0] content = '\n'.join(self.content) latex = self.prepare_latex(content) - math_node = self.make_math_node(latex) + docname = self.state.document.settings.env.docname + math_node = make_math_node(latex, docname, nowrap=False) tid = nodes.make_id(title) target = nodes.target('', '', ids=['inference-' + tid]) @@ -827,23 +893,28 @@ class CoqtopBlocksTransform(Transform): kept_node['classes'] = [c for c in kept_node['classes'] if c != 'coqtop-hidden'] - def merge_consecutive_coqtop_blocks(self): + @staticmethod + def merge_consecutive_coqtop_blocks(app, doctree, _): """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate.""" - for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): + for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block): if node.parent: + rawsources, names = [node.rawsource], set(node['names']) for sibling in node.traverse(include_self=False, descend=False, siblings=True, ascend=False): if CoqtopBlocksTransform.is_coqtop_block(sibling): - self.merge_coqtop_classes(node, sibling) + CoqtopBlocksTransform.merge_coqtop_classes(node, sibling) + rawsources.append(sibling.rawsource) + names.update(sibling['names']) node.extend(sibling.children) node.parent.remove(sibling) sibling.parent = None else: break + node.rawsource = "\n\n".join(rawsources) + node['names'] = list(names) def apply(self): self.add_coqtop_output() - self.merge_consecutive_coqtop_blocks() class CoqSubdomainsIndex(Index): """Index subclass to provide subdomain-specific indices. @@ -876,7 +947,7 @@ class CoqTacticIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] + name, localname, shortname, subdomains = "optindex", "Flags, options and Tables Index", "options", ["flag", "opt", "table"] class CoqGallinaIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] @@ -949,6 +1020,8 @@ class CoqDomain(Domain): 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), + 'flag': ObjType('flag', 'flag'), + 'table': ObjType('table', 'table'), 'thm': ObjType('thm', 'thm'), 'prodn': ObjType('prodn', 'prodn'), 'exn': ObjType('exn', 'exn'), @@ -965,6 +1038,8 @@ class CoqDomain(Domain): 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, + 'flag': FlagObject, + 'table': TableObject, 'thm': GallinaObject, 'prodn' : ProductionObject, 'exn': ExceptionObject, @@ -976,6 +1051,8 @@ class CoqDomain(Domain): 'cmd': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), + 'flag': XRefRole(warn_dangling=True), + 'table': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), 'prodn' : XRefRole(warn_dangling=True), 'exn': XRefRole(warn_dangling=True), @@ -997,6 +1074,8 @@ class CoqDomain(Domain): 'cmd': {}, 'tacn': {}, 'opt': {}, + 'flag': {}, + 'table': {}, 'thm': {}, 'prodn' : {}, 'exn': {}, @@ -1059,7 +1138,6 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: pygments if available. This prevents the LaTeX builder from getting confused. """ - is_html = app.builder.tags.has("html") for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: @@ -1096,6 +1174,7 @@ def setup(app): app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) + app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles app.add_stylesheet("fonts.css") @@ -1108,4 +1187,11 @@ def setup(app): # Tell Sphinx about extra settings app.add_config_value("report_undocumented_coq_objects", None, 'env') - return {'version': '0.1', "parallel_read_safe": True} + # ``env_version`` is used by Sphinx to know when to invalidate + # coqdomain-specific bits in its caches. It should be incremented when the + # contents of ``env.domaindata['coq']`` change. See + # `https://github.com/sphinx-doc/sphinx/issues/4460`. + meta = { "version": "0.1", + "env_version": 1, + "parallel_read_safe": True } + return meta diff --git a/ide/coqide.opam b/ide/coqide.opam index 1b46efdee2..ba05b9edcf 100644 --- a/ide/coqide.opam +++ b/ide/coqide.opam @@ -16,4 +16,4 @@ depends: [ "coq" ] -build: [ [ "dune" "build" "-p" package "-j" jobs ] ] +build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/ide/idetop.ml b/ide/idetop.ml index d846b3abb5..8a221a93e9 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -204,27 +204,35 @@ let export_pre_goals pgs = Interface.given_up_goals = pgs.Proof.given_up_goals } -let add_diffs oldp newp intf = - let open Interface in - let (hyps_pp_list, concl_pp) = Proof_diffs.diff_first_goal oldp newp in - match intf.fg_goals with - | [] -> intf - | first_goal :: tl -> - { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl } - let goals () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; try let newp = Proof_global.give_me_the_proof () in - let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in - if Proof_diffs.show_diffs () then + if Proof_diffs.show_diffs () then begin let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in + let diff_goal_map = Proof_diffs.make_goal_map oldp newp in + let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *) + try Evar.Map.find ng diff_goal_map with Not_found -> ng + in + + let process_goal_diffs nsigma ng = + let open Evd in + let og = map_goal_for_diff ng in + let og_s = match oldp with + | Some oldp -> + let (_,_,_,_,osigma) = Proof.proof oldp in + Some { it = og; sigma = osigma } + | None -> None + in + let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in + { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } + in try - Some (add_diffs oldp (Some newp) intf) - with Pp_diff.Diff_Failure _ -> Some intf - else - Some intf + Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs)) + with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal)) + end else + Some (export_pre_goals (Proof.map_structured_proof newp process_goal)) with Proof_global.NoCurrentProof -> None;; let evars () = diff --git a/library/goptions.ml b/library/goptions.ml index eafcb8fea6..dcbc46ab72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -412,7 +412,7 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - str "Synchronous options:" ++ fnl () ++ + str "Options:" ++ fnl () ++ OptionMap.fold (fun key (name, depr, (read,_,_)) p -> p ++ print_option key name (read ()) depr) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bbc0a37c69..fd2d90e9cf 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1469,7 +1469,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((CAst.make @@ relnames.(i)), None), + ((CAst.make @@ relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1499,14 +1499,14 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = @@ -1521,7 +1521,7 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 84f13d2131..73490a2dfd 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -94,7 +94,7 @@ let let_evar name typ = in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) + (Tactics.pose_tac (Name.Name id) evar) end let hget_evar n = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f4313a8fa3..71da6c7667 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1664,16 +1664,18 @@ and interp_atomic ist tac : unit Proofview.tactic = (* We try to fully-typecheck the term *) let flags = open_constr_use_classes_flags () in let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in - let let_tac b na c cl eqpat = - let id = Option.default (make IntroAnonymous) eqpat in - let with_eq = if b then None else Some (true,id) in - Tactics.letin_tac with_eq na c None cl - in let na = interp_name ist env sigma na in + let let_tac = + if b then Tactics.pose_tac na c_interp + else + let id = Option.default (make IntroAnonymous) eqpat in + let with_eq = Some (true, id) in + Tactics.letin_tac with_eq na c_interp None Locusops.nowhere + in Tacticals.New.tclWITHHOLES ev (name_atomic ~env (TacLetTac(ev,na,c_interp,clp,b,eqpat)) - (let_tac b na c_interp clp eqpat)) sigma + let_tac) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 59fd9b8017..094adfda7a 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -85,6 +85,7 @@ Ltac zify_binop t thm a b:= Ltac zify_op_1 := match goal with + | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b @@ -114,6 +115,7 @@ Ltac hide_Z_of_nat t := Ltac zify_nat_rel := match goal with (* I: equalities *) + | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *) | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H | |- context [ @eq nat ?a ?b ] => rewrite <- (Nat2Z.inj_iff a b) @@ -223,6 +225,7 @@ Ltac hide_Zpos t := Ltac zify_positive_rel := match goal with (* I: equalities *) + | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq positive ?a ?b) => apply Pos2Z.inj | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H | |- context [ @eq positive ?a ?b ] => rewrite <- (Pos2Z.inj_iff a b) @@ -348,6 +351,7 @@ Ltac hide_Z_of_N t := Ltac zify_N_rel := match goal with (* I: equalities *) + | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *) | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H | |- context [ @eq N ?a ?b ] => rewrite <- (N2Z.inj_iff a b) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index e367cd32d6..f67cf20e49 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *) (** Defined identifier *) - -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let ssrposetac (id, (_, t)) gl = let ist, t = diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 83581f3416..f12f9fac0f 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Locusops open Ssrast open Ssrcommon @@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq = let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false -let settac id c = Tactics.letin_tac None (Name id) c None -let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere) +let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl) let hidetacs clseq idhide cl0 = if not (hidden_clseq clseq) then [] else diff --git a/printing/printer.ml b/printing/printer.ml index 5b3ead181f..67d71332b0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -494,17 +494,17 @@ let pr_transparent_state (ids, csts) = str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) (* display complete goal - prev_gs has info on the previous proof step for diffs - gs has info on the current proof step + og_s has goal+sigma on the previous proof step for diffs + g_s has goal+sigma on the current proof step *) -let pr_goal ?(diffs=false) ?prev_gs gs = - let g = sig_it gs in - let sigma = project gs in +let pr_goal ?(diffs=false) ?og_s g_s = + let g = sig_it g_s in + let sigma = project g_s in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = if diffs then - Proof_diffs.diff_goals ?prev_gs (Some gs) + Proof_diffs.diff_goal ?og_s g sigma else pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ @@ -525,13 +525,18 @@ let pr_goal_name sigma g = let pr_goal_header nme sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"") - ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) + ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) (* display the conclusion of a goal *) -let pr_concl n sigma g = +let pr_concl n ?(diffs=false) ?og_s sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in + let pc = + if diffs then + Proof_diffs.diff_concl ?og_s sigma g + else + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) + in let header = pr_goal_header (int n) sigma g in header ++ str " is:" ++ cut () ++ str" " ++ pc @@ -698,13 +703,25 @@ let print_dependent_evars gl sigma seeds = in constraints ++ evars () +module GoalMap = Evar.Map + (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -(* [prev] is the previous proof step, used for diffs *) -let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev +(* [os_map] is derived from the previous proof step, used for diffs *) +let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = + let diff_goal_map = + match os_map with + | Some (_, diff_goal_map) -> diff_goal_map + | None -> GoalMap.empty + in + + let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *) + try GoalMap.find ng diff_goal_map with Not_found -> ng + in + (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -738,23 +755,23 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev else str" " (* non-breakable space *) in + let get_ogs g = + match os_map with + | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma } + | None -> None + in let rec pr_rec n = function | [] -> (mt ()) | g::rest -> - let pc = pr_concl n sigma g in + let og_s = get_ogs g in + let pc = pr_concl n ~diffs ?og_s sigma g in let prest = pr_rec (n+1) rest in (cut () ++ pc ++ prest) in let print_multiple_goals g l = if pr_first then - let prev_gs = - match prev with - | Some (prev_goals, prev_sigma) -> - if prev_goals = [] then None - else Some { it = List.hd prev_goals; sigma = prev_sigma} - | None -> None - in - pr_goal ~diffs ?prev_gs { it = g ; sigma = sigma } + let og_s = get_ogs g in + pr_goal ~diffs ?og_s { it = g ; sigma = sigma } ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l else @@ -797,7 +814,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev ++ print_dependent_evars (Some g1) sigma seeds ) -let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof proof = +let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = (* spiwack: it shouldn't be the job of the printer to look up stuff in the [evar_map], I did stuff that way because it was more straightforward, but seriously, [Proof.proof] should return @@ -833,15 +850,15 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof proof = let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in - let prev = match prev_proof with - | Some op -> - let (ogoals , _, _, _, _) = Proof.proof op in - let { Evd.it = obgoals; sigma = osigma } = Proof.V82.background_subgoals op in - let obgoals_focused = List.filter (fun x -> List.mem x ogoals) obgoals in - Some (obgoals_focused, osigma) - | None -> None + let os_map = match oproof with + | Some op when diffs -> + let (_,_,_,_, osigma) = Proof.proof op in + let diff_goal_map = Proof_diffs.make_goal_map oproof proof in + Some (osigma, diff_goal_map) + | _ -> None in - pr_subgoals ~pr_first:true ~diffs ?prev None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused + pr_subgoals ~pr_first:true ~diffs ?os_map None bsigma ~seeds ~shelf ~stack:[] + ~unfocused:unfocused_if_needed ~goals:bgoals_focused end let pr_open_subgoals ~proof = @@ -930,8 +947,8 @@ let pr_assumptionset env sigma s = let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in - let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ + let safe_pr_ltype env sigma typ = + try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = @@ -942,7 +959,7 @@ let pr_assumptionset env sigma s = let pr_axiom env ax typ = match ax with | Constant kn -> - safe_pr_constant env kn ++ safe_pr_ltype typ + safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") | Guarded kn -> @@ -952,7 +969,7 @@ let pr_assumptionset env sigma s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = pr_id id ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in (var :: v, a, o, tr) | Axiom (axiom, []) -> let ax = pr_axiom env axiom typ in @@ -966,10 +983,10 @@ let pr_assumptionset env sigma s = l in (v, ax :: a, o, tr) | Opaque kn -> - let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in + let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, opq :: o, tr) | Transparent kn -> - let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in + let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, o, tran :: tr) in let (vars, axioms, opaque, trans) = @@ -1023,22 +1040,14 @@ let print_and_diff oldp newp = | Some proof -> let output = if Proof_diffs.show_diffs () then - try pr_open_subgoals_diff ~diffs:true ?prev_proof:oldp proof + try pr_open_subgoals_diff ~diffs:true ?oproof:oldp proof with Pp_diff.Diff_Failure msg -> begin (* todo: print the unparsable string (if we know it) *) - Feedback.msg_warning Pp.(str ("Diff failure:" ^ msg ^ "; showing results without diff highlighting" )); + Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() + ++ str "Showing results without diff highlighting" ); pr_open_subgoals ~proof end else pr_open_subgoals ~proof in Feedback.msg_notice output;; - -(* Do diffs on the first goal returning a Pp. *) -let diff_pr_open_subgoals ?(quiet=false) o_proof n_proof = - match n_proof with - | None -> Pp.mt () - | Some proof -> - try pr_open_subgoals_diff ~quiet ~diffs:true ?prev_proof:o_proof proof - with Pp_diff.Diff_Failure _ -> pr_open_subgoals ~proof - (* todo: print the unparsable string (if we know it) *) diff --git a/printing/printer.mli b/printing/printer.mli index 971241d5f9..518c5b930b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -171,26 +171,46 @@ val pr_transparent_state : transparent_state -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) -val pr_goal : ?diffs:bool -> ?prev_gs:(goal sigma) -> goal sigma -> Pp.t - -(** [pr_subgoals ~pr_first ~prev_proof pp sigma seeds shelf focus_stack unfocused goals] - prints the goals of the list [goals] followed by the goals in - [unfocused], in a short way (typically only the conclusion) except - for the first goal if [pr_first] is true. Also, if [diffs] is true - and [pr_first] is true, then highlight diffs relative to [prev] in the - output for first goal. This function prints only the - focused goals unless the conrresponding option - [enable_unfocused_goal_printing] is set. [seeds] is for printing - dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?prev:(goal list * evar_map) -> Pp.t option -> evar_map +(** [pr_goal ~diffs ~og_s g_s] prints the goal specified by [g_s]. If [diffs] is true, + highlight the differences between the old goal, [og_s], and [g_s]. [g_s] and [og_s] are + records containing the goal and sigma for, respectively, the new and old proof steps, + e.g. [{ it = g ; sigma = sigma }]. +*) +val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t + +(** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals] + prints the goals in [goals] followed by the goals in [unfocused] in a compact form + (typically only the conclusion). If [pr_first] is true, print the first goal in full. + [close_cmd] is printed afterwards verbatim. + + If [diffs] is true, then highlight diffs relative to [os_map] in the output for first goal. + [os_map] contains sigma for the old proof step and the goal map created by + [Proof_diffs.make_goal_map]. + + This function prints only the focused goals unless the corresponding option [enable_unfocused_goal_printing] is set. + [seeds] is for printing dependent evars (mainly for emacs proof tree mode). [shelf] is from + Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but + there are non-instantiated existential variables. [stack] is used to print summary info on unfocused + goals. +*) +val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused: goal list -> goals:goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t -val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?prev_proof:Proof.t -> Proof.t -> Pp.t -val diff_pr_open_subgoals : ?quiet:bool -> Proof.t option -> Proof.t option -> Pp.t +(** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output + is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion, + [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }]. +*) +val pr_concl : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t + +(** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop. + The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their + conclusions. If [diffs] is true, highlight the differences between the old proof, [oproof], and [proof]. [quiet] + disables printing messages as Feedback. +*) +val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t @@ -200,13 +220,14 @@ val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t val pr_prim_rule : prim_rule -> Pp.t +[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"] val print_and_diff : Proof.t option -> Proof.t option -> unit (** Backwards compatibility *) val prterm : constr -> Pp.t (** = pr_lconstr *) - +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] (** Declarations for the "Print Assumption" command *) type axiom = diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 3a81e908a7..5bb1053645 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -14,39 +14,26 @@ Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. See pp_diff.ml for details on how the diff works. -Diffs are computed for the hypotheses and conclusion of the first goal between -the old and new proofs. +Diffs are computed for the hypotheses and conclusion of each goal in the new +proof with its matching goal in the old proof. -Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or -'-diffs "on"|"off"|"removed"' on the OS command line. The "on" option shows only the -new item with added text, while "removed" shows each modified item twice--once -with the old value showing removed text and once with the new value showing -added text. +Diffs can be enabled in coqtop with 'Set Diffs "on"|"off"|"removed"' or +'-diffs on|off|removed' on the OS command line. In CoqIDE, they can be enabled +from the View menu. The "on" option shows only the new item with added text, +while "removed" shows each modified item twice--once with the old value showing +removed text and once with the new value showing added text. In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel. For coqtop, these can be set through the COQ_COLORS environment variable. Limitations/Possible enhancements: -- If you go back to a prior proof step, diffs are not shown on the new current -step. Diffs will be shown again once you do another proof step. - -- Diffs are done between the first active goal in the old and new proofs. -If, for example, the proof step completed a goal, then the new goal is a -different goal, not a transformation of the old goal, so a diff is probably -not appropriate. (There's currently no way to tell when this happens or to -accurately match goals across old and new proofs. -See https://github.com/coq/coq/issues/7653) This is also why only the -first goal is diffed. - -- "Set Diffs "xx"." should reprint the current goal using the new option. - - coqtop colors were chosen for white text on a black background. They're not the greatest. I didn't want to change the existing green highlight. Suggestions welcome. - coqtop underlines removed text because (per Wikipedia) the ANSI escape code -for strikeout is not commonly supported (it didn't work on mine). CoqIDE +for strikeout is not commonly supported (it didn't work on my system). CoqIDE uses strikeout on removed text. *) @@ -54,8 +41,6 @@ open Pp_diff let diff_option = ref `OFF -(* todo: Is there a way to persist the setting between sessions? - Eg if the user wants this as a permanent config setting? *) let read_diffs_option () = match !diff_option with | `OFF -> "off" | `ON -> "on" @@ -136,7 +121,8 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = (* use the order from the old line in case it's changed in the new *) let old_ids = if old_ids_uo = [] then [] else let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in - List.concat (List.map (contains orig) old_ids_uo) in + List.concat (List.map (contains orig) old_ids_uo) + in let setup ids map = if ids = [] then ("", Pp.mt ()) else let open Pp in @@ -233,6 +219,12 @@ let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * ' (* XXX: Very unfortunately we cannot use the Proofview interface as Proof is still using the "legacy" one. *) +let process_goal_concl sigma g : Constr.t * Environ.env = + let env = Goal.V82.env sigma g in + let ty = Goal.V82.concl sigma g in + let ty = EConstr.to_constr sigma ty in + (ty, env) + let process_goal sigma g : Constr.t reified_goal = let env = Goal.V82.env sigma g in let hyps = Goal.V82.hyps sigma g in @@ -256,14 +248,29 @@ let pr_leconstr_core goal_concl_style env sigma t = let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) +let diff_concl ?og_s nsigma ng = + let open Evd in + let o_concl_pp = match og_s with + | Some { it=og; sigma=osigma } -> + let (oty, oenv) = process_goal_concl osigma og in + pp_of_type oenv osigma oty + | None -> Pp.mt() + in + let (nty, nenv) = process_goal_concl nsigma ng in + let n_concl_pp = pp_of_type nenv nsigma nty in + + let show_removed = Some (show_removed ()) in + + diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp + (* fetch info from a goal, returning (idents, map, concl_pp) where -idents is a list with one entry for each hypothesis, each entry is the list of -idents on the lhs of the hypothesis. map is a map from ident to hyp_info -reoords. For example: for the hypotheses: +idents is a list with one entry for each hypothesis, in which each entry +is the list of idents on the lhs of the hypothesis. map is a map from +ident to hyp_info reoords. For example: for the hypotheses: b : bool n, m : nat -list will be [ ["b"]; ["n"; "m"] ] +idents will be [ ["b"]; ["n"; "m"] ] map will contain: "b" -> { ["b"], Pp.t for ": bool"; false } @@ -317,31 +324,314 @@ let hyp_list_to_pp hyps = | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl | [] -> mt ();; -(* Special purpuse, use only for the IDE interface, *) -let diff_first_goal o_proof n_proof = - let first_goal_info proof = - match proof with - | None -> ([], StringMap.empty, Pp.mt ()) - | Some proof2 -> - let (goals,_,_,_,sigma) = Proof.proof proof2 in - match goals with - | hd :: tl -> goal_info hd sigma; - | _ -> ([], StringMap.empty, Pp.mt ()) - in - diff_goal_info (first_goal_info o_proof) (first_goal_info n_proof);; - -let diff_goals ?prev_gs n_gs = - let unwrap gs = - match gs with - | Some gs -> - let goal = Evd.sig_it gs in - let sigma = Refiner.project gs in - goal_info goal sigma - | None -> ([], StringMap.empty, Pp.mt ()) - in - let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap prev_gs) (unwrap n_gs) in +let unwrap g_s = + match g_s with + | Some g_s -> + let goal = Evd.sig_it g_s in + let sigma = Refiner.project g_s in + goal_info goal sigma + | None -> ([], StringMap.empty, Pp.mt ()) + +let diff_goal_ide og_s ng nsigma = + diff_goal_info (unwrap og_s) (goal_info ng nsigma) + +let diff_goal ?og_s ng ns = + let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap og_s) (goal_info ng ns) in let open Pp in v 0 ( (hyp_list_to_pp hyps_pp_list) ++ cut () ++ str "============================" ++ cut () ++ concl_pp);; + + +(*** Code to determine which calls to compare between the old and new proofs ***) + +open Constrexpr +open Glob_term +open Names +open CAst + +(* Compare the old and new proof trees to identify the correspondence between +new and old goals. Returns a map from the new evar name to the old, +e.g. "Goal2" -> "Goal1". Assumes that proof steps only rewrite CEvar nodes +and that CEvar nodes cannot contain other CEvar nodes. + +The comparison works this way: +1. Traverse the old and new trees together (ogname = "", ot != nt): +- if the old and new trees both have CEvar nodes, add an entry to the map from + the new evar name to the old evar name. (Position of goals is preserved but + evar names may not be--see below.) +- if the old tree has a CEvar node and the new tree has a different type of node, + we've found a changed goal. Set ogname to the evar name of the old goal and + go to step 2. +- any other mismatch violates the assumptions, raise an exception +2. Traverse the new tree from the point of the difference (ogname <> "", ot = nt). +- if the node is a CEvar, generate a map entry from the new evar name to ogname. + +Goal ids for unchanged goals appear to be preserved across proof steps. +However, the evar name associated with a goal id may change in a proof step +even if that goal is not changed by the tactic. You can see this by enabling +the call to db_goal_map and entering the following: + + Parameter P : nat -> Prop. + Goal (P 1 /\ P 2 /\ P 3) /\ P 4. + split. + Show Proof. + split. + Show Proof. + + Which gives you this summarized output: + + > split. + New Goals: 3 -> Goal 4 -> Goal0 <--- goal 4 is "Goal0" + Old Goals: 1 -> Goal + Goal map: 3 -> 1 4 -> 1 + > Show Proof. + (conj ?Goal ?Goal0) <--- goal 4 is the rightmost goal in the proof + > split. + New Goals: 6 -> Goal0 7 -> Goal1 4 -> Goal <--- goal 4 is now "Goal" + Old Goals: 3 -> Goal 4 -> Goal0 + Goal map: 6 -> 3 7 -> 3 + > Show Proof. + (conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof + *) +let match_goals ot nt = + let nevar_to_oevar = ref StringMap.empty in + (* ogname is "" when there is no difference on the current path. + It's set to the old goal's evar name once a rewitten goal is found, + at which point the code only searches for the replacing goals + (and ot is set to nt). *) + let rec match_goals_r ogname ot nt = + let constr_expr ogname exp exp2 = + match_goals_r ogname exp.v exp2.v + in + let constr_expr_opt ogname exp exp2 = + match exp, exp2 with + | Some expa, Some expb -> constr_expr ogname expa expb + | None, None -> () + | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)") + in + let local_binder_expr ogname exp exp2 = + match exp, exp2 with + | CLocalAssum (nal,bk,ty), CLocalAssum(nal2,bk2,ty2) -> + constr_expr ogname ty ty2 + | CLocalDef (n,c,t), CLocalDef (n2,c2,t2) -> + constr_expr ogname c c2; + constr_expr_opt ogname t t2 + | CLocalPattern p, CLocalPattern p2 -> + let (p,ty), (p2,ty2) = p.v,p2.v in + constr_expr_opt ogname ty ty2 + | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)") + in + let recursion_order_expr ogname exp exp2 = + match exp, exp2 with + | CStructRec, CStructRec -> () + | CWfRec c, CWfRec c2 -> + constr_expr ogname c c2 + | CMeasureRec (m,r), CMeasureRec (m2,r2) -> + constr_expr ogname m m2; + constr_expr_opt ogname r r2 + | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)") + in + let fix_expr ogname exp exp2 = + let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in + recursion_order_expr ogname ro ro2; + List.iter2 (local_binder_expr ogname) lb lb2; + constr_expr ogname ce1 ce12; + constr_expr ogname ce2 ce22 + in + let cofix_expr ogname exp exp2 = + let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in + List.iter2 (local_binder_expr ogname) lb lb2; + constr_expr ogname ce1 ce12; + constr_expr ogname ce2 ce22 + in + let case_expr ogname exp exp2 = + let (ce,l,cp), (ce2,l2,cp2) = exp,exp2 in + constr_expr ogname ce ce2 + in + let branch_expr ogname exp exp2 = + let (cpe,ce), (cpe2,ce2) = exp.v,exp2.v in + constr_expr ogname ce ce2 + in + let constr_notation_substitution ogname exp exp2 = + let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in + List.iter2 (constr_expr ogname) ce ce2; + List.iter2 (fun a a2 -> List.iter2 (constr_expr ogname) a a2) cel cel2; + List.iter2 (fun a a2 -> List.iter2 (local_binder_expr ogname) a a2) lb lb2 + in + begin + match ot, nt with + | CRef (ref,us), CRef (ref2,us2) -> () + | CFix (id,fl), CFix (id2,fl2) -> + List.iter2 (fix_expr ogname) fl fl2 + | CCoFix (id,cfl), CCoFix (id2,cfl2) -> + List.iter2 (cofix_expr ogname) cfl cfl2 + | CProdN (bl,c2), CProdN (bl2,c22) + | CLambdaN (bl,c2), CLambdaN (bl2,c22) -> + List.iter2 (local_binder_expr ogname) bl bl2; + constr_expr ogname c2 c22 + | CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) -> + constr_expr ogname c1 c12; + constr_expr_opt ogname t t2; + constr_expr ogname c2 c22 + | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) -> + List.iter2 (constr_expr ogname) args args2 + | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) -> + constr_expr ogname f f2; + List.iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in + constr_expr ogname c c2) args args2 + | CRecord fs, CRecord fs2 -> + List.iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in + constr_expr ogname c c2) fs fs2 + | CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) -> + constr_expr_opt ogname rtnpo rtnpo2; + List.iter2 (case_expr ogname) tms tms2; + List.iter2 (branch_expr ogname) eqns eqns2 + | CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) -> + constr_expr_opt ogname po po2; + constr_expr ogname b b2; + constr_expr ogname c c2 + | CIf (c,(na,po),b1,b2), CIf (c2,(na2,po2),b12,b22) -> + constr_expr ogname c c2; + constr_expr_opt ogname po po2; + constr_expr ogname b1 b12; + constr_expr ogname b2 b22 + | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> () + | CPatVar _, CPatVar _ -> () + | CEvar (n,l), CEvar (n2,l2) -> + let oevar = if ogname = "" then Id.to_string n else ogname in + nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar; + List.iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 + | CEvar (n,l), nt' -> + (* pass down the old goal evar name *) + match_goals_r (Id.to_string n) nt' nt' + | CSort s, CSort s2 -> () + | CCast (c,c'), CCast (c2,c'2) -> + constr_expr ogname c c2; + (match c', c'2 with + | CastConv a, CastConv a2 + | CastVM a, CastVM a2 + | CastNative a, CastNative a2 -> + constr_expr ogname a a2 + | CastCoerce, CastCoerce -> () + | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)")) + | CNotation (ntn,args), CNotation (ntn2,args2) -> + constr_notation_substitution ogname args args2 + | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) -> + constr_expr ogname c c2 + | CPrim p, CPrim p2 -> () + | CDelimiters (key,e), CDelimiters (key2,e2) -> + constr_expr ogname e e2 + | CProj (pr,c), CProj (pr2,c2) -> + constr_expr ogname c c2 + | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)") + end + in + + (match ot with + | Some ot -> match_goals_r "" ot nt + | None -> ()); + !nevar_to_oevar + + +let to_constr p = + let open CAst in + let pprf = Proof.partial_proof p in + (* pprf generally has only one element, but it may have more in the derive plugin *) + let t = List.hd pprf in + let sigma, env = Pfedit.get_current_context ~p () in + let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *) + x.v + + +module GoalMap = Evar.Map + +let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma) + +[@@@ocaml.warning "-32"] +let db_goal_map op np ng_to_og = + Printf.printf "New Goals: "; + let (ngoals,_,_,_,nsigma) = Proof.proof np in + List.iter (fun ng -> Printf.printf "%d -> %s " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals; + (match op with + | Some op -> + let (ogoals,_,_,_,osigma) = Proof.proof op in + Printf.printf "\nOld Goals: "; + List.iter (fun og -> Printf.printf "%d -> %s " (Evar.repr og) (goal_to_evar og osigma)) ogoals + | None -> ()); + Printf.printf "\nGoal map: "; + GoalMap.iter (fun og ng -> Printf.printf "%d -> %d " (Evar.repr og) (Evar.repr ng)) ng_to_og; + Printf.printf "\n" +[@@@ocaml.warning "+32"] + +(* Create a map from new goals to old goals for proof diff. The map only + has entries for new goals that are not the same as the corresponding old + goal; there are no entries for unchanged goals. + + It proceeds as follows: + 1. Find the goal ids that were removed from the old proof and that were + added in the new proof. If the same goal id is present in both proofs + then conclude the goal is unchanged (assumption). + + 2. The code assumes that proof changes only take the form of replacing + one or more goal symbols (CEvars) with new terms. Therefore: + - if there are no removals, the proofs are the same. + - if there are removals but no additions, then there are no new goals + that aren't the same as their associated old goals. For the both of + these cases, the map is empty because there are no new goals that differ + from their old goals + - if there is only one removal, then any added goals should be mapped to + the removed goal. + - if there are more than 2 removals and more than one addition, call + match_goals to get a map between old and new evar names, then use this + to create the map from new goal ids to old goal ids for the differing goals. +*) +let make_goal_map_i op np = + let ng_to_og = ref GoalMap.empty in + match op with + | None -> !ng_to_og + | Some op -> + let open Goal.Set in + let ogs = Proof.all_goals op in + let ngs = Proof.all_goals np in + let rem_gs = diff ogs ngs in + let num_rems = cardinal rem_gs in + let add_gs = diff ngs ogs in + let num_adds = cardinal add_gs in + + if num_rems = 0 then + !ng_to_og (* proofs are the same *) + else if num_adds = 0 then + !ng_to_og (* only removals *) + else if num_rems = 1 then begin + (* only 1 removal, some additions *) + let removed_g = List.hd (elements rem_gs) in + Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x removed_g !ng_to_og) add_gs; + !ng_to_og + end else begin + (* >= 2 removals, >= 1 addition, need to match *) + let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in + + let oevar_to_og = ref StringMap.empty in + let (_,_,_,_,osigma) = Proof.proof op in + List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og) + (Goal.Set.elements rem_gs); + + try + let (_,_,_,_,nsigma) = Proof.proof np in + let get_og ng = + let nevar = goal_to_evar ng nsigma in + let oevar = StringMap.find nevar nevar_to_oevar in + let og = StringMap.find oevar !oevar_to_og in + og + in + Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs; + !ng_to_og + with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)") + end + +let make_goal_map op np = + let ng_to_og = make_goal_map_i op np in + (*db_goal_map op np ng_to_og;*) + ng_to_og diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 482f03b686..832393e15f 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -15,8 +15,13 @@ val write_diffs_option : string -> unit (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool -(** Computes the diff between the first goal of two Proofs and returns -the highlighted hypotheses and conclusion. +open Evd +open Proof_type +open Environ +open Constr + +(** Computes the diff between the goals of two Proofs and returns +the highlighted lists of hypotheses and conclusions. If the strings used to display the goal are not lexable (this is believed unlikely), this routine will generate a Diff_Failure. This routine may also @@ -26,12 +31,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t - -open Evd -open Proof_type -open Environ -open Constr +val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t (** Computes the diff between two goals @@ -43,7 +43,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t +val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list @@ -52,6 +52,17 @@ val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.type val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_lconstr_env : env -> evar_map -> constr -> Pp.t +(** Computes diffs for a single conclusion *) +val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t + +(** Generates a map from [np] to [op] that maps changed goals to their prior +forms. The map doesn't include entries for unchanged goals; unchanged goals +will have the same goal id in both versions. + +[op] and [np] must be from the same proof document and [op] must be for a state +before [np]. *) +val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t + (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) val log_out_ch : out_channel ref diff --git a/proofs/goal.ml b/proofs/goal.ml index 1440d1636b..c14c0a8a77 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -143,3 +143,5 @@ module V82 = struct ) ~init:(concl sigma gl) env end + +module Set = Set.Make(struct type t = goal let compare = Evar.compare end) diff --git a/proofs/goal.mli b/proofs/goal.mli index b8c979ad7a..a033d6daab 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -71,3 +71,5 @@ module V82 : sig val abstract_type : Evd.evar_map -> goal -> EConstr.types end + +module Set : sig include Set.S with type elt = goal end diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d971c28a26..e6507332b1 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -51,23 +51,22 @@ let _ = CErrors.register_handler begin function | _ -> raise CErrors.Unhandled end -let get_nth_V82_goal i = - let p = Proof_global.give_me_the_proof () in +let get_nth_V82_goal p i = let goals,_,_,_,sigma = Proof.proof p in try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal -let get_goal_context_gen i = - let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in +let get_goal_context_gen p i = + let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = - try get_goal_context_gen i + try get_goal_context_gen (Proof_global.give_me_the_proof ()) i with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = - try get_goal_context_gen 1 + try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1 with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, @@ -75,14 +74,18 @@ let get_current_goal_context () = let env = Global.env () in (Evd.from_env env, env) -let get_current_context () = - try get_goal_context_gen 1 +let get_current_context ?p () = + let current_proof_by_default = function + | Some p -> p + | None -> Proof_global.give_me_the_proof () + in + try get_goal_context_gen (current_proof_by_default p) 1 with Proof_global.NoCurrentProof -> let env = Global.env () in (Evd.from_env env, env) | NoSuchGoal -> (* No more focused goals ? *) - let p = Proof_global.give_me_the_proof () in + let p = (current_proof_by_default p) in let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index e02b5ab956..5feb5bd645 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -60,7 +60,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env If there is no pending proof then it returns the current global environment and empty evar_map. *) -val get_current_context : unit -> Evd.evar_map * env +val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env (** [current_proof_statement] *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 0d355890c5..8bbd82bb0a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -488,3 +488,12 @@ module V82 = struct { pr with proofview ; shelf } end + +let all_goals p = + let add gs set = + List.fold_left (fun s g -> Goal.Set.add g s) set gs in + let (goals,stack,shelf,given_up,_) = proof p in + let set = add goals Goal.Set.empty in + let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in + let set = add shelf set in + add given_up set diff --git a/proofs/proof.mli b/proofs/proof.mli index 33addf13d7..511dcc2e00 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -210,3 +210,6 @@ module V82 : sig (* Implements the Existential command *) val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end + +(* returns the set of all goals in the proof *) +val all_goals : t -> Goal.Set.t diff --git a/stm/stm.ml b/stm/stm.ml index 2e9bf71e49..635bf9bf31 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1231,9 +1231,22 @@ end = struct (* {{{ *) let get_prev_proof ~doc id = try - let did = fold_until back_tactic 1 id in - get_proof ~doc did - with Not_found -> None + let np = get_proof ~doc id in + match np with + | None -> None + | Some cp -> + let did = ref id in + let rv = ref np in + let done_ = ref false in + while not !done_ do + did := fold_until back_tactic 1 !did; + rv := get_proof ~doc !did; + done_ := match !rv with + | Some rv -> not (Goal.Set.equal (Proof.all_goals rv) (Proof.all_goals cp)) + | None -> true + done; + !rv + with Not_found | Proof_global.NoCurrentProof -> None end (* }}} *) diff --git a/stm/stm.mli b/stm/stm.mli index 7f70ea18da..1e5ceb7e23 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -111,7 +111,8 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* Returns the proof state before the last tactic that was applied at or before -the specified state. Used to compute proof diffs. *) +the specified state AND that has differences in the underlying proof (i.e., +ignoring proofview-only changes). Used to compute proof diffs. *) val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option (* [query at ?report_with cmd] Executes [cmd] at a given state [at], diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d536204ec3..95d545b046 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2690,6 +2690,34 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in (sigma, mkNamedLetIn id c t x) +let pose_tac na c = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let hyps = named_context_val env in + let concl = Proofview.Goal.concl gl in + let t = typ_of env sigma c in + let (sigma, t) = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in + let id = match na with + | Name id -> + let () = if mem_named_context_val id hyps then + user_err (str "Variable " ++ Id.print id ++ str " is already declared.") + in + id + | Anonymous -> + let id = id_of_name_using_hdchar env sigma t Anonymous in + next_ident_away_in_goal id (ids_of_named_context_val hyps) + in + Proofview.Unsafe.tclEVARS sigma <*> + Refine.refine ~typecheck:false begin fun sigma -> + let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in + let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in + let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in + let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in + (sigma, mkLetIn (Name id, c, t, body)) + end + end + let letin_tac with_eq id c ty occs = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 57f20d2ff2..c088e404b0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -390,6 +390,8 @@ val cut : types -> unit Proofview.tactic (** {6 Tactics for adding local definitions. } *) +val pose_tac : Name.t -> constr -> unit Proofview.tactic + val letin_tac : (bool * intro_pattern_naming) option -> Name.t -> constr -> types option -> clause -> unit Proofview.tactic diff --git a/test-suite/bugs/2428.v b/test-suite/bugs/closed/2428.v index a4f587a58d..b398a76d91 100644 --- a/test-suite/bugs/2428.v +++ b/test-suite/bugs/closed/2428.v @@ -5,6 +5,6 @@ Definition myFact := forall x, P x. Hint Extern 1 (P _) => progress (unfold myFact in *). Lemma test : (True -> myFact) -> P 3. -Proof. +Proof. intros. debug eauto. Qed. diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/closed/4623.v index 7ecfd98b67..7ecfd98b67 100644 --- a/test-suite/bugs/4623.v +++ b/test-suite/bugs/closed/4623.v diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/closed/4624.v index f5ce981cd0..f5ce981cd0 100644 --- a/test-suite/bugs/4624.v +++ b/test-suite/bugs/closed/4624.v diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/closed/7333.v index fba5b9029d..fba5b9029d 100644 --- a/test-suite/bugs/7333.v +++ b/test-suite/bugs/closed/7333.v diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v new file mode 100644 index 0000000000..229df93773 --- /dev/null +++ b/test-suite/bugs/closed/7754.v @@ -0,0 +1,21 @@ + +Set Universe Polymorphism. + +Module OK. + + Inductive one@{i j} : Type@{i} := + with two : Type@{j} := . + Check one@{Set Type} : Set. + Fail Check two@{Set Type} : Set. + +End OK. + +Module Bad. + + Fail Inductive one := + with two@{i +} : Type@{i} := . + + Fail Inductive one@{i +} := + with two@{i +} := . + +End Bad. diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v index 58ae5b8fb8..a724592749 100644 --- a/test-suite/success/ROmega4.v +++ b/test-suite/success/ROmega4.v @@ -3,12 +3,12 @@ See also #148 for the corresponding improvement in Omega. *) -Require Import ZArith ROmega. +Require Import ZArith Lia. Open Scope Z. Goal let x := 3 in x = 3. intros. -romega. +lia. Qed. (** Example seen in #4132 @@ -22,5 +22,5 @@ Lemma foo (H : - zxy' <= zxy) (H' : zxy' <= x') : - b <= zxy. Proof. -romega. +lia. Qed. diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune new file mode 100644 index 0000000000..8e05c7d97e --- /dev/null +++ b/tools/coqdoc/dune @@ -0,0 +1,6 @@ +(executable + (name main) + (public_name coqdoc) + (libraries str coq.config)) + +(ocamllex cpretty) diff --git a/tools/dune b/tools/dune index 2ba0e3fe8a..05a620fb07 100644 --- a/tools/dune +++ b/tools/dune @@ -10,6 +10,10 @@ (modules coq_makefile) (libraries coq.lib)) +(install + (section lib) + (files (CoqMakefile.in as tools/CoqMakefile.in))) + (executable (name coqdep) (public_name coqdep) @@ -19,6 +23,14 @@ (ocamllex coqdep_lexer) (executable + (name coqwc) + (public_name coqwc) + (modules coqwc) + (libraries)) + +(ocamllex coqwc) + +(executable (name coq_tex) (public_name coq_tex) (modules coq_tex) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index fb9d21c429..7b28895814 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -67,7 +67,6 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -348,13 +347,12 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations cum poly prv finite = +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; if not (List.is_empty uparamsl) && not (List.is_empty notations) then user_err (str "Inductives with uniform parameters may not have attached notations."); - let pl = (List.hd indl).ind_univs in - let sigma, decl = interp_univ_decl_opt env0 pl in + let sigma, udecl = interp_univ_decl_opt env0 udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = interp_context_evars env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = @@ -424,7 +422,7 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params arities constructors in - let uctx = Evd.check_univ_decl ~poly sigma decl in + let uctx = Evd.check_univ_decl ~poly sigma udecl in List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -478,8 +476,8 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template (paramsl,indl) notations cum poly prv finite = - interp_mutual_inductive_gen (Global.env()) ~template ([],paramsl,indl) notations cum poly prv finite +let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite = + interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -500,8 +498,8 @@ let extract_params indl = params let extract_inductive indl = - List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { - ind_name = indname; ind_univs = pl; + List.map (fun ({CAst.v=indname},_,ar,lc) -> { + ind_name = indname; ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl @@ -567,11 +565,11 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -let do_mutual_inductive ~template indl cum poly prv ~uniform finite = +let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in - let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template indl ntns cum poly prv finite in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 8a2c9b8719..f23085a538 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -24,7 +24,8 @@ type uniform_inductive_flag = | NonUniformParameters val do_mutual_inductive : - template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + template:bool option -> universe_decl_expr option -> + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> polymorphic -> private_flag -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit @@ -54,7 +55,6 @@ val should_auto_template : unit -> bool type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -69,6 +69,7 @@ val extract_mutual_inductive_declaration_components : (** Typing mutual inductive definitions *) val interp_mutual_inductive : - template:bool option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + template:bool option -> universe_decl_expr option -> structured_inductive_expr -> + decl_notation list -> cumulative_inductive_flag -> polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list diff --git a/vernac/record.ml b/vernac/record.ml index 7ab2b50764..724b6e62fe 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -628,7 +628,7 @@ let check_unique_names records = | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in let allnames = - List.fold_left (fun acc (_, id, _, _, cfs, _, _) -> + List.fold_left (fun acc (_, id, _, cfs, _, _) -> id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records in match List.duplicates Id.equal allnames with @@ -637,19 +637,19 @@ let check_unique_names records = let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - let has_priority (_, _, _, _, cfs, _, _) = + let has_priority (_, _, _, cfs, _, _) = List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs in if isnot_class && List.exists has_priority records then user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = - let map (is_coe, id, _, _, cfs, idbuild, s) = + let map (is_coe, id, _, cfs, idbuild, s) = let fs = List.map (fun (((_, f), _), _) -> f) cfs in id.CAst.v, s, List.map snd cfs, fs in let data = List.map map records in - let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in + let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in let ps = match pss with | [] -> CErrors.anomaly (str "Empty record block") | ps :: rem -> @@ -661,30 +661,28 @@ let extract_record_data records = in ps in - (** FIXME: Same issue as #7754 *) - let _, _, pl, _, _, _, _ = List.hd records in - pl, ps, data + ps, data (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure kind ~template cum poly finite records = +let definition_structure udecl kind ~template cum poly finite records = let () = check_unique_names records in let () = check_priorities kind records in - let pl, ps, data = extract_record_data records in - let pl, univs, auto_template, params, implpars, data = + let ps, data = extract_record_data records in + let ubinders, univs, auto_template, params, implpars, data = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in + typecheck_params_and_fields finite (kind = Class true) poly udecl ps data) () in let template = template, auto_template in match kind with | Class def -> - let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with | [r], [d] -> r, d | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") in let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - declare_class finite def cum pl univs id.CAst.v idbuild + declare_class finite def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in @@ -699,11 +697,11 @@ let definition_structure kind ~template cum poly finite records = | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) = + let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in - let inds = declare_structure finite pl univs implpars params template data in + let inds = declare_structure finite ubinders univs implpars params template data in List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index 055a17895a..953d5ec3b6 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,12 +26,11 @@ val declare_projections : (Name.t * bool) list * Constant.t option list val definition_structure : - inductive_kind -> template:bool option -> + universe_decl_expr option -> inductive_kind -> template:bool option -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Declarations.recursivity_kind -> (coercion_flag * Names.lident * - universe_decl_expr option * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option) list -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 28abd1e6ef..015d5fabef 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -555,9 +555,9 @@ let should_treat_as_uniform () = then ComInductive.UniformParameters else ComInductive.NonUniformParameters -let vernac_record ~template cum k poly finite records = +let vernac_record ~template udecl cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in - let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = + let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with | None -> add_prefix "Build_" id.v | Some lid -> @@ -574,10 +574,22 @@ let vernac_record ~template cum k poly finite records = in List.iter iter cfs in - coe, id, pl, binders, cfs, const, sort + coe, id, binders, cfs, const, sort in let records = List.map map records in - ignore(Record.definition_structure ~template k is_cumulative poly finite records) + ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records) + +let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = + match indl with + | [] -> assert false + | (((coe,(id,udecl)),b,c,k,d),e) :: rest -> + let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) -> + if Option.has_some udecl + then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.") + else (((coe,id),b,c,k,d),e)) + rest + in + udecl, (((coe,id),b,c,k,d),e) :: rest (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] @@ -585,8 +597,9 @@ let vernac_record ~template cum k poly finite records = neither. *) let vernac_inductive ~atts cum lo finite indl = let open Pp in + let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then - List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> + List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> match cstrs with | Constructors cstrs -> Dumpglob.dump_definition lid false "ind"; @@ -594,6 +607,7 @@ let vernac_inductive ~atts cum lo finite indl = Dumpglob.dump_definition lid false "constr") cstrs | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let is_record = function | ((_ , _ , _ , _, RecordDecl _), _) -> true | _ -> false @@ -613,7 +627,7 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in - vernac_record ~template cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (** Mutual record case *) let check_kind ((_, _, _, kind, _), _) = match kind with @@ -636,7 +650,7 @@ let vernac_inductive ~atts cum lo finite indl = let ((_, _, _, kind, _), _) = List.hd indl in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - vernac_record ~template cum kind atts.polymorphic finite recordl + vernac_record ~template udecl cum kind atts.polymorphic finite recordl else if List.for_all is_constructor indl then (** Mutual inductive case *) let check_kind ((_, _, _, kind, _), _) = match kind with @@ -662,7 +676,7 @@ let vernac_inductive ~atts cum lo finite indl = let indl = List.map unpack indl in let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template indl is_cumulative atts.polymorphic lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ea69ed59a3..0c0204a728 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -202,7 +202,7 @@ type inductive_expr = constructor_list_or_record_decl_expr type one_inductive_expr = - ident_decl * local_binder_expr list * constr_expr option * constructor_expr list + lident * local_binder_expr list * constr_expr option * constructor_expr list type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr and typeclass_context = typeclass_constraint list |