diff options
122 files changed, 1779 insertions, 2050 deletions
diff --git a/.gitignore b/.gitignore index b665b2f86d..adbf9dd189 100644 --- a/.gitignore +++ b/.gitignore @@ -184,11 +184,6 @@ plugins/ssr/ssrvernac.ml META.coq # Files automatically generated by Dune. -plugins/*/dune -theories/*/dune -theories/*/*/dune -theories/*/*/*/dune -/user-contrib/Ltac2/dune *.install !Makefile.install diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index caed21f5c3..837636cbb3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-03-27-V12" + CACHEKEY: "bionic_coq-V2020-03-13-V69" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -105,6 +105,7 @@ before_script: script: # flambda can be pretty stack hungry, specially with -O3 # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244 + # and https://github.com/coq/coq/pull/11916#issuecomment-609977375 - ulimit -s 16384 - set -e - make -f Makefile.dune world @@ -667,8 +668,11 @@ library:ci-cross-crypto: library:ci-fcsl-pcm: extends: .ci-template +# We cannot use flambda due to +# https://github.com/ocaml/ocaml/issues/7842, see +# https://github.com/coq/coq/pull/11916#issuecomment-609977375 library:ci-fiat-crypto: - extends: .ci-template-flambda + extends: .ci-template stage: stage-4 needs: - build:edge+flambda diff --git a/.ocamlformat b/.ocamlformat index 4480935e3b..62e609fb55 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.13.0 +version=0.14.0 profile=ocamlformat # to enable a whole directory, put "disable=false" in dir/.ocamlformat @@ -11,4 +11,4 @@ cases-exp-indent=2 field-space=loose exp-grouping=preserve break-cases=fit -doc-comments=before +doc-comments-val=before diff --git a/Makefile.doc b/Makefile.doc index 9da175f0e5..effd624cff 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -248,7 +248,7 @@ PLUGIN_MLGS := $(wildcard plugins/*/*.mlg) OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) -DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) +DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst) doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS) $(SHOW)'DOC_GRAM' diff --git a/Makefile.dune b/Makefile.dune index b77e78db69..b002c7709d 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,122 +1,109 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help voboot states world watch check # Main developer targets -.PHONY: coq coqide coqide-server # Package targets -.PHONY: quickbyte quickopt quickide # Partial / quick developer targets +.PHONY: help states world watch check # Main developer targets .PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets -.PHONY: test-suite release # Accessory targets +.PHONY: test-suite .PHONY: fmt ocheck ireport clean # Maintenance targets +.PHONY: voboot release install # Added just not to break old scripts # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short -BOOT_DIR=_build_boot -BOOT_CONTEXT=$(BOOT_DIR)/default - help: - @echo "Welcome to Coq's Dune-based build system. Targets are:" + @echo "Welcome to Coq's Dune-based build system. Common developer targets are:" @echo "" @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - world: build all public binaries and libraries" + @echo " - watch: build all public binaries and libraries [continuous build]" @echo " - check: build all ML files as fast as possible" + @echo " - test-suite: run Coq's test suite" @echo "" - @echo " - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]" - @echo " - coqide-server: build package coqide-server [XML protocol language server]" - @echo " - coqide: build package CoqIDE [gtk application]" + @echo " Note: these targets produce a developer build," + @echo " not suitable for distribution to end-users" @echo "" - @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" - @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" - @echo " - quickide: build main IDE files [client + server + prelude] using the optimizing compiler" + @echo " Documentation targets:" @echo "" - @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" - @echo " - release: build Coq in release mode" + @echo "" + @echo " Miscellaneous targets:" @echo "" @echo " - fmt: run ocamlformat on the codebase" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" + @echo "" + @echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:" + @echo "" + @echo " - use 'dune exec -- dev/shim/app-prelude args'" + @echo "" + @echo " Provided opam/dune packages are:" + @echo "" + @echo " - coq: base Coq package, toplevel compilers, tools, stdlib, no GTK" + @echo " - coqide-server: XML protocol language server" + @echo " - coqide: CoqIDE gtk application" + @echo "" + @echo " To build a package, you can use:" + @echo "" + @echo " - 'dune build package.install' : build package in developer mode" + @echo " - 'dune build -p package' : build package in release mode" + @echo "" + @echo " Packages _must_ be installed using release mode, use: 'dune install -p package'" + @echo " See Dune documentation for more information." -# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work. -plugins/ltac/dune: - @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune - -voboot: plugins/ltac/dune - dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps - dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d +voboot: + @echo "This target is empty and not needed anymore" -states: voboot - dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude +states: + dune build $(DUNEOPT) dev/shim/coqtop-prelude NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install -world: voboot +world: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -coq: voboot - dune build $(DUNEOPT) coq.install - -coqide: voboot - dune build $(DUNEOPT) coqide.install - -coqide-server: voboot - dune build $(DUNEOPT) coqide-server.install - -watch: voboot +watch: dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w -check: voboot +check: dune build $(DUNEOPT) @check -COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc -PLUGIN_FILES=$(wildcard plugins/*/*.mlpack) -PRINTER_FILES=dev/top_printers.cma -QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc -QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe - -quickbyte: voboot - dune build $(DUNEOPT) $(QUICKBYTE_TARGETS) - -quickopt: voboot - dune build $(DUNEOPT) $(QUICKOPT_TARGETS) - -quickide: states - dune build $(DUNEOPT) dev/shim/coqide-prelude - -test-suite: voboot +test-suite: dune runtest --no-buffer $(DUNEOPT) -refman-html: voboot +refman-html: dune build @refman-html -refman-pdf: voboot +refman-pdf: dune build @refman-pdf -stdlib-html: voboot +stdlib-html: dune build @stdlib-html -apidoc: voboot +apidoc: dune build $(DUNEOPT) @doc -release: voboot +release: + @echo "release target is deprecated, use dune directly" dune build $(DUNEOPT) -p coq -fmt: voboot +# We define this target as to override Make's built-in one +install: + @echo "To install Coq using dune, use 'dune install -p PACKAGE' where" + @echo "PACKAGE is any of the packages defined by opam files in the root dira" + +fmt: dune build @fmt --auto-promote -ocheck: voboot +ocheck: dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all ireport: dune clean - dune build --build-dir=$(BOOT_DIR) $(DUNEOPT) @vodeps - dune exec --build-dir=$(BOOT_DIR) -- ./tools/coq_dune.exe $(BOOT_CONTEXT)/.vfiles.d dune build $(DUNEOPT) @install --profile=ireport clean: diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 0bc30f0196..770cc5193e 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -6,37 +6,37 @@ variables: NJOBS: "2" jobs: -- job: Windows - pool: - vmImage: 'vs2017-win2016' +#- job: Windows +# pool: +# vmImage: 'vs2017-win2016' - steps: - - checkout: self - fetchDepth: 10 +# steps: +# - checkout: self +# fetchDepth: 10 # cygwin package list not checked for minimality - - script: | - powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" - SET CYGROOT=C:\cygwin64 - SET CYGCACHE=%CYGROOT%\var\cache\setup - setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3 - - SET TARGET_ARCH=x86_64-w64-mingw32 - SET CD_MFMT=%cd:\=/% - SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% - C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh - displayName: 'Install cygwin' - env: - CYGMIRROR: "http://mirror.easyname.at/cygwin" - - - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh - displayName: 'Install opam' - - - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh - displayName: 'Build Coq' - - - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh - displayName: 'Test Coq' +# - script: | +# powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" +# SET CYGROOT=C:\cygwin64 +# SET CYGCACHE=%CYGROOT%\var\cache\setup +# setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3 + +# SET TARGET_ARCH=x86_64-w64-mingw32 +# SET CD_MFMT=%cd:\=/% +# SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/% +# C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh +# displayName: 'Install cygwin' +# env: +# CYGMIRROR: "http://mirror.easyname.at/cygwin" + +# - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh +# displayName: 'Install opam' + +# - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh +# displayName: 'Build Coq' + +# - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh +# displayName: 'Test Coq' - job: macOS pool: @@ -22,13 +22,12 @@ version: "dev" depends: [ "ocaml" { >= "4.05.0" } - "dune" { >= "2.0.0" } + "dune" { >= "2.5.0" } "ocamlfind" { build } "num" ] build: [ [ "./configure" "-prefix" prefix ] - [ "make" "-f" "Makefile.dune" "voboot" ] [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 0c8733c75a..e240ea3ba1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-03-27-V12" +# CACHEKEY: "bionic_coq-V2020-03-13-V69" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. -RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam +RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # 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.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.10.2" @@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" + BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0506216541..8b0bf216e3 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by the make-based system. -If you want to build the standard libraries and plugins you should -call `make -f Makefile.dune voboot`. It is usually enough to do that -once per-session. - More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. @@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and `coqide` in a fast build. In order to use them, do: ``` -$ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` @@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors: ## Dropping from coqtop: -After doing `make -f Makefile.dune voboot`, the following commands should work: +The following commands should work: ``` dune exec -- dev/shim/coqbyte-prelude > Drop. diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index b8a696ef21..fb84155392 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; - sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; + url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz"; + sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p"; }) diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 633913aac6..448e224f2e 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -16,6 +16,15 @@ then 1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting." fi +# Verify that the version of ocamlformat matches the one in .ocamlformat +# The following command will print an error message if that's not the case +# (and will print nothing if the versions match) +if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null +then + 1>&2 echo "Warning: Cannot check formatting." + ocamlformat=true +fi + 1>&2 echo "Auto fixing whitespace and formatting issues..." # We fix whitespace in the index and in the working tree @@ -43,7 +52,7 @@ if [ -s "$index" ]; then git apply --cached --whitespace=fix "$index" git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null git add -u 1>&2 echo #newline fi @@ -59,7 +68,7 @@ if [ -s "$tree" ]; then 1>&2 echo "Fixing unstaged changes..." git apply --whitespace=fix "$tree" git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null 1>&2 echo #newline fi diff --git a/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst b/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst new file mode 100644 index 0000000000..47e7be4d0e --- /dev/null +++ b/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst @@ -0,0 +1,6 @@ +- **Added:** + New Ltac2 function ``Fresh.Free.of_goal`` to return the list of + names of declarations of the current goal; new Ltac2 function + ``Fresh.in_goal`` to return a variable fresh in the current goal + (`#11882 <https://github.com/coq/coq/pull/11882>`_, + by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst new file mode 100644 index 0000000000..7bcbb9a8e3 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst @@ -0,0 +1,3 @@ +- **Added:** Support for universe bindings and universe contrainsts in + :cmd:`Let` definitions (`#11534 + <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann). diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst new file mode 100644 index 0000000000..affb685fcb --- /dev/null +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -0,0 +1,5 @@ +- **Removed:** + Confusingly-named and deprecated since 8.11 `-require` option. + Use the equivalent `-require-import` instead + (`#12005 <https://github.com/coq/coq/pull/12005>`_, + by Théo Zimmermann). diff --git a/doc/changelog/08-tools/12006-issue5632.rst b/doc/changelog/08-tools/12006-issue5632.rst new file mode 100644 index 0000000000..162d56b1b6 --- /dev/null +++ b/doc/changelog/08-tools/12006-issue5632.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Makefile`` generated by ``coq_makefile`` erases ``.lia.cache`` and ``.nia.cache`` by ``make cleanall``. + (`#12006 <https://github.com/coq/coq/pull/12006>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/11909-fix-≡-level.rst b/doc/changelog/10-standard-library/11909-fix-≡-level.rst new file mode 100644 index 0000000000..96551be537 --- /dev/null +++ b/doc/changelog/10-standard-library/11909-fix-≡-level.rst @@ -0,0 +1,7 @@ +- **Changed:** + The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70, + no associativity, in line with :g:`=`. Note that this is a minor + incompatibility with developments that declare their own :g:`≡` + notation and import ``Int63`` (fixes `#11905 + <https://github.com/coq/coq/issues/11905>`_, `#11909 + <https://github.com/coq/coq/pull/11909>`_, by Jason Gross). diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 1f33775a01..cfaa681d20 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -257,7 +257,7 @@ Activating the Printing of Coercions :name: Printing Coercion 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. + :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. .. _coercions-classes-as-records: diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index d380d83d6c..928378f55e 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -112,13 +112,13 @@ You can override the display format for specified types by adding entries to the :name: Printing Record 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` and :cmd:`Remove` commands to update the set of qualids. .. table:: Printing Constructor @qualid :name: Printing Constructor 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. + :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. This syntax can also be used for pattern matching. diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 9ad8df2b1b..df50dbafe3 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -72,7 +72,7 @@ Sections create local contexts which can be shared across multiple definitions. Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which appear inside a section are canceled when the section is closed. -.. cmd:: Let @ident @def_body +.. cmd:: Let @ident_decl @def_body Let Fixpoint @fix_definition {* with @fix_definition } Let CoFixpoint @cofix_definition {* with @cofix_definition } :name: Let; Let Fixpoint; Let CoFixpoint diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index fb762a00f1..36ce2fdd25 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -273,14 +273,14 @@ Declaring Implicit Arguments .. prodn:: smart_qualid ::= @qualid | @by_notation - by_notation ::= @string {? % @ident } + by_notation ::= @string {? % @scope } argument_spec_block ::= @argument_spec | / | & - | ( {+ @argument_spec } ) {? % @ident } - | [ {+ @argument_spec } ] {? % @ident } - | %{ {+ @argument_spec } %} {? % @ident } - argument_spec ::= {? ! } @name {? % @ident } + | ( {+ @argument_spec } ) {? % @scope } + | [ {+ @argument_spec } ] {? % @scope } + | %{ {+ @argument_spec } %} {? % @scope } + argument_spec ::= {? ! } @name {? % @scope } more_implicits_block ::= @name | [ {+ @name } ] | %{ {+ @name } %} diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index a859aa46eb..78b1f02383 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -238,7 +238,7 @@ written using the first destructuring let syntax. 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. + Use the :cmd:`Add` and :cmd:`Remove` commands to update this set. Printing matching on booleans @@ -252,7 +252,7 @@ which types are written this way: :name: Printing If Specifies a set of qualids for which pattern matching is displayed using - ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add` and :cmd:`Remove` commands to update this set. This example emphasizes what the printing settings offer. @@ -719,7 +719,7 @@ accessible, absolute names can never be hidden. Locate nat. -.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`. +.. seealso:: Commands :cmd:`Locate`. .. _libraries-and-filesystem: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index f4592f8f37..ccb236a174 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -161,7 +161,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. one_term ::= @term1 | @ @qualid {? @univ_annot } term1 ::= @term_projection - | @term0 % @ident + | @term0 % @scope | @term0 term0 ::= @qualid {? @univ_annot } | @sort @@ -373,12 +373,10 @@ the propositional implication and function types. Applications ------------ -The expression :n:`@term__fun @term` denotes the application of -:n:`@term__fun` (which is expected to have a function type) to -:token:`term`. +:n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`. -The expression :n:`@term__fun {+ @term__i }` denotes the application -of the term :n:`@term__fun` to the arguments :n:`@term__i`. It is +:n:`@term__fun {+ @term__i }` denotes applying +:n:`@term__fun` to the arguments :n:`@term__i`. It is equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: associativity is to the left. @@ -458,7 +456,7 @@ Definition by cases: match pattern10 ::= @pattern1 as @name | @pattern1 {* @pattern1 } | @ @qualid {* @pattern1 } - pattern1 ::= @pattern0 % @ident + pattern1 ::= @pattern0 % @scope | @pattern0 pattern0 ::= @qualid | %{%| {* @qualid := @pattern } %|%} @@ -636,13 +634,18 @@ co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When The Vernacular ============== -.. insertprodn vernacular vernacular +.. insertprodn vernacular sentence .. prodn:: - vernacular ::= {* {? @all_attrs } {| @command | @ltac_expr } . } - -The top-level input to |Coq| is a series of :production:`command`\s and :production:`tactic`\s, -each terminated with a period + vernacular ::= {* @sentence } + sentence ::= {? @all_attrs } @command . + | {? @all_attrs } {? @num : } @query_command . + | {? @all_attrs } {? @toplevel_selector } @ltac_expr {| . | ... } + | @control_command + +The top-level input to |Coq| is a series of :n:`@sentence`\s, +which are :production:`tactic`\s or :production:`command`\s, +generally terminated with a period and optionally decorated with :ref:`gallina-attributes`. :n:`@ltac_expr` syntax supports both simple and compound tactics. For example: ``split`` is a simple tactic while ``split; auto`` combines two simple tactics. @@ -718,7 +721,7 @@ has type :n:`@type`. :name: @ident already exists. (Axiom) :undocumented: -.. warn:: @ident is declared as a local axiom [local-declaration,scope] +.. warn:: @ident is declared as a local axiom Warning generated when using :cmd:`Variable` or its equivalent instead of :n:`Local Parameter` or its equivalent. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index aa4b6edd7d..545bba4930 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -164,6 +164,8 @@ and ``coqtop``, unless stated otherwise: it is executed. :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This is equivalent to running :cmd:`Require` :n:`qualid`. +:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is equivalent to running :cmd:`Require Import` :n:`@qualid`. :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. @@ -172,7 +174,6 @@ and ``coqtop``, unless stated otherwise: This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. -:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only @@ -379,7 +380,7 @@ Compiled libraries checker (coqchk) ---------------------------------------- The ``coqchk`` command takes a list of library paths as argument, described either -by their logical name or by their physical filename, hich must end in ``.vo``. The +by their logical name or by their physical filename, which must end in ``.vo``. The corresponding compiled libraries (``.vo`` files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type checked. The effect of ``coqchk`` is only to return with diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index d61e5ddce7..921c7bbbf7 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -42,6 +42,8 @@ As of today it is possible to build Coq projects using two tools: - coq_makefile, which is distributed by Coq and is based on generating a makefile, - Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries. +.. _coq_makefile: + Building a |Coq| project with coq_makefile ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b2b426ada5..62708b01ed 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -258,6 +258,9 @@ following form: Goal selectors ~~~~~~~~~~~~~~ +.. todo: mention this applies to Print commands and the Info command + + We can restrict the application of a tactic to a subset of the currently focused goals with: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 03eebc32f9..3b5233502d 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -41,8 +41,8 @@ terms are called *proof terms*. .. _proof-editing-mode: -Switching on/off the proof editing mode -------------------------------------------- +Entering and leaving proof editing mode +--------------------------------------- The proof editing mode is entered by asserting a statement, which typically is the assertion of a theorem using an assertion command like :cmd:`Theorem`. The diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 19573eee43..6a280b74c2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -51,6 +51,11 @@ specified, the default selector is used. tactic_invocation : `toplevel_selector` : `tactic`. : `tactic`. +.. todo: fully describe selectors. At the moment, ltac has a fairly complete description + +.. todo: mention selectors can be applied to some commands, such as + Check, Search, SearchHead, SearchPattern, SearchRewrite. + .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -3032,8 +3037,8 @@ following: For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. -.. tacn:: cbv {* @flag} - lazy {* @flag} +.. tacn:: {? @strategy_flag } + lazy {? @strategy_flag } :name: cbv; lazy These parameterized reduction tactics apply to any goal and perform diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index b22c5286fe..7d031b9b7a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -6,18 +6,28 @@ Vernacular commands .. _displaying: Displaying --------------- +---------- .. _Print: -.. cmd:: Print @qualid - :name: Print +.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list } + + .. insertprodn univ_name_list univ_name_list + + .. prodn:: + univ_name_list ::= @%{ {* @name } %} - This command displays on the screen information about the declared or - defined object referred by :n:`@qualid`. + Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`. - Error messages: + * :n:`Term` - a syntactic marker to allow printing a term + that is the same as one of the various :n:`Print` commands. For example, + :cmd:`Print All` is a different command, while :n:`Print Term All` shows + information on the object whose name is ":n:`All`". + + * :n:`@univ_name_list` - locally renames the + polymorphic universes of :n:`@smart_qualid`. + The name `_` means the usual name is printed. .. exn:: @qualid not a defined object. :undocumented: @@ -29,48 +39,22 @@ Displaying :undocumented: - .. cmdv:: Print Term @qualid - :name: Print Term - - This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid` - denotes a global constant. - - .. cmdv:: Print {? Term } @qualid\@@name - - This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the usual name is printed. - - -.. cmd:: About @qualid - :name: About - - This displays various information about the object - denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive, - constructor, abbreviation, …), long name, type, implicit arguments and - argument scopes. It does not print the body of definitions or proofs. - - .. cmdv:: About @qualid\@@name - - This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the usual name is printed. - - .. cmd:: Print All This command displays information about the current state of the environment, including sections and modules. - .. cmdv:: Inspect @num - :name: Inspect +.. cmd:: Inspect @num - This command displays the :n:`@num` last objects of the - current environment, including sections and modules. + This command displays the :n:`@num` last objects of the + current environment, including sections and modules. - .. cmdv:: Print Section @ident +.. cmd:: Print Section @qualid - The name :n:`@ident` should correspond to a currently open section, - this command displays the objects defined since the beginning of this - section. + Displays the objects defined since the beginning of the section named :n:`@qualid`. + + .. todo: "A.B" is permitted but unnecessary for modules/sections. + should the command just take an @ident? .. _flags-options-tables: @@ -81,9 +65,9 @@ Flags, Options and Tables Coq has many settings to control its behavior. Setting types include flags, options and tables: -* 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. +* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`. +* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A *table* contains a set of strings or qualids. * In addition, some commands provide settings, such as :cmd:`Extraction Language`. .. FIXME Convert "Extraction Language" to an option. @@ -91,68 +75,64 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: Set @flag +.. cmd:: Set @setting_name {? {| @int | @string } } :name: Set - Sets :token:`flag` on. + .. insertprodn setting_name setting_name -.. cmd:: Unset @flag - :name: Unset + .. prodn:: + setting_name ::= {+ @ident } - Sets :token:`flag` off. + If :n:`@setting_name` is a flag, no value may be provided; the flag + is set to on. + If :n:`@setting_name` is an option, a value of the appropriate type + must be provided; the option is set to the specified value. -.. cmd:: Test @flag + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here <set_unset_scope_qualifiers>`. - Prints the current value of :token:`flag`. + .. warn:: There is no option @setting_name. + This message also appears for unknown flags. -.. cmd:: Set @option {| @num | @string } - :name: Set @option - - Sets :token:`option` to the specified value. - -.. cmd:: Unset @option - :name: Unset @option - - Sets :token:`option` to its default value. - -.. cmd:: Test @option - - Prints the current value of :token:`option`. - -.. cmd:: Print Options +.. cmd:: Unset @setting_name + :name: Unset - Prints the current value of all flags and options, and the names of all tables. + If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is + set to its default value. + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: Add @table {| @string | @qualid } - :name: Add @table +.. cmd:: Add @setting_name {+ {| @qualid | @string } } - Adds the specified value to :token:`table`. + Adds the specified values to the table :n:`@setting_name`. -.. cmd:: Remove @table {| @string | @qualid } - :name: Remove @table +.. cmd:: Remove @setting_name {+ {| @qualid | @string } } - Removes the specified value from :token:`table`. + Removes the specified value from the table :n:`@setting_name`. -.. cmd:: Test @table for {| @string | @qualid } - :name: Test @table for +.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } } - Reports whether :token:`table` contains the specified value. + If :n:`@setting_name` is a flag or option, prints its current value. + If :n:`@setting_name` is a table: if the `for` clause is specified, reports + whether the table contains each specified value, otherise this is equivalent to + :cmd:`Print Table`. The `for` clause is not valid for flags and options. -.. cmd:: Print Table @table - :name: Print Table @table +.. cmd:: Print Options - Prints the values in :token:`table`. + Prints the current value of all flags and options, and the names of all tables. -.. cmd:: Test @table +.. cmd:: Print Table @setting_name - A synonym for :cmd:`Print Table @table`. + Prints the values in the table :n:`@setting_name`. .. cmd:: Print Tables A synonym for :cmd:`Print Options`. +.. _set_unset_scope_qualifiers: + Locality attributes supported by :cmd:`Set` and :cmd:`Unset` ```````````````````````````````````````````````````````````` @@ -185,194 +165,128 @@ Newly opened modules and sections inherit the current settings. arguments ``-set`` and ``-unset`` for setting flags and options (cf. :ref:`command-line-options`). -.. _requests-to-the-environment: +Query commands +-------------- -Requests to the environment -------------------------------- +Unlike other commands, :production:`query_command`\s may be prefixed with +a goal selector (:n:`@num:`) to specify which goal context it applies to. +If no selector is provided, +the command applies to the current goal. If no proof is open, then the command only applies +to accessible objects. (see Section :ref:`invocation-of-tactics`). -.. cmd:: Check @term +.. cmd:: About @smart_qualid {? @univ_name_list } - This command displays the type of :n:`@term`. When called in proof mode, the - term is checked in the local context of the current subgoal. - - .. cmdv:: @selector: Check @term + Displays information about the :n:`@smart_qualid` object, which, + if a proof is open, may be a hypothesis of the selected goal, + or an accessible theorem, axiom, etc.: + its kind (module, constant, assumption, inductive, + constructor, abbreviation, …), long name, type, implicit arguments and + argument scopes. It does not print the body of definitions or proofs. - This variant specifies on which subgoal to perform typing - (see Section :ref:`invocation-of-tactics`). +.. cmd:: Check @term + Displays the type of :n:`@term`. When called in proof mode, the + term is checked in the local context of the selected goal. .. cmd:: Eval @red_expr in @term - This command performs the specified reduction on :n:`@term`, and displays - the resulting term with its type. The term to be reduced may depend on - hypothesis introduced in the first subgoal (if a proof is in - progress). + Performs the specified reduction on :n:`@term` and displays + the resulting term with its type. If a proof is open, :n:`@term` + may reference hypotheses of the selected goal. .. seealso:: Section :ref:`performingcomputations`. .. cmd:: Compute @term - This command performs a call-by-value evaluation of term by using the - bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in`` - :n:`@term`. + Evaluates :n:`@term` using the bytecode-based virtual machine. + It is a shortcut for :cmd:`Eval` :n:`vm_compute in @term`. .. seealso:: Section :ref:`performingcomputations`. +.. cmd:: Search {+ {? - } @search_item } {? {| inside | outside } {+ @qualid } } -.. cmd:: Print Assumptions @qualid - - This commands display all the assumptions (axioms, parameters and - variables) a theorem or definition depends on. Especially, it informs - on the assumptions with respect to which the validity of a theorem - relies. - - .. cmdv:: Print Opaque Dependencies @qualid - :name: Print Opaque Dependencies - - Displays the set of opaque constants :n:`@qualid` relies on in addition to - the assumptions. - - .. cmdv:: Print Transparent Dependencies @qualid - :name: Print Transparent Dependencies - - Displays the set of transparent constants :n:`@qualid` relies on - in addition to the assumptions. - - .. cmdv:: Print All Dependencies @qualid - :name: Print All Dependencies - - Displays all assumptions and constants :n:`@qualid` relies on. - - -.. cmd:: Search @qualid - - This command displays the name and type of all objects (hypothesis of - the current goal, theorems, axioms, etc) of the current context whose - statement contains :n:`@qualid`. This command is useful to remind the user - of the name of library lemmas. - - .. exn:: The reference @qualid was not found in the current environment. - - There is no constant in the environment named qualid. - - .. cmdv:: Search @string - - If :n:`@string` is a valid identifier, this command - displays the name and type of all objects (theorems, axioms, etc) of - the current context whose name contains string. If string is a - notation’s string denoting some reference :n:`@qualid` (referred to by its - main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or - `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`. - - .. cmdv:: Search @string%@ident - - The string string must be a notation or the main - symbol of a notation which is then interpreted in the scope bound to - the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`). - - .. cmdv:: Search @term_pattern + .. insertprodn search_item search_item - This searches for all statements or types of - definition that contains a subterm that matches the pattern - :token:`term_pattern` (holes of the pattern are either denoted by `_` or by - :n:`?@ident` when non linear patterns are expected). + .. prodn:: + search_item ::= @one_term + | @string {? % @scope } - .. cmdv:: Search {+ {? -}@term_pattern_string} + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context + matching :n:`@search_item`\s. + It's useful for finding the names of library lemmas. - where - :n:`@term_pattern_string` is a term_pattern, a string, or a string followed - by a scope delimiting key `%key`. This generalization of ``Search`` searches - for all objects whose statement or type contains a subterm matching - :n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference - qualid) and whose name contains all string of the request that - correspond to valid identifiers. If a term_pattern or a string is - prefixed by `-`, the search excludes the objects that mention that - term_pattern or that string. + * :n:`@one_term` - Search for objects containing a subterm matching the pattern + :n:`@one_term` in which holes of the pattern are indicated by `_` or :n:`?@ident`. + If the same :n:`?@ident` occurs more than once in the pattern, all occurrences must + match the same value. - .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid } + * :n:`@string` - If :n:`@string` is a substring of a valid identifier, + search for objects whose name contains :n:`@string`. If :n:`@string` is a notation + string associated with a :n:`@qualid`, that's equivalent to :cmd:`Search` :n:`@qualid`. + For example, specifying `"+"` or `"_ + _"`, which are notations for `Nat.add`, are equivalent + to :cmd:`Search` `Nat.add`. - This restricts the search to constructions defined in the modules - named by the given :n:`qualid` sequence. + * :n:`% @scope` - limits the search to the scope bound to + the delimiting key :n:`@scope`, such as, for example, :n:`%nat`. + This clause may be used only if :n:`@string` contains a notation string. + (see Section :ref:`LocalInterpretationRulesForNotations`) - .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid } + If you specify multiple :n:`@search_item`\s, all the conditions must be satisfied + for the object to be displayed. The minus sign `-` excludes objects that contain + the :n:`@search_item`. - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. + Additional clauses: - .. cmdv:: @selector: Search {+ {? -}@term_pattern_string} + * :n:`inside {+ @qualid }` - limit the search to the specified modules + * :n:`outside {+ @qualid }` - exclude the specified modules from the search - This specifies the goal on which to search hypothesis (see - Section :ref:`invocation-of-tactics`). - By default the 1st goal is searched. This variant can - be combined with other variants presented here. + .. exn:: Module/section @qualid not found. - .. example:: + There is no constant in the environment named :n:`@qualid`, where :n:`@qualid` + is in an `inside` or `outside` clause. - .. coqtop:: in + .. example:: :cmd:`Search` examples - Require Import ZArith. + .. coqtop:: in - .. coqtop:: all + Require Import ZArith. - Search Z.mul Z.add "distr". + .. coqtop:: all - Search "+"%Z "*"%Z "distr" -positive -Prop. + Search Z.mul Z.add "distr". + Search "+"%Z "*"%Z "distr" -Prop. + Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - Search (?x * _ + ?x * _)%Z outside OmegaLemmas. +.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } } -.. cmd:: SearchHead @term + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context that have the + form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term` + matches a prefix of `C`. For example, a :n:`@one_term` of `f _ b` + matches `f a b`, which is a prefix of `C` when `C` is `f a b c`. - This command displays the name and type of all hypothesis of the - current goal (if any) and theorems of the current context whose - statement’s conclusion has the form `(term t1 .. tn)`. This command is - useful to remind the user of the name of library lemmas. + See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - .. example:: + .. example:: :cmd:`SearchHead` examples .. coqtop:: reset all SearchHead le. - SearchHead (@eq bool). - .. cmdv:: SearchHead @term inside {+ @qualid } - - This restricts the search to constructions defined in the modules named - by the given :n:`qualid` sequence. - - .. cmdv:: SearchHead @term outside {+ @qualid } - - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. - - .. exn:: Module/section @qualid not found. - - No module :n:`@qualid` has been required (see Section :ref:`compiled-files`). - - .. cmdv:: @selector: SearchHead @term - - This specifies the goal on which to - search hypothesis (see Section :ref:`invocation-of-tactics`). - By default the 1st goal is searched. This variant can be combined - with other variants presented here. +.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } } - .. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``. + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context + ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern + :n:`@one_term`. + See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. -.. cmd:: SearchPattern @term - - This command displays the name and type of all hypothesis of the - current goal (if any) and theorems of the current context whose - statement’s conclusion or last hypothesis and conclusion matches the - expressionterm where holes in the latter are denoted by `_`. - It is a variant of :n:`Search @term_pattern` that does not look for subterms - but searches for statements whose conclusion has exactly the expected - form, or whose statement finishes by the given series of - hypothesis/conclusion. - - .. example:: + .. example:: :cmd:`SearchPattern` examples .. coqtop:: in @@ -381,123 +295,118 @@ Requests to the environment .. coqtop:: all SearchPattern (_ + _ = _ + _). - SearchPattern (nat -> bool). - SearchPattern (forall l : list _, _ l l). - Patterns need not be linear: you can express that the same expression - must occur in two places by using pattern variables `?ident`. - - - .. example:: - .. coqtop:: all SearchPattern (?X1 + _ = _ + ?X1). - .. cmdv:: SearchPattern @term inside {+ @qualid } +.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } } - This restricts the search to constructions defined in the modules - named by the given :n:`qualid` sequence. + Displays the name and type of all hypotheses of the + selected goal (if any) and theorems of the current context that have the form + :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term` + matches either `LHS` or `RHS`. - .. cmdv:: SearchPattern @term outside {+ @qualid } + See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. + .. example:: :cmd:`SearchRewrite` examples - .. cmdv:: @selector: SearchPattern @term + .. coqtop:: in - This specifies the goal on which to - search hypothesis (see Section :ref:`invocation-of-tactics`). - By default the 1st goal is - searched. This variant can be combined with other variants presented - here. + Require Import Arith. + .. coqtop:: all -.. cmd:: SearchRewrite @term + SearchRewrite (_ + _ + _). - This command displays the name and type of all hypothesis of the - current goal (if any) and theorems of the current context whose - statement’s conclusion is an equality of which one side matches the - expression term. Holes in term are denoted by “_”. +.. table:: Search Blacklist @string + :name: Search Blacklist - .. example:: + 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_``. - .. coqtop:: in + Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of + blacklisted strings. - Require Import Arith. - .. coqtop:: all +.. _requests-to-the-environment: - SearchRewrite (_ + _ + _). +Requests to the environment +------------------------------- - .. cmdv:: SearchRewrite @term inside {+ @qualid } +.. cmd:: Print Assumptions @smart_qualid - This restricts the search to constructions defined in the modules - named by the given :n:`qualid` sequence. + Displays all the assumptions (axioms, parameters and + variables) a theorem or definition depends on. - .. cmdv:: SearchRewrite @term outside {+ @qualid } + The message "Closed under the global context" indicates that the theorem or + definition has no dependencies. - This restricts the search to constructions not defined in the modules - named by the given :n:`qualid` sequence. +.. cmd:: Print Opaque Dependencies @smart_qualid - .. cmdv:: @selector: SearchRewrite @term + Displays the assumptions and opaque constants that :n:`@smart_qualid` depends on. - This specifies the goal on which to - search hypothesis (see Section :ref:`invocation-of-tactics`). - By default the 1st goal is - searched. This variant can be combined with other variants presented - here. +.. cmd:: Print Transparent Dependencies @smart_qualid -.. note:: + Displays the assumptions and transparent constants that :n:`@smart_qualid` depends on. - .. table:: Search Blacklist @string - :name: Search Blacklist +.. cmd:: Print All Dependencies @smart_qualid - 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_``. + Displays all the assumptions and constants :n:`@smart_qualid` depends on. - Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of - blacklisted strings. +.. cmd:: Locate @smart_qualid -.. cmd:: Locate @qualid + Displays the full name of objects from |Coq|'s various qualified namespaces such as terms, + modules and Ltac. It also displays notation definitions. - This command displays the full name of objects whose name is a prefix - of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in - which they are defined. It searches for objects from the different - qualified namespaces of |Coq|: terms, modules, Ltac, etc. + If the argument is: - .. example:: + * :n:`@qualid` - displays the full name of objects that + end with :n:`@qualid`, thereby showing the module they are defined in. + * :n:`@string {? "%" @ident }` - displays the definition of a notation. :n:`@string` + can be a single token in the notation such as "`->`" or a pattern that matches the + notation. See :ref:`locating-notations`. - .. coqtop:: all + .. todo somewhere we should list all the qualified namespaces + +.. cmd:: Locate Term @smart_qualid - Locate nat. + Like :cmd:`Locate`, but limits the search to terms - Locate Datatypes.O. +.. cmd:: Locate Module @qualid - Locate Init.Datatypes.O. + Like :cmd:`Locate`, but limits the search to modules - Locate Coq.Init.Datatypes.O. +.. cmd:: Locate Ltac @qualid - Locate I.Dont.Exist. + Like :cmd:`Locate`, but limits the search to tactics - .. cmdv:: Locate Term @qualid +.. cmd:: Locate Library @qualid - As Locate but restricted to terms. + Displays the full name, status and file system path of the module :n:`@qualid`, whether loaded or not. + +.. cmd:: Locate File @string - .. cmdv:: Locate Module @qualid + Displays the file system path of the file ending with :n:`@string`. + Typically, :n:`@string` has a suffix such as ``.cmo`` or ``.vo`` or ``.v`` file, such as :n:`Nat.v`. - As Locate but restricted to modules. + .. todo: also works for directory names such as "Data" (parent of Nat.v) + also "Data/Nat.v" works, but not a substring match - .. cmdv:: Locate Ltac @qualid +.. example:: Locate examples - As Locate but restricted to tactics. + .. coqtop:: all -.. seealso:: Section :ref:`locating-notations` + Locate nat. + Locate Datatypes.O. + Locate Init.Datatypes.O. + Locate Coq.Init.Datatypes.O. + Locate I.Dont.Exist. .. _printing-flags: @@ -522,35 +431,32 @@ Loading files |Coq| offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded -files are ASCII files containing sequences of commands for |Coq|’s +files are text files containing sequences of commands for |Coq|’s toplevel. This kind of file is called a *script* for |Coq|. The standard (and default) extension of |Coq|’s script files is .v. -.. cmd:: Load @ident +.. cmd:: Load {? Verbose } {| @string | @ident } - This command loads the file named :n:`ident`.v, searching successively in + Loads a file. If :n:`@ident` is specified, the command loads a file + named :n:`@ident.v`, searching successively in each of the directories specified in the *loadpath*. (see Section :ref:`libraries-and-filesystem`) - Files loaded this way cannot leave proofs open, and the ``Load`` - command cannot be used inside a proof either. + If :n:`@string` is specified, it must specify a complete filename. + `~` and .. abbreviations are + allowed as well as shell variables. If no extension is specified, |Coq| + will use the default extension ``.v``. - .. cmdv:: Load @string + Files loaded this way can't leave proofs open, nor can :cmd:`Load` + be used inside a proof. - Loads the file denoted by the string :n:`@string`, where - string is any complete filename. Then the `~` and .. abbreviations are - allowed as well as shell variables. If no extension is specified, |Coq| - will use the default extension ``.v``. + We discourage the use of :cmd:`Load`; use :cmd:`Require` instead. + :cmd:`Require` loads `.vo` files that were previously + compiled from `.v` files. - .. cmdv:: Load Verbose @ident - Load Verbose @string - - Display, while loading, - the answers of |Coq| to each command (including tactics) contained in - the loaded file. - - .. seealso:: Section :ref:`controlling-display`. + :n:`Verbose` displays the |Coq| output for each command and tactic + in the loaded file, as if the commands and tactics were entered interactively. .. exn:: Can’t find file @ident on loadpath. :undocumented: @@ -568,67 +474,50 @@ Compiled files This section describes the commands used to load compiled files (see Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A compiled -file is a particular case of module called *library file*. - - -.. cmd:: Require @qualid - - This command looks in the loadpath for a file containing module :n:`@qualid` - and adds the corresponding module to the environment of |Coq|. As - library files have dependencies in other library files, the command - :cmd:`Require` :n:`@qualid` recursively requires all library files the module - qualid depends on and adds the corresponding modules to the - environment of |Coq| too. |Coq| assumes that the compiled files have been - produced by a valid |Coq| compiler and their contents are then not - replayed nor rechecked. - - To locate the file in the file system, :n:`@qualid` is decomposed under the - form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical - directory of the file system that is mapped in |Coq| loadpath to the - logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between - physical directories and logical names at the time of requiring the - file must be consistent with the mapping used to compile the file. If - several files match, one of them is picked in an unspecified fashion. +file is a particular case of a module called a *library file*. - .. cmdv:: Require Import @qualid - :name: Require Import +.. cmd:: Require {? {| Import | Export } } {+ @qualid } + :name: Require; Require Import; Require Export - This loads and declares the module :n:`@qualid` - and its dependencies then imports the contents of :n:`@qualid` as described - for :cmd:`Import`. It does not import the modules that - :n:`@qualid` depends on unless these modules were themselves required in module - :n:`@qualid` - using :cmd:`Require Export`, or recursively required - through a series of :cmd:`Require Export`. If the module required has - already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as - :cmd:`Import` :n:`@qualid` would. + Loads compiled modules into the |Coq| environment. For each :n:`@qualid`, which has the form + :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented + by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated + filesystem directory. - .. cmdv:: Require Export @qualid - :name: Require Export + The process is applied recursively to all the loaded files; + if they contain :cmd:`Require` commands, those commands are executed as well. + The compiled files must have been compiled with the same version of |Coq|. + The compiled files are neither replayed nor rechecked. - This command acts as :cmd:`Require Import` :n:`@qualid`, - but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, - then the command :cmd:`Require Import` `A` also imports the module `B.` + * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined + in the module available by their short names + * :n:`Export` - additionally does an :cmd:`Export` on the loaded module, making components defined + in the module available by their short names *and* marking them to be exported by the current + module - .. cmdv:: Require {| Import | Export } {+ @qualid } + If the required module has already been loaded, :n:`Import` and :n:`Export` make the command + equivalent to :cmd:`Import` or :cmd:`Export`. - This loads the - modules named by the :token:`qualid` sequence and their recursive - dependencies. If - ``Import`` or ``Export`` is given, it also imports these modules and - all the recursive dependencies that were marked or transitively marked - as ``Export``. + The loadpath must contain the same mapping used to compile the file + (see Section :ref:`libraries-and-filesystem`). If + several files match, one of them is picked in an unspecified fashion. + Therefore, library authors should use a unique name for each module and + users are encouraged to use fully-qualified names + or the :cmd:`From ... Require` command to load files. - .. cmdv:: From @dirpath Require @qualid - :name: From ... Require ... - This command acts as :cmd:`Require`, but picks - any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` - for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library - comes from a given package by making explicit its absolute root. + .. todo common user error on dirpaths see https://github.com/coq/coq/pull/11961#discussion_r402852390 - .. exn:: Cannot load qualid: no physical path bound to dirpath. + .. cmd:: From @dirpath Require {? {| Import | Export } } {+ @qualid } + :name: From ... Require + + Works like :cmd:`Require`, but loads, for each :n:`@qualid`, + the library whose fully-qualified name matches :n:`@dirpath.{* @ident . }@qualid` + for some :n:`{* @ident . }`. This is useful to ensure that the :n:`@qualid` library + comes from a particular package. + + .. exn:: Cannot load @qualid: no physical path bound to @dirpath. :undocumented: .. exn:: Cannot find library foo in loadpath. @@ -637,7 +526,7 @@ file is a particular case of module called *library file*. file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`). - .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid. + .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library @qualid. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the @@ -651,13 +540,13 @@ file is a particular case of module called *library file*. |Coq| compiled module, or it was compiled with an incompatible version of |Coq|. - .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’. - - The library file :n:`@dirpath’` is indirectly required by the - ``Require`` command but it is bound in the current loadpath to the - file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at - the time it was compiled. + .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2. + The library :n:`@qualid__2` is indirectly required by a :cmd:`Require` or + :cmd:`From ... Require` command. The loadpath maps :n:`@qualid__2` to :n:`@ident.vo`, + which was compiled using a loadpath that bound it to :n:`@qualid__1`. Usually + the appropriate solution is to recompile :n:`@ident.v` using the correct loadpath. + See :ref:`libraries-and-filesystem`. .. warn:: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. @@ -668,33 +557,26 @@ file is a particular case of module called *library file*. .. cmd:: Print Libraries This command displays the list of library files loaded in the - current |Coq| session. For each of these libraries, it also tells if it - is imported. - + current |Coq| session. .. cmd:: Declare ML Module {+ @string } - This commands loads the OCaml compiled files - with names given by the :token:`string` sequence - (dynamic link). It is mainly used to load tactics dynamically. The - files are searched into the current OCaml loadpath (see the - command :cmd:`Add ML Path`). - Loading of OCaml files is only possible under the bytecode version of - ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter - :ref:`thecoqcommands`), or when |Coq| has been compiled with a - version of OCaml that supports native Dynlink (≥ 3.11). + This commands dynamically loads OCaml compiled code from + a :n:`.mllib` file. + It is used to load plugins dynamically. The + files must be accessible in the current OCaml loadpath (see the + command :cmd:`Add ML Path`). The :n:`.mllib` suffix may be omitted. - .. cmdv:: Local Declare ML Module {+ @string } + This command is reserved for plugin developers, who should provide + a .v file containing the command. Users of the plugins will then generally + load the .v file. - This variant is not exported to the modules that import the module - where they occur, even if outside a section. + This command supports the :attr:`local` attribute. If present, + the listed files are not exported, even if they're outside a section. .. exn:: File not found on loadpath: @string. :undocumented: - .. exn:: Loading of ML object file forbidden in a native Coq. - :undocumented: - .. cmd:: Print ML Modules @@ -709,7 +591,7 @@ Loadpath ------------ Loadpaths are preferably managed using |Coq| command line options (see -Section `libraries-and-filesystem`) but there remain vernacular commands to manage them +Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them for practical purposes. Such commands are only meant to be issued in the toplevel, and using them in source files is discouraged. @@ -719,22 +601,27 @@ the toplevel, and using them in source files is discouraged. This command displays the current working directory. -.. cmd:: Cd @string +.. cmd:: Cd {? @string } - This command changes the current directory according to :token:`string` which - can be any valid path. + If :n:`@string` is specified, changes the current directory according to :token:`string` which + can be any valid path. Otherwise, it displays the current directory. - .. cmdv:: Cd - Is equivalent to Pwd. +.. cmd:: Add LoadPath @string as @dirpath + .. insertprodn dirpath dirpath -.. cmd:: Add LoadPath @string as @dirpath + .. prodn:: + dirpath ::= {* @ident . } @ident This command is equivalent to the command line option - :n:`-Q @string @dirpath`. It adds the physical directory string to the current - |Coq| loadpath and maps it to the logical directory dirpath. + :n:`-Q @string @dirpath`. It adds a mapping to the loadpath from + the logical name :n:`@dirpath` to the file system directory :n:`@string`. + * :n:`@dirpath` is a prefix of a module name. The module name hierarchy + follows the file system hierarchy. On Linux, for example, the prefix + `A.B.C` maps to the directory :n:`@string/B/C`. Avoid using spaces after a `.` in the + path because the parser will interpret that as the end of a command or tactic. .. cmd:: Add Rec LoadPath @string as @dirpath @@ -748,42 +635,24 @@ the toplevel, and using them in source files is discouraged. This command removes the path :n:`@string` from the current |Coq| loadpath. -.. cmd:: Print LoadPath +.. cmd:: Print LoadPath {? @dirpath } - This command displays the current |Coq| loadpath. - - .. cmdv:: Print LoadPath @dirpath - - Works as :cmd:`Print LoadPath` but displays only - the paths that extend the :n:`@dirpath` prefix. + This command displays the current |Coq| loadpath. If :n:`@dirpath` is specified, + displays only the paths that extend that prefix. .. cmd:: Add ML Path @string This command adds the path :n:`@string` to the current OCaml - loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). + loadpath (cf. :cmd:`Declare ML Module`). -.. cmd:: Print ML Path @string +.. cmd:: Print ML Path This command displays the current OCaml loadpath. This command makes sense only under the bytecode version of ``coqtop``, i.e. using option ``-byte`` - (see the command Declare ML Module in Section :ref:`compiled-files`). - -.. _locate-file: - -.. cmd:: Locate File @string - - This command displays the location of file string in the current - loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file. - - -.. cmd:: Locate Library @dirpath - - This command gives the status of the |Coq| module dirpath. It tells if - the module is loaded and if not searches in the load path for a module - of logical name :n:`@dirpath`. + (cf. :cmd:`Declare ML Module`). .. _backtracking: @@ -806,30 +675,22 @@ interactively, they cannot be part of a vernacular file loaded via .. exn:: @ident: no such entry. :undocumented: - .. cmdv:: Reset Initial +.. cmd:: Reset Initial - Goes back to the initial state, just after the start - of the interactive session. + Goes back to the initial state, just after the start + of the interactive session. -.. cmd:: Back +.. cmd:: Back {? @num } - This command undoes all the effects of the last vernacular command. - Commands read from a vernacular file via a :cmd:`Load` are considered as a - single command. Proof management commands are also handled by this - command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than - one command in order to reach a state where the proof management - information is available. For instance, when the last command is a - :cmd:`Qed`, the management information about the closed proof has been - discarded. In this case, :cmd:`Back` will then undo all the proof steps up to - the statement of this proof. - - .. cmdv:: Back @num - - Undo :n:`@num` vernacular commands. As for Back, some extra - commands may be undone in order to reach an adequate state. For - instance Back :n:`@num` will not re-enter a closed proof, but rather go just - before that proof. + Undoes all the effects of the last :n:`@num @sentence`\s. If + :n:`@num` is not specified, the command undoes one sentence. + Sentences read from a `.v` file via a :cmd:`Load` are considered a + single sentence. While :cmd:`Back` can undo tactics and commands executed + within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all + the statements executed within are thereafter considered a single sentence. + :cmd:`Back` immediately following :cmd:`Qed` gets you back to the state + just after the statement of the proof. .. exn:: Invalid backtrack. @@ -850,18 +711,17 @@ interactively, they cannot be part of a vernacular file loaded via Quitting and debugging -------------------------- - .. cmd:: Quit - This command permits to quit |Coq|. + Causes |Coq| to exit. Valid only in coqtop. .. cmd:: Drop - This is used mostly as a debug facility by |Coq|’s implementers and does - not concern the casual user. This command permits to leave |Coq| - temporarily and enter the OCaml toplevel. The OCaml - command: + This command temporarily enters the OCaml toplevel. + It is a debug facility used by |Coq|’s implementers. Valid only in the + bytecode version of coqtop. + The OCaml command: :: @@ -886,49 +746,53 @@ Quitting and debugging (see Section `customization-by-environment-variables`). -.. TODO : command is not a syntax entry - -.. cmd:: Time @command +.. cmd:: Time @sentence - This command executes the vernacular command :n:`@command` and displays the + Executes :n:`@sentence` and displays the time needed to execute it. -.. cmd:: Redirect @string @command +.. cmd:: Redirect @string @sentence - This command executes the vernacular command :n:`@command`, redirecting its - output to ":n:`@string`.out". + Executes :n:`@sentence`, redirecting its + output to the file ":n:`@string`.out". -.. cmd:: Timeout @num @command +.. cmd:: Timeout @num @sentence - This command executes the vernacular command :n:`@command`. If the command - has not terminated after the time specified by the :n:`@num` (time - expressed in seconds), then it is interrupted and an error message is + Executes :n:`@sentence`. If the operation + has not terminated after :n:`@num` seconds, then it is interrupted and an error message is 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 - :cmd:`Timeout` are unaffected. + If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`, + except for :cmd:`Timeout` commands themselves. If unset, + no timeout is applied. -.. cmd:: Fail @command +.. cmd:: Fail @sentence For debugging scripts, sometimes it is desirable to know whether a - command or a tactic fails. If the given :n:`@command` fails, then - :n:`Fail @command` succeeds (excepts in the case of - critical errors, like a "stack overflow"), without changing the - proof state, and in interactive mode, the system prints a message + command or a tactic fails. If :n:`@sentence` fails, then + :n:`Fail @sentence` succeeds (except for + critical errors, such as "stack overflow"), without changing the + proof state. In interactive mode, the system prints a message confirming the failure. .. exn:: The command has not failed! - If the given :n:`@command` succeeds, then :n:`Fail @command` + If the given :n:`@command` succeeds, then :n:`Fail @sentence` fails with this error message. +.. note:: + + :cmd:`Time`, :cmd:`Redirect`, :cmd:`Timeout` and :cmd:`Fail` are + :production:`control_command`\s. For these commands, attributes and goal + selectors, when specified, are part of the :n:`@sentence` argument, and thus come after + the control command prefix and before the inner command or tactic. For + example: `Time #[ local ] Definition foo := 0.` or `Fail Timeout 10 all: auto.` .. _controlling-display: @@ -1010,13 +874,16 @@ as numbers, and for reflection-based tactics. The commands to fine- tune the reduction strategies and the lazy conversion algorithm are described first. -.. cmd:: Opaque {+ @qualid } +.. cmd:: Opaque {+ @smart_qualid } + + This command accepts the :attr:`global` attribute. By default, the scope + of :cmd:`Opaque` is limited to the current section or module. This command has an effect on unfoldable constants, i.e. on constants defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc, or by a proof ended by :cmd:`Defined`. The command tells not to unfold the - constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding + constants in the :n:`@smart_qualid` sequence in tactics using δ-conversion (unfolding a constant is replacing it by its definition). :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling @@ -1024,24 +891,15 @@ described first. has to check the conversion (see Section :ref:`conversion-rules`) of two distinct applied constants. - .. cmdv:: Global Opaque {+ @qualid } - :name: Global Opaque - - The scope of :cmd:`Opaque` is limited to the current section, or current - file, unless the variant :cmd:`Global Opaque` is used. - .. seealso:: Sections :ref:`performingcomputations`, :ref:`tactics-automating`, :ref:`proof-editing-mode` - .. exn:: The reference @qualid was not found in the current environment. - - There is no constant referred by :n:`@qualid` in the environment. - Nevertheless, if you asked :cmd:`Opaque` `foo` `bar` and if `bar` does - not exist, `foo` is set opaque. +.. cmd:: Transparent {+ @smart_qualid } -.. cmd:: Transparent {+ @qualid } + This command accepts the :attr:`global` attribute. By default, the scope + of :cmd:`Transparent` is limited to the current section or module. This command is the converse of :cmd:`Opaque` and it applies on unfoldable constants to restore their unfoldability after an Opaque command. @@ -1054,16 +912,9 @@ described first. the usual defined constants, whose actual values are of course relevant in general. - .. cmdv:: Global Transparent {+ @qualid } - :name: Global Transparent - - The scope of Transparent is limited to the current section, or current - file, unless the variant :cmd:`Global Transparent` is - used. - .. exn:: The reference @qualid was not found in the current environment. - There is no constant referred by :n:`@qualid` in the environment. + There is no constant named :n:`@qualid` in the environment. .. seealso:: @@ -1072,63 +923,66 @@ described first. .. _vernac-strategy: -.. cmd:: Strategy @level [ {+ @qualid } ] +.. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - This command generalizes the behavior of Opaque and Transparent + .. insertprodn strategy_level strategy_level + + .. prodn:: + strategy_level ::= opaque + | @int + | expand + | transparent + + This command accepts the :attr:`local` attribute, which limits its effect + to the current section or module, in which case the section and module + behavior is the same as :cmd:`Opaque` and :cmd:`Transparent` (without :attr:`global`). + + This command generalizes the behavior of the :cmd:`Opaque` and :cmd:`Transparent` commands. It is used to fine-tune the strategy for unfolding constants, both at the tactic level and at the kernel level. This - command associates a level to the qualified names in the :n:`@qualid` + command associates a :n:`@strategy_level` with the qualified names in the :n:`@smart_qualid` sequence. Whenever two expressions with two distinct head constants are compared (for instance, this comparison can be triggered by a type cast), the one with lower level is expanded first. In case of a tie, the second one (appearing in the cast type) is expanded. - .. prodn:: level ::= {| opaque | @num | expand } - Levels can be one of the following (higher to lower): + ``opaque`` : level of opaque constants. They cannot be expanded by tactics (behaves like +∞, see next item). - + :n:`@num` : levels indexed by an integer. Level 0 corresponds to the + + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the default behavior, which corresponds to transparent constants. This - level can also be referred to as transparent. Negative levels + level can also be referred to as ``transparent``. Negative levels correspond to constants to be expanded before normal transparent constants, while positive levels correspond to constants to be expanded after normal transparent constants. + ``expand`` : level of constants that should be expanded first (behaves like −∞) + + ``transparent`` : Equivalent to level 0 - .. cmdv:: Local Strategy @level [ {+ @qualid } ] +.. cmd:: Print Strategy @smart_qualid - These directives survive section and module closure, unless the - command is prefixed by ``Local``. In the latter case, the behavior - regarding sections and modules is the same as for the :cmd:`Transparent` and - :cmd:`Opaque` commands. - - -.. cmd:: Print Strategy @qualid - - This command prints the strategy currently associated to :n:`@qualid`. It - fails if :n:`@qualid` is not an unfoldable reference, that is, neither a + This command prints the strategy currently associated with :n:`@smart_qualid`. It + fails if :n:`@smart_qualid` is not an unfoldable reference, that is, neither a variable nor a constant. .. exn:: The reference is not unfoldable. :undocumented: - .. cmdv:: Print Strategies +.. cmd:: Print Strategies - Print all the currently non-transparent strategies. + Print all the currently non-transparent strategies. .. cmd:: Declare Reduction @ident := @red_expr - This command allows giving a short name to a reduction expression, for + Declares a short name for the reduction expression :n:`@red_expr`, for instance ``lazy beta delta [foo bar]``. This short name can then be used - in :n:`Eval @ident in` or ``eval`` directives. This command - accepts the - ``Local`` modifier, for discarding this reduction name at the end of the - file or module. For the moment, the name is not qualified. In + in :n:`Eval @ident in` or ``eval`` constructs. This command + accepts the :attr:`local` attribute, which indicates that the reduction + will be discarded at the end of the + file or module. The name is not qualified. In particular declaring the same name in several modules or in several functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but @@ -1274,14 +1128,15 @@ in support libraries of plug-ins. .. _exposing-constants-to-ocaml-libraries: Exposing constants to OCaml libraries -```````````````````````````````````````````````````````````````` +````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 - This command exposes the constant :n:`@qualid__1` to OCaml libraries under - the name :n:`@qualid__2`. This constant can then be dynamically located - calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known - where is the constant defined (file, module, library, etc.). + Makes the constant :n:`@qualid__1` accessible to OCaml libraries under + the name :n:`@qualid__2`. The constant can then be dynamically located + in OCaml code by + calling :n:`Coqlib.lib_ref "@qualid__2"`. The OCaml code doesn't need + to know where the constant is defined (what file, module, library, etc.). As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, the constant is exposed to the kernel. For instance, the `Int63` module @@ -1291,27 +1146,41 @@ Exposing constants to OCaml libraries Register bool as kernel.ind_bool. - This makes the kernel aware of what is the type of boolean values. This - information is used for instance to define the return type of the - :g:`#int63_eq` primitive. + This makes the kernel aware of the `bool` type, which is used, for example, + to define the return type of the :g:`#int63_eq` primitive. .. seealso:: :ref:`primitive-integers` Inlining hints for the fast reduction machines -```````````````````````````````````````````````````````````````` +`````````````````````````````````````````````` .. cmd:: Register Inline @qualid - This command gives as a hint to the reduction machines (VM and native) that + Gives a hint to the reduction machines (VM and native) that the body of the constant :n:`@qualid` should be inlined in the generated code. Registering primitive operations ```````````````````````````````` -.. cmd:: Primitive @ident__1 := #@ident__2. +.. cmd:: Primitive @ident {? : @term } := #@ident__prim + + Makes the primitive type or primitive operator :n:`#@ident__prim` defined in OCaml + accessible in |Coq| commands and tactics. + For internal use by implementors of |Coq|'s standard library or standard library + replacements. No space is allowed after the `#`. Invalid values give a syntax + error. + + For example, the standard library files `Int63.v` and `PrimFloat.v` use :cmd:`Primitive` + to support, respectively, the features described in :ref:`primitive-integers` and + :ref:`primitive-floats`. + + The types associated with an operator must be declared to the kernel before declaring operations + that use the type. Do this with :cmd:`Primitive` for primitive types and + :cmd:`Register` with the :g:`kernel` prefix for other types. For example, + in `Int63.v`, `#int63_type` must be declared before the associated operations. + + .. exn:: The type @ident must be registered before this construction can be typechecked. + :undocumented: - Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When - running this command, the type of the primitive should be already known by - the kernel (this is achieved through this command for primitive types and - through the :cmd:`Register` command with the :g:`kernel` name-space for other - types). + The type must be defined with :cmd:`Primitive` command before this + :cmd:`Primitive` command (declaring an operation using the type) will succeed. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 669975ba7e..512378b9fc 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -902,7 +902,7 @@ Syntax of notations +++++++++++++++++++ The different syntactic forms taken by the commands declaring -notations are given below. The optional :production:`scope` is described in +notations are given below. The optional :n:`@scope` is described in :ref:`Scopes`. .. productionlist:: coq @@ -1001,6 +1001,11 @@ Notations disappear when a section is closed. Interpretation scopes ---------------------- + .. insertprodn scope scope + + .. prodn:: + scope ::= @ident + An *interpretation scope* is a set of notations for terms with their interpretations. Interpretation scopes provide a weak, purely syntactical form of notation overloading: the same notation, for @@ -1090,7 +1095,7 @@ Local opening of an interpretation scope It is possible to locally extend the interpretation scope stack using the syntax :n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a -special identifier called *delimiting key* and bound to a given scope. +special identifier called a *delimiting key* and bound to a given scope. In such a situation, the term term, and all its subterms, are interpreted in the scope stack extended with the scope bound to :token:`ident`. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 60b845c4be..a01f57eb22 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -151,8 +151,7 @@ fields: [ | DELETENT ] dirpath: [ | REPLACE ident LIST0 field -| WITH ident -| dirpath field_ident +| WITH LIST0 ( ident "." ) ident ] binders: [ @@ -220,6 +219,15 @@ tactic_expr0: [ | WITH "[>" tactic_then_gen "]" ] +(* lexer token *) +IDENT: [ +| ident +] + +scope: [ +| IDENT +] + operconstr100: [ | MOVETO term_cast operconstr99 "<:" operconstr200 | MOVETO term_cast operconstr99 "<<:" operconstr200 @@ -240,7 +248,9 @@ operconstr9: [ operconstr1: [ | REPLACE operconstr0 ".(" global LIST0 appl_arg ")" -| WITH operconstr0 ".(" global LIST0 appl_arg ")" +| WITH operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *) +| REPLACE operconstr0 "%" IDENT +| WITH operconstr0 "%" scope | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")" | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" ] @@ -364,6 +374,11 @@ pattern10: [ | DELETE pattern1 ] +pattern1: [ +| REPLACE pattern0 "%" IDENT +| WITH pattern0 "%" scope +] + pattern0: [ | REPLACE "(" pattern200 ")" | WITH "(" LIST1 pattern200 SEP "|" ")" @@ -419,6 +434,8 @@ gallina: [ | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) | REPLACE "Scheme" LIST1 scheme SEP "with" | WITH "Scheme" scheme LIST0 ( "with" scheme ) +| REPLACE "Primitive" identref OPT [ ":" lconstr ] ":=" register_token +| WITH "Primitive" identref OPT [ ":" lconstr ] ":=" "#" identref ] constructor_list_or_record_decl: [ @@ -494,10 +511,6 @@ strategy_flag: [ | OPTINREF ] -export_token: [ -| OPTINREF -] - functor_app_annot: [ | OPTINREF ] @@ -536,20 +549,23 @@ gallina_ext: [ | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] | WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] +(* don't show Export for Set, Unset *) | REPLACE "Export" "Set" option_table option_setting -| WITH OPT "Export" "Set" option_table option_setting +| WITH "Set" option_table option_setting | REPLACE "Export" "Unset" option_table -| WITH OPT "Export" "Unset" option_table +| WITH "Unset" option_table | REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] +| REPLACE "From" global "Require" export_token LIST1 global +| WITH "From" dirpath "Require" export_token LIST1 global ] -(* lexer stuff *) -IDENT: [ -| ident +export_token: [ +| OPTINREF ] +(* lexer stuff *) integer: [ | DELETENT ] RENAME: [ | integer int (* todo: review uses in .mlg files, some should be "natural" *) @@ -859,6 +875,7 @@ bar_cbrace: [ printable: [ | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string +| DELETE "Term" smart_global OPT univ_name_list (* readded in commands *) | INSERTALL "Print" ] @@ -878,15 +895,18 @@ command: [ | DELETE "Back" | REPLACE "Back" natural | WITH "Back" OPT natural -| REPLACE "Test" option_table "for" LIST1 option_ref_value -| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) -| DELETE "Test" option_table | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ] | WITH "Load" OPT "Verbose" [ ne_string | IDENT ] | DELETE "Unset" option_table -| DELETE "Set" option_table option_setting +| REPLACE "Set" option_table option_setting +| WITH OPT "Export" "Set" option_table (* set flag *) +| REPLACE "Test" option_table "for" LIST1 option_ref_value +| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) +| DELETE "Test" option_table + +(* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Add" IDENT IDENT LIST1 option_ref_value -| WITH "Add" IDENT OPT IDENT LIST1 option_ref_value +| WITH "Add" option_table LIST1 option_ref_value | DELETE "Add" IDENT LIST1 option_ref_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident @@ -941,7 +961,11 @@ command: [ | REPLACE "Preterm" "of" ident | WITH "Preterm" OPT ( "of" ident ) | DELETE "Preterm" -| EDIT "Remove" ADD_OPT IDENT IDENT LIST1 option_ref_value + +(* hide the fact that table names are limited to 2 IDENTs *) +| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value +| WITH "Remove" option_table LIST1 option_ref_value +| DELETE "Remove" IDENT LIST1 option_ref_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string | "Restore" "State" [ IDENT | ne_string ] @@ -976,6 +1000,16 @@ command: [ | REPLACE "Abort" identref | WITH "Abort" OPT [ "All" | identref ] +(* show the locate options as separate commands *) +| DELETE "Locate" locatable +| locatable +| REPLACE "Print" smart_global OPT univ_name_list +| WITH "Print" OPT "Term" smart_global OPT univ_name_list + +] + +option_setting: [ +| OPTINREF ] only_parsing: [ @@ -1062,9 +1096,7 @@ legacy_attr: [ | DELETE "NonCumulative" ] -vernacular: [ -| LIST0 ( OPT all_attrs [ command | tactic ] "." ) -] +sentence: [ ] (* productions defined below *) rec_definition: [ | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations @@ -1124,7 +1156,7 @@ query_command: [ | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" searchabout_query searchabout_queries "." -| WITH "Search" searchabout_query searchabout_queries +| WITH "Search" searchabout_queries ] vernac_toplevel: [ @@ -1142,37 +1174,25 @@ vernac_toplevel: [ | DELETE vernac_control ] -positive_search_mark: [ -| OPTINREF -] - in_or_out_modules: [ | OPTINREF ] -searchabout_queries: [ -| OPTINREF -] - vernac_control: [ (* replacing vernac_control with command is cheating a little; they can't refer to the vernac_toplevel commands. cover this the descriptions of these commands *) | REPLACE "Time" vernac_control -| WITH "Time" command +| WITH "Time" sentence | REPLACE "Redirect" ne_string vernac_control -| WITH "Redirect" ne_string command +| WITH "Redirect" ne_string sentence | REPLACE "Timeout" natural vernac_control -| WITH "Timeout" natural command +| WITH "Timeout" natural sentence | REPLACE "Fail" vernac_control -| WITH "Fail" command +| WITH "Fail" sentence | DELETE decorated_vernac ] -option_setting: [ -| OPTINREF -] - orient: [ | OPTINREF ] @@ -1351,6 +1371,51 @@ module_expr: [ | DELETE module_expr module_expr_atom ] +locatable: [ +| INSERTALL "Locate" +] + +ne_in_or_out_modules: [ +| REPLACE "inside" LIST1 global +| WITH [ "inside" | "outside" ] LIST1 global +| DELETE "outside" LIST1 global +] + +searchabout_query: [ +| REPLACE positive_search_mark ne_string OPT scope_delimiter +| WITH ne_string OPT scope_delimiter +| REPLACE positive_search_mark constr_pattern +| WITH constr_pattern +] + +searchabout_queries: [ +| DELETE ne_in_or_out_modules +| REPLACE searchabout_query searchabout_queries +| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules +| DELETE (* empty *) +] + +positive_search_mark: [ +| OPTINREF +] + +by_notation: [ +| REPLACE ne_string OPT [ "%" IDENT ] +| WITH ne_string OPT [ "%" scope ] +] + +scope_delimiter: [ +| REPLACE "%" IDENT +| WITH "%" scope +] + +(* Don't show these details *) +DELETE: [ +| register_token +| register_prim_token +| register_type_token +] + SPLICE: [ | noedit_mode | bigint @@ -1435,9 +1500,7 @@ SPLICE: [ | mode | mult_pattern | open_constr -| option_table | record_declaration -| register_type_token | tactic | uconstr | impl_ident_head @@ -1466,14 +1529,12 @@ SPLICE: [ | assum_coe | inline | occs -| univ_name_list | ltac_info | field_mods | ltac_production_sep | ltac_tactic_level | printunivs_subgraph | ring_mods -| scope_delimiter | eliminator (* todo: splice or not? *) | quoted_attributes (* todo: splice or not? *) | printable @@ -1486,7 +1547,6 @@ SPLICE: [ | option_ref_value | positive_search_mark | in_or_out_modules -| register_prim_token | option_setting | orient | with_bindings @@ -1518,6 +1578,10 @@ SPLICE: [ | ltac_def_kind | intropatterns | instance_name +| ne_in_or_out_modules +| searchabout_queries +| locatable +| scope_delimiter ] (* end SPLICE *) RENAME: [ @@ -1567,8 +1631,12 @@ RENAME: [ | record_binder_body field_body | class_rawexpr class | smart_global smart_qualid +| searchabout_query search_item +| option_table setting_name ] +(* todo: positive_search_mark is a lousy name for OPT "-" *) + (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *) clause_dft_concl: [ | OPTINREF @@ -1656,3 +1724,18 @@ SPLICE: [ | tactic_notation_tactics ] (* todo: ssrreflect*.rst ref to fix_body is incorrect *) + +(* not included in insertprodn; defined in rst with :production: *) +control_command: [ ] +query_command: [ ] (* re-add since previously spliced *) + +sentence: [ +| OPT all_attrs command "." +| OPT all_attrs OPT ( num ":" ) query_command "." +| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ] +| control_command +] + +vernacular: [ +| LIST0 sentence +] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index eea1d5081d..f00fda0e8c 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -189,6 +189,9 @@ let rec db_output_prodn = function and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) +(* identify special chars that don't get a trailing space in output *) +let omit_space s = List.mem s ["?"; "."; "#"] + let rec output_prod plist need_semi = function | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s | Snterm s -> @@ -225,7 +228,7 @@ let rec output_prod plist need_semi = function and prod_to_str_r plist prod = match prod with - | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] && plist -> + | Sterm s :: Snterm "ident" :: tl when omit_space s && plist -> (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl) | p :: tl -> let need_semi = @@ -282,7 +285,7 @@ and output_sep sep = and prod_to_prodn_r prod = match prod with - | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] -> + | Sterm s :: Snterm "ident" :: tl when omit_space s -> (sprintf "%s@ident" s) :: (prod_to_prodn_r tl) | p :: tl -> (output_prodn p) :: (prod_to_prodn_r tl) | [] -> [] @@ -1621,6 +1624,7 @@ let open_temp_bin file = open_out_bin (sprintf "%s.new" file) let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+" +let match_subscripts = Str.regexp "__[a-zA-Z0-9]+" let find_longest_match prods str = let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in @@ -1634,19 +1638,26 @@ let find_longest_match prods str = in aux 0 in + let remove_subscrs str = Str.global_replace match_subscripts "" str in let slen = String.length str in let str_pfx = get_pfx str in + let no_subscrs = remove_subscrs str in + let has_subscrs = no_subscrs <> str in let rec longest best multi best_len prods = match prods with | [] -> best, multi, best_len | prod :: tl -> let pstr = String.trim prod in (* todo: should be pretrimmed *) let clen = common_prefix_len str pstr in - if str_pfx = "" || str_pfx <> get_pfx pstr then + if has_subscrs && no_subscrs = pstr then + str, false, clen (* exact match ignoring subscripts *) + else if pstr = str then + pstr, false, clen (* exact match of full line *) + else if str_pfx = "" || str_pfx <> get_pfx pstr then longest best multi best_len tl (* prefixes don't match *) else if clen = slen && slen = String.length pstr then - pstr, false, clen (* exact match *) + pstr, false, clen (* exact match on prefix *) else if clen > best_len then longest pstr false clen tl (* better match *) else if clen = best_len then @@ -1654,7 +1665,11 @@ let find_longest_match prods str = else longest best multi best_len tl (* worse match *) in - longest "" false 0 prods + let mtch, multi, _ = longest "" false 0 prods in + if has_subscrs && mtch <> str then + "", multi, mtch (* no match for subscripted entry *) + else + mtch, multi, "" type seen = { nts: (string * int) NTMap.t; @@ -1753,8 +1768,14 @@ let process_rst g file args seen tac_prods cmd_prods = (* in*) let cmd_replace_files = [ + "doc/sphinx/language/core/records.rst"; + "doc/sphinx/language/core/sections.rst"; + "doc/sphinx/language/extensions/implicit-arguments.rst"; + "doc/sphinx/language/using/libraries/funind.rst"; + "doc/sphinx/language/gallina-specification-language.rst"; - "doc/sphinx/language/gallina-extensions.rst" + "doc/sphinx/language/gallina-extensions.rst"; + "doc/sphinx/proof-engine/vernacular-commands.rst" ] in @@ -1763,11 +1784,14 @@ let process_rst g file args seen tac_prods cmd_prods = if StringSet.is_empty prods || not (List.mem file cmd_replace_files) then rhs (* no change *) else - let mtch, multi, len = find_longest_match prods rhs in + let mtch, multi, best = find_longest_match prods rhs in +(* Printf.printf "mtch = '%s' rhs = '%s'\n" mtch rhs;*) if mtch = rhs then rhs (* no change *) else if mtch = "" then begin warn "%s line %d: NO MATCH `%s`\n" file !linenum rhs; + if best <> "" then + warn "%s line %d: BEST `%s`\n" file !linenum best; rhs end else if multi then begin warn "%s line %d: MULTIMATCH `%s`\n" file !linenum rhs; diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 272d17bb35..dc7e0fba37 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -773,7 +773,7 @@ gallina: [ | assumption_token inline assum_list | assumptions_token inline assum_list | def_token ident_decl def_body -| "Let" identref def_body +| "Let" ident_decl def_body | finite_token LIST1 inductive_definition SEP "with" | "Fixpoint" LIST1 rec_definition SEP "with" | "Let" "Fixpoint" LIST1 rec_definition SEP "with" @@ -1027,7 +1027,6 @@ gallina_ext: [ | "Module" "Type" identref LIST0 module_binder check_module_types is_module_type | "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl | "Section" identref -| "Chapter" identref | "End" identref | "Collection" identref ":=" section_subset_expr | "Require" export_token LIST1 global diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 0c9d7a853b..ac986f9adf 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -47,7 +47,7 @@ one_term: [ term1: [ | term_projection -| term0 "%" ident +| term0 "%" scope | term0 ] @@ -159,7 +159,20 @@ where: [ ] vernacular: [ -| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." ) +| LIST0 sentence +] + +sentence: [ +| OPT all_attrs command "." +| OPT all_attrs OPT ( num ":" ) query_command "." +| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ] +| control_command +] + +control_command: [ +] + +query_command: [ ] tacticals: [ @@ -330,7 +343,7 @@ pattern10: [ ] pattern1: [ -| pattern0 "%" ident +| pattern0 "%" scope | pattern0 ] @@ -367,53 +380,6 @@ decl_notation: [ | string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ] ] -register_token: [ -| "#int63_type" -| "#float64_type" -| "#int63_head0" -| "#int63_tail0" -| "#int63_add" -| "#int63_sub" -| "#int63_mul" -| "#int63_div" -| "#int63_mod" -| "#int63_lsr" -| "#int63_lsl" -| "#int63_land" -| "#int63_lor" -| "#int63_lxor" -| "#int63_addc" -| "#int63_subc" -| "#int63_addcarryc" -| "#int63_subcarryc" -| "#int63_mulc" -| "#int63_diveucl" -| "#int63_div21" -| "#int63_addmuldiv" -| "#int63_eq" -| "#int63_lt" -| "#int63_le" -| "#int63_compare" -| "#float64_opp" -| "#float64_abs" -| "#float64_eq" -| "#float64_lt" -| "#float64_le" -| "#float64_compare" -| "#float64_classify" -| "#float64_add" -| "#float64_sub" -| "#float64_mul" -| "#float64_div" -| "#float64_sqrt" -| "#float64_of_int63" -| "#float64_normfr_mantissa" -| "#float64_frshiftexp" -| "#float64_ldshiftexp" -| "#float64_next_up" -| "#float64_next_down" -] - thm_token: [ | "Theorem" | "Lemma" @@ -601,20 +567,20 @@ smart_qualid: [ ] by_notation: [ -| string OPT [ "%" ident ] +| string OPT [ "%" scope ] ] argument_spec_block: [ | argument_spec | "/" | "&" -| "(" LIST1 argument_spec ")" OPT ( "%" ident ) -| "[" LIST1 argument_spec "]" OPT ( "%" ident ) -| "{" LIST1 argument_spec "}" OPT ( "%" ident ) +| "(" LIST1 argument_spec ")" OPT ( "%" scope ) +| "[" LIST1 argument_spec "]" OPT ( "%" scope ) +| "{" LIST1 argument_spec "}" OPT ( "%" scope ) ] argument_spec: [ -| OPT "!" name OPT ( "%" ident ) +| OPT "!" name OPT ( "%" scope ) ] more_implicits_block: [ @@ -637,10 +603,14 @@ arguments_modifier: [ | "extra" "scopes" ] +scope: [ +| ident +] + strategy_level: [ -| "expand" | "opaque" | int +| "expand" | "transparent" ] @@ -660,12 +630,16 @@ command: [ | "Cd" OPT string | "Load" OPT "Verbose" [ string | ident ] | "Declare" "ML" "Module" LIST1 string -| "Locate" locatable +| "Locate" smart_qualid +| "Locate" "Term" smart_qualid +| "Locate" "Module" qualid +| "Locate" "Ltac" qualid +| "Locate" "Library" qualid +| "Locate" "File" string | "Add" "LoadPath" string "as" dirpath | "Add" "Rec" "LoadPath" string "as" dirpath | "Remove" "LoadPath" string | "Type" term -| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" ) | "Print" "All" | "Print" "Section" qualid | "Print" "Grammar" ident @@ -702,18 +676,17 @@ command: [ | "Print" "Strategy" smart_qualid | "Print" "Strategies" | "Print" "Registered" -| "Print" smart_qualid OPT ( "@{" LIST0 name "}" ) +| "Print" OPT "Term" smart_qualid OPT univ_name_list | "Print" "Module" "Type" qualid | "Print" "Module" qualid | "Print" "Namespace" dirpath | "Inspect" num | "Add" "ML" "Path" string -| OPT "Export" "Set" LIST1 ident OPT [ int | string ] -| OPT "Export" "Unset" LIST1 ident -| "Print" "Table" LIST1 ident -| "Add" ident OPT ident LIST1 [ qualid | string ] -| "Test" LIST1 ident OPT ( "for" LIST1 [ qualid | string ] ) -| "Remove" OPT ident ident LIST1 [ qualid | string ] +| OPT "Export" "Set" setting_name +| "Print" "Table" setting_name +| "Add" setting_name LIST1 [ qualid | string ] +| "Test" setting_name OPT ( "for" LIST1 [ qualid | string ] ) +| "Remove" setting_name LIST1 [ qualid | string ] | "Write" "State" [ ident | string ] | "Restore" "State" [ ident | string ] | "Reset" "Initial" @@ -806,7 +779,6 @@ command: [ | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid -| "Locate" "Ltac" qualid | "Ltac" tacdef_body LIST0 ( "with" tacdef_body ) | "Print" "Ltac" "Signatures" | "Set" "Firstorder" "Solver" ltac_expr @@ -851,7 +823,7 @@ command: [ | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] | [ "Definition" | "Example" ] ident_decl def_body -| "Let" ident def_body +| "Let" ident_decl def_body | "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) | "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) @@ -861,7 +833,7 @@ command: [ | "Combined" "Scheme" ident "from" LIST1 ident SEP "," | "Register" qualid "as" qualid | "Register" "Inline" qualid -| "Primitive" ident OPT [ ":" term ] ":=" register_token +| "Primitive" ident OPT [ ":" term ] ":=" "#" ident | "Universe" LIST1 ident | "Universes" LIST1 ident | "Constraint" LIST1 univ_constraint SEP "," @@ -873,11 +845,10 @@ command: [ | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" ) | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl | "Section" ident -| "Chapter" ident | "End" ident | "Collection" ident ":=" section_subset_expr | "Require" OPT [ "Import" | "Export" ] LIST1 qualid -| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid +| "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid | "Import" LIST1 qualid | "Export" LIST1 qualid | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) @@ -899,6 +870,8 @@ command: [ | "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | "Implicit" [ "Type" | "Types" ] reserv_list | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ] +| "Set" setting_name OPT [ int | string ] +| "Unset" setting_name | "Open" "Scope" ident | "Close" "Scope" ident | "Delimit" "Scope" ident "with" ident @@ -913,15 +886,15 @@ command: [ | "Eval" red_expr "in" term | "Compute" term | "Check" term -| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) -| "SearchHead" one_term OPT ne_in_or_out_modules -| "SearchPattern" one_term OPT ne_in_or_out_modules -| "SearchRewrite" one_term OPT ne_in_or_out_modules -| "Search" searchabout_query OPT searchabout_queries -| "Time" command -| "Redirect" string command -| "Timeout" num command -| "Fail" command +| "About" smart_qualid OPT univ_name_list +| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "Time" sentence +| "Redirect" string sentence +| "Timeout" num sentence +| "Fail" sentence | "Drop" | "Quit" | "BackTo" num @@ -960,20 +933,15 @@ starredidentref: [ ] dirpath: [ -| ident -| dirpath field_ident +| LIST0 ( ident "." ) ident ] bignat: [ | numeral ] -locatable: [ -| smart_qualid -| "Term" smart_qualid -| "File" string -| "Library" qualid -| "Module" qualid +setting_name: [ +| LIST1 ident ] comment: [ @@ -982,6 +950,15 @@ comment: [ | num ] +search_item: [ +| one_term +| string OPT ( "%" scope ) +] + +univ_name_list: [ +| "@{" LIST0 name "}" +] + hint: [ | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info | "Resolve" "->" LIST1 qualid OPT num @@ -1069,21 +1046,6 @@ class: [ | smart_qualid ] -ne_in_or_out_modules: [ -| "inside" LIST1 qualid -| "outside" LIST1 qualid -] - -searchabout_query: [ -| OPT "-" string OPT ( "%" ident ) -| OPT "-" one_term -] - -searchabout_queries: [ -| ne_in_or_out_modules -| searchabout_query searchabout_queries -] - level: [ | "level" num | "next" "level" @@ -18,29 +18,10 @@ ; ; (_ (flags :standard -rectypes))) -; Rules for coq_dune -(rule - (targets .vfiles.d) - (deps - (source_tree theories) - (source_tree plugins) - (source_tree user-contrib)) - (action - (with-stdout-to .vfiles.d - (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ - `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \ - `find theories user-contrib -type f -name *.v`")))) - -(alias - (name vodeps) - (deps tools/coq_dune.exe .vfiles.d)) - ; (action (run coq_dune .vfiles.d)))) - (install (section lib) (package coq) - (files - revision)) + (files revision)) (rule (targets revision) diff --git a/dune-project b/dune-project index fa05f5fb41..873d03e8dd 100644 --- a/dune-project +++ b/dune-project @@ -1,11 +1,10 @@ -(lang dune 2.0) +(lang dune 2.5) (name coq) -(using coq 0.1) +(using coq 0.2) (formatting (enabled_for ocaml)) -; We cannot set this to true until as long as the build is not -; properly bootstrapped [that is, we remove the voboot target] +; TODO ; ; (generate_opam_files true) diff --git a/engine/namegen.ml b/engine/namegen.ml index 370f35f6ed..c4472050f8 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -219,22 +219,22 @@ let get_mangle_names = ~key:["Mangle";"Names"] ~value:false -let mangle_names_prefix = ref (Id.of_string "_0") - -let set_prefix x = mangle_names_prefix := forget_subscript x - -let () = Goptions.( - declare_string_option - { optdepr = false; - optkey = ["Mangle";"Names";"Prefix"]; - optread = (fun () -> Id.to_string !mangle_names_prefix); - optwrite = begin fun x -> - set_prefix - (try Id.of_string x - with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) - end }) - -let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id +let mangle_names_prefix = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Mangle";"Names";"Prefix"] + ~value:(Id.of_string "_0") + (fun x -> + (try + Id.of_string x + with + | CErrors.UserError _ -> + CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")) + ) |> forget_subscript + ) + (fun x -> Id.to_string x) + +let mangle_id id = if get_mangle_names () then mangle_names_prefix () else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/uState.ml b/engine/uState.ml index d532129dc5..ff85f09efa 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -176,8 +176,11 @@ let instantiate_variable l b v = exception UniversesDiffer -let drop_weak_constraints = ref false - +let drop_weak_constraints = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Cumulativity";"Weak";"Constraints"] + ~value:false let process_universe_constraints ctx cstrs = let open UnivSubst in @@ -270,7 +273,7 @@ let process_universe_constraints ctx cstrs = | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local | UWeak (l, r) -> - if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local + if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local | UEq (l, r) -> equalize_universes l r local in let local = diff --git a/engine/uState.mli b/engine/uState.mli index 3959373ead..cd1c9a174e 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -69,8 +69,6 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry (** {5 Constraints handling} *) -val drop_weak_constraints : bool ref - val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1316dfe069..c31cdae6f5 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -678,6 +678,8 @@ let rec zip m stk = let fapp_stack (m,stk) = zip m stk +let term_of_process c stk = term_of_fconstr (zip c stk) + (*********************************************************************) (* The assertions in the functions below are granted because they are diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 9e94248113..79092813bc 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -227,6 +227,10 @@ val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack val kl : clos_infos -> clos_tab -> fconstr -> constr +val zip : fconstr -> stack -> fconstr + +val term_of_process : fconstr -> stack -> constr + val to_constr : lift -> fconstr -> constr (** End of cbn debug section i*) diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d2c9a454b..de8692ff21 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -128,7 +128,7 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_sprop_allowed = false; + env_sprop_allowed = true; env_universes_lbound = Univ.Level.set; env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index dde1274152..494282d4e1 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -37,7 +37,7 @@ let ( / ) = Filename.concat let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") let () = at_exit (fun () -> - if Lazy.is_val my_temp_dir then + if not !Flags.debug && Lazy.is_val my_temp_dir then try let d = Lazy.force my_temp_dir in Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 6cfe44c5ff..a5fcfae1fc 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -96,14 +96,14 @@ let mk_accu (a : atom) : t = else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Obj.repr (accumulate data) in - let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in + let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in ans in let acc = { acc_atm = a; acc_arg = [] } in let ans = Obj.repr (accumulate acc) in (** FIXME: use another representation for accumulators, this causes naked pointers. *) - let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in + let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in (Obj.obj ans : t) let get_accu (k : accumulator) = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 181ec4860c..50922ffc52 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -301,6 +301,7 @@ sig type t val repr : t -> side_effect list val empty : t + val is_empty : t -> bool val add : side_effect -> t -> t val concat : t -> t -> t end = @@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t } let repr eff = eff.seff let empty = { seff = []; elts = SeffSet.empty } +let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts let add x es = if SeffSet.mem x es.elts then es else { seff = x :: es.seff; elts = SeffSet.add x es.elts } @@ -349,6 +351,7 @@ let push_private_constants env eff = List.fold_left add_if_undefined env eff let empty_private_constants = SideEffects.empty +let is_empty_private_constants c = SideEffects.is_empty c let concat_private = SideEffects.concat let universes_of_private eff = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f8d5d319a9..b42746a882 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants val empty_private_constants : private_constants +val is_empty_private_constants : private_constants -> bool + val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index d1548ab12e..62d465c703 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -106,8 +106,10 @@ let print_gen ~anomaly (e, info) = try print_gen ~anomaly ~extra_msg !handle_stack e with exn -> + let exn, info = Exninfo.capture exn in (* exception in error printer *) - str "<in exception printer>" ++ fnl () ++ print_anomaly anomaly exn + str "<in exception printer>:" ++ print_backtrace info ++ + str "<original exception:" ++ print_anomaly anomaly exn (** The standard exception printer *) let iprint (e, info) = diff --git a/library/goptions.ml b/library/goptions.ml index 75eef5b411..73132868d7 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -296,6 +296,48 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) + +type 'a opt_decl = depr:bool -> key:option_name -> 'a + +let declare_int_option_and_ref ~depr ~key ~(value:int) = + let r_opt = ref value in + let optwrite v = r_opt := Option.default value v in + let optread () = Some !r_opt in + let _ = declare_int_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + +let declare_intopt_option_and_ref ~depr ~key = + let r_opt = ref None in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_int_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + optread + +let declare_nat_option_and_ref ~depr ~key ~(value:int) = + assert (value >= 0); + let r_opt = ref value in + let optwrite v = + let v = Option.default value v in + if v < 0 then + CErrors.user_err Pp.(str "This option expects a non-negative value."); + r_opt := v + in + let optread () = Some !r_opt in + let _ = declare_int_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + let declare_bool_option_and_ref ~depr ~key ~(value:bool) = let r_opt = ref value in let optwrite v = r_opt := v in @@ -307,6 +349,39 @@ let declare_bool_option_and_ref ~depr ~key ~(value:bool) = } in optread +let declare_string_option_and_ref ~depr ~key ~(value:string) = + let r_opt = ref value in + let optwrite v = r_opt := Option.default value v in + let optread () = Some !r_opt in + let _ = declare_stringopt_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + +let declare_stringopt_option_and_ref ~depr ~key = + let r_opt = ref None in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_stringopt_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + optread + +let declare_interpreted_string_option_and_ref ~depr ~key ~(value:'a) from_string to_string = + let r_opt = ref value in + let optwrite v = r_opt := Option.default value @@ Option.map from_string v in + let optread () = Some (to_string !r_opt) in + let _ = declare_stringopt_option { + optdepr = depr; + optkey = key; + optread; optwrite + } in + fun () -> !r_opt + (* 3- User accessible commands *) (* Setting values of options *) diff --git a/library/goptions.mli b/library/goptions.mli index 8fcc258d47..336cae420c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -104,9 +104,15 @@ end (** {6 Options. } *) -(** These types and function are for declaring a new option of name [key] - and access functions [read] and [write]; the parameter [name] is the option name - used when printing the option value (command "Print Toto Titi." *) +(** These types and function are for declaring a new option of name + [key] and access functions [read] and [write]; the parameter [name] + is the option name used when printing the option value (command + "Print Toto Titi." + + The declare_*_option functions are low-level, to be used when + implementing complex option workflows, e.g. when setting one option + changes the value of another. For most use cases, you should use + the helper functions declare_*_option_and_ref. *) type 'a option_sig = { optdepr : bool; @@ -118,7 +124,11 @@ type 'a option_sig = { } (** The [preprocess] function is triggered before setting the option. It can be - used to emit a warning on certain values, and clean-up the final value. *) + used to emit a warning on certain values, and clean-up the final value. + + [declare_stringopt_option] should be preferred to [declare_string_option] + because it supports "Unset". + Only "Warnings" option is declared using the latter.*) val declare_int_option : ?preprocess:(int option -> int option) -> int option option_sig -> unit @@ -129,9 +139,18 @@ val declare_string_option: ?preprocess:(string -> string) -> val declare_stringopt_option: ?preprocess:(string option -> string option) -> string option option_sig -> unit -(** Helper to declare a reference controlled by an option. Read-only +(** Helpers to declare a reference controlled by an option. Read-only as to avoid races. *) -val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool) +type 'a opt_decl = depr:bool -> key:option_name -> 'a + +val declare_int_option_and_ref : (value:int -> (unit -> int)) opt_decl +val declare_intopt_option_and_ref : (unit -> int option) opt_decl +val declare_nat_option_and_ref : (value:int -> (unit -> int)) opt_decl +val declare_bool_option_and_ref : (value:bool -> (unit -> bool)) opt_decl +val declare_string_option_and_ref : (value:string -> (unit -> string)) opt_decl +val declare_stringopt_option_and_ref : (unit -> string option) opt_decl +val declare_interpreted_string_option_and_ref : + (value:'a -> (string -> 'a) -> ('a -> string) -> (unit -> 'a)) opt_decl (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/man/coqide.1 b/man/coqide.1 index 62a102af03..c1af046019 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -69,7 +69,7 @@ Load Coq library (Require .IR path .). .TP -.BI \-require\ path +.BI \-require-import\ path Load Coq library .IR path and import it (Require Import diff --git a/man/coqtop.1 b/man/coqtop.1 index 25d0ef7718..e799bc7748 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -79,7 +79,7 @@ load Coq library (Require path.) .TP -.BI \-require \ path +.BI \-require-import \ path load Coq library .I path and import it (Require Import path.) diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/dune index 6a024358c3..d2f5b65980 100644 --- a/plugins/btauto/plugin_base.dune +++ b/plugins/btauto/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.btauto) (synopsis "Coq's btauto plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_btauto)) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 74043d6bc8..6f5c910297 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -25,19 +25,14 @@ open Util let init_size=5 -let cc_verbose=ref false +let cc_verbose= + declare_bool_option_and_ref + ~depr:false + ~key:["Congruence";"Verbose"] + ~value:false let debug x = - if !cc_verbose then Feedback.msg_debug (x ()) - -let () = - let gdopt= - { optdepr=false; - optkey=["Congruence";"Verbose"]; - optread=(fun ()-> !cc_verbose); - optwrite=(fun b -> cc_verbose := b)} - in - declare_bool_option gdopt + if cc_verbose () then Feedback.msg_debug (x ()) (* Signature table *) diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/dune index 2a92996d2a..f7fa3adb56 100644 --- a/plugins/cc/plugin_base.dune +++ b/plugins/cc/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.cc) (synopsis "Coq's congruence closure plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_congruence)) diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/dune index ba9cd595ce..1931339471 100644 --- a/plugins/derive/plugin_base.dune +++ b/plugins/derive/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.derive) (synopsis "Coq's derive plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_derive)) diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/dune index 037b0d5053..0c01dcd488 100644 --- a/plugins/extraction/plugin_base.dune +++ b/plugins/extraction/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.extraction) (synopsis "Coq's extraction plugin") (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_extraction)) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a53c2395f0..f8449bcda1 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -498,16 +498,8 @@ let info_file f = (* The objects defined below should survive an arbitrary time, so we register them to coq save/undo mechanism. *) -let my_bool_option name initval = - let flag = ref initval in - let access = fun () -> !flag in - let () = declare_bool_option - {optdepr = false; - optkey = ["Extraction"; name]; - optread = access; - optwrite = (:=) flag } - in - access +let my_bool_option name value = + declare_bool_option_and_ref ~depr:false ~key:["Extraction"; name] ~value (*s Extraction AccessOpaque *) @@ -588,25 +580,18 @@ let () = declare_int_option (* This option controls whether "dummy lambda" are removed when a toplevel constant is defined. *) -let conservative_types_ref = ref false -let conservative_types () = !conservative_types_ref - -let () = declare_bool_option - {optdepr = false; - optkey = ["Extraction"; "Conservative"; "Types"]; - optread = (fun () -> !conservative_types_ref); - optwrite = (fun b -> conservative_types_ref := b) } - +let conservative_types = + declare_bool_option_and_ref + ~depr:false + ~key:["Extraction"; "Conservative"; "Types"] + ~value:false (* Allows to print a comment at the beginning of the output files *) -let file_comment_ref = ref "" -let file_comment () = !file_comment_ref - -let () = declare_string_option - {optdepr = false; - optkey = ["Extraction"; "File"; "Comment"]; - optread = (fun () -> !file_comment_ref); - optwrite = (fun s -> file_comment_ref := s) } +let file_comment = + declare_string_option_and_ref + ~depr:false + ~key:["Extraction"; "File"; "Comment"] + ~value:"" (*s Extraction Lang *) diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/dune index d88daa23fc..1b05452d8f 100644 --- a/plugins/firstorder/plugin_base.dune +++ b/plugins/firstorder/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.firstorder) (synopsis "Coq's first order logic solver plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ground)) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 49e4c91182..6ddc6ba21e 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -31,20 +31,8 @@ DECLARE PLUGIN "ground_plugin" { -let ground_depth=ref 3 - -let ()= - let gdopt= - { optdepr=false; - optkey=["Firstorder";"Depth"]; - optread=(fun ()->Some !ground_depth); - optwrite= - (function - None->ground_depth:=3 - | Some i->ground_depth:=(max i 0))} - in - declare_int_option gdopt - +let ground_depth = + declare_nat_option_and_ref ~depr:false ~key:["Firstorder";"Depth"] ~value:3 let default_intuition_tac = let tac _ _ = Auto.h_auto None [] (Some []) in @@ -85,7 +73,7 @@ let gen_ground_tac flag taco ids bases = | None-> snd (default_solver ()) in let startseq k = Proofview.Goal.enter begin fun gl -> - let seq=empty_seq !ground_depth in + let seq=empty_seq (ground_depth ()) in let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/dune index 6ccf15df29..e594ffbd02 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.funind) (synopsis "Coq's functional induction plugin") (libraries coq.plugins.extraction)) + +(coq.pp (modules g_indfun)) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7d87fc0220..ec23355ce1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -107,9 +107,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in - let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in + let old_printallowmatchdefaultclause = Detyping.print_allow_match_default_clause () in Constrextern.print_universes := true; - Detyping.print_allow_match_default_clause := false; + Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -122,7 +122,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; - Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; + Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -132,7 +132,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; - Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; + Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise @@ -309,33 +309,18 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) (* Debugging *) -let functional_induction_rewrite_dependent_proofs = ref true -let function_debug = ref false -open Goptions -let functional_induction_rewrite_dependent_proofs_sig = - { - optdepr = false; - optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; - optread = (fun () -> !functional_induction_rewrite_dependent_proofs); - optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) - } -let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let do_rewrite_dependent = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Functional";"Induction";"Rewrite";"Dependent"] + ~value:true -let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true - -let function_debug_sig = - { - optdepr = false; - optkey = ["Function_debug"]; - optread = (fun () -> !function_debug); - optwrite = (fun b -> function_debug := b) - } - -let () = declare_bool_option function_debug_sig - - -let do_observe () = !function_debug +let do_observe = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Function_debug"] + ~value:false let observe strm = if do_observe () @@ -405,18 +390,11 @@ let observe_tac ~header s tac = end -let strict_tcc = ref false -let is_strict_tcc () = !strict_tcc -let strict_tcc_sig = - { - optdepr = false; - optkey = ["Function_raw_tcc"]; - optread = (fun () -> !strict_tcc); - optwrite = (fun b -> strict_tcc := b) - } - -let () = declare_bool_option strict_tcc_sig - +let is_strict_tcc = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Function_raw_tcc"] + ~value:false exception Building_graph of exn exception Defining_principle of exn diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune index 5611f5ba16..6558ecbfe8 100644 --- a/plugins/ltac/plugin_base.dune +++ b/plugins/ltac/dune @@ -11,3 +11,5 @@ (synopsis "Coq's tauto tactic") (modules tauto) (libraries coq.plugins.ltac)) + +(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 50c3ed1248..2bd4211c90 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -359,21 +359,15 @@ open Vernacextend open Goptions open Libnames -let print_info_trace = ref None - -let () = declare_int_option { - optdepr = false; - optkey = ["Info" ; "Level"]; - optread = (fun () -> !print_info_trace); - optwrite = fun n -> print_info_trace := n; -} +let print_info_trace = + declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"] let vernac_solve ~pstate n info tcom b = let open Goal_select in let pstate, status = Proof_global.map_fold_proof_endline (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info !print_info_trace in + let info = Option.append info (print_info_trace ()) in let (p,status) = Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p in diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 1958fff4cc..9eeba614c7 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -27,7 +27,13 @@ open NumCompat open Q.Notations open Mutils -let use_simplex = ref true +let use_simplex = + Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true + +(* If set to some [file], arithmetic goals are dumped in [file].v *) + +let dump_file = + Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"] type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res @@ -203,19 +209,19 @@ let fourier_linear_prover l = | Inl _ -> None let direct_linear_prover l = - if !use_simplex then Simplex.find_unsat_certificate l + if use_simplex () then Simplex.find_unsat_certificate l else fourier_linear_prover l let find_point l = let open Util in - if !use_simplex then Simplex.find_point l + if use_simplex () then Simplex.find_point l else match Mfourier.Fourier.find_point l with | Inr _ -> None | Inl cert -> Some cert let optimise v l = - if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l + if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l let dual_raw_certificate l = if debug then begin @@ -981,13 +987,11 @@ let xlia_simplex env red sys = with FoundProof prf -> compile_prf sys (Step (0, prf, Done)) let xlia env0 en red sys = - if !use_simplex then xlia_simplex env0 red sys else xlia en red sys - -let dump_file = ref None + if use_simplex () then xlia_simplex env0 red sys else xlia en red sys let gen_bench (tac, prover) can_enum prfdepth sys = let res = prover can_enum prfdepth sys in - ( match !dump_file with + ( match dump_file () with | None -> () | Some file -> let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli index cabd36ebb7..5b215549b0 100644 --- a/plugins/micromega/certificate.mli +++ b/plugins/micromega/certificate.mli @@ -12,16 +12,12 @@ module Mc = Micromega (** [use_simplex] is bound to the Coq option Simplex. If set, use the Simplex method, otherwise use Fourier *) -val use_simplex : bool ref +val use_simplex : unit -> bool type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res type qres = (Mc.q Mc.psatz, int * Mc.q list) res -(** [dump_file] is bound to the Coq option Dump Arith. - If set to some [file], arithmetic goals are dumped in filexxx.v *) -val dump_file : string option ref - (** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *) val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 43f6f5a35e..7e4c4ce5c6 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -37,74 +37,31 @@ let debug = false let max_depth = max_int (* Search limit for provers over Q R *) -let lra_proof_depth = ref max_depth +let lra_proof_depth = + declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth (* Search limit for provers over Z *) -let lia_enum = ref true -let lia_proof_depth = ref max_depth -let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth) -let get_lra_option () = !lra_proof_depth +let lia_enum = + declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true + +let lia_proof_depth = + declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth + +let get_lia_option () = + (Certificate.use_simplex (), lia_enum (), lia_proof_depth ()) (* Enable/disable caches *) -let use_lia_cache = ref true -let use_nia_cache = ref true -let use_nra_cache = ref true -let use_csdp_cache = ref true - -let () = - let int_opt l vref = - { optdepr = false - ; optkey = l - ; optread = (fun () -> Some !vref) - ; optwrite = - (fun x -> vref := match x with None -> max_depth | Some v -> v) } - in - let lia_enum_opt = - { optdepr = false - ; optkey = ["Lia"; "Enum"] - ; optread = (fun () -> !lia_enum) - ; optwrite = (fun x -> lia_enum := x) } - in - let solver_opt = - { optdepr = false - ; optkey = ["Simplex"] - ; optread = (fun () -> !Certificate.use_simplex) - ; optwrite = (fun x -> Certificate.use_simplex := x) } - in - let dump_file_opt = - { optdepr = false - ; optkey = ["Dump"; "Arith"] - ; optread = (fun () -> !Certificate.dump_file) - ; optwrite = (fun x -> Certificate.dump_file := x) } - in - let lia_cache_opt = - { optdepr = false - ; optkey = ["Lia"; "Cache"] - ; optread = (fun () -> !use_lia_cache) - ; optwrite = (fun x -> use_lia_cache := x) } - in - let nia_cache_opt = - { optdepr = false - ; optkey = ["Nia"; "Cache"] - ; optread = (fun () -> !use_nia_cache) - ; optwrite = (fun x -> use_nia_cache := x) } - in - let nra_cache_opt = - { optdepr = false - ; optkey = ["Nra"; "Cache"] - ; optread = (fun () -> !use_nra_cache) - ; optwrite = (fun x -> use_nra_cache := x) } - in - let () = declare_bool_option solver_opt in - let () = declare_bool_option lia_cache_opt in - let () = declare_bool_option nia_cache_opt in - let () = declare_bool_option nra_cache_opt in - let () = declare_stringopt_option dump_file_opt in - let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in - let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in - let () = declare_bool_option lia_enum_opt in - () +let use_lia_cache = + declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true + +let use_nia_cache = + declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true + +let use_nra_cache = + declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true + +let use_csdp_cache () = true (** * Initialize a tag type to the Tag module declaration (see Mutils). @@ -2101,7 +2058,7 @@ struct let memo_opt use_cache cache_file f = let memof = memo cache_file f in - fun x -> if !use_cache then memof x else f x + fun x -> if use_cache () then memof x else f x end module CacheCsdp = MakeCache (struct @@ -2281,7 +2238,7 @@ let memo_nra = let linear_prover_Q = { name = "linear prover" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = (fun (o, l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o) l) @@ -2292,7 +2249,7 @@ let linear_prover_Q = let linear_prover_R = { name = "linear prover" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = (fun (o, l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o) l) @@ -2303,7 +2260,7 @@ let linear_prover_R = let nlinear_prover_R = { name = "nra" - ; get_option = get_lra_option + ; get_option = lra_proof_depth ; prover = memo_nra ; hyps = hyps_of_cone ; compact = compact_cone diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/dune index 4153d06161..33ad3a0138 100644 --- a/plugins/micromega/plugin_base.dune +++ b/plugins/micromega/dune @@ -20,3 +20,5 @@ (modules g_zify zify) (synopsis "Coq's zify plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_micromega g_zify)) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index f157a807ad..9051bbb5ca 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -41,13 +41,21 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct type mode = Closed | Open type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t} - let finally f rst = - try - let res = f () in - rst (); res - with reraise -> - (try rst () with any -> raise reraise); - raise reraise + (* XXX: Move to Fun.protect once in Ocaml 4.08 *) + let fun_protect ~(finally : unit -> unit) work = + let finally_no_exn () = + let exception Finally_raised of exn in + try finally () + with e -> + let bt = Printexc.get_raw_backtrace () in + Printexc.raise_with_backtrace (Finally_raised e) bt + in + match work () with + | result -> finally_no_exn (); result + | exception work_exn -> + let work_bt = Printexc.get_raw_backtrace () in + finally_no_exn (); + Printexc.raise_with_backtrace work_exn work_bt let read_key_elem inch = try Some (Marshal.from_channel inch) with @@ -76,21 +84,23 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct let unlock fd = let pos = lseek fd 0 SEEK_CUR in - try - ignore (lseek fd 0 SEEK_SET); - lockf fd F_ULOCK 1 - with Unix.Unix_error (_, _, _) -> - () - (* Here, this is really bad news -- - there is a pending lock which could cause a deadlock. - Should it be an anomaly or produce a warning ? - *); - ignore (lseek fd pos SEEK_SET) + let () = + try + ignore (lseek fd 0 SEEK_SET); + lockf fd F_ULOCK 1 + with Unix.Unix_error (_, _, _) -> + (* Here, this is really bad news -- + there is a pending lock which could cause a deadlock. + Should it be an anomaly or produce a warning ? + *) + () + in + ignore (lseek fd pos SEEK_SET) (* We make the assumption that an acquired lock can always be released *) let do_under_lock kd fd f = - if lock kd fd then finally f (fun () -> unlock fd) else f () + if lock kd fd then fun_protect f ~finally:(fun () -> unlock fd) else f () let open_in f = let flags = [O_RDONLY; O_CREAT] in diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/dune index 9da5b39972..b921c9c408 100644 --- a/plugins/nsatz/plugin_base.dune +++ b/plugins/nsatz/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.nsatz) (synopsis "Coq's nsatz solver plugin") (libraries num coq.plugins.ltac)) + +(coq.pp (modules g_nsatz)) diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/dune index f512501c78..0db71ed6fb 100644 --- a/plugins/omega/plugin_base.dune +++ b/plugins/omega/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.omega) (synopsis "Coq's omega plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_omega)) diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/dune index 233845ae0f..43efa0eca5 100644 --- a/plugins/rtauto/plugin_base.dune +++ b/plugins/rtauto/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.rtauto) (synopsis "Coq's rtauto plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_rtauto)) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 537c37810e..1371c671a2 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -45,15 +45,11 @@ let reset_info () = s_info.branch_successes <- 0; s_info.nd_branching <- 0 -let pruning = ref true - -let opt_pruning= - {optdepr=false; - optkey=["Rtauto";"Pruning"]; - optread=(fun () -> !pruning); - optwrite=(fun b -> pruning:=b)} - -let () = declare_bool_option opt_pruning +let pruning = + declare_bool_option_and_ref + ~depr:false + ~key:["Rtauto";"Pruning"] + ~value:true type form= Atom of int @@ -182,7 +178,7 @@ let rec fill stack proof = [] -> Complete proof.dep_it | slice::super -> if - !pruning && + pruning () && List.is_empty slice.proofs_done && not (slice.changes_goal && proof.dep_goal) && not (Int.Set.exists @@ -529,7 +525,7 @@ let pp = let pp_info () = let count_info = - if !pruning then + if pruning () then str "Proof steps : " ++ int s_info.created_steps ++ str " created / " ++ int s_info.pruned_steps ++ str " pruned" ++ fnl () ++ diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 63dae1417e..d464ec4c06 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -221,27 +221,17 @@ let build_env gamma= mkApp(force node_count l_push,[|mkProp;p;e|])) gamma.env (mkApp (force node_count l_empty,[|mkProp|])) -open Goptions - -let verbose = ref false - -let opt_verbose= - {optdepr=false; - optkey=["Rtauto";"Verbose"]; - optread=(fun () -> !verbose); - optwrite=(fun b -> verbose:=b)} - -let () = declare_bool_option opt_verbose - -let check = ref false - -let opt_check= - {optdepr=false; - optkey=["Rtauto";"Check"]; - optread=(fun () -> !check); - optwrite=(fun b -> check:=b)} - -let () = declare_bool_option opt_check +let verbose = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Rtauto";"Verbose"] + ~value:false + +let check = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Rtauto";"Check"] + ~value:false open Pp @@ -267,7 +257,7 @@ let rtauto_tac = let () = begin reset_info (); - if !verbose then + if verbose () then Feedback.msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in @@ -276,7 +266,7 @@ let rtauto_tac = with Not_found -> user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in - let () = if !verbose then + let () = if verbose () then begin Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); @@ -292,7 +282,7 @@ let rtauto_tac = let term= applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in let build_end_time=System.get_time () in - let () = if !verbose then + let () = if verbose () then begin Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ @@ -306,14 +296,14 @@ let rtauto_tac = let tac_start_time = System.get_time () in let term = EConstr.of_constr term in let result= - if !check then + if check () then Tactics.exact_check term else Tactics.exact_no_check term in let tac_end_time = System.get_time () in let () = - if !check then Feedback.msg_info (str "Proof term type-checking is on"); - if !verbose then + if check () then Feedback.msg_info (str "Proof term type-checking is on"); + if verbose () then Feedback.msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/dune index d83857edad..60522cd3f5 100644 --- a/plugins/setoid_ring/plugin_base.dune +++ b/plugins/setoid_ring/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.setoid_ring) (synopsis "Coq's setoid ring plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_newring)) diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/dune index a13524bb52..a117d09a16 100644 --- a/plugins/ssr/plugin_base.dune +++ b/plugins/ssr/dune @@ -5,3 +5,5 @@ (modules_without_implementation ssrast) (flags :standard -open Gramlib) (libraries coq.plugins.ssrmatching)) + +(coq.pp (modules ssrvernac ssrparser)) diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/dune index 06f67c3774..629d723816 100644 --- a/plugins/ssrmatching/plugin_base.dune +++ b/plugins/ssrmatching/dune @@ -3,3 +3,5 @@ (public_name coq.plugins.ssrmatching) (synopsis "Coq ssrmatching plugin") (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ssrmatching)) diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/dune index 512752135d..b395695c8a 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/dune @@ -32,3 +32,5 @@ (synopsis "Coq syntax plugin: float") (modules float_syntax) (libraries coq.vernac)) + +(coq.pp (modules g_numeral g_string)) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 73be36d031..857918c928 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -221,53 +221,35 @@ module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet) (* Flags.for printing or not wildcard and synthetisable types *) -open Goptions - -let wildcard_value = ref true -let force_wildcard () = !wildcard_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Wildcard"]; - optread = force_wildcard; - optwrite = (:=) wildcard_value } - -let fast_name_generation = ref false - -let () = declare_bool_option { - optdepr = false; - optkey = ["Fast";"Name";"Printing"]; - optread = (fun () -> !fast_name_generation); - optwrite = (:=) fast_name_generation; -} - -let synth_type_value = ref true -let synthetize_type () = !synth_type_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Synth"]; - optread = synthetize_type; - optwrite = (:=) synth_type_value } - -let reverse_matching_value = ref true -let reverse_matching () = !reverse_matching_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Matching"]; - optread = reverse_matching; - optwrite = (:=) reverse_matching_value } - -let print_primproj_params_value = ref false -let print_primproj_params () = !print_primproj_params_value - -let () = declare_bool_option - { optdepr = false; - optkey = ["Printing";"Primitive";"Projection";"Parameters"]; - optread = print_primproj_params; - optwrite = (:=) print_primproj_params_value } - +let force_wildcard = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Wildcard"] + ~value:true + +let fast_name_generation = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Fast";"Name";"Printing"] + ~value:false + +let synthetize_type = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Synth"] + ~value:true + +let reverse_matching = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Matching"] + ~value:true + +let print_primproj_params = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Primitive";"Projection";"Parameters"] + ~value:false (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) @@ -338,27 +320,23 @@ let lookup_index_as_renamed env sigma t n = (**********************************************************************) (* Factorization of match patterns *) -let print_factorize_match_patterns = ref true - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Factorizable";"Match";"Patterns"]; - optread = (fun () -> !print_factorize_match_patterns); - optwrite = (fun b -> print_factorize_match_patterns := b) } - -let print_allow_match_default_clause = ref true +let print_factorize_match_patterns = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Factorizable";"Match";"Patterns"] + ~value:true -let () = - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; - optread = (fun () -> !print_allow_match_default_clause); - optwrite = (fun b -> print_allow_match_default_clause := b) } +let print_allow_match_default_opt_name = + ["Printing";"Allow";"Match";"Default";"Clause"] +let print_allow_match_default_clause = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:print_allow_match_default_opt_name + ~value:true let rec join_eqns (ids,rhs as x) patll = function | ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest -> - if not !Flags.raw_print && !print_factorize_match_patterns && + if not !Flags.raw_print && print_factorize_match_patterns () && List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' then join_eqns x (patl'::patll) rest @@ -404,7 +382,7 @@ let factorize_eqns eqns = let eqns = aux [] (List.rev eqns) in let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in let open CAst in - if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + if not !Flags.raw_print && print_allow_match_default_clause () && eqns <> [] then match select_default_clause eqns with (* At least two clauses and the last one is disjunctive with no variables *) | Some {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) -> @@ -925,16 +903,16 @@ let detype_rel_context d flags where avoid env sigma sign = let detype_names isgoal avoid nenv env sigma t = let flags = { flg_isgoal = isgoal; flg_lax = false } in - let avoid = Avoid.make ~fast:!fast_name_generation avoid in + let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in detype Now flags avoid (nenv,env) sigma t let detype d ?(lax=false) isgoal avoid env sigma t = let flags = { flg_isgoal = isgoal; flg_lax = lax } in - let avoid = Avoid.make ~fast:!fast_name_generation avoid in + let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in detype d flags avoid (names_of_rel_context env, env) sigma t let detype_rel_context d ?(lax = false) where avoid env sigma sign = let flags = { flg_isgoal = false; flg_lax = lax } in - let avoid = Avoid.make ~fast:!fast_name_generation avoid in + let avoid = Avoid.make ~fast:(fast_name_generation ()) avoid in detype_rel_context d flags where avoid env sigma sign let detype_closed_glob ?lax isgoal avoid env sigma t = diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 5723b47715..254f772ff8 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -29,11 +29,12 @@ val print_evar_arguments : bool ref (** If true, contract branches with same r.h.s. and same matching variables in a disjunctive pattern *) -val print_factorize_match_patterns : bool ref +val print_factorize_match_patterns : unit -> bool -(** If true and the last non unique clause of a "match" is a +(** If this flag is true and the last non unique clause of a "match" is a variable-free disjunctive pattern, turn it into a catch-call case *) -val print_allow_match_default_clause : bool ref +val print_allow_match_default_clause : unit -> bool +val print_allow_match_default_opt_name : string list val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 26bf02aa25..3d887e1a95 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -47,21 +47,17 @@ let default_flags env = let ts = default_transparent_state env in default_flags_of ts -let debug_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"Unification"]; - optread = (fun () -> !debug_unification); - optwrite = (fun a -> debug_unification:=a); -}) - -let debug_ho_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"HO";"Unification"]; - optread = (fun () -> !debug_ho_unification); - optwrite = (fun a -> debug_ho_unification:=a); -}) +let debug_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"Unification"] + ~value:false + +let debug_ho_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"HO";"Unification"] + ~value:false (*******************************************) (* Functions to deal with impossible cases *) @@ -767,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) - let () = if !debug_unification then + let () = if debug_unification () then let open Pp in Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, @@ -1224,16 +1220,16 @@ let apply_on_subterm env evd fixedref f test c t = (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t else - (if !debug_ho_unification then + (if debug_ho_unification () then Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); let b, evd = try test env !evdref k c t with e when CErrors.noncritical e -> assert false in - if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); + if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded"); let evd', t' = f !evdref k t in evdref := evd'; t') else ( - if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed"); + if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed"); map_constr_with_binders_left_to_right !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) @@ -1337,7 +1333,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let env_evar = evar_filtered_env env_rhs evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); let args = Array.map (nf_evar evd) args in @@ -1374,7 +1370,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let rec set_holes env_rhs evd rhs = function | (id,idty,c,cty,evsref,filter,occs)::subst -> let c = nf_evar evd c in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"set holes for: " ++ prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ prc env_rhs evd c ++ str" in " ++ @@ -1382,7 +1378,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let occ = ref 1 in let set_var evd k inst = let oc = !occ in - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"Found one occurrence"); Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); incr occ; @@ -1393,7 +1389,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | Unspecified prefer_abstraction -> let evd, evty = set_holes env_rhs evd cty subst in let evty = nf_evar evd evty in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ str" of type: " ++ prc env_evar evd evty ++ str " for " ++ prc env_rhs evd c); @@ -1413,7 +1409,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = evd, ev in let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); let () = check_selected_occs env_rhs evd c !occ occs in let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in @@ -1427,7 +1423,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (* Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let evd,rhs' = @@ -1437,7 +1433,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd) in let rhs' = nf_evar evd rhs' in (* We instantiate the evars of which the value is forced by typing *) - if !debug_ho_unification then + if debug_ho_unification () then (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); @@ -1445,7 +1441,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | (id,idty,c,cty,evsref,_,_)::l -> let id = id.binder_name in let c = nf_evar evd c in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracting: " ++ prc env_rhs evd (mkVar id) ++ spc () ++ prc env_rhs evd c); @@ -1476,7 +1472,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | _ -> evd) with e -> user_err (Pp.str "Cannot find an instance") else - ((if !debug_ho_unification then + ((if debug_ho_unification () then let evi = Evd.find evd evk in let env = Evd.evar_env env_rhs evi in Feedback.msg_debug Pp.(str"evar is defined: " ++ @@ -1491,7 +1487,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if Evd.is_defined evd evk then (* Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) - (if !debug_ho_unification then + (if debug_ho_unification () then begin let evi = Evd.find evd evk in let evenv = evar_env env_rhs evi in @@ -1504,13 +1500,13 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let evi = Evd.find_undefined evd evk in let evenv = evar_env env_rhs evi in let rhs' = nf_evar evd rhs' in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ prc evenv evd rhs'); (* solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in - if !debug_ho_unification then + if debug_ho_unification () then Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); let flags = default_flags_of TransparentState.full in Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' @@ -1564,7 +1560,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in - let () = if !debug_unification then + let () = if debug_unification () then let open Pp in Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4eae0cf86c..e475e4c52b 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -416,19 +416,10 @@ let get_alias_chain_of sigma aliases x = match x with | RelAlias n -> (try Int.Map.find n aliases.rel_aliases with Not_found -> empty_aliasing) | VarAlias id -> (try cast_aliasing (Id.Map.find id aliases.var_aliases) with Not_found -> empty_aliasing) -let normalize_alias_opt_alias sigma aliases x = - match get_alias_chain_of sigma aliases x with - | _, [] -> None - | _, a :: _ -> Some a - -let normalize_alias_opt sigma aliases x = match to_alias sigma x with -| None -> None -| Some a -> normalize_alias_opt_alias sigma aliases a - let normalize_alias sigma aliases x = - match normalize_alias_opt_alias sigma aliases x with - | Some a -> a - | None -> x + match get_alias_chain_of sigma aliases x with + | _, [] -> x + | _, a :: _ -> a let normalize_alias_var sigma var_aliases id = let aliases = { var_aliases; rel_aliases = Int.Map.empty } in @@ -678,7 +669,7 @@ let make_projectable_subst aliases sigma evi args = let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in Constrmap.add (fst cstr) ((args,id)::l) cstrs | _ -> cstrs in - let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in + let all = Int.Map.add i [a, id] all in (rest,all,cstrs,revmap) | LocalDef ({binder_name=id},c,_), a::rest -> let revmap = Id.Map.add id i revmap in @@ -688,13 +679,13 @@ let make_projectable_subst aliases sigma evi args = let ic, sub = try let ic = Id.Map.find idc revmap in ic, Int.Map.find ic all with Not_found -> i, [] (* e.g. [idc] is a filtered variable: treat [id] as an assumption *) in - if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then + if List.exists (fun (c, _) -> EConstr.eq_constr sigma a c) sub then (rest,all,cstrs,revmap) else - let all = Int.Map.add ic ((a,normalize_alias_opt sigma aliases a,id)::sub) all in + let all = Int.Map.add ic ((a, id)::sub) all in (rest,all,cstrs,revmap) | _ -> - let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in + let all = Int.Map.add i [a, id] all in (rest,all,cstrs,revmap)) | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0 sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in @@ -862,47 +853,47 @@ type evar_projection = exception NotUnique exception NotUniqueInType of (Id.t * evar_projection) list -let rec assoc_up_to_alias sigma aliases y yc = function +let rec assoc_up_to_alias sigma aliases y = function | [] -> raise Not_found - | (c,cc,id)::l -> - if is_alias sigma c y then id + | (c, id)::l -> + match to_alias sigma c with + | None -> assoc_up_to_alias sigma aliases y l + | Some c -> + if eq_alias c y then id else match l with - | _ :: _ -> assoc_up_to_alias sigma aliases y yc l + | _ :: _ -> assoc_up_to_alias sigma aliases y l | [] -> (* Last chance, we reason up to alias conversion *) - match (normalize_alias_opt sigma aliases c) with - | Some cc when eq_alias yc cc -> id - | _ -> if is_alias sigma c yc then id else raise Not_found + let cc = normalize_alias sigma aliases c in + let yc = normalize_alias sigma aliases y in + if eq_alias cc yc then id else raise Not_found -let rec find_projectable_vars with_evars aliases sigma y subst = - let yc = normalize_alias sigma aliases y in - let is_projectable idc idcl (subst1,subst2 as subst') = +let rec find_projectable_vars aliases sigma y subst = + let is_projectable _ idcl (subst1,subst2 as subst') = (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *) try - let id = assoc_up_to_alias sigma aliases y yc idcl in + let id = assoc_up_to_alias sigma aliases y idcl in (id,ProjectVar)::subst1,subst2 with Not_found -> (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) - if with_evars then - let f (c,_,id) = isEvar sigma c in - let idcl' = List.filter f idcl in - match idcl' with - | [c,_,id] -> - begin - let (evk,argsv as t) = destEvar sigma c in - let evi = Evd.find sigma evk in - let subst,_ = make_projectable_subst aliases sigma evi argsv in - let l = find_projectable_vars with_evars aliases sigma y subst in - match l with - | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2) - | _ -> subst' - end - | [] -> subst' - | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") - else - subst' in + let f (c, id) = isEvar sigma c in + let idcl' = List.filter f idcl in + match idcl' with + | [c, id] -> + begin + let (evk,argsv as t) = destEvar sigma c in + let evi = Evd.find sigma evk in + let subst,_ = make_projectable_subst aliases sigma evi argsv in + let l = find_projectable_vars aliases sigma y subst in + match l with + | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2) + | _ -> subst' + end + | [] -> subst' + | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") + in let subst1,subst2 = Int.Map.fold is_projectable subst ([],[]) in (* We return the substitution with ProjectVar first (from most recent to oldest var), followed by ProjectEvar (from most recent @@ -914,14 +905,15 @@ let rec find_projectable_vars with_evars aliases sigma y subst = let filter_solution = function | [] -> raise Not_found - | (id,p)::_::_ -> raise NotUnique - | [id,p] -> (mkVar id, p) + | _ :: _ :: _ -> raise NotUnique + | [id] -> mkVar id -let project_with_effects aliases sigma effects t subst = - let c, p = - filter_solution (find_projectable_vars false aliases sigma t subst) in - effects := p :: !effects; - c +let project_with_effects aliases sigma t subst = + let is_projectable _ idcl accu = + try assoc_up_to_alias sigma aliases t idcl :: accu + with Not_found -> accu + in + filter_solution (Int.Map.fold is_projectable subst []) open Context.Named.Declaration let rec find_solution_type evarenv = function @@ -981,28 +973,27 @@ let rec do_projection_effects unify flags define_fun env ty evd = function type projectibility_kind = | NoUniqueProjection - | UniqueProjection of EConstr.constr * evar_projection list + | UniqueProjection of EConstr.constr type projectibility_status = | CannotInvert | Invertible of projectibility_kind let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = - let effects = ref [] in let rec aux k t = match EConstr.kind evd t with | Rel i when i>k0+k -> aux' k (RelAlias (i-k)) | Var id -> aux' k (VarAlias id) | _ -> map_with_binders evd succ aux k t and aux' k t = - try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders + try project_with_effects aliases evd t subst_in_env_extended_with_k_binders with Not_found -> match expand_alias_once evd aliases t with | None -> raise Not_found | Some c -> aux k (Alias.eval (Alias.lift k c)) in try let c = aux 0 c_in_env_extended_with_k_binders in - Invertible (UniqueProjection (c,!effects)) + Invertible (UniqueProjection c) with | Not_found -> CannotInvert | NotUnique -> Invertible NoUniqueProjection @@ -1010,7 +1001,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in match res with - | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c) + | Invertible (UniqueProjection c) when not (noccur_evar fullenv evd evk c) -> CannotInvert | _ -> @@ -1019,7 +1010,7 @@ let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_ exception NotEnoughInformationToInvert let extract_unique_projection = function -| Invertible (UniqueProjection (c,_)) -> c +| Invertible (UniqueProjection c) -> c | _ -> (* For instance, there are evars with non-invertible arguments and *) (* we cannot arbitrarily restrict these evars before knowing if there *) @@ -1518,7 +1509,7 @@ let rec invert_definition unify flags choose imitate_defs let project_variable t = (* Evar/Var problem: unifiable iff variable projectable from ev subst *) try - let sols = find_projectable_vars true aliases !evdref t subst in + let sols = find_projectable_vars aliases !evdref t subst in let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index f989dae4c9..c1ca40329a 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -28,16 +28,22 @@ exception Find_at of int (* timing *) -let timing_enabled = ref false +let get_timing_enabled = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Timing"] + ~value:false (* profiling *) -let profiling_enabled = ref false +let get_profiling_enabled = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Profiling"] + ~value:false (* for supported platforms, filename for profiler results *) -let profile_filename = ref "native_compute_profile.data" - let profiler_platform () = match [@warning "-8"] Sys.os_type with | "Unix" -> @@ -48,10 +54,11 @@ let profiler_platform () = | "Win32" -> "Windows (Win32)" | "Cygwin" -> "Windows (Cygwin)" -let get_profile_filename () = !profile_filename - -let set_profile_filename fn = - profile_filename := fn +let get_profile_filename = + Goptions.declare_string_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Profile"; "Filename"] + ~value:"native_compute_profile.data" (* find unused profile filename *) let get_available_profile_filename () = @@ -77,18 +84,6 @@ let get_available_profile_filename () = let _ = Feedback.msg_info (Pp.str msg) in assert false -let get_profiling_enabled () = - !profiling_enabled - -let set_profiling_enabled b = - profiling_enabled := b - -let get_timing_enabled () = - !timing_enabled - -let set_timing_enabled b = - timing_enabled := b - let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 4f18174261..73a8add6ec 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -14,16 +14,6 @@ open Evd (** This module implements normalization by evaluation to OCaml code *) -val get_profile_filename : unit -> string -val set_profile_filename : string -> unit - -val get_profiling_enabled : unit -> bool -val set_profiling_enabled : bool -> unit - -val get_timing_enabled : unit -> bool -val set_timing_enabled : bool -> unit - - val native_norm : env -> evar_map -> constr -> types -> constr (** Conversion with inference of universe constraints *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8bb268a92e..f7456ef35e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -30,14 +30,6 @@ exception Elimconst their parameters in its stack. *) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Cumulativity";"Weak";"Constraints"]; - optread = (fun () -> not !UState.drop_weak_constraints); - optwrite = (fun a -> UState.drop_weak_constraints:=not a); -}) - - (** Support for reduction effects *) open Mod_subst @@ -966,13 +958,11 @@ module CredNative = RedNative(CNativeEntries) contract_* in any case . *) -let debug_RAKAM = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"RAKAM"]; - optread = (fun () -> !debug_RAKAM); - optwrite = (fun a -> debug_RAKAM:=a); -}) +let debug_RAKAM = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"RAKAM"] + ~value:false let equal_stacks sigma (x, l) (y, l') = let f_equal x y = eq_constr sigma x y in @@ -983,7 +973,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in let open ReductionBehaviour in let rec whrec cst_l (x, stack) = - let () = if !debug_RAKAM then + let () = if debug_RAKAM () then let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_debug @@ -994,7 +984,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = in let c0 = EConstr.kind sigma x in let fold () = - let () = if !debug_RAKAM then + let () = if debug_RAKAM () then let open Pp in Feedback.msg_debug (str "<><><><><>") in ((EConstr.of_kind c0, stack),cst_l) in @@ -1746,26 +1736,46 @@ let is_sort env sigma t = let whd_betaiota_deltazeta_for_iota_state ts env sigma s = let refold = false in let tactic_mode = false in - let rec whrec csts s = - let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in + let all' = CClosure.RedFlags.red_add_transparent CClosure.all ts in + (* Unset the sharing flag to get a call-by-name reduction. This matters for + the shape of the generated term. *) + let env' = Environ.set_typing_flags { (Environ.typing_flags env) with Declarations.share_reduction = false } env in + let whd_opt c = + let open CClosure in + let evars ev = safe_evar_value sigma ev in + let infos = create_clos_infos ~evars all' env' in + let tab = create_tab () in + let c = inject (EConstr.Unsafe.to_constr (Stack.zip sigma c)) in + let (c, stk) = whd_stack infos tab c [] in + match fterm_of c with + | (FConstruct _ | FCoFix _) -> + (* Non-neutral normal, can trigger reduction below *) + let c = EConstr.of_constr (term_of_process c stk) in + Some (decompose_app_vect sigma c) + | _ -> None + in + let rec whrec s = + let (t, stack as s), _ = whd_state_gen ~refold ~tactic_mode CClosure.betaiota env sigma s in match Stack.strip_app stack with |args, (Stack.Case _ :: _ as stack') -> - let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode - (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in - if reducible_mind_case sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' + begin match whd_opt (t, args) with + | Some (t_o, args) when reducible_mind_case sigma t_o -> whrec (t_o, Stack.append_app args stack') + | (Some _ | None) -> s + end |args, (Stack.Fix _ :: _ as stack') -> - let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode - (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in - if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' + begin match whd_opt (t, args) with + | Some (t_o, args) when isConstruct sigma t_o -> whrec (t_o, Stack.append_app args stack') + | (Some _ | None) -> s + end |args, (Stack.Proj (p,_) :: stack'') -> - let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode - (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in - if isConstruct sigma t_o then - whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'') - else s,csts' - |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts' + begin match whd_opt (t, args) with + | Some (t_o, args) when isConstruct sigma t_o -> + whrec (args.(Projection.npars p + Projection.arg p), stack'') + | (Some _ | None) -> s + end + |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s in - fst (whrec Cst_stack.empty s) + whrec s let find_conclusion env sigma = let rec decrec env c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 90dde01915..e168f6d1b6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -43,23 +43,17 @@ type subst0 = module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let keyed_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Keyed";"Unification"]; - optread = (fun () -> !keyed_unification); - optwrite = (fun a -> keyed_unification:=a); -}) - -let is_keyed_unification () = !keyed_unification - -let debug_unification = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Debug";"Tactic";"Unification"]; - optread = (fun () -> !debug_unification); - optwrite = (fun a -> debug_unification:=a); -}) +let is_keyed_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Keyed";"Unification"] + ~value:false + +let debug_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Debug";"Tactic";"Unification"] + ~value:false (** Making this unification algorithm correct w.r.t. the evar-map abstraction breaks too much stuff. So we redefine incorrect functions here. *) @@ -702,7 +696,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = - if !debug_unification then + if debug_unification () then Feedback.msg_debug ( Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++ Termops.Internal.print_constr_env curenv sigma cN) @@ -1127,7 +1121,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if !debug_unification then Feedback.msg_debug (str "Starting unification"); + if debug_unification () then Feedback.msg_debug (str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = @@ -1152,11 +1146,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst m n in - if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); + if debug_unification () then Feedback.msg_debug (str "Leaving unification with success"); a with e -> let e = Exninfo.capture e in - if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); + if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure"); Exninfo.iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env @@ -1745,7 +1739,7 @@ let make_abstraction env evd ccl abs = env evd c ty occs check_occs ccl let keyed_unify env evd kop = - if not !keyed_unification then fun cl -> true + if not (is_keyed_unification ()) then fun cl -> true else match kop with | None -> fun _ -> true @@ -1767,7 +1761,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = (try if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then (try - if !keyed_unification then + if is_keyed_unification () then let f1, l1 = decompose_app_vect evd op in let f2, l2 = decompose_app_vect evd cl in w_typed_unify_array env evd flags f1 l1 f2 l2,cl @@ -1913,7 +1907,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = else let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = - if unsafe_occur_meta_or_existential op || !keyed_unification then + if unsafe_occur_meta_or_existential op || is_keyed_unification () then (* This is up to delta for subterms w/o metas ... *) flags else diff --git a/printing/printer.ml b/printing/printer.ml index 32dc4bb0f0..81c0a36f53 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -25,42 +25,26 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration -let enable_unfocused_goal_printing = ref false -let enable_goal_tags_printing = ref false -let enable_goal_names_printing = ref false - -let should_tag() = !enable_goal_tags_printing -let should_unfoc() = !enable_unfocused_goal_printing -let should_gname() = !enable_goal_names_printing - - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Unfocused"]; - optread = (fun () -> !enable_unfocused_goal_printing); - optwrite = (fun b -> enable_unfocused_goal_printing:=b) } - (* This is set on by proofgeneral proof-tree mode. But may be used for other purposes *) -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Goal";"Tags"]; - optread = (fun () -> !enable_goal_tags_printing); - optwrite = (fun b -> enable_goal_tags_printing:=b) } - - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Goal";"Names"]; - optread = (fun () -> !enable_goal_names_printing); - optwrite = (fun b -> enable_goal_names_printing:=b) } - +let print_goal_tag_opt_name = ["Printing";"Goal";"Tags"] +let should_tag = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:print_goal_tag_opt_name + ~value:false + +let should_unfoc = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Unfocused"] + ~value:false + +let should_gname = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Goal";"Names"] + ~value:false (**********************************************************************) (** Terms *) @@ -407,17 +391,10 @@ let pr_context_limit_compact ?n env sigma = (* The number of printed hypothesis in a goal *) (* If [None], no limit *) -let print_hyps_limit = ref (None : int option) +let print_hyps_limit = + Goptions.declare_intopt_option_and_ref ~depr:false ~key:["Hyps";"Limit"] -let () = - let open Goptions in - declare_int_option - { optdepr = false; - optkey = ["Hyps";"Limit"]; - optread = (fun () -> !print_hyps_limit); - optwrite = (fun x -> print_hyps_limit := x) } - -let pr_context_of env sigma = match !print_hyps_limit with +let pr_context_of env sigma = match print_hyps_limit () with | None -> hv 0 (pr_context_limit_compact env sigma) | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) @@ -615,18 +592,14 @@ let print_evar_constraints gl sigma = str" with candidates:" ++ fnl () ++ hov 0 ppcandidates else mt () -let should_print_dependent_evars = ref false - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Printing";"Dependent";"Evars";"Line"]; - optread = (fun () -> !should_print_dependent_evars); - optwrite = (fun v -> should_print_dependent_evars := v) } +let should_print_dependent_evars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Dependent";"Evars";"Line"] + ~value:false let print_dependent_evars gl sigma seeds = - if !should_print_dependent_evars then + if should_print_dependent_evars () then let mt_pp = mt () in let evars = Evarutil.gather_dependent_evars sigma seeds in let evars_pp = Evar.Map.fold (fun e i s -> diff --git a/printing/printer.mli b/printing/printer.mli index 936426949c..8c633b5e79 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -19,9 +19,7 @@ open Notation_term (** These are the entry points for printing terms, context, tac, ... *) -val enable_unfocused_goal_printing: bool ref -val enable_goal_tags_printing : bool ref -val enable_goal_names_printing : bool ref +val print_goal_tag_opt_name : string list (** Terms *) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 3a6424ba9f..c78cc96a83 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -46,36 +46,37 @@ let write_color_enabled enabled = let color_enabled () = !term_color -let diff_option = ref `OFF +type diffOpt = DiffOff | DiffOn | DiffRemoved -let read_diffs_option () = match !diff_option with -| `OFF -> "off" -| `ON -> "on" -| `REMOVED -> "removed" +let diffs_to_string = function + | DiffOff -> "off" + | DiffOn -> "on" + | DiffRemoved -> "removed" -let write_diffs_option opt = - let enable opt = - if not (color_enabled ()) then - CErrors.user_err Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") - else - diff_option := opt - in - match opt with - | "off" -> diff_option := `OFF - | "on" -> enable `ON - | "removed" -> enable `REMOVED + +let assert_color_enabled () = + if not (color_enabled ()) then + CErrors.user_err + Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") + +let string_to_diffs = function + | "off" -> DiffOff + | "on" -> assert_color_enabled (); DiffOn + | "removed" -> assert_color_enabled (); DiffRemoved | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".") -let () = - Goptions.(declare_string_option { - optdepr = false; - optkey = ["Diffs"]; - optread = read_diffs_option; - optwrite = write_diffs_option - }) +let opt_name = ["Diffs"] + +let diff_option = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:opt_name + ~value:DiffOff + string_to_diffs + diffs_to_string -let show_diffs () = !diff_option <> `OFF;; -let show_removed () = !diff_option = `REMOVED;; +let show_diffs () = match diff_option () with DiffOff -> false | _ -> true +let show_removed () = match diff_option () with DiffRemoved -> true | _ -> false (* DEBUG/UNIT TEST *) diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 24b171770a..ea64439456 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -10,8 +10,8 @@ (* diff options *) -(** Controls whether to show diffs. Takes values "on", "off", "removed" *) -val write_diffs_option : string -> unit +(** Name of Diffs option *) +val opt_name : string list (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index 29e19778e4..e847535aaf 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -22,11 +22,6 @@ type t = | SelectId of Id.t | SelectAll -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (SelectNth 1) -let get_default_goal_selector () = !default_goal_selector - let pr_range_selector (i, j) = if i = j then Pp.int i else Pp.(int i ++ str "-" ++ int j) @@ -53,15 +48,12 @@ let parse_goal_selector = function with Failure _ -> CErrors.user_err Pp.(str err_msg) end -let () = let open Goptions in - declare_string_option - { optdepr = false; - optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> - Pp.string_of_ppcmds - (pr_goal_selector !default_goal_selector) - end; - optwrite = begin fun n -> - default_goal_selector := parse_goal_selector n - end - } +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let get_default_goal_selector = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Default";"Goal";"Selector"] + ~value:(SelectNth 1) + parse_goal_selector + (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v) diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index f1f7361317..f619bc86a1 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -174,28 +174,22 @@ module Strict = struct end (* Current bullet behavior, controlled by the option *) -let current_behavior = ref Strict.strict - -let () = - Goptions.(declare_string_option { - optdepr = false; - optkey = ["Bullet";"Behavior"]; - optread = begin fun () -> - (!current_behavior).name - end; - optwrite = begin fun n -> - current_behavior := - try Hashtbl.find behaviors n - with Not_found -> - CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) - end - }) +let current_behavior = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Bullet";"Behavior"] + ~value:Strict.strict + (fun n -> + try Hashtbl.find behaviors n + with Not_found -> + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))) + (fun v -> v.name) let put p b = - (!current_behavior).put p b + (current_behavior ()).put p b let suggest p = - (!current_behavior).suggest p + (current_behavior ()).suggest p (* Better printing for bullet exceptions *) exception SuggestNoSuchGoals of int * Proof.t diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index c8eb7b08f1..87d844edb3 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -138,7 +138,9 @@ module Make(T : Task) () = struct set_slave_opt tl (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" - | "-require" | "-w" | "-color" | "-init-file" + | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from" + | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object" + | "-w" | "-color" | "-init-file" | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 92d56d2904..57eab7ddf8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -38,33 +38,48 @@ let typeclasses_db = "typeclass_instances" (** Options handling *) let typeclasses_debug = ref 0 -let typeclasses_depth = ref None + +let typeclasses_depth_opt_name = ["Typeclasses";"Depth"] +let get_typeclasses_depth = + Goptions.declare_intopt_option_and_ref + ~depr:false + ~key:typeclasses_depth_opt_name + +let set_typeclasses_depth = + Goptions.set_int_option_value typeclasses_depth_opt_name (** When this flag is enabled, the resolution of type classes tries to avoid useless introductions. This is no longer useful since we have eta, but is here for compatibility purposes. Another compatibility issues is that the cost (in terms of search depth) can differ. *) -let typeclasses_limit_intros = ref true -let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d -let get_typeclasses_limit_intros () = !typeclasses_limit_intros - -let typeclasses_dependency_order = ref false -let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d -let get_typeclasses_dependency_order () = !typeclasses_dependency_order - -let typeclasses_iterative_deepening = ref false -let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d -let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening +let get_typeclasses_limit_intros = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Limit";"Intros"] + ~value:true + +let get_typeclasses_dependency_order = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Dependency";"Order"] + ~value:false + +let iterative_deepening_opt_name = ["Typeclasses";"Iterative";"Deepening"] +let get_typeclasses_iterative_deepening = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:iterative_deepening_opt_name + ~value:false (** [typeclasses_filtered_unif] governs the unification algorithm used by type classes. If enabled, a new algorithm based on pattern filtering and refine will be used. When disabled, the previous algorithm based on apply will be used. *) -let typeclasses_filtered_unification = ref false -let set_typeclasses_filtered_unification d = - (:=) typeclasses_filtered_unification d -let get_typeclasses_filtered_unification () = - !typeclasses_filtered_unification +let get_typeclasses_filtered_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Filtered";"Unification"] + ~value:false let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0) let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false @@ -75,40 +90,8 @@ let set_typeclasses_verbose = let get_typeclasses_verbose () = if !typeclasses_debug = 0 then None else Some !typeclasses_debug -let set_typeclasses_depth d = (:=) typeclasses_depth d -let get_typeclasses_depth () = !typeclasses_depth - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Limit";"Intros"]; - optread = get_typeclasses_limit_intros; - optwrite = set_typeclasses_limit_intros; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Dependency";"Order"]; - optread = get_typeclasses_dependency_order; - optwrite = set_typeclasses_dependency_order; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Iterative";"Deepening"]; - optread = get_typeclasses_iterative_deepening; - optwrite = set_typeclasses_iterative_deepening; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Filtered";"Unification"]; - optread = get_typeclasses_filtered_unification; - optwrite = set_typeclasses_filtered_unification; } - let () = + let open Goptions in declare_bool_option { optdepr = false; optkey = ["Typeclasses";"Debug"]; @@ -116,24 +99,18 @@ let () = optwrite = set_typeclasses_debug; } let _ = + let open Goptions in declare_int_option { optdepr = false; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } -let () = - declare_int_option - { optdepr = false; - optkey = ["Typeclasses";"Depth"]; - optread = get_typeclasses_depth; - optwrite = set_typeclasses_depth; } - type search_strategy = Dfs | Bfs let set_typeclasses_strategy = function - | Dfs -> set_typeclasses_iterative_deepening false - | Bfs -> set_typeclasses_iterative_deepening true + | Dfs -> Goptions.set_bool_option_value iterative_deepening_opt_name false + | Bfs -> Goptions.set_bool_option_value iterative_deepening_opt_name true let pr_ev evs ev = Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev) @@ -977,7 +954,7 @@ module Search = struct | None -> None (* This happens only because there's no evar having p *) | Some (goals, nongoals) -> let goalsl = - if !typeclasses_dependency_order then + if get_typeclasses_dependency_order () then top_sort evm goals else Evar.Set.elements goals in diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index e26338436d..b97b90d777 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -19,10 +19,8 @@ val catchable : exn -> bool [@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] val set_typeclasses_debug : bool -> unit -val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit -val get_typeclasses_depth : unit -> int option type search_strategy = Dfs | Bfs diff --git a/tactics/hints.ml b/tactics/hints.ml index a907b9e783..f8a46fcb1d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -188,27 +188,26 @@ type hints_expr = | HintsConstructors of qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument -type import_level = [ `LAX | `WARN | `STRICT ] - -let warn_hint : import_level ref = ref `LAX -let read_warn_hint () = match !warn_hint with -| `LAX -> "Lax" -| `WARN -> "Warn" -| `STRICT -> "Strict" - -let write_warn_hint = function -| "Lax" -> warn_hint := `LAX -| "Warn" -> warn_hint := `WARN -| "Strict" -> warn_hint := `STRICT -| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") - -let () = - Goptions.(declare_string_option - { optdepr = false; - optkey = ["Loose"; "Hint"; "Behavior"]; - optread = read_warn_hint; - optwrite = write_warn_hint; - }) +type import_level = HintLax | HintWarn | HintStrict + +let warn_hint_to_string = function +| HintLax -> "Lax" +| HintWarn -> "Warn" +| HintStrict -> "Strict" + +let string_to_warn_hint = function +| "Lax" -> HintLax +| "Warn" -> HintWarn +| "Strict" -> HintStrict +| _ -> user_err Pp.(str "Only the following values are accepted: Lax, Warn, Strict.") + +let warn_hint = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Loose"; "Hint"; "Behavior"] + ~value:HintLax + string_to_warn_hint + warn_hint_to_string let fresh_key = let id = Summary.ref ~name:"HINT-COUNTER" 0 in @@ -1690,12 +1689,12 @@ let wrap_hint_warning_fun env sigma t = in (ans, set_extra_data store sigma) -let run_hint tac k = match !warn_hint with -| `LAX -> k tac.obj -| `WARN -> +let run_hint tac k = match warn_hint () with +| HintLax -> k tac.obj +| HintWarn -> if is_imported tac then k tac.obj else Proofview.tclTHEN (log_hint tac) (k tac.obj) -| `STRICT -> +| HintStrict -> if is_imported tac then k tac.obj else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 22d0ce5328..c139594f13 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -14,15 +14,11 @@ open Names open Environ open Evd -let use_unification_heuristics_ref = ref true -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Solve";"Unification";"Constraints"]; - optread = (fun () -> !use_unification_heuristics_ref); - optwrite = (fun a -> use_unification_heuristics_ref:=a); -}) - -let use_unification_heuristics () = !use_unification_heuristics_ref +let use_unification_heuristics = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Solve";"Unification";"Constraints"] + ~value:true exception NoSuchGoal let () = CErrors.register_handler begin function diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index d7dcc13e79..98de0c848b 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -130,28 +130,27 @@ let get_open_goals ps = type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t let private_poly_univs = - let b = ref true in - let _ = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Private";"Polymorphic";"Universes"]; - optread = (fun () -> !b); - optwrite = ((:=) b); - }) - in - fun () -> !b + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Private";"Polymorphic";"Universes"] + ~value:true (* XXX: This is still separate from close_proof below due to drop_pt in the STM *) -let return_proof { proof } = - let Proof.{name=pid;entry} = Proof.data proof in +(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *) +let prepare_proof ~unsafe_typ { proof } = + let Proof.{name=pid;entry;poly} = Proof.data proof in let initial_goals = Proofview.initial_goals entry in let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in - let proof_opt c = + let to_constr_body c = match EConstr.to_constr_opt evd c with | Some p -> p | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") in + let to_constr_typ t = + if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t + in (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) @@ -164,31 +163,24 @@ let return_proof { proof } = equations and so far there is no code in the CI that will actually call those and do a side-effect, TTBOMK *) (* EJGA: likely the right solution is to attach side effects to the first constant only? *) - let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in + let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in proofs, Evd.evar_universe_context evd let close_proof ~opaque ~keep_body_ucst_separate ps = - let elist, uctx = return_proof ps in + let { section_vars; proof; udecl; initial_euctx } = ps in - let { Proof.name; poly; entry; sigma } = Proof.data proof in + let { Proof.name; poly } = Proof.data proof in + let unsafe_typ = keep_body_ucst_separate && not poly in + let elist, uctx = prepare_proof ~unsafe_typ ps in let opaque = match opaque with Opaque -> true | Transparent -> false in - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in + let make_entry ((body, eff), typ) = - let make_entry (body, eff) (_, typ) = let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) + not poly && + (keep_body_ucst_separate + || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private)) in - (* EJGA: Why are we doing things this way? *) - let typ = EConstr.Unsafe.to_constr typ in - let typ = if allow_deferred then typ else nf typ in - (* EJGA: End "Why are we doing things this way?" *) - let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in let used_univs = Univ.LSet.union used_univs_body used_univs_typ in @@ -223,7 +215,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = in Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in - let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in + let entries = CList.map make_entry elist in { name; entries; uctx } let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = @@ -280,6 +272,10 @@ let return_partial_proof { proof } = let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd +let return_proof ps = + let p, uctx = prepare_proof ~unsafe_typ:false ps in + List.map fst p, uctx + let update_global_env = map_proof (fun p -> let { Proof.sigma } = Proof.data p in diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index db09a2e69e..f681e4e99e 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -53,13 +53,8 @@ let whd_cbn flags env sigma t = let strong_cbn flags = strong_with_flags whd_cbn flags -let simplIsCbn = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["SimplIsCbn"]; - optread = (fun () -> !simplIsCbn); - optwrite = (fun a -> simplIsCbn:=a); -}) +let simplIsCbn = + Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false let set_strategy_one ref l = let k = @@ -228,10 +223,10 @@ let reduction_of_red_expr env = else (e_red red_product,DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> - let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in - let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in + let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in + let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in let () = - if not (!simplIsCbn || List.is_empty f.rConst) then + if not (simplIsCbn () || List.is_empty f.rConst) then warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) diff --git a/test-suite/Makefile b/test-suite/Makefile index eade52b6eb..954a922c8c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -354,8 +354,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primit } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ - $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ + $(coqchk) -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -381,7 +380,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -405,7 +404,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v index 13c47edc8f..e9e9c552f6 100644 --- a/test-suite/bugs/closed/bug_4544.v +++ b/test-suite/bugs/closed/bug_4544.v @@ -1003,7 +1003,8 @@ Proof. = loops_functor (group_loops_functor (pmap_compose psi phi)) g). rewrite <- p. - Fail Timeout 1 Time rewrite !loops_functor_group. + Timeout 1 Time rewrite !loops_functor_group. + Undo. (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) Timeout 1 do 3 rewrite loops_functor_group. Abort. diff --git a/test-suite/success/let_universes.v b/test-suite/success/let_universes.v new file mode 100644 index 0000000000..c780ec010f --- /dev/null +++ b/test-suite/success/let_universes.v @@ -0,0 +1,5 @@ +Section S. +Let bla@{} := Prop. +Let bli@{u} := Type@{u}. +Fail Let blo@{} := Type. +End S. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 82055c4752..f78c0ecc1e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -550,14 +550,14 @@ Ltac intuition_in := repeat (intuition; inv In; inv MapsTo). Let's do its job by hand: *) Ltac join_tac := - intros l; induction l as [| ll _ lx ld lr Hlr lh]; - [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE]; + intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh]; + [ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join; + [ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE]; [ match goal with |- context [ bal ?u ?v ?w ?z ] => replace (bal u v w z) with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] end - | destruct (gt_le_dec rh (lh+2)) as [GT'|LE']; + | destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE']; [ match goal with |- context [ bal ?u ?v ?w ?z ] => replace (bal u v w z) with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index c4f738ac39..bacc4a7650 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -690,7 +690,7 @@ Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed. Lemma tail00_spec x : φ x = 0 -> φ (tail0 x) = φ digits. Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed. -Infix "≡" := (eqm wB) (at level 80) : int63_scope. +Infix "≡" := (eqm wB) (at level 70, no associativity) : int63_scope. Lemma eqm_mod x y : x mod wB ≡ y mod wB → x ≡ y. Proof. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 387ab75362..4179765dca 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1753,7 +1753,7 @@ Qed. Ltac destr_pggcdn IHn := match goal with |- context [ ggcdn _ ?x ?y ] => - generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl + generalize (IHn x y); destruct ggcdn as (?g,(?u,?v)); simpl end. Lemma ggcdn_correct_divisors : forall n a b, diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 288aa0c789..83c690ab71 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -317,6 +317,82 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. End PositiveOrderedTypeBits. +Module Ascii_as_OT <: UsualOrderedType. + Definition t := ascii. + + Definition eq := @eq ascii. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. + + Definition cmp (a b : ascii) : comparison := + N.compare (N_of_ascii a) (N_of_ascii b). + + Lemma cmp_eq (a b : ascii): + cmp a b = Eq <-> a = b. + Proof. + unfold cmp. + rewrite N.compare_eq_iff. + split. 2:{ intro. now subst. } + intro H. + rewrite<- (ascii_N_embedding a). + rewrite<- (ascii_N_embedding b). + now rewrite H. + Qed. + + Lemma cmp_lt_nat (a b : ascii): + cmp a b = Lt <-> (nat_of_ascii a < nat_of_ascii b)%nat. + Proof. + unfold cmp. unfold nat_of_ascii. + rewrite N2Nat.inj_compare. + rewrite Nat.compare_lt_iff. + reflexivity. + Qed. + + Lemma cmp_antisym (a b : ascii): + cmp a b = CompOpp (cmp b a). + Proof. + unfold cmp. + apply N.compare_antisym. + Qed. + + Definition lt (x y : ascii) := (N_of_ascii x < N_of_ascii y)%N. + + Lemma lt_trans (x y z : ascii): + lt x y -> lt y z -> lt x z. + Proof. + apply N.lt_trans. + Qed. + + Lemma lt_not_eq (x y : ascii): + lt x y -> x <> y. + Proof. + intros L H. subst. + exact (N.lt_irrefl _ L). + Qed. + + Local Lemma compare_helper_eq {a b : ascii} (E : cmp a b = Eq): + a = b. + Proof. + now apply cmp_eq. + Qed. + + Local Lemma compare_helper_gt {a b : ascii} (G : cmp a b = Gt): + lt b a. + Proof. + now apply N.compare_gt_iff. + Qed. + + Definition compare (a b : ascii) : Compare lt eq a b := + match cmp a b as z return _ = z -> _ with + | Lt => fun E => LT E + | Gt => fun E => GT (compare_helper_gt E) + | Eq => fun E => EQ (compare_helper_eq E) + end Logic.eq_refl. + + Definition eq_dec (x y : ascii): {x = y} + { ~ (x = y)} := ascii_dec x y. +End Ascii_as_OT. + (** [String] is an ordered type with respect to the usual lexical order. *) Module String_as_OT <: UsualOrderedType. @@ -378,32 +454,106 @@ Module String_as_OT <: UsualOrderedType. apply Nat.lt_irrefl in H2; auto. Qed. - Definition compare x y : Compare lt eq x y. + Fixpoint cmp (a b : string) : comparison := + match a, b with + | EmptyString, EmptyString => Eq + | EmptyString, _ => Lt + | String _ _, EmptyString => Gt + | String a_head a_tail, String b_head b_tail => + match Ascii_as_OT.cmp a_head b_head with + | Lt => Lt + | Gt => Gt + | Eq => cmp a_tail b_tail + end + end. + + Lemma cmp_eq (a b : string): + cmp a b = Eq <-> a = b. Proof. - generalize dependent y. - induction x as [ | a s1]; destruct y as [ | b s2]. - - apply EQ; constructor. - - apply LT; constructor. - - apply GT; constructor. - - destruct ((nat_of_ascii a) ?= (nat_of_ascii b))%nat eqn:ltb. - + assert (a = b). - { - apply Nat.compare_eq in ltb. - assert (ascii_of_nat (nat_of_ascii a) - = ascii_of_nat (nat_of_ascii b)) by auto. - repeat rewrite ascii_nat_embedding in H. - auto. - } - subst. - destruct (IHs1 s2). - * apply LT; constructor; auto. - * apply EQ. unfold eq in e. subst. constructor; auto. - * apply GT; constructor; auto. - + apply nat_compare_lt in ltb. - apply LT; constructor; auto. - + apply nat_compare_gt in ltb. - apply GT; constructor; auto. - Defined. + revert b. + induction a, b; try easy. + cbn. + remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc. + destruct c; split; try discriminate; + try rewrite Ascii_as_OT.cmp_eq in Heqc; try subst; + try rewrite IHa; intro H. + { now subst. } + { now inversion H. } + { inversion H; subst. rewrite<- Heqc. now rewrite Ascii_as_OT.cmp_eq. } + { inversion H; subst. rewrite<- Heqc. now rewrite Ascii_as_OT.cmp_eq. } + Qed. + + Lemma cmp_antisym (a b : string): + cmp a b = CompOpp (cmp b a). + Proof. + revert b. + induction a, b; try easy. + cbn. rewrite IHa. clear IHa. + remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc. + destruct c; rewrite Ascii_as_OT.cmp_antisym in Heqc; + destruct Ascii_as_OT.cmp; cbn in *; easy. + Qed. + + Lemma cmp_lt (a b : string): + cmp a b = Lt <-> lt a b. + Proof. + revert b. + induction a as [ | a_head a_tail ], b; try easy; cbn. + { split; trivial. intro. apply lts_empty. } + remember (Ascii_as_OT.cmp _ _) as c eqn:Heqc. symmetry in Heqc. + destruct c; split; intro H; try discriminate; trivial. + { + rewrite Ascii_as_OT.cmp_eq in Heqc. subst. + apply String_as_OT.lts_tail. + apply IHa_tail. + assumption. + } + { + rewrite Ascii_as_OT.cmp_eq in Heqc. subst. + inversion H; subst. { rewrite IHa_tail. assumption. } + exfalso. apply (Nat.lt_irrefl (nat_of_ascii a)). assumption. + } + { + apply String_as_OT.lts_head. + rewrite<- Ascii_as_OT.cmp_lt_nat. + assumption. + } + { + exfalso. inversion H; subst. + { + assert(X: Ascii_as_OT.cmp a a = Eq). { apply Ascii_as_OT.cmp_eq. trivial. } + rewrite Heqc in X. discriminate. + } + rewrite<- Ascii_as_OT.cmp_lt_nat in *. rewrite Heqc in *. discriminate. + } + Qed. + + Local Lemma compare_helper_lt {a b : string} (L : cmp a b = Lt): + lt a b. + Proof. + now apply cmp_lt. + Qed. + + Local Lemma compare_helper_gt {a b : string} (G : cmp a b = Gt): + lt b a. + Proof. + rewrite cmp_antisym in G. + rewrite CompOpp_iff in G. + now apply cmp_lt. + Qed. + + Local Lemma compare_helper_eq {a b : string} (E : cmp a b = Eq): + a = b. + Proof. + now apply cmp_eq. + Qed. + + Definition compare (a b : string) : Compare lt eq a b := + match cmp a b as z return _ = z -> _ with + | Lt => fun E => LT (compare_helper_lt E) + | Gt => fun E => GT (compare_helper_gt E) + | Eq => fun E => EQ (compare_helper_eq E) + end Logic.eq_refl. Definition eq_dec (x y : string): {x = y} + { ~ (x = y)} := string_dec x y. End String_as_OT. diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000000..b9af76d699 --- /dev/null +++ b/theories/dune @@ -0,0 +1,38 @@ +(coq.theory + (name Coq) + (package coq) + (synopsis "Coq's Standard Library") + (flags -q) + ; (mode native) + (boot) + ; (per_file + ; (Init/*.v -> -boot)) + (libraries + coq.plugins.ltac + coq.plugins.tauto + + coq.plugins.cc + coq.plugins.firstorder + + coq.plugins.numeral_notation + coq.plugins.string_notation + coq.plugins.int63_syntax + coq.plugins.r_syntax + coq.plugins.float_syntax + + coq.plugins.btauto + coq.plugins.rtauto + + coq.plugins.setoid_ring + coq.plugins.nsatz + coq.plugins.omega + + coq.plugins.zify + coq.plugins.micromega + + coq.plugins.funind + + coq.plugins.ssreflect + coq.plugins.derive)) + +(include_subdirs qualified) diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index f3b70f61d2..3d955fec4f 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -21,7 +21,7 @@ Declare ML Module "micromega_plugin". Ltac zchecker := - intros __wit __varmap __ff ; + intros ?__wit ?__varmap ?__ff ; exact (ZTautoChecker_sound __ff __wit (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). diff --git a/theories/micromega/Lqa.v b/theories/micromega/Lqa.v index 786c9275f0..8a4d59b1bd 100644 --- a/theories/micromega/Lqa.v +++ b/theories/micromega/Lqa.v @@ -23,7 +23,7 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac rchange := - intros __wit __varmap __ff ; + intros ?__wit ?__varmap ?__ff ; change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit). diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v index 3ac4772ba4..22cef50e0d 100644 --- a/theories/micromega/Lra.v +++ b/theories/micromega/Lra.v @@ -23,7 +23,7 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac rchange := - intros __wit __varmap __ff ; + intros ?__wit ?__varmap ?__ff ; change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ; apply (RTautoChecker_sound __ff __wit). diff --git a/theories/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v index 89a5ca6740..15b2618e47 100644 --- a/theories/setoid_ring/Field_tac.v +++ b/theories/setoid_ring/Field_tac.v @@ -215,7 +215,7 @@ Ltac fold_field_cond req := Ltac simpl_PCond FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); + try (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req; try exact I. @@ -223,7 +223,7 @@ Ltac simpl_PCond FLD := Ltac simpl_PCond_BEURK FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); + (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index b8e498898b..597351db9b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -54,7 +54,7 @@ OCAMLWARN := $(COQMF_WARN) # # Parameters are make variable assignments. # They can be passed to (each call to) make on the command line. -# They can also be put in @LOCAL_FILE@ once an for all. +# They can also be put in @LOCAL_FILE@ once and for all. # For retro-compatibility reasons they can be put in the _CoqProject, but this # practice is discouraged since _CoqProject better not contain make specific # code (be nice to user interfaces). @@ -616,6 +616,7 @@ cleanall:: clean $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache .PHONY: cleanall archclean:: diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml deleted file mode 100644 index 472e6b4948..0000000000 --- a/tools/coq_dune.ml +++ /dev/null @@ -1,301 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license: - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - *) - -(* coq_dune: generate dune build rules for .vo files *) -(* *) -(* At some point this file will become a Dune plugin, so it is very *) -(* important that this file can be bootstrapped with: *) -(* *) -(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune *) - -open Format - -(* Keeping this file self-contained as it is a "bootstrap" utility *) -(* Is OCaml missing these basic functions in the stdlib? *) -module Aux = struct - - let option_iter f o = match o with - | Some x -> f x - | None -> () - - let option_cata d f o = match o with - | Some x -> f x - | None -> d - - let list_compare f = let rec lc x y = match x, y with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r - in lc - - let rec pp_list pp sep fmt l = match l with - | [] -> () - | [l] -> fprintf fmt "%a" pp l - | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs - - let rec pmap f l = match l with - | [] -> [] - | x :: xs -> - begin match f x with - | None -> pmap f xs - | Some r -> r :: pmap f xs - end - - let sep fmt () = fprintf fmt "@;" - - (* Creation of paths, aware of the platform separator. *) - let bpath l = String.concat Filename.dir_sep l - - module DirOrd = struct - type t = string list - let compare = list_compare String.compare - end - - module DirMap = Map.Make(DirOrd) - - (* Functions available in newer OCaml versions *) - (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) - module Legacy = struct - - - (* Fix once we move to OCaml >= 4.06.0 *) - let list_init len f = - let rec init_aux i n f = - if i >= n then [] - else let r = f i in r :: init_aux (i+1) n f - in init_aux 0 len f - - (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) - let dirmap_update key f map = - match begin - try f (Some (DirMap.find key map)) - with Not_found -> f None - end with - | None -> DirMap.remove key map - | Some x -> DirMap.add key x map - - end - - let add_map_list key elem map = - (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) - Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map - - let replace_ext ~file ~newext = - Filename.(remove_extension file) ^ newext - -end - -open Aux - -(* Once this is a Dune plugin the flags will be taken from the env *) -module Options = struct - - type flag = { - enabled : bool; - cmd : string; - } - - let all_opts = - [ { enabled = false; cmd = "-debug"; } - ; { enabled = false; cmd = "-native_compiler"; } - ; { enabled = true; cmd = "-w +default"; } - ] - - let build_coq_flags () = - let popt o = if o.enabled then Some o.cmd else None in - String.concat " " @@ pmap popt all_opts -end - -type vodep = { - target: string; - deps : string list; -} - -type ldep = | VO of vodep | MLG of string -type ddir = ldep list DirMap.t - -(* Filter `.vio` etc... *) -let filter_no_vo = - List.filter (fun f -> Filename.check_suffix f ".vo") - -(* We could have coqdep to output dune files directly *) - -let gen_sub n = - (* Move to List.init once we can depend on OCaml >= 4.06.0 *) - bpath @@ Legacy.list_init n (fun _ -> "..") - -let pp_rule fmt targets deps action = - (* Special printing of the first rule *) - let ppl = pp_list pp_print_string sep in - let pp_deps fmt l = match l with - | [] -> - () - | x :: xs -> - fprintf fmt "(:pp-file %s)%a" x sep (); - pp_list pp_print_string sep fmt xs - in - fprintf fmt - "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" - ppl targets pp_deps deps pp_print_string action - -let gen_coqc_targets vo = - [ vo.target - ; replace_ext ~file:vo.target ~newext:".glob" - ; replace_ext ~file:vo.target ~newext:".vos" - ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] - -(* Generate the dune rule: *) -let pp_vo_dep dir fmt vo = - let depth = List.length dir in - let sdir = gen_sub depth in - (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) - let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in - (* Coq flags *) - let cflag = Options.build_coq_flags () in - (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) - let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in - (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in - (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) - let libflag = "-coqlib %{project_root}" in - (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in - let all_targets = gen_coqc_targets vo in - pp_rule fmt all_targets deps action - -let pp_mlg_dep _dir fmt ml = - fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml) - -let pp_dep dir fmt oo = match oo with - | VO vo -> pp_vo_dep dir fmt vo - | MLG f -> pp_mlg_dep dir fmt f - -let out_install fmt dir ff = - let itarget = String.concat "/" dir in - let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" - (pp_list pp_ispec sep) ff - -(* For each directory, we must record two things, the build rules and - the install specification. *) -let record_dune d ff = - let sd = bpath d in - if Sys.file_exists sd && Sys.is_directory sd then - let out = open_out (bpath [sd;"dune"]) in - let fmt = formatter_of_out_channel out in - if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then - fprintf fmt "(include plugin_base.dune)@\n"; - out_install fmt d ff; - List.iter (pp_dep d fmt) ff; - fprintf fmt "%!"; - close_out out - else - eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd - -(* File Scanning *) -let scan_mlg ~root m d = - let dir = [root; d] in - let m = DirMap.add dir [] m in - let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg")) - Array.(to_list @@ readdir (bpath dir))) in - List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg - -let scan_dir ~root m = - let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in - let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in - List.fold_left (scan_mlg ~root) m dirs - -let scan_plugins m = scan_dir ~root:"plugins" m -let scan_usercontrib m = scan_dir ~root:"user-contrib" m - -(* This will be removed when we drop support for Make *) -let fix_cmo_cma file = - if String.equal Filename.(extension file) ".cmo" - then replace_ext ~file ~newext:".cma" - else file - -(* Process .vfiles.d and generate a skeleton for the dune file *) -let parse_coqdep_line l = - match Str.(split (regexp ":") l) with - | [targets;deps] -> - let targets = Str.(split (regexp "[ \t]+") targets) in - let deps = Str.(split (regexp "[ \t]+") deps) in - let targets = filter_no_vo targets in - begin match targets with - | [target] -> - let dir, target = Filename.(dirname target, basename target) in - (* coqdep outputs with the '/' directory separator regardless of - the platform. Anyways, I hope we can link to coqdep instead - of having to parse its output soon, that should solve this - kind of issues *) - let deps = List.map fix_cmo_cma deps in - Some (String.split_on_char '/' dir, VO { target; deps; }) - (* Otherwise a vio file, we ignore *) - | _ -> None - end - (* Strange rule, we ignore *) - | _ -> None - -let rec read_vfiles ic map = - try - let rule = parse_coqdep_line (input_line ic) in - (* Add vo_entry to its corresponding map entry *) - let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in - read_vfiles ic map - with End_of_file -> map - -let out_map map = - DirMap.iter record_dune map - -let exec_ifile f = - match Array.length Sys.argv with - | 1 -> f stdin - | 2 -> - let in_file = Sys.argv.(1) in - begin try - let ic = open_in in_file in - (try f ic - with exn -> - eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); - close_in ic) - with _ -> - eprintf "Error: cannot open input file %s@\n%!" in_file - end - | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 - -let _ = - exec_ifile (fun ic -> - let map = scan_plugins DirMap.empty in - let map = scan_usercontrib map in - let map = read_vfiles ic map in - out_map map) diff --git a/tools/dune b/tools/dune index c0e4e20f72..d591bb0c37 100644 --- a/tools/dune +++ b/tools/dune @@ -49,8 +49,8 @@ (ocamllex coqwc) (executables - (names coq_tex coq_dune) - (public_names coq-tex coq_dune) + (names coq_tex) + (public_names coq-tex) (package coq) - (modules coq_tex coq_dune) + (modules coq_tex) (libraries str)) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 4963a806f5..1988c7cc42 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -44,7 +44,6 @@ type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; toplevel_name : Stm.interactive_top; - allow_sprop : bool; cumulative_sprop : bool; } @@ -59,7 +58,6 @@ type coqargs_config = { native_include_dirs : CUnix.physical_path list; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; - diffs_set : bool; time : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; @@ -112,7 +110,6 @@ let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; toplevel_name = Stm.TopLogical default_toplevel; - allow_sprop = true; cumulative_sprop = false; } @@ -127,7 +124,6 @@ let default_config = { native_include_dirs = []; stm_flags = Stm.AsyncOpts.default_opts; debug = false; - diffs_set = false; time = false; print_emacs = false; set_options = []; @@ -178,9 +174,12 @@ let add_vo_require opts d p export = let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} +let add_set_option opts opt_name value = + { opts with config = { opts.config with set_options = (opt_name, value) :: opts.config.set_options }} + (** Options for proof general *) let set_emacs opts = - Printer.enable_goal_tags_printing := true; + Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true; { opts with config = { opts.config with color = `EMACS; print_emacs = true }} let set_logic f oval = @@ -203,10 +202,6 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") -let warn_deprecated_simple_require = - CWarnings.create ~name:"deprecated-boot" ~category:"deprecated" - (fun () -> Pp.strbrk "The -require option is deprecated, please use -require-import instead.") - let set_inputstate opts s = warn_deprecated_inputstate (); { opts with pre = { opts.pre with inputstate = Some s }} @@ -422,10 +417,6 @@ let parse_args ~help ~init arglist : t * string list = |"-rfrom" -> let from = next () in add_vo_require oval (next ()) (Some from) None - |"-require" -> - warn_deprecated_simple_require (); - add_vo_require oval (next ()) None (Some false) - |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) @@ -481,14 +472,11 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with native_compiler }} | "-set" -> - let opt = next() in - let opt, v = parse_option_set opt in - { oval with config = { oval.config with set_options = (opt, OptionSet v) :: oval.config.set_options }} + let opt, v = parse_option_set @@ next() in + add_set_option oval opt (OptionSet v) | "-unset" -> - let opt = next() in - let opt = to_opt_key opt in - { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }} + add_set_option oval (to_opt_key @@ next ()) OptionUnset |"-native-output-dir" -> let native_output_dir = next () in @@ -511,18 +499,16 @@ let parse_args ~help ~init arglist : t * string list = |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval - |"-diffs" -> let opt = next () in - if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then - Proof_diffs.write_diffs_option opt - else - error_wrong_arg "Error: on|off|removed expected after -diffs"; - { oval with config = { oval.config with diffs_set = true }} + |"-diffs" -> + add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval |"-impredicative-set" -> set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval - |"-allow-sprop" -> set_logic (fun o -> { o with allow_sprop = true }) oval - |"-disallow-sprop" -> set_logic (fun o -> { o with allow_sprop = false }) oval + |"-allow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) + |"-disallow-sprop" -> + add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 3d709db54d..8723d21bb4 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -20,7 +20,6 @@ type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; toplevel_name : Stm.interactive_top; - allow_sprop : bool; cumulative_sprop : bool; } @@ -35,7 +34,6 @@ type coqargs_config = { native_include_dirs : CUnix.physical_path list; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; - diffs_set : bool; time : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7d08244d49..1175494bad 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -199,7 +199,6 @@ let init_execution opts custom_init = Global.set_VM opts.config.enable_VM; Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true); - Global.set_allow_sprop opts.config.logic.allow_sprop; if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative (); (* Native output dir *) diff --git a/user-contrib/Ltac2/Fresh.v b/user-contrib/Ltac2/Fresh.v index 548bf74a30..5ad9badc8c 100644 --- a/user-contrib/Ltac2/Fresh.v +++ b/user-contrib/Ltac2/Fresh.v @@ -9,6 +9,8 @@ (************************************************************************) Require Import Ltac2.Init. +Require Ltac2.Control. +Require Ltac2.List. Module Free. @@ -21,8 +23,12 @@ Ltac2 @ external of_ids : ident list -> t := "ltac2" "fresh_free_of_ids". Ltac2 @ external of_constr : constr -> t := "ltac2" "fresh_free_of_constr". +Ltac2 of_goal () := of_ids (List.map (fun (id, _, _) => id) (Control.hyps ())). + End Free. Ltac2 @ external fresh : Free.t -> ident -> ident := "ltac2" "fresh_fresh". (** Generate a fresh identifier with the given base name which is not a member of the provided set of free variables. *) + +Ltac2 in_goal id := Fresh.fresh (Free.of_goal ()) id. diff --git a/user-contrib/Ltac2/dune b/user-contrib/Ltac2/dune new file mode 100644 index 0000000000..90869a46a0 --- /dev/null +++ b/user-contrib/Ltac2/dune @@ -0,0 +1,14 @@ +(coq.theory + (name Ltac2) + (package coq) + (synopsis "Ltac2 tactic language") + (libraries coq.plugins.ltac2)) + +(library + (name ltac2_plugin) + (public_name coq.plugins.ltac2) + (synopsis "Ltac2 plugin") + (modules_without_implementation tac2expr tac2qexpr tac2types) + (libraries coq.plugins.ltac)) + +(coq.pp (modules g_ltac2)) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1607771598..601e7e060c 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -171,7 +171,7 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let ce = definition_entry ?opaque ?inline ?types ~univs body in let env = Global.env () in let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); + assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); RetrieveObl.check_evars env sigma; let c = EConstr.of_constr c in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 31fc54c1fa..1f52641b82 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -199,8 +199,8 @@ GRAMMAR EXTEND Gram VernacAssumption (stre, nl, bl) } | d = def_token; id = ident_decl; b = def_body -> { VernacDefinition (d, name_of_ident_decl id, b) } - | IDENT "Let"; id = identref; b = def_body -> - { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) } + | IDENT "Let"; id = ident_decl; b = def_body -> + { VernacDefinition ((DoDischarge, Let), name_of_ident_decl id, b) } (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> { VernacInductive (f, indl) } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2e509921c1..3195f339b6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1251,10 +1251,12 @@ let vernac_generalizable ~local = let local = Option.default true local in Implicit_quantifiers.declare_generalizable ~local +let allow_sprop_opt_name = ["Allow";"StrictProp"] + let () = declare_bool_option { optdepr = false; - optkey = ["Allow";"StrictProp"]; + optkey = allow_sprop_opt_name; optread = (fun () -> Global.sprop_allowed()); optwrite = Global.set_allow_sprop } @@ -1435,27 +1437,6 @@ let () = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } -let () = - declare_string_option - { optdepr = false; - optkey = ["NativeCompute"; "Profile"; "Filename"]; - optread = Nativenorm.get_profile_filename; - optwrite = Nativenorm.set_profile_filename } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["NativeCompute"; "Profiling"]; - optread = Nativenorm.get_profiling_enabled; - optwrite = Nativenorm.set_profiling_enabled } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["NativeCompute"; "Timing"]; - optread = Nativenorm.get_timing_enabled; - optwrite = Nativenorm.set_timing_enabled } - let _ = declare_bool_option { optdepr = false; diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index f5cf9702cd..2ac8458ad5 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -24,3 +24,5 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr (** Miscellaneous stuff *) val command_focus : unit Proof.focus_kind + +val allow_sprop_opt_name : string list diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 15a19c06c2..eb299222dd 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -51,24 +51,17 @@ let interp_typed_vernac c ~stack = (* Default proof mode, to be set at the beginning of proofs for programs that cannot be statically classified. *) -let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) -let get_default_proof_mode () = !default_proof_mode +let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode -let set_default_proof_mode_opt name = - default_proof_mode := - match Pvernac.lookup_proof_mode name with +let get_default_proof_mode = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:proof_mode_opt_name + ~value:(Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) + (fun name -> match Pvernac.lookup_proof_mode name with | Some pm -> pm - | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.declare_string_option Goptions.{ - optdepr = false; - optkey = proof_mode_opt_name; - optread = get_default_proof_mode_opt; - optwrite = set_default_proof_mode_opt; - } + | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))) + Pvernac.proof_mode_to_string (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) |