diff options
80 files changed, 898 insertions, 611 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 8b6b43a55..451b711be 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -54,7 +54,6 @@ opam-switch: &opam-switch - restore_cache: keys: - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}- # this grabs old cache if checksum doesn't match - run: name: Update opam lists command: | @@ -127,7 +126,7 @@ jobs: <<: *opam-boot-template environment: <<: *envvars - EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" + EXTRA_OPAM: "ocamlgraph elpi" # Build and prepare test environment build: *build-template @@ -207,6 +206,12 @@ jobs: math-comp: <<: *ci-template + mtac2: + <<: *ci-template + + pidetop: + <<: *ci-template + sf: <<: *ci-template environment: @@ -251,6 +256,7 @@ workflows: requires: - build - bignums + - mtac2: *req-main - corn: requires: - build @@ -263,6 +269,7 @@ workflows: - iris-lambda-rust: *req-main - ltac2: *req-main - math-comp: *req-main + - pidetop: *req-main - sf: *req-main - unimath: *req-main - vst: *req-main diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 7f3ee5c37..74bbda553 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -302,6 +302,12 @@ /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes +# This file belongs to CI +/Makefile.ci @ejgallego +# Secondary maintainer @SkySkimmer + +/Makefile.doc @maximedenes +# Secondary maintainer @silene ########## Developer tools ########## diff --git a/.gitignore b/.gitignore index 25c0996cb..e2a97b3a1 100644 --- a/.gitignore +++ b/.gitignore @@ -61,6 +61,7 @@ plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty +coqdoc.css time-of-build.log time-of-build-pretty.log time-of-build-before.log diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7d6b53964..d16dc5b78 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,12 +1,15 @@ -image: ubuntu:latest +image: ubuntu:bionic stages: - opam-boot - build - test +# some default values variables: - # some default values + # Format: $IMAGE-V$DATE-$HOUR-$MINUTE + CACHEKEY: bionic-V2018-04-29-00-50 + DEBIAN_FRONTEND: "noninteractive" NJOBS: "2" COMPILER: "4.02.3" CAMLP5_VER: "6.14" @@ -16,26 +19,26 @@ variables: # some useful values COMPILER_32BIT: "4.02.3+32bit" - COMPILER_BLEEDING_EDGE: "4.06.0" - CAMLP5_VER_BLEEDING_EDGE: "7.03" + COMPILER_BLEEDING_EDGE: "4.06.1" + CAMLP5_VER_BLEEDING_EDGE: "7.05" - TIMING_PACKAGES: "time python" + TIMING_PACKAGES: "time python3" COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" - COQIDE_OPAM: "lablgtk-extras" - COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6" - COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa python3-pip" - COQDOC_OPAM: "hevea" - SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex" - ELPI_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - + COQIDE_OPAM: "lablgtk.2.18.5 conf-gtksourceview.2" + COQIDE_OPAM_BE: "lablgtk.2.18.6 conf-gtksourceview.2" + COQDOC_PACKAGES: "texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip" + SPHINX_PACKAGES: "antlr4-python3-runtime" + ELPI_OPAM: "elpi" before_script: + - cat /proc/{cpu,mem}info || true - ls -a # figure out if artifacts are around - printenv # - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi - apt-get update -qq && apt-get install -y -qq m4 opam ${EXTRA_PACKAGES} + # This should be replaced by standard debian packages once python3-antlr4 makes to the archive. - if [ -n "${PIP_PACKAGES}" ]; then pip3 install ${PIP_PACKAGES}; fi # if no cache running opam config fails! - if [ -d .opamcache ]; then eval $(opam config env); fi @@ -57,9 +60,6 @@ before_script: - .opamcache expire_in: 1 week script: - # the default repo in this docker image is a local directory - # at the time of 4aaeb8abf it lagged behind the official - # repository such that camlp5 7.01 was not available - opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org - eval $(opam config env) - opam update @@ -178,16 +178,16 @@ opam-boot: cache: paths: &cache-paths - .opamcache - key: main + key: "main-$CACHEKEY" variables: - EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM ocamlgraph $ELPI_OPAM" + EXTRA_OPAM: "$COQIDE_OPAM ocamlgraph $ELPI_OPAM" EXTRA_PACKAGES: "$COQIDE_PACKAGES" opam-boot:32bit: <<: *opam-boot-template cache: paths: *cache-paths - key: 32bit + key: "32bit-$CACHEKEY" variables: COMPILER: "$COMPILER_32BIT" EXTRA_PACKAGES: "gcc-multilib" @@ -196,7 +196,7 @@ opam-boot:bleeding-edge: <<: *opam-boot-template cache: paths: *cache-paths - key: be + key: "be-$CACHEKEY" variables: COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" @@ -360,6 +360,12 @@ ci-math-classes: ci-math-comp: <<: *ci-template +ci-mtac2: + <<: *ci-template + +ci-pidetop: + <<: *ci-template + ci-sf: <<: *ci-template variables: diff --git a/.travis.yml b/.travis.yml index fe376431e..fce19f9d9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -54,7 +54,7 @@ env: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}" + - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" matrix: @@ -76,7 +76,7 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" + - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi" # ppx_tools_versioned requires a specific version findlib - FINDLIB_VER="" - if: NOT (type = pull_request) @@ -117,6 +117,12 @@ matrix: - TEST_TARGET="ci-math-comp" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-mtac2" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-pidetop" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-sf" - if: NOT (type = pull_request) env: @@ -160,8 +166,6 @@ matrix: - texlive-fonts-extra - latex-xcolor - ghostscript - - transfig - - imagemagick - tipa - python3 - python3-pip @@ -173,7 +177,7 @@ matrix: - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" before_install: *sphinx-install addons: apt: @@ -189,7 +193,7 @@ matrix: - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" before_install: *sphinx-install addons: apt: @@ -218,7 +222,7 @@ matrix: - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" addons: apt: sources: @@ -276,7 +280,7 @@ install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y num camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} - opam list script: @@ -1,6 +1,12 @@ Changes from 8.8.2 to 8.9+beta1 =============================== +Tactics + +- Added toplevel goal selector ! which expects a single focused goal. + Use with Set Default Goal Selector to force focusing before tactics + are called. + Tools - Coq_makefile lets one override or extend the following variables from @@ -13,6 +19,12 @@ Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments (not the option). Use the Arguments command instead. +Tactics + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + Tactic language - Support for fix/cofix added in Ltac "match" and "lazymatch". diff --git a/INSTALL.doc b/INSTALL.doc index 625c36869..f8a085280 100644 --- a/INSTALL.doc +++ b/INSTALL.doc @@ -22,10 +22,7 @@ To produce all the documents, the following tools are needed: - dvips - bibtex - makeindex - - fig2dev (transfig) - - convert (ImageMagick) - hevea - - hacha - Python 3 - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - sphinx_rtd_theme @@ -34,17 +31,26 @@ To produce all the documents, the following tools are needed: - Antlr4 runtime for Python 3 -Under Debian based operating systems (Debian, Ubuntu, ...) a -working set of packages for compiling the documentation for Coq is: +Under recent Debian based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) a working set of packages for compiling the +documentation for Coq is: - texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra - texlive-humanities texlive-pictures latex-xcolor hevea transfig - imagemagick - python3 python-pip3 + texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx + python3-pexpect python3-sphinx-rtd-theme python3-bs4 + python3-sphinxcontrib.bibtex python3-pip -To install the Python packages required to build the user manual, run: - pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex +Then, install the Python3 Antlr4 package: + + pip3 install antlr4-python3-runtime + +Nix users should get the correct development environment to build the +Sphinx documentation from Coq's `default.nix`. [Note Nix setup doesn't +include the LaTeX packages needed to build the full documentation.] +If you are in an older/different distribution you can install the +Python packages required to build the user manual using python3-pip: + + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex Compilation ----------- diff --git a/Makefile.ci b/Makefile.ci index 6b30f8723..78fec466c 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -28,7 +28,8 @@ CI_TARGETS=ci-bignums \ ci-ltac2 \ ci-math-classes \ ci-math-comp \ - ci-metacoq \ + ci-mtac2 \ + ci-pidetop \ ci-sf \ ci-tlc \ ci-unimath \ diff --git a/Makefile.doc b/Makefile.doc index ce31c5fcb..9b6013d8d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -32,10 +32,7 @@ BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex DVIPS:=dvips -FIG2DEV:=fig2dev -CONVERT:=convert HEVEA:=hevea -HACHA:=hacha HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=coqremote @@ -110,20 +107,6 @@ endif %.ps: %.dvi (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) -%.png: %.fig - $(FIG2DEV) -L png -m 2 $< $@ - -%.pdf: %.fig - $(FIG2DEV) -L pdftex $< $@ - $(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t - -%.eps: %.fig - $(FIG2DEV) -L pstex $< $@ - $(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t - -%.eps: %.png - $(CONVERT) $< $@ - ###################################################################### # Macros for filtering outputs ###################################################################### diff --git a/configure.ml b/configure.ml index 2ac705ad2..e77310eb7 100644 --- a/configure.ml +++ b/configure.ml @@ -21,11 +21,18 @@ let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr"; let verbose = ref false (* for debugging this script *) +let red, yellow, reset = + if Unix.isatty Unix.stdout && Unix.isatty Unix.stderr && Sys.os_type = "Unix" + then "\027[31m", "\027[33m", "\027[0m" + else "", "", "" + (** * Utility functions *) let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc let cprintf s = cfprintf stdout s let ceprintf s = cfprintf stderr s -let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1 +let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1 + +let warn s = cprintf ("%sWarning: " ^^ s ^^ "%s") yellow reset let s2i = int_of_string let i2s = string_of_int @@ -109,7 +116,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args = let cmd = String.concat " " (prog::args) in let exn = match e with Failure s -> s | _ -> Printexc.to_string e in let msg = sprintf "Error while running '%s' (%s)" cmd exn in - if fatal then die msg else (cprintf "W: %s" msg; "", []) + if fatal then die msg else (warn "%s" msg; "", []) let tryrun prog args = run ~fatal:false ~err:DevNull prog args @@ -205,7 +212,7 @@ let win_aware_quote_executable str = sprintf "%S" str else let _ = if contains_suspicious_characters str then - cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in + warn "The string %S contains suspicious characters; ocamlfind might fail" str in Str.global_replace (Str.regexp "\\\\") "/" str (** * Date *) @@ -414,8 +421,8 @@ let args_options = Arg.align [ " Do not add debugging information in the Coq executables"; "-profiling", arg_set (fun p profile -> { p with profile }), " Add profiling information in the Coq executables"; - "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."), - " Deprecated. Please use -annot or -bin-annot instead"; + "-annotate", Arg.Unit (fun () -> die "-annotate has been removed. Please use -annot or -bin-annot instead."), + " Removed option. Please use -annot or -bin-annot instead"; "-annot", arg_set (fun p annot -> { p with annot }), " Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)"; "-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }), @@ -598,7 +605,7 @@ let check_caml_version () = else let () = cprintf "Your version of OCaml is %s." caml_version in if !prefs.force_caml_version then - cprintf "*Warning* Your version of OCaml is outdated." + warn "Your version of OCaml is outdated." else die "You need OCaml 4.02.1 or later." @@ -620,7 +627,7 @@ let check_findlib_version () = else let () = cprintf "Your version of OCamlfind is %s." findlib_version in if !prefs.force_findlib_version then - cprintf "*Warning* Your version of OCamlfind is outdated." + warn "Your version of OCamlfind is outdated." else die "You need OCamlfind 1.4.1 or later." @@ -731,17 +738,17 @@ let camlp5libdir = shorten_camllib fullcamlp5libdir (** * Native compiler *) -let msg_byteonly () = - cprintf "Only the bytecode version of Coq will be available." +let msg_byteonly = + "Only the bytecode version of Coq will be available." let msg_no_ocamlopt () = - cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly () + warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly let msg_no_camlp5_cmxa () = - cprintf "Cannot find the native-code library of camlp5."; msg_byteonly () + warn "Cannot find the native-code library of camlp5.\n%s" msg_byteonly let msg_no_dynlink_cmxa () = - cprintf "Cannot find native-code dynlink library."; msg_byteonly (); + warn "Cannot find native-code dynlink library.\n%s" msg_byteonly; cprintf "For building a native-code Coq, you may try to first"; cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)"; cprintf "and then run ./configure -natdynlink no" @@ -757,8 +764,7 @@ let check_native () = else let () = if version <> caml_version then - cprintf - "Warning: Native and bytecode compilers do not have the same version!" + warn "Native and bytecode compilers do not have the same version!" in cprintf "You have native-code compilation. Good!" let best_compiler = @@ -813,7 +819,7 @@ let get_source = function (** Is some location a suitable LablGtk2 installation ? *) let check_lablgtkdir ?(fatal=false) src dir = - let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in + let yell msg = if fatal then die msg else (warn "%s" msg; false) in let msg = get_source src in if not (dir_exists dir) then yell (sprintf "No such directory '%s' (%s)." dir msg) @@ -849,7 +855,7 @@ let get_lablgtkdir () = let check_lablgtk_version src dir = match src with | Manual | Stdlib -> - cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3."; + warn "Could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3."; (true, "an unknown version") | OCamlFind -> let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in @@ -860,7 +866,11 @@ let check_lablgtk_version src dir = match src with else if vi < [2; 18; 3] then begin (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *) - cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v; + warn "Your installed lablgtk reports as %s.\n\ +It is possible that the installed version is actually more recent\n\ +but reports an incorrect version. If the installed version is\n\ +actually more recent than 2.18.3, that's fine; if it is not,\n +CoqIDE will compile but may be very unstable." v; (true, "an unknown version") end else diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5566a5117..1ae2ad0ac 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -19,13 +19,13 @@ : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}" ######################################################################## -# Unicoq + Metacoq +# Unicoq + Mtac2 ######################################################################## : "${unicoq_CI_BRANCH:=master}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" -: "${metacoq_CI_BRANCH:=master}" -: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}" +: "${mtac2_CI_BRANCH:=master-sync}" +: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}" ######################################################################## # Mathclasses + Corn @@ -156,3 +156,9 @@ ######################################################################## : "${fcsl_pcm_CI_BRANCH:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" + +######################################################################## +# pidetop +######################################################################## +: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-mtac2.sh index a66dc1e76..1372acb8e 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-mtac2.sh @@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq +mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 # Setup UniCoq @@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" # Setup MetaCoq -git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}" +git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}" -( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) +( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 000000000..d04b9637c --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" + +git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" + +( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) + +echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 3c0044bfe..79001c547 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -8,6 +8,6 @@ VST_CI_DIR="${CI_BUILD_DIR}/VST" # opam install -j ${NJOBS} -y menhir git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# Targets are: msl veric floyd progs , we remove progs to save time -# Patch to avoid the upper version limit -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd ) +# We have to omit progs as otherwise we timeout on Travis; on Gitlab +# we will be able to just use `make` +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs ) diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fd3cbd1bc..14a1cc693 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs 7. some hints: - To debug a failure/error/anomaly, add a breakpoint in - Vernac.vernac_com at the with clause of the "try ... interp com + `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com with ..." block, then go "back" a few steps to find where the failure/error/anomaly has been raised - Alternatively, for an error or an anomaly, add breakpoints in the middle diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f9b402586..8d5b5bef4 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(Termops.pr_metaset metas) -let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) -let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 1a7628d89..a93e9b156 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -874,7 +874,7 @@ In the syntax of module application, the ! prefix indicates that any Starts an interactive module satisfying each `module_type`. - .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }. + .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. Starts an interactive functor with parameters given by the list of `module_binding`. The output module type is verified against each `module_type`. @@ -1436,7 +1436,9 @@ For instance, the first argument of in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A` will always be inferable from the type :g:`list A` of the third argument of -:g:`cons`. On the contrary, the second argument of a term of type +:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one, +since the first argument is exactly the type of the second argument. +On the contrary, the second argument of a term of type :: forall P:nat->Prop, forall n:nat, P n -> ex nat P diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 009758319..7ab11889f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -272,6 +272,12 @@ focused goals with: In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. + .. tacv:: !: @expr + + In this variant, if exactly one goal is focused :n:`expr` is + applied to it. Otherwise the tactical fails. ``!:`` can only be + used at the toplevel of a tactic expression. + .. tacv:: par: @expr In this variant, :n:`@expr` is applied to all focused goals in parallel. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7a45272f2..6c1b1c08c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -53,13 +53,20 @@ specified, the default selector is used. .. opt:: Default Goal Selector @toplevel_selector - This option controls the default selector – used when no selector is - specified when applying a tactic – is set to the chosen value. The initial - value is 1, hence the tactics are, by default, applied to the first goal. - Using value ``all`` will make is so that tactics are, by default, applied to - every goal simultaneously. Then, to apply a tactic tac to the first goal - only, you can write ``1:tac``. Although more selectors are available, only - ``all`` or a single natural number are valid default goal selectors. + This option controls the default selector, used when no selector is + specified when applying a tactic. The initial value is 1, hence the + tactics are, by default, applied to the first goal. + + Using value ``all`` will make it so that tactics are, by default, + applied to every goal simultaneously. Then, to apply a tactic tac + to the first goal only, you can write ``1:tac``. + + Using value ``!`` enforces that all tactics are used either on a + single focused goal or with a local selector (’’strict focusing + mode’’). + + Although more selectors are available, only ``all``, ``!`` or a + single natural number are valid default goal selectors. .. _bindingslist: @@ -627,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -If the goal is neither a product nor starting with a let definition, +If the goal is an existential variable, ``intro`` forces the resolution of the +existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to +depend on :g:`x`. + +If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 065b42bf6..710491f84 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -342,7 +342,15 @@ let update_var src tgt subst = let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in { subst with csubst_var; csubst_rev } -let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + +let push_rel_decl_to_named_context + ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) + sigma decl (subst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = @@ -373,7 +381,9 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> + | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames || + hypnaming = KeepUserNameAndRenameExistingButSectionNames && + not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given by the user) and rename [id0] into [id] in the named @@ -382,6 +392,8 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = List.map (replace_var_named_declaration id0 id) nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) + | Some id0 when hypnaming = FailIfConflict -> + user_err Pp.(Id.print id0 ++ str " is already used.") | _ -> (* spiwack: if [id0] is a section variable renaming it is incorrect. We revert to a less robust behaviour where @@ -390,7 +402,7 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in (push_var id subst, Id.Set.add id avoid, d :: nc) -let push_rel_context_to_named_context env sigma typ = +let push_rel_context_to_named_context ?hypnaming env sigma typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in let open EConstr in @@ -405,7 +417,7 @@ let push_rel_context_to_named_context env sigma typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, _, env) = - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc) (rel_context env) ~init:(empty_csubst, avoid, named_context env) in (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) @@ -468,8 +480,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in +let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = + let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = @@ -478,13 +490,13 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal rigid = +let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in +let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid = + let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in evdref := evd; c @@ -498,8 +510,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = evdref := evd'; EConstr.mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in evdref := evd'; ev @@ -522,7 +534,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option exception Depends of Id.t @@ -533,13 +545,13 @@ let rec check_and_clear_in_constr env evdref err ids global c = is a section variable *) match kind c with | Var id' -> - if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c + if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c | ( Const _ | Ind _ | Construct _ ) -> let () = if global then let check id' = if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err)) + raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) in Id.Set.iter check (Environ.vars_of_global env c) in @@ -587,8 +599,8 @@ let rec check_and_clear_in_constr env evdref err ids global c = let global = Id.Set.exists is_section_variable nids in let concl = EConstr.Unsafe.to_constr (evar_concl evi) in check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl - with ClearDependencyError (rid,err) -> - raise (ClearDependencyError (Id.Map.find rid rids,err)) in + with ClearDependencyError (rid,err,where) -> + raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in if Id.Map.is_empty rids then c else diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 40c1ee082..e3e8f16c8 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -30,11 +30,17 @@ val new_evar_from_context : ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> evar_map * EConstr.t +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + val new_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t val new_pure_evar : named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> @@ -49,18 +55,20 @@ val e_new_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> evar_map * (constr * Sorts.t) val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr @@ -178,11 +186,14 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t @@ -224,7 +235,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types @@ -240,10 +251,11 @@ val csubst_subst : csubst -> constr -> constr type ext_named_context = csubst * Id.Set.t * named_context -val push_rel_decl_to_named_context : +val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> +val push_rel_context_to_named_context : ?hypnaming:naming_mode -> + Environ.env -> evar_map -> types -> named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index 6dcec2760..af22de5cd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1290,30 +1290,14 @@ module MiniEConstr = struct let unsafe_eq = Refl let to_constr ?(abort_on_undefined_evars=true) sigma c = - let rec to_constr c = match Constr.kind c with - | Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> to_constr c - | None -> - if abort_on_undefined_evars then - anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") - else - Constr.map (fun c -> to_constr c) c - end - | Sort (Sorts.Type u) -> - let u' = normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> Constr.map (fun c -> to_constr c) c - in to_constr c + let evar_value = + if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev + else fun ev -> + match safe_evar_value sigma ev with + | Some _ as v -> v + | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") + in + Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c let of_named_decl d = d let unsafe_to_named_decl d = d diff --git a/engine/universes.ml b/engine/universes.ml index e5f9212a7..0410d1aea 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -524,8 +524,6 @@ let new_global_univ () = (** Simplification *) -module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) - let add_list_map u t map = try let l = LMap.find u map in @@ -533,8 +531,6 @@ let add_list_map u t map = with Not_found -> LMap.add u [t] map -module UF = LevelUnionFind - (** Precondition: flexible <= ctx *) let choose_canonical ctx flexible algs s = let global = LSet.diff s ctx in @@ -596,35 +592,6 @@ let subst_univs_constr = CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr -let subst_univs_fn_puniverses lsubst (c, u as cu) = - let u' = Instance.subst_fn lsubst u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_opt_subst f subst = - let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - let lsubst = level_subst_of subst in - let rec aux c = - match kind c with - | Evar (evk, args) -> - let args = Array.map aux args in - (match try f (evk, args) with Not_found -> None with - | None -> c - | Some c -> aux c) - | Const pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> Constr.map aux c - in aux - let fresh_universe_context_set_instance ctx = if ContextSet.is_empty ctx then LMap.empty, ctx else @@ -683,6 +650,35 @@ let normalize_opt_subst ctx = type universe_opt_subst = Universe.t option universe_map +let subst_univs_fn_puniverses f (c, u as cu) = + let u' = Instance.subst_fn f u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_opt_subst f subst = + let subst = normalize_univ_variable_opt_subst (ref subst) in + let lsubst = level_subst_of subst in + let rec aux c = + match kind c with + | Evar (evk, args) -> + let args = Array.map aux args in + (match try f (evk, args) with Not_found -> None with + | None -> mkEvar (evk, args) + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> Constr.map aux c + in aux + let make_opt_subst s = fun x -> (match Univ.LMap.find x s with @@ -709,6 +705,7 @@ let pr_universe_body = function let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body +(* Eq < Le < Lt *) let compare_constraint_type d d' = match d, d' with | Eq, Eq -> 0 @@ -742,10 +739,12 @@ let lower_add l c m = let lower_of_list l = List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l +type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap } + exception Found of Level.t * lowermap let find_inst insts v = - try LMap.iter (fun k (enf,alg,v',lower) -> - if not alg && enf && Universe.equal v' v then raise (Found (k, lower))) + try LMap.iter (fun k {enforce;alg;lbound=v';lower} -> + if not alg && enforce && Universe.equal v' v then raise (Found (k, lower))) insts; raise Not_found with Found (f,l) -> (f,l) @@ -765,18 +764,18 @@ let compute_lbound left = sup (Universe.super l) lbound else None)) None left - -let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) = + +let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) = if enforce then let inst = Universe.make u in let cstrs' = enforce_leq lbound inst cstrs in (ctx, us, LSet.remove u algs, - LMap.add u (enforce,alg,lbound,lower) insts, cstrs'), - (enforce, alg, inst, lower) + LMap.add u {enforce;alg;lbound;lower} insts, cstrs'), + {enforce; alg; lbound=inst; lower} else (* Actually instantiate *) (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u (enforce,alg,lbound,lower) insts, cstrs), - (enforce, alg, lbound, lower) + LMap.add u {enforce;alg;lbound;lower} insts, cstrs), + {enforce; alg; lbound; lower} type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t @@ -790,73 +789,82 @@ let _pr_constraints_map (cmap:constraints_map) = let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) -let remove_lower u lower = - let levels = Universe.levels u in - LSet.fold (fun l acc -> LMap.remove l acc) levels lower - +let not_lower lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + +exception UpperBoundedAlg +(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper + constraints to [lbound], adding them to [cstrs]. + + @raise UpperBoundedAlg if any [upper] constraints are strict and + [lbound] algebraic. *) +let enforce_uppers upper lbound cstrs = + List.fold_left (fun cstrs (d, r) -> + if d == Univ.Le then + enforce_leq lbound (Universe.make r) cstrs + else + match Universe.level lbound with + | Some lev -> Constraint.add (lev, d, r) cstrs + | None -> raise UpperBoundedAlg) + cstrs upper + let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc else (* Fixed universe, just compute its glb for sharing *) - let lbounds' = + let lbounds = match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with | None -> lbounds - | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower) + | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} lbounds - in (Univ.LMap.remove r left, lbounds')) + in (Univ.LMap.remove r left, lbounds)) left (left, Univ.LMap.empty) in - let rec instance (ctx', us, algs, insts, cstrs as acc) u = + let rec instance (ctx, us, algs, insts, cstrs as acc) u = let acc, left, lower = - try - let l = LMap.find u left in + match LMap.find u left with + | exception Not_found -> acc, [], LMap.empty + | l -> let acc, left, newlow, lower = List.fold_left - (fun (acc, left', newlow, lower') (d, l) -> - let acc', (enf,alg,l',lower) = aux acc l in + (fun (acc, left, newlow, lower') (d, l) -> + let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in let l' = if enf then Universe.make l else l' - in acc', (d, l') :: left', + in acc', (d, l') :: left, lower_add l d newlow, lower_union lower lower') (acc, [], LMap.empty, LMap.empty) l in - let not_lower (d,l) = - (* We're checking if (d,l) is already implied by the lower - constraints on some level u. If it represents l < u (d is Lt - or d is Le and i > 0, the i < 0 case is impossible due to - invariants of Univ), and the lower constraints only have l <= - u then it is not implied. *) - Univ.Universe.exists - (fun (l,i) -> - let d = - if i == 0 then d - else match d with - | Le -> Lt - | d -> d - in - try let d' = LMap.find l lower in - (* If d is stronger than the already implied lower - * constraints we must keep it. *) - compare_constraint_type d d' > 0 - with Not_found -> - (** No constraint existing on l *) true) l - in - let left = List.uniquize (List.filter not_lower left) in + let left = List.uniquize (List.filter (not_lower lower) left) in (acc, left, LMap.union newlow lower) - with Not_found -> acc, [], LMap.empty - and right = - try Some (LMap.find u right) - with Not_found -> None in let instantiate_lbound lbound = let alg = LSet.mem u algs in if alg then (* u is algebraic: we instantiate it with its lower bound, if any, or enforce the constraints if it is bounded from the top. *) - let lower = remove_lower lbound lower in - instantiate_with_lbound u lbound lower true false acc + let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in + instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc else (* u is non algebraic *) match Universe.level lbound with | Some l -> (* The lowerbound is directly a level *) @@ -867,125 +875,96 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - let acc' = remove_alg l acc in - instantiate_with_lbound u lbound lower false false acc' - else acc, (true, false, lbound, lower) + let acc = remove_alg l acc in + instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc + else acc, {enforce=true; alg=false; lbound; lower} | None -> - try - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let can, lower = find_inst insts lbound in - let lower = LMap.remove can lower in - instantiate_with_lbound u (Universe.make can) lower false false acc - with Not_found -> - (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound lower false true acc + begin match find_inst insts lbound with + | can, lower -> + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc + | exception Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc + end in - let acc' acc = - match right with - | None -> acc - | Some cstrs -> - let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in - if List.is_empty dangling then acc - else - let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in - let cstrs' = List.fold_left (fun cstrs (d, r) -> - if d == Univ.Le then - enforce_leq inst (Universe.make r) cstrs - else - try let lev = Option.get (Universe.level inst) in - Constraint.add (lev, d, r) cstrs - with Option.IsNone -> failwith "") - cstrs dangling - in - (ctx', us, algs, insts, cstrs'), b + let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) = + match LMap.find u right with + | exception Not_found -> acc + | upper -> + let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in + let cstrs = enforce_uppers upper b.lbound cstrs in + (ctx, us, algs, insts, cstrs), b in - if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower)) - else - let lbound = compute_lbound left in - match lbound with - | None -> (* Nothing to do *) - acc' (acc, (true, false, Universe.make u, lower)) - | Some lbound -> - try acc' (instantiate_lbound lbound) - with Failure _ -> acc' (acc, (true, false, Universe.make u, lower)) - and aux (ctx', us, algs, seen, cstrs as acc) u = + if not (LSet.mem u ctx) + then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + else + let lbound = compute_lbound left in + match lbound with + | None -> (* Nothing to do *) + enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower}) + | Some lbound -> + try enforce_uppers (instantiate_lbound lbound) + with UpperBoundedAlg -> + enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + and aux (ctx, us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u in - LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> + LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) -> if v == None then fst (aux acc u) - else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) + else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) let normalize_context_set g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in - let uf = UF.create () in (** Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> - if d == Le then - if Univ.Level.is_small l then - if is_set_minimization () && LSet.mem r ctx then - (Constraint.add cstr smallles, noneqs) - else (smallles, noneqs) - else if Level.is_small r then - if Level.is_prop r then - raise (Univ.UniverseInconsistency - (Le,Universe.make l,Universe.make r,None)) - else (smallles, Constraint.add (l,Eq,r) noneqs) - else (smallles, Constraint.add cstr noneqs) - else (smallles, Constraint.add cstr noneqs)) - csts (Constraint.empty, Constraint.empty) + Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + in + let smallles = if is_set_minimization () + then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles + else Constraint.empty in - let csts = + let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe v false g) ctx UGraph.initial_universes in - let g = - Univ.Constraint.fold - (fun (l, d, r) g -> - let g = - if not (Level.is_small l || LSet.mem l ctx) then - try UGraph.add_universe l false g - with UGraph.AlreadyDeclared -> g - else g - in - let g = - if not (Level.is_small r || LSet.mem r ctx) then - try UGraph.add_universe r false g - with UGraph.AlreadyDeclared -> g - else g - in g) csts g + let add_soft u g = + if not (Level.is_small u || LSet.mem u ctx) + then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + else g + in + let g = Constraint.fold + (fun (l, d, r) g -> add_soft r (add_soft l g)) + csts g in - let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + let g = UGraph.merge_constraints csts g in UGraph.constraints_of_universes g in + (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = - Constraint.fold (fun (l,d,r as cstr) noneqs -> - if d == Eq then (UF.union l r uf; noneqs) - else (* We ignore the trivial Prop/Set <= i constraints. *) - if d == Le && Univ.Level.is_small l then noneqs - else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r - then noneqs - else Constraint.add cstr noneqs) - csts Constraint.empty + Constraint.filter + (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (Level.is_prop l && d == Lt && Level.is_set r))) + csts in let noneqs = Constraint.union noneqs smallles in - let partition = UF.partition uf in let flex x = LMap.mem x us in let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) global + Constraint.add (canon, Eq, g) cst) global cstrs in (* Also add equalities for rigid variables *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) rigid + Constraint.add (canon, Eq, g) cst) rigid cstrs in let canonu = Some (Universe.make canon) in diff --git a/engine/universes.mli b/engine/universes.mli index 4823c5746..a0a7749f8 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -162,8 +162,6 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -module UF : Unionfind.PartitionSig with type elt = Level.t - val level_subst_of : universe_subst_fn -> universe_level_subst_fn val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 70dc6867a..a771945dd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -829,6 +829,8 @@ let is_univ_copy max u = else false +let dump_bytecode = ref false + let dump_bytecodes init code fvs = let open Pp in (str "code =" ++ fnl () ++ @@ -872,7 +874,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in - (if !Flags.dump_bytecode then + (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive msg -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index abab58b60..1c4cdcbeb 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -25,3 +25,6 @@ val compile_constant_body : fail_on_error:bool -> (** Shortcut of the previous function used during module strengthening *) val compile_alias : Names.Constant.t -> body_code + +(** Dump the bytecode after compilation (for debugging purposes) *) +val dump_bytecode : bool ref diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7b637c20e..641d424e2 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -807,7 +807,7 @@ and lambda_of_args env start args = (*********************************) - +let dump_lambda = ref false let optimize_lambda lam = let lam = simplify subst_id lam in @@ -819,7 +819,7 @@ let lambda_of_constr ~optimize genv c = Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in - if !Flags.dump_lambda then + if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 89b7fd8e3..6cf46163e 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -25,3 +25,6 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda (*spiwack: compiling function to insert dynamic decompilation before matching integers (in case they are in processor representation) *) val int31_escape_before_match : bool -> lambda -> lambda + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5d1644614..e6b27077b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -21,7 +21,7 @@ open Univ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *) -let error_inconsistency o u v (p:explanation option) = +let error_inconsistency o u v p = raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) (* Universes are stratified by a partial ordering $\le$. @@ -557,8 +557,7 @@ let get_explanation strict u v g = else match traverse strict u with Some exp -> exp | None -> assert false let get_explanation strict u v g = - if !Flags.univ_print then Some (get_explanation strict u v g) - else None + Some (lazy (get_explanation strict u v g)) (* To compare two nodes, we simply do a forward search. We implement two improvements: @@ -768,18 +767,18 @@ let normalize_universes g = g.entries g let constraints_of_universes g = + let module UF = Unionfind.Make (LSet) (LMap) in + let uf = UF.create () in let constraints_of u v acc = match v with | Canonical {univ=u; ltle} -> UMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in Constraint.add (u,typ,v) acc) ltle acc - | Equiv v -> Constraint.add (u,Eq,v) acc + | Equiv v -> UF.union u v uf; acc in - UMap.fold constraints_of g.entries Constraint.empty - -let constraints_of_universes g = - constraints_of_universes (normalize_universes g) + let csts = UMap.fold constraints_of g.entries Constraint.empty in + csts, UF.partition uf (** [sort_universes g] builds a totally ordered universe graph. The output graph should imply the input graph (and the implication diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index d4fba63fb..cca2eb472 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -59,7 +59,10 @@ val empty_universes : t val sort_universes : t -> t -val constraints_of_universes : t -> Constraint.t +(** [constraints_of_universes g] returns [csts] and [partition] where + [csts] are the non-Eq constraints and [partition] is the partition + of the universes into equivalence classes. *) +val constraints_of_universes : t -> Constraint.t * LSet.t list val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of diff --git a/kernel/univ.ml b/kernel/univ.ml index ea3a52295..8e19fa4e5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -541,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) -type univ_inconsistency = constraint_type * universe * universe * explanation option +type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency -let error_inconsistency o u v (p:explanation option) = +let error_inconsistency o u v p = raise (UniverseInconsistency (o,make u,make v,p)) (* Constraints and sets of constraints. *) @@ -1235,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) = | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" in let reason = match p with - | None | Some [] -> mt() + | None -> mt() | Some p -> - str " because" ++ spc() ++ pr_uni v ++ + let p = Lazy.force p in + if p = [] then mt () + else + str " because" ++ spc() ++ pr_uni v ++ prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) - p ++ + p ++ (if Universe.equal (snd (List.last p)) u then mt() else - (spc() ++ str "= " ++ pr_uni u)) + (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ pr_rel o ++ spc() ++ pr_uni v ++ reason diff --git a/kernel/univ.mli b/kernel/univ.mli index aaed899bf..b68bbdf35 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -205,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function Constraint.t... *) type explanation = (constraint_type * Universe.t) list -type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option +type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency diff --git a/lib/flags.ml b/lib/flags.ml index 8491873e0..56940f1cf 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,7 +60,6 @@ let profile = false let ide_slave = ref false let raw_print = ref false -let univ_print = ref false let we_are_parsing = ref false @@ -160,11 +159,3 @@ let print_mod_uid = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 - -let dump_bytecode = ref false -let set_dump_bytecode = (:=) dump_bytecode -let get_dump_bytecode () = !dump_bytecode - -let dump_lambda = ref false -let set_dump_lambda = (:=) dump_lambda -let get_dump_lambda () = !dump_lambda diff --git a/lib/flags.mli b/lib/flags.mli index 85aaf879f..17776d68a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -10,6 +10,25 @@ (** Global options of the system. *) +(** WARNING: don't add new entries to this file! + + This file is own its way to deprecation in favor of a purely + functional state, but meanwhile it will contain options that are + truly global to the system such as [compat] or [debug] + + If you are thinking about adding a global flag, well, just + don't. First of all, options make testins exponentially more + expensive, due to the growth of flag combinations. So please make + some effort in order for your idea to work in a configuration-free + manner. + + If you absolutely must pass an option to your new system, then do + so as a functional argument so flags are exposed to unit + testing. Then, register such parameters with the proper + state-handling mechanism of the top-level subsystem of Coq. + + *) + (** Command-line flags *) val boot : bool ref @@ -42,9 +61,6 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -(* Univ print flag, never set anywere. Maybe should belong to Univ? *) -val univ_print : bool ref - type compat_version = V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int @@ -129,13 +145,3 @@ val print_mod_uid : bool ref val profile_ltac : bool ref val profile_ltac_cutoff : float ref - -(** Dump the bytecode after compilation (for debugging purposes) *) -val dump_bytecode : bool ref -val set_dump_bytecode : bool -> unit -val get_dump_bytecode : unit -> bool - -(** Dump the VM lambda code after compilation (for debugging purposes) *) -val dump_lambda : bool ref -val set_dump_lambda : bool -> unit -val get_dump_lambda : unit -> bool diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b3bc895ba..a1c563f53 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -48,6 +48,7 @@ let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" let make_bullet s = + let open Proof_bullet in let n = String.length s in match s.[0] with | '-' -> Dash n diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 845104c3c..e331dc014 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -563,8 +563,8 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in - let ctx, f = Evarutil.nf_evars_and_universes ctx in - let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in + let ctx = Evd.minimize_universes ctx in + let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fb9ae64bf..e41bf71dd 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1533,14 +1533,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars env evd type_of_f in - let function_type = EConstr.Unsafe.to_constr function_type in - let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in - let ty = EConstr.Unsafe.to_constr ty in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in - let function_type = nf function_type in + let evd = Evd.minimize_universes evd in + let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in + let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 0c42a8bb2..4857beffa 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -325,6 +325,7 @@ GEXTEND Gram ; toplevel_selector: [ [ sel = selector_body; ":" -> sel + | "!"; ":" -> SelectAlreadyFocused | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: @@ -415,7 +416,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in + let g = Option.default (Goal_select.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 11bb7a234..bd02d85d5 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -515,6 +515,7 @@ let string_of_genarg_arg (ArgumentType arg) = else int i ++ str "-" ++ int j let pr_goal_selector toplevel = function + | SelectAlreadyFocused -> str "!:" | SelectNth i -> int i ++ str ":" | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" | SelectId id -> str "[" ++ Id.print id ++ str "]:" diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index aea00c240..799a52cc8 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -84,7 +84,7 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t +val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 3baa475ab..17f5e5d41 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -35,7 +35,8 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -269,7 +270,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 3baa475ab..17f5e5d41 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -35,7 +35,8 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -269,7 +270,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 99bb8440c..33c30e4d3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -186,8 +186,8 @@ let dummy_goal env sigma = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} -let constr_of v = match Value.to_constr v with - | Some c -> EConstr.Unsafe.to_constr c +let constr_of evd v = match Value.to_constr v with + | Some c -> EConstr.to_constr evd c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -221,8 +221,8 @@ let exec_tactic env evd n f args = (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in - let nf c = nf (constr_of c) in + let evd = Evd.minimize_universes (Refiner.project gls) in + let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd let stdlib_modules = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb563220b..56e582891 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -36,7 +36,7 @@ type _ delay = | Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) -let print_universes = Flags.univ_print +let print_universes = ref false (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 947469ca0..e68a25a87 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1118,7 +1118,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index f0e5f5746..3a49d6cf8 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -16,16 +16,13 @@ open Libnames (** Vernac expressions, produced by the parser *) type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation -(* spiwack: I'm choosing, for now, to have [goal_selector] be a - different type than [goal_reference] mostly because if it makes sense - to print a goal that is out of focus (or already solved) it doesn't - make sense to apply a tactic to it. Hence it the types may look very - similar, they do not seem to mean the same thing. *) -type goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Goal_select.t"] type goal_identifier = string type scope_name = string @@ -68,7 +65,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option + | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -199,7 +196,6 @@ type one_inductive_expr = ident_decl * local_binder_expr list * constr_expr option * constructor_expr list type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr - and typeclass_context = typeclass_constraint list type proof_expr = @@ -271,13 +267,11 @@ type extend_name = (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) -type register_kind = +type register_kind = | RegisterInline -type bullet = - | Dash of int - | Star of int - | Plus of int +type bullet = Proof_bullet.t +[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] (** {6 Types concerning the module layer} *) @@ -427,11 +421,11 @@ type nonrec vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr | VernacGlobalCheck of constr_expr | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable - | VernacSearch of searchable * goal_selector option * search_restriction + | VernacSearch of searchable * Goal_select.t option * search_restriction | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list @@ -445,8 +439,8 @@ type nonrec vernac_expr = | VernacFocus of int option | VernacUnfocus | VernacUnfocused - | VernacBullet of bullet - | VernacSubproof of goal_selector option + | VernacBullet of Proof_bullet.t + | VernacSubproof of Goal_select.t option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6ad857233..f26ac0bf9 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -145,7 +145,7 @@ open Pputils | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -508,7 +508,7 @@ open Pputils | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,l,gopt) -> - pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -1122,7 +1122,7 @@ open Pputils | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in + | Some i -> Goal_select.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) @@ -1176,7 +1176,8 @@ open Pputils | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) | VernacBullet b -> - return (begin match b with + (* XXX: Redundant with Proof_bullet.print *) + return (let open Proof_bullet in begin match b with | Dash n -> str (String.make n '-') | Star n -> str (String.make n '*') | Plus n -> str (String.make n '+') @@ -1184,7 +1185,7 @@ open Pputils | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") + return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml new file mode 100644 index 000000000..65a94a2c6 --- /dev/null +++ b/proofs/goal_select.ml @@ -0,0 +1,68 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +open Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | 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) + +let pr_goal_selector = function + | SelectAlreadyFocused -> Pp.str "!" + | SelectAll -> Pp.str "all" + | SelectNth i -> Pp.int i + | SelectList l -> + Pp.(str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]") + | SelectId id -> Names.Id.print id + +let parse_goal_selector = function + | "!" -> SelectAlreadyFocused + | "all" -> SelectAll + | i -> + let err_msg = "The default selector must be \"all\" or a natural number." in + begin try + let i = int_of_string i in + if i < 0 then CErrors.user_err Pp.(str err_msg); + SelectNth i + with Failure _ -> CErrors.user_err Pp.(str err_msg) + end + +let _ = let open Goptions in + declare_string_option + { optdepr = false; + optname = "default goal selector" ; + 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 + } diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli new file mode 100644 index 000000000..b1c572388 --- /dev/null +++ b/proofs/goal_select.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +open Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +val pr_goal_selector : t -> Pp.t +val get_default_goal_selector : unit -> t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index abda04ff1..03c0969fa 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -100,11 +100,23 @@ let solve ?with_end_tac gi info_lvl tac pr = | None -> tac | Some _ -> Proofview.Trace.record_info_trace tac in - let tac = match gi with - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac - | Vernacexpr.SelectAll -> tac + let tac = let open Goal_select in match gi with + | SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if n == 1 then tac + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + Proofview.tclZERO e + + | SelectNth i -> Proofview.tclFOCUS i i tac + | SelectList l -> Proofview.tclFOCUSLIST l tac + | SelectId id -> Proofview.tclFOCUSID id tac + | SelectAll -> tac in let tac = if use_unification_heuristics () then @@ -121,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr = with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") -let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) +let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 65cde3a3a..805635dfa 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -75,7 +75,7 @@ val current_proof_statement : tac] applies [tac] to all subgoals. *) val solve : ?with_end_tac:unit Proofview.tactic -> - Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> + Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index e22d382f7..cc3e79f85 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -10,19 +10,22 @@ open Proof -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int let bullet_eq b1 b2 = match b1, b2 with -| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 -| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 -| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 +| Dash n1, Dash n2 -> n1 = n2 +| Star n1, Star n2 -> n1 = n2 +| Plus n1, Plus n2 -> n1 = n2 | _ -> false let pr_bullet b = match b with - | Vernacexpr.Dash n -> Pp.(str (String.make n '-')) - | Vernacexpr.Star n -> Pp.(str (String.make n '*')) - | Vernacexpr.Plus n -> Pp.(str (String.make n '+')) + | Dash n -> Pp.(str (String.make n '-')) + | Star n -> Pp.(str (String.make n '*')) + | Plus n -> Pp.(str (String.make n '+')) type behavior = { @@ -195,52 +198,5 @@ let put p b = let suggest p = (!current_behavior).suggest p -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - - -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (Vernacexpr.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) - -let pr_goal_selector = function - | Vernacexpr.SelectAll -> Pp.str "all" - | Vernacexpr.SelectNth i -> Pp.int i - | Vernacexpr.SelectList l -> - Pp.(str "[" - ++ prlist_with_sep pr_comma pr_range_selector l - ++ str "]") - | Vernacexpr.SelectId id -> Names.Id.print id - -let parse_goal_selector = function - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in - begin try - let i = int_of_string i in - if i < 0 then CErrors.user_err Pp.(str err_msg); - Vernacexpr.SelectNth i - with Failure _ -> CErrors.user_err Pp.(str err_msg) - end - -let _ = - Goptions.(declare_string_option{optdepr = false; - optname = "default goal selector" ; - 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 - }) - +let pr_goal_selector = Goal_select.pr_goal_selector +let get_default_goal_selector = Goal_select.get_default_goal_selector diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index ffbaa0fac..a09a7ec1d 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -14,7 +14,10 @@ (* *) (**********************************************************) -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int (** A [behavior] is the data of a put function which is called when a bullet prefixes a tactic, a suggest function @@ -42,12 +45,8 @@ val register_behavior : behavior -> unit val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - +(** Deprecated *) +val pr_goal_selector : Goal_select.t -> Pp.t +[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] +val get_default_goal_selector : unit -> Goal_select.t +[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index fc7c437e6..842003bc8 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -83,6 +83,7 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * Misctypes.lident option * proof_object + type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 058e839b4..197f71ca9 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_type Logic Refine Proof +Goal_select Proof_bullet Proof_global Redexpr diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 0af766219..b8af2bcd5 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : static_block_declaration option val unit_val : Stm.DynBlockData.t -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index 9784de114..eacd3687a 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -38,6 +38,6 @@ val crawl : val unit_val : Stm.DynBlockData.t (* Bullets *) -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t diff --git a/stm/stm.ml b/stm/stm.ml index cbd324f5c..9ea6a305e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2288,7 +2288,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; - fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); + fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6bd4866c6..70f73df5c 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams in let sigma, sort = Evd.fresh_sort_in_family env sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in - let sigma, nf = Evarutil.nf_evars_and_universes sigma in - (nf c', Evd.evar_universe_context sigma), eff + let sigma = Evd.minimize_universes sigma in + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5e81e2d4b..6c7db26c7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -492,11 +492,13 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 340d8fbf3..bc2f60186 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -223,7 +223,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index aae4bc088..59c035e83 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -198,32 +198,40 @@ end let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y -let clear_dependency_msg env sigma id = function +let clear_in_global_msg = function + | None -> mt () + | Some ref -> str " implicitly in " ++ Printer.pr_global ref + +let clear_dependency_msg env sigma id err inglobal = + let pp = clear_in_global_msg inglobal in + match err with | Evarutil.OccurHypInSimpleClause None -> - Id.print id ++ str " is used in conclusion." + Id.print id ++ str " is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"." + Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." -let error_clear_dependency env sigma id err = - user_err (clear_dependency_msg env sigma id err) +let error_clear_dependency env sigma id err inglobal = + user_err (clear_dependency_msg env sigma id err inglobal) -let replacing_dependency_msg env sigma id = function +let replacing_dependency_msg env sigma id err inglobal = + let pp = clear_in_global_msg inglobal in + match err with | Evarutil.OccurHypInSimpleClause None -> - str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion." + str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> str "Cannot change " ++ Id.print id ++ - strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"." + strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." -let error_replacing_dependency env sigma id err = - user_err (replacing_dependency_msg env sigma id err) +let error_replacing_dependency env sigma id err inglobal = + user_err (replacing_dependency_msg env sigma id err inglobal) (* This tactic enables the user to remove hypotheses from the signature. * Some care is taken to prevent him from removing variables that are @@ -242,7 +250,7 @@ let clear_gen fail = function let evdref = ref sigma in let (hyps, concl) = try clear_hyps_in_evi env evdref (named_context_val env) concl ids - with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err + with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal in let env = reset_with_named_context hyps env in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) @@ -426,8 +434,8 @@ let clear_hyps2 env sigma ids sign t cl = let evdref = ref (Evd.clear_metas sigma) in let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in (hyps, t, cl, !evdref) - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency env sigma id err + with Evarutil.ClearDependencyError (id,err,inglobal) -> + error_replacing_dependency env sigma id err inglobal let internal_cut_gen ?(check=true) dir replace id t = Proofview.Goal.enter begin fun gl -> @@ -971,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) @@ -3007,8 +3020,24 @@ let unfold_body x = end end +let warn_cannot_remove_as_expected = + CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics" + (fun (id,inglobal) -> + let pp = match inglobal with + | None -> mt () + | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in + str "Cannot remove " ++ Id.print id ++ pp ++ str ".") + +let clear_for_destruct ids = + Proofview.tclORELSE + (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids) + (function + | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT () + | e -> iraise e) + (* Either unfold and clear if defined or simply clear if not a definition *) -let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] +let expand_hyp id = + Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id] (*****************************) (* High-level induction *) @@ -4929,9 +4958,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd, nf = nf_evars_and_universes !evdref in + let evd = Evd.minimize_universes !evdref in let ctx = Evd.universe_context_set evd in - evd, ctx, nf concl + evd, ctx, Evarutil.nf_evars_universes evd concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in diff --git a/test-suite/Makefile b/test-suite/Makefile index 8239600b1..9d84cd5c7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -79,6 +79,8 @@ log_anomaly = "==========> FAILURE <==========" log_failure = "==========> FAILURE <==========" log_intro = "==========> TESTING $(1) <==========" +FAIL = >&2 echo 'FAILED $@' + ####################################################################### # Testing subsystems ####################################################################### @@ -115,25 +117,24 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace .lia.cache - $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>" + rm -f trace .lia.cache output/MExtraction.out + $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>" $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \ + -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ \) -print0 | xargs -0 rm -f distclean: clean - $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f + $(SHOW) "RM <**/*.aux>" + $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f ####################################################################### # Per-subsystem targets ####################################################################### -define mkstamp -$(1): $(1).stamp ; @true -$(1).stamp: $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) ; \ - $(HIDE)touch $$@ +define vdeps +$(1): $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) endef -$(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)))) +$(foreach S,$(VSUBSYSTEMS),$(eval $(call vdeps,$(S)))) ####################################################################### # Summary @@ -221,6 +222,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (bug seems to be closed, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -236,6 +238,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (bug seems to be opened, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -251,6 +254,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ + $(FAIL); \ else \ echo $(log_success); \ echo " $<...correctly prepared" ; \ @@ -269,6 +273,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %. else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -285,6 +290,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -299,6 +305,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should be rejected)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -321,6 +328,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ } > "$@" @@ -363,6 +371,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ rm $$tmpexpected; \ @@ -379,6 +388,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -411,6 +421,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should run faster)"; \ + $(FAIL); \ fi; \ fi; \ } > "$@" @@ -428,6 +439,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG else \ echo $(log_failure); \ echo " $<...Good news! (wish seems to be granted, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -462,6 +474,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -480,6 +493,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -499,6 +513,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -517,6 +532,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -536,6 +552,7 @@ coqwc/%.v.log : coqwc/%.v else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ } > "$@" @@ -556,6 +573,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ ) > "$@" @@ -580,5 +598,6 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ } > "$@" diff --git a/test-suite/output/UnclosedBlocks.out b/test-suite/output/UnclosedBlocks.out index b83e94ad4..31481e84a 100644 --- a/test-suite/output/UnclosedBlocks.out +++ b/test-suite/output/UnclosedBlocks.out @@ -1,3 +1,2 @@ - Error: The section Baz, module type Bar and module Foo need to be closed. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 5b13f35d5..253b48e4d 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -421,3 +421,8 @@ Goal exists n : nat, n = n -> True. eexists. set (H := _ = _). Abort. + +(* Check interpretation of default evar instance in pretyping *) +(* (reported as bug #7356) *) + +Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 868140517..0951c5c8d 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -53,3 +53,17 @@ Goal True -> exists (x : Prop), x. Proof. intro H; eexists ?[x]; only [x]: exact True. 1: assumption. Qed. + +(* Strict focusing! *) +Set Default Goal Selector "!". + +Goal True -> True /\ True /\ True. +Proof. + intro. + split;only 2:split. + Fail exact I. + Fail !:exact I. + 1:exact I. + - !:exact H. + - exact I. +Qed. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index a329894aa..d37ad9f52 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -127,4 +127,28 @@ induction 1 as (n,H,IH). exact Logic.I. Qed. +(* Make "intro"/"intros" progress on existential variables *) +Module Evar. + +Goal exists (A:Prop), A. +eexists. +unshelve (intro x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Goal exists (A:Prop), A. +eexists. +unshelve (intros x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Definition d := ltac:(intro x; exact (x*x)). + +Definition d' : nat -> _ := ltac:(intros;exact 0). + +End Evar. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6539d80b..e5f22f25e 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -382,7 +382,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONE: real-all.timing.diff +.PHONY: real-all.timing.diff bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index a1a07fce8..17e848c5a 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -10,8 +10,8 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s)) -let fatal_error ?extra exn = - Topfmt.print_err_exn ?extra exn; +let fatal_error exn = + Topfmt.print_err_exn Topfmt.ParsingCommandLine exn; let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in exit exit_code diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 63b8b538a..da9169514 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -150,29 +150,28 @@ let print_highlight_location ib loc = let valid_buffer_loc ib loc = let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e - (* Toplevel error explanation. *) -let error_info_for_buffer ?loc buf = - Option.map (fun loc -> +let error_info_for_buffer ?loc phase buf = + match loc with + | None -> Topfmt.pr_phase ?loc phase + | Some loc -> let fname = loc.Loc.fname in - let hl, loc = (* We are in the toplevel *) - match fname with - | Loc.ToplevelInput -> - let nloc = adjust_loc_buf buf loc in - if valid_buffer_loc buf loc then - (fnl () ++ print_highlight_location buf nloc, nloc) - (* in the toplevel, but not a valid buffer *) - else (mt (), nloc) - (* we are in batch mode, don't adjust location *) - | Loc.InFile _ -> - (mt (), loc) - in Topfmt.pr_loc loc ++ hl - ) loc + match fname with + | Loc.ToplevelInput -> + let nloc = adjust_loc_buf buf loc in + if valid_buffer_loc buf loc then + match Topfmt.pr_phase ~loc:nloc phase with + | None -> None + | Some hd -> Some (hd ++ fnl () ++ print_highlight_location buf nloc) + (* in the toplevel, but not a valid buffer *) + else Topfmt.pr_phase ~loc phase + (* we are in batch mode, don't adjust location *) + | Loc.InFile _ -> Topfmt.pr_phase ~loc phase (* Actual printing routine *) -let print_error_for_buffer ?loc lvl msg buf = - let pre_hdr = error_info_for_buffer ?loc buf in +let print_error_for_buffer ?loc phase lvl msg buf = + let pre_hdr = error_info_for_buffer ?loc phase buf in if !print_emacs then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg @@ -282,7 +281,7 @@ let extract_default_loc loc doc_id sid : Loc.t option = with _ -> loc (** Coqloop Console feedback handler *) -let coqloop_feed (fb : Feedback.feedback) = let open Feedback in +let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in match fb.contents with | Processed -> () | Incomplete -> () @@ -301,9 +300,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) | Message (Warning,loc,msg) -> let loc = extract_default_loc loc fb.doc_id fb.span_id in - TopErr.print_error_for_buffer ?loc Warning msg top_buffer + TopErr.print_error_for_buffer ?loc phase Warning msg top_buffer | Message (lvl,loc,msg) -> - TopErr.print_error_for_buffer ?loc lvl msg top_buffer + TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -353,7 +352,7 @@ let top_goal_print oldp newp = let (e, info) = CErrors.push exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer + TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer (* Careful to keep this loop tail-rec *) let rec vernac_loop ~state = @@ -395,7 +394,7 @@ let rec vernac_loop ~state = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer; vernac_loop ~state let rec loop ~state = diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 39a9de4f8..6d9867fb9 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -30,7 +30,7 @@ val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) -val coqloop_feed : Feedback.feedback -> unit +val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit (** Main entry point of Coq: read and execute vernac commands. *) val loop : state:Vernac.State.t -> Vernac.State.t diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 668f9b893..38351a377 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -35,12 +35,16 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) -let coqtop_init_feed = Coqloop.coqloop_feed +let coqtop_init_feed = Coqloop.coqloop_feed Topfmt.Initialization + +let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude + +let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile (* Default toplevel loop *) let console_toploop_run opts ~state = (* We initialize the console only if we run the toploop_run *) - let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in + let tl_feed = Feedback.add_feeder (Coqloop.coqloop_feed Topfmt.InteractiveLoop) in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () @@ -101,9 +105,16 @@ let load_vernacular opts ~state = else load_vernac s ) state (List.rev opts.load_vernacular_list) -let load_init_vernaculars opts ~state = - let state = if opts.load_rcfile then - Coqinit.load_rcfile ~rcfile:opts.rcfile ~state +let load_init_vernaculars cur_feeder opts ~state = + let state = + if opts.load_rcfile then begin + Feedback.del_feeder !cur_feeder; + let rc_feeder = Feedback.add_feeder coqtop_rcfile_feed in + let state = Coqinit.load_rcfile ~rcfile:opts.rcfile ~state in + Feedback.del_feeder rc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; + state + end else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -147,8 +158,8 @@ let fatal_error msg = flush_all (); exit 1 -let fatal_error_exn ?extra exn = - Topfmt.print_err_exn ?extra exn; +let fatal_error_exn exn = + Topfmt.print_err_exn Topfmt.Initialization exn; flush_all (); let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 @@ -194,7 +205,7 @@ let ensure_exists f = fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile opts ~echo ~f_in ~f_out = +let compile cur_feeder opts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in @@ -218,13 +229,18 @@ let compile opts ~echo ~f_in ~f_out = | None -> long_f_dot_v ^ "o" | Some f -> ensure_vo long_f_dot_v f in - let doc, sid = Stm.(new_doc + Feedback.del_feeder !cur_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars opts ~state in + let state = load_init_vernaculars cur_feeder opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) @@ -265,13 +281,18 @@ let compile opts ~echo ~f_in ~f_out = async_proofs_tac_error_resilience = `None; } in - let doc, sid = Stm.(new_doc + Feedback.del_feeder !cur_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; let state = { doc; sid; proof = None; time = opts.time } in - let state = load_init_vernaculars opts ~state in + let state = load_init_vernaculars cur_feeder opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in @@ -288,21 +309,21 @@ let compile opts ~echo ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile opts ~echo ~f_in ~f_out = +let compile cur_feeder opts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts ~echo ~f_in ~f_out; + compile cur_feeder opts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts (f_in, echo) = +let compile_file cur_feeder opts (f_in, echo) = if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts ~echo ~f_in ~f_out:None) f_in + (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out:None) f_in else - compile opts ~echo ~f_in ~f_out:None + compile cur_feeder opts ~echo ~f_in ~f_out:None -let compile_files opts = +let compile_files cur_feeder opts = let compile_list = List.rev opts.compile_list in - List.iter (compile_file opts) compile_list + List.iter (compile_file cur_feeder opts) compile_list (******************************************************************************) (* VIO Dispatching *) @@ -420,7 +441,7 @@ let init_toplevel arglist = CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - let init_feeder = Feedback.add_feeder coqtop_init_feed in + let init_feeder = ref (Feedback.add_feeder coqtop_init_feed) in Lib.init(); (* Coq's init process, phase 2: @@ -435,10 +456,22 @@ let init_toplevel arglist = * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); - if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); - if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); - if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then begin + print_endline (Envars.coqlib ()); + exit (exitcode opts) + end; + if opts.print_config then begin + Envars.print_config stdout Coq_config.all_src_dirs; + exit (exitcode opts) + end; + if opts.print_tags then begin + print_style_tags opts; + exit (exitcode opts) + end; + if opts.filter_opts then begin + print_string (String.concat "\n" extras); + exit 0; + end; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; Option.iter Mltop.load_ml_object_raw opts.toploop; @@ -477,34 +510,33 @@ let init_toplevel arglist = let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.stm_flags in - try - let open Vernac.State in - let doc, sid = - Stm.(new_doc - { doc_type = Interactive opts.toplevel_name; - iload_path; require_libs; stm_options; - }) in - let state = { doc; sid; proof = None; time = opts.time } in - Some (load_init_vernaculars opts ~state), opts - with any -> flush_all(); fatal_error_exn any + let open Vernac.State in + Feedback.del_feeder !init_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc + { doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + }) in + Feedback.del_feeder doc_feeder; + init_feeder := Feedback.add_feeder coqtop_init_feed; + let state = { doc; sid; proof = None; time = opts.time } in + Some (load_init_vernaculars init_feeder opts ~state), opts (* Non interactive: we perform a sequence of compilation steps *) end else begin - try - compile_files opts; - (* Careful this will modify the load-path and state so after - this point some stuff may not be safe anymore. *) - do_vio opts; - (* Allow the user to output an arbitrary state *) - outputstate opts; - None, opts - with any -> flush_all(); fatal_error_exn any + compile_files init_feeder opts; + (* Careful this will modify the load-path and state so after + this point some stuff may not be safe anymore. *) + do_vio opts; + (* Allow the user to output an arbitrary state *) + outputstate opts; + None, opts end; with any -> flush_all(); - let extra = Some (str "Error during initialization: ") in - fatal_error_exn ?extra any + fatal_error_exn any end in - Feedback.del_feeder init_feeder; + Feedback.del_feeder !init_feeder; res let start () = diff --git a/vernac/classes.ml b/vernac/classes.ml index 906b4a959..1ac597695 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -195,7 +195,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in Pretyping.check_evars env Evd.empty sigma termtype; let univs = Evd.check_univ_decl ~poly sigma decl in let termtype = to_constr sigma termtype in @@ -288,7 +288,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in let sigma = Evarutil.nf_evar_map_undefined sigma in (* Beware of this step, it is required as to minimize universes. *) - let sigma, _nf = Evarutil.nf_evar_map_universes sigma in + let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) Pretyping.check_evars env Evd.empty sigma termtype; let termtype = to_constr sigma termtype in @@ -364,7 +364,7 @@ let context poly l = let sigma = Evd.from_env env in let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in (* Note, we must use the normalized evar from now on! *) - let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env Evd.empty sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1466fa243..7b382dacc 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -224,7 +224,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in - let sigma, _ = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in (* XXX: We still have evars here in Program *) let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 05c40dbdd..101298ef4 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -304,14 +304,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in (* Compute renewed arities *) - let sigma, nf = nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in - let sigma, nf' = nf_evars_and_universes sigma in - let arities = List.map nf' arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let arities = List.map nf arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 30dd6ec74..aba5e32db 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook = (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in - let evd, _nf = Evarutil.nf_evars_and_universes evd in + let evd = Evd.minimize_universes evd in (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in diff --git a/vernac/record.ml b/vernac/record.ml index 78e68e8a3..b89c0060d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,7 +168,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in - let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in let typ = EConstr.to_constr sigma typ in diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 055f6676e..dbfad51a6 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -289,6 +289,14 @@ let init_terminal_output ~color = let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) + +type execution_phase = + | ParsingCommandLine + | Initialization + | LoadingPrelude + | LoadingRcFile + | InteractiveLoop + let pr_loc loc = let fname = loc.Loc.fname in match fname with @@ -301,13 +309,28 @@ let pr_loc loc = int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ str":") -let print_err_exn ?extra any = +let pr_phase ?loc phase = + match phase, loc with + | LoadingRcFile, loc -> + (* For when all errors go through feedback: + str "While loading rcfile:" ++ + Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc *) + Option.map pr_loc loc + | LoadingPrelude, loc -> + Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc) + | _, Some loc -> Some (pr_loc loc) + | ParsingCommandLine, _ + | Initialization, _ -> None + | InteractiveLoop, _ -> + (* Note: interactive messages such as "foo is defined" are not located *) + None + +let print_err_exn phase any = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in - let msg_loc = Option.cata pr_loc (mt ()) loc in - let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in + let pre_hdr = pr_phase ?loc phase in let msg = CErrors.iprint (e, info) ++ fnl () in - std_logger ~pre_hdr Feedback.Error msg + std_logger ?pre_hdr Feedback.Error msg let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 579b456a2..73dcb0064 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -53,8 +53,17 @@ val init_terminal_output : color:bool -> unit (** Error printing *) (* To be deprecated when we can fully move to feedback-based error printing. *) + +type execution_phase = + | ParsingCommandLine + | Initialization + | LoadingPrelude + | LoadingRcFile + | InteractiveLoop + val pr_loc : Loc.t -> Pp.t -val print_err_exn : ?extra:Pp.t -> exn -> unit +val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option +val print_err_exn : execution_phase -> exn -> unit (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 19658806c..f0e41d27c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -909,7 +909,7 @@ let vernac_set_used_variables e = if List.is_empty to_clear then (p, ()) else let tac = Tactics.clear to_clear in - fst (Pfedit.solve SelectAll None tac p), () + fst (Pfedit.solve Goal_select.SelectAll None tac p), () end (*****************************) @@ -1465,22 +1465,22 @@ let _ = optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } - + let _ = declare_bool_option { optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; - optread = Flags.get_dump_bytecode; - optwrite = Flags.set_dump_bytecode } + optread = (fun () -> !Cbytegen.dump_bytecode); + optwrite = (:=) Cbytegen.dump_bytecode } let _ = declare_bool_option { optdepr = false; optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; - optread = Flags.get_dump_lambda; - optwrite = Flags.set_dump_lambda } + optread = (fun () -> !Clambda.dump_lambda); + optwrite = (:=) Clambda.dump_lambda } let _ = declare_bool_option @@ -1611,7 +1611,7 @@ let get_current_context_of_args = function let query_command_selector ?loc = function | None -> None - | Some (SelectNth n) -> Some n + | Some (Goal_select.SelectNth n) -> Some n | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") @@ -1619,17 +1619,16 @@ let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in - let c = EConstr.Unsafe.to_constr c in let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; - let sigma',nf = Evarutil.nf_evars_and_universes sigma' in + let sigma' = Evd.minimize_universes sigma' in let uctx = Evd.universe_context_set sigma' in let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in - let c = nf c in let j = - if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) + if Evarutil.has_undefined_evars sigma' c then + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) else + let c = EConstr.to_constr sigma' c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in @@ -1912,7 +1911,7 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p | _ -> user_err ~hdr:"bracket_selector" (str "Brackets only support the single numbered goal selector.")) |