diff options
111 files changed, 911 insertions, 654 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 00db64f26..f811f26e1 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 @@ -165,6 +164,9 @@ jobs: geocoq: <<: *ci-template + fcsl-pcm: + <<: *ci-template + fiat-crypto: <<: *ci-template @@ -204,6 +206,9 @@ jobs: math-comp: <<: *ci-template + mtac2: + <<: *ci-template + sf: <<: *ci-template environment: @@ -240,6 +245,7 @@ workflows: - elpi: *req-main - equations: *req-main - geocoq: *req-main + - fcsl-pcm: *req-main - fiat-crypto: *req-main - fiat-parsers: *req-main - flocq: *req-main @@ -247,6 +253,7 @@ workflows: requires: - build - bignums + - mtac2: *req-main - corn: requires: - build diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2d8fc791b..329697ca4 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -11,6 +11,9 @@ /dev/ci/*.sh @ejgallego # Secondary maintainer @SkySkimmer +/.circleci/ @SkySkimmer +# Secondary maintainer @ejgallego + /.travis.yml @ejgallego # Secondary maintainer @SkySkimmer @@ -83,11 +86,6 @@ /interp/ @herbelin # Secondary maintainer @ejgallego -########## Interfaces ########## - -/intf/ @letouzey -# Secondary maintainer @ppedrot - ########## Kernel ########## /kernel/ @maximedenes @@ -304,6 +302,9 @@ /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes +# This file belongs to CI +Makefile.ci @ejgallego +# Secondary maintainer @SkySkimmer ########## 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 f0d7463fc..6b42ac7eb 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,61 +1,76 @@ -image: ocaml/opam:ubuntu - -# this doesn't seem to work -cache: - paths: - - .opamcache +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: "system" + COMPILER: "4.02.3" CAMLP5_VER: "6.14" + OPAMROOT: "$CI_PROJECT_DIR/.opamcache" + OPAMROOTISOK: "true" # 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" - + 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: - - ls # figure out if artifacts are around + - 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 - - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -qq && sudo apt-get install -y -qq ${EXTRA_PACKAGES}; fi - - if [ -n "${PIP_PACKAGES}" ]; then sudo pip3 install ${PIP_PACKAGES}; fi - - # setup cache - - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi - - ln -s $(readlink -f .opamcache) ~/.opam - - # 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 repository set-url default https://opam.ocaml.org - - opam update - - opam switch ${COMPILER} - - eval $(opam config env) - - opam config list - - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM} - - rm -rf ~/.opam/log/ - - opam list + - 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 + +################ OPAM SYSTEM ###################### +# - use cache between pipelines +# - use artifacts between jobs +# (in https://gitlab.com/SkySkimmer/coq/-/jobs/63255417 +# the cache wasn't available at the build step) +# every non opam-boot job must set dependencies (for ci it's in the template) +# otherwise all opam-boot artifacts are used together and we get some random switch + +# set cache key when using +.opam-boot-template: &opam-boot-template + stage: opam-boot + artifacts: + name: "opam-$COMPILER" + paths: + - .opamcache + expire_in: 1 week + script: + - opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org + - eval $(opam config env) + - opam update + - opam config list + - opam list + - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM} + - rm -rf ~/.opam/log/ + - opam list # TODO figure out how to build doc for installed coq +# set dependencies when using .build-template: &build-template stage: build artifacts: @@ -65,8 +80,13 @@ before_script: - config/Makefile - test-suite/misc/universes/all_stdlib.v expire_in: 1 week + dependencies: + - not-a-real-job script: - set -e + - printenv + - opam config list + - opam list - echo 'start:coq.config' - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF} @@ -86,10 +106,12 @@ before_script: - set +e +# set dependencies when using .warnings-template: &warnings-template # keep warnings in test stage so we can test things even when warnings occur stage: test - dependencies: [] + dependencies: + - not-a-real-job script: - set -e @@ -107,8 +129,11 @@ before_script: EXTRA_PACKAGES: "$COQIDE_PACKAGES" EXTRA_OPAM: "$COQIDE_OPAM" +# set dependencies when using .test-suite-template: &test-suite-template stage: test + dependencies: + - not-a-real-job script: - cd test-suite - make clean @@ -122,8 +147,11 @@ before_script: paths: - test-suite/logs +# set dependencies when using .validate-template: &validate-template stage: test + dependencies: + - not-a-real-job script: - cd _install_ci - find lib/coq/ -name '*.vo' -print0 > vofiles @@ -139,57 +167,90 @@ before_script: - echo 'end:coq.test' - set +e dependencies: + - opam-boot - build variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" EXTRA_PACKAGES: "$TIMING_PACKAGES" +opam-boot: + <<: *opam-boot-template + cache: + paths: &cache-paths + - .opamcache + key: "main-$CACHEKEY" + variables: + EXTRA_OPAM: "$COQIDE_OPAM ocamlgraph $ELPI_OPAM" + EXTRA_PACKAGES: "$COQIDE_PACKAGES" + +opam-boot:32bit: + <<: *opam-boot-template + cache: + paths: *cache-paths + key: "32bit-$CACHEKEY" + variables: + COMPILER: "$COMPILER_32BIT" + EXTRA_PACKAGES: "gcc-multilib" + +opam-boot:bleeding-edge: + <<: *opam-boot-template + cache: + paths: *cache-paths + key: "be-$CACHEKEY" + variables: + COMPILER: "$COMPILER_BLEEDING_EDGE" + CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + EXTRA_PACKAGES: "$COQIDE_PACKAGES" + EXTRA_OPAM: "$COQIDE_OPAM_BE" + build: <<: *build-template + dependencies: + - opam-boot variables: EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM" PIP_PACKAGES: "$SPHINX_PACKAGES" # no coqide for 32bit: libgtk installation problems build:32bit: <<: *build-template + dependencies: + - opam-boot:32bit variables: EXTRA_CONF: "-native-compiler yes" EXTRA_PACKAGES: "gcc-multilib" - COMPILER: "$COMPILER_32BIT" build:bleeding-edge: <<: *build-template + dependencies: + - opam-boot:bleeding-edge variables: EXTRA_CONF: "-native-compiler yes -coqide opt" - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" EXTRA_PACKAGES: "$COQIDE_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM_BE" warnings: <<: *warnings-template + dependencies: + - opam-boot # warnings:32bit: # <<: *warnings-template # variables: # <<: *warnings-variables # EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT" -# COMPILER: "$COMPILER_32BIT" +# dependencies: +# - opam-boot:32bit warnings:bleeding-edge: <<: *warnings-template - variables: - <<: *warnings-variables - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" - EXTRA_OPAM: "$COQIDE_OPAM_BE" + dependencies: + - opam-boot:bleeding-edge test-suite: <<: *test-suite-template dependencies: + - opam-boot - build variables: EXTRA_PACKAGES: "$TIMING_PACKAGES" @@ -197,31 +258,31 @@ test-suite: test-suite:32bit: <<: *test-suite-template dependencies: + - opam-boot:32bit - build:32bit variables: - COMPILER: "$COMPILER_32BIT" EXTRA_PACKAGES: "gcc-multilib $TIMING_PACKAGES" test-suite:bleeding-edge: <<: *test-suite-template dependencies: + - opam-boot:bleeding-edge - build:bleeding-edge variables: - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" EXTRA_PACKAGES: "$TIMING_PACKAGES" validate: <<: *validate-template dependencies: + - opam-boot - build validate:32bit: <<: *validate-template dependencies: + - opam-boot:32bit - build:32bit variables: - COMPILER: "$COMPILER_32BIT" EXTRA_PACKAGES: "gcc-multilib" ci-bignums: @@ -240,7 +301,6 @@ ci-coq-dpdgraph: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_OPAM: "ocamlgraph" EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-coquelicot: @@ -251,9 +311,6 @@ ci-coquelicot: ci-elpi: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" ci-equations: <<: *ci-template @@ -262,6 +319,9 @@ ci-geocoq: <<: *ci-template allow_failure: true +ci-fcsl-pcm: + <<: *ci-template + # ci-fiat-crypto: # <<: *ci-template # # out of memory error @@ -300,6 +360,9 @@ ci-math-classes: ci-math-comp: <<: *ci-template +ci-mtac2: + <<: *ci-template + ci-sf: <<: *ci-template variables: @@ -10,8 +10,6 @@ S kernel B kernel S kernel/byterun B kernel/byterun -S intf -B intf S library B library S engine diff --git a/.travis.yml b/.travis.yml index e56204b0e..a60d68de5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -76,9 +76,9 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi" # ppx_tools_versioned requires a specific version findlib - FINDLIB_VER="" - - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-equations" @@ -87,6 +87,9 @@ matrix: - TEST_TARGET="ci-geocoq" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-fcsl-pcm" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-fiat-crypto" - if: NOT (type = pull_request) env: @@ -114,6 +117,9 @@ 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-sf" - if: NOT (type = pull_request) env: @@ -157,8 +163,6 @@ matrix: - texlive-fonts-extra - latex-xcolor - ghostscript - - transfig - - imagemagick - tipa - python3 - python3-pip @@ -199,8 +203,6 @@ matrix: - MAIN_TARGET="coqocaml" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="hevea ${LABLGTK}" - # dummy target - - BUILD_TARGET="clean" addons: apt: sources: @@ -218,8 +220,6 @@ matrix: - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" - # dummy target - - BUILD_TARGET="clean" addons: apt: sources: @@ -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 @@ -19,6 +25,7 @@ Tactic language - Ltac backtraces now include trace information about tactics called by OCaml-defined tactics. +- Option "Ltac Debug" now applies also to terms built using Ltac functions. Changes from 8.8+beta1 to 8.8.0 =============================== 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 ----------- @@ -90,19 +90,6 @@ package "library" ( ) -package "intf" ( - - description = "Coq Public Data Types" - version = "8.8" - - requires = "coq.library" - - directory = "intf" - - archive(byte) = "intf.cma" - archive(native) = "intf.cmxa" -) - package "engine" ( description = "Coq Tactic Engine" diff --git a/Makefile.ci b/Makefile.ci index 3c26bf964..37b14ed91 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \ ci-cpdt \ ci-elpi \ ci-equations \ + ci-fcsl-pcm \ ci-fiat-crypto \ ci-fiat-parsers \ ci-flocq \ @@ -27,7 +28,7 @@ CI_TARGETS=ci-bignums \ ci-ltac2 \ ci-math-classes \ ci-math-comp \ - ci-metacoq \ + ci-mtac2 \ ci-sf \ ci-tlc \ ci-unimath \ diff --git a/Makefile.common b/Makefile.common index 9a30e2a4c..eed41fbe7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -75,7 +75,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ - config clib lib kernel intf kernel/byterun library \ + config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel @@ -102,7 +102,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ +CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma 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 6c052b63b..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 @@ -1212,7 +1222,7 @@ let write_configml f = let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; - "tactics"; "toplevel"; "printing"; "intf"; + "tactics"; "toplevel"; "printing"; "grammar"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" diff --git a/default.nix b/default.nix index 26c6e4b90..0b4794274 100644 --- a/default.nix +++ b/default.nix @@ -32,6 +32,7 @@ }: with pkgs; +with stdenv.lib; stdenv.mkDerivation rec { @@ -61,8 +62,7 @@ stdenv.mkDerivation rec { ] else []) ++ (if doCheck then # Test-suite dependencies - let inherit (stdenv.lib) versionAtLeast optional; in - /* ncurses is required to build an OCaml REPL */ + # ncurses is required to build an OCaml REPL optional (!versionAtLeast ocaml.version "4.07") ncurses ++ [ python @@ -90,6 +90,10 @@ stdenv.mkDerivation rec { prefixKey = "-prefix "; + buildFlags = optionals buildDoc [ "world" "sphinx" ]; + + installTargets = [ "install" ] ++ optional buildDoc "install-doc-sphinx"; + inherit doCheck; } diff --git a/dev/base_include b/dev/base_include index e76044f41..2f7183dd6 100644 --- a/dev/base_include +++ b/dev/base_include @@ -15,7 +15,6 @@ #directory "tactics";; #directory "printing";; #directory "grammar";; -#directory "intf";; #directory "stm";; #directory "vernac";; diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 2adc7d8dc..5cee72cc7 100644..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 @@ -150,3 +150,9 @@ ######################################################################## : "${Elpi_CI_BRANCH:=coq-master}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}" + +######################################################################## +# fcsl-pcm +######################################################################## +: "${fcsl_pcm_CI_BRANCH:=master}" +: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh new file mode 100755 index 000000000..fdc4c729b --- /dev/null +++ b/dev/ci/ci-fcsl-pcm.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm" + +install_ssreflect + +git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}" + +( cd "${fcsl_pcm_CI_DIR}" && make ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 6c8dce5bd..845addb4c 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -8,4 +8,4 @@ fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) -( cd "${fiat_crypto_CI_DIR}" && make lite ) +( cd "${fiat_crypto_CI_DIR}" && make lite lite-display ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index b019fa059..1af0f634c 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -9,27 +9,20 @@ lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust" install_ssreflect -# Add or update the opam repo we need for dependency resolution -opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev - # Setup lambdaRust first git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" # Extract required version of Iris -Iris_VERSION=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o) -Iris_URL=$(opam show "coq-iris.$Iris_VERSION" -f upstream-url) -read -r -a Iris_URL_PARTS <<< "$(echo "$Iris_URL" | tr '#' ' ')" +Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout "${Iris_CI_BRANCH}" "${Iris_URL_PARTS[0]}" "${Iris_CI_DIR}" "${Iris_URL_PARTS[1]}" +git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" # Extract required version of std++ -stdpp_VERSION=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o) -stdpp_URL=$(opam show "coq-stdpp.$stdpp_VERSION" -f upstream-url) -read -r -a stdpp_URL_PARTS <<< "$(echo "$stdpp_URL" | tr '#' ' ')" +stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout "${stdpp_CI_BRANCH}" "${stdpp_URL_PARTS[0]}" "${stdpp_CI_DIR}" "${stdpp_URL_PARTS[1]}" +git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" # Build std++ ( cd "${stdpp_CI_DIR}" && make && make install ) 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-vst.sh b/dev/ci/ci-vst.sh index 3c0044bfe..3817edf0c 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -8,6 +8,10 @@ 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 ) +# HACK: from the upstream makefile: +# +# default_target: _CoqProject version.vo msl veric floyd progs +# +# We have to omit progs as otherwise we timeout on Travis; once we +# move to Gitlab we will able to just use `make` +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true _CoqProject version.vo msl veric floyd ) diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh new file mode 100644 index 000000000..7e554684e --- /dev/null +++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + # ltac2_CI_BRANCH=ssr+correct_packing + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Elpi_CI_BRANCH=api+vernac_expr_iso + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/dev/core.dbg b/dev/core.dbg index 57c136900..edf67020a 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,5 +16,4 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer intf.cma load_printer ltac_plugin.cmo diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 3a2df6a81..84ff94c66 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -70,7 +70,7 @@ To merge the PR proceed in the following way ``` $ git checkout master $ git pull -$ dev/tools/merge-pr XXXX +$ dev/tools/merge-pr.sh XXXX $ git push upstream ``` where `XXXX` is the number of the PR to be merged and `upstream` is the name diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 1a24f23e5..2bad21bb2 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -5,7 +5,18 @@ Proof engine More functions have been changed to use `EConstr`, notably the - functions in `Evd`. + functions in `Evd`, and in particular `Evd.define`. + + Note that the core function `EConstr.to_constr` now _enforces_ by + default that the resulting term is ground, that is to say, free of + Evars. This is usually what you want, as open terms should be of + type `EConstr.t` to benefit from the invariants the `EConstr` API is + meant to guarantee. + + In case you'd like to violate this API invariant, you can use the + `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note + that setting this flag to false is deprecated so it is only meant to + be used as to help port pre-EConstr code. ## Changes between Coq 8.7 and Coq 8.8 diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e5..764d48295 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used 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/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f3e60edea..8f1c165dd 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -18,7 +18,7 @@ exec $OCAMLDEBUG \ -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 1c94f630f..00d04e6b3 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -5,7 +5,7 @@ set -o pipefail API=https://api.github.com/repos/coq/coq OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq" -OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq" +OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" # This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ @@ -91,8 +91,10 @@ fi REMOTE_URL=$(git remote get-url "$REMOTE" --all) if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \ - [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}" ] && \ - [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}.git" ]; then + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}" ] && \ + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \ + [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \ + [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" error "it points to ${BLUE}$REMOTE_URL${RESET} instead" 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..a3d06ae04 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: diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/intf/evar_kinds.ml b/engine/evar_kinds.ml index c964ecf1f..c964ecf1f 100644 --- a/intf/evar_kinds.ml +++ b/engine/evar_kinds.ml 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/universes.ml b/engine/universes.ml index e5f9212a7..e98708724 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 @@ -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/ide/ide_slave.ml b/ide/ide_slave.ml index 2e552b60b..c66d69c03 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -511,7 +511,7 @@ let () = Coqtop.toploop_init := (fun coq_args extra_args -> let args = parse extra_args in Flags.quiet := true; CoqworkmgrApi.(init High); - args) + coq_args, args) let () = Coqtop.toploop_run := loop diff --git a/interp/interp.mllib b/interp/interp.mllib index bb22cf468..61313acc4 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,6 +1,7 @@ Tactypes Stdarg Genintern +Notation_term Notation_ops Notation Syntax_def diff --git a/intf/notation_term.ml b/interp/notation_term.ml index a9c2e2a53..a9c2e2a53 100644 --- a/intf/notation_term.ml +++ b/interp/notation_term.ml diff --git a/intf/intf.mllib b/intf/intf.mllib deleted file mode 100644 index 2b8960d3f..000000000 --- a/intf/intf.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Constrexpr -Evar_kinds -Genredexpr -Locus -Extend -Notation_term -Decl_kinds -Glob_term -Misctypes -Pattern -Vernacexpr diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index af89712d5..cfeb0a9ee 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -163,8 +163,11 @@ extern void caml_process_pending_signals(void); /* The interpreter itself */ value coq_interprete -(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args) +(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args) { + /* coq_accu is not allocated on the OCaml heap */ + CAMLparam2(coq_atom_tbl, coq_global_data); + /*Declaration des variables */ #ifdef PC_REG register code_t pc PC_REG; @@ -196,7 +199,7 @@ value coq_interprete coq_instr_table = (char **) coq_jumptable; coq_instr_base = coq_Jumptbl_base; #endif - return Val_unit; + CAMLreturn(Val_unit); } #if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) coq_jumptbl_base = coq_Jumptbl_base; @@ -1460,7 +1463,7 @@ value coq_interprete Instruct(STOP){ print_instr("STOP"); coq_sp = sp; - return accu; + CAMLreturn(accu); } @@ -1512,12 +1515,16 @@ value coq_push_vstack(value stk, value max_stack_size) { return Val_unit; } -value coq_interprete_ml(value tcode, value a, value e, value ea) { +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, e, Long_val(ea)); + return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea)); print_instr("end coq_interprete"); } -value coq_eval_tcode (value tcode, value e) { - return coq_interprete_ml(tcode, Val_unit, e, 0); +value coq_interprete_byte(value* argv, int argn){ + return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]); +} + +value coq_eval_tcode (value tcode, value t, value g, value e) { + return coq_interprete_ml(tcode, Val_unit, t, g, e, 0); } diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h index 60865c32e..c04e9e00b 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -17,11 +17,10 @@ value coq_push_arguments(value args); value coq_push_vstack(value stk); -value coq_interprete_ml(value tcode, value a, value e, value ea); +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea); +value coq_interprete_byte(value* argv, int argn); value coq_interprete - (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args); - -value coq_eval_tcode (value tcode, value e); - + (code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args); +value coq_eval_tcode (value tcode, value t, value g, value e); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 45cfae509..b2917a55e 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -24,10 +24,6 @@ value * coq_stack_threshold; asize_t coq_max_stack_size = Coq_max_stack_size; /* global_data */ - -value coq_global_data; -value coq_atom_tbl; - int drawinstr; /* interp state */ @@ -58,9 +54,6 @@ static void (*coq_prev_scan_roots_hook) (scanning_action); static void coq_scan_roots(scanning_action action) { register value * i; - /* Scan the global variables */ - (*action)(coq_global_data, &coq_global_data); - (*action)(coq_atom_tbl, &coq_atom_tbl); /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { (*action) (*i, i); @@ -79,24 +72,10 @@ void init_coq_stack() coq_max_stack_size = Coq_max_stack_size; } -void init_coq_global_data(long requested_size) -{ - int i; - coq_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) - Field (coq_global_data, i) = Val_unit; -} - -void init_coq_atom_tbl(long requested_size){ - int i; - coq_atom_tbl = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit; -} - void init_coq_interpreter() { coq_sp = coq_stack_high; - coq_interprete(NULL, Val_unit, Val_unit, 0); + coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0); } static int coq_vm_initialized = 0; @@ -112,8 +91,6 @@ value init_coq_vm(value unit) /* ML */ #endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); - init_coq_global_data(Coq_global_data_Size); - init_coq_atom_tbl(40); /* Initialing the interpreter */ init_coq_interpreter(); @@ -157,53 +134,6 @@ void realloc_coq_stack(asize_t required_space) #undef shift } -value get_coq_global_data(value unit) /* ML */ -{ - return coq_global_data; -} - -value get_coq_atom_tbl(value unit) /* ML */ -{ - return coq_atom_tbl; -} - -value realloc_coq_global_data(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_global_data; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_global_data); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_global_data, i), Field(coq_global_data, i)); - for (i = actual_size; i < requested_size; i++){ - Field (new_global_data, i) = Val_long (0); - } - coq_global_data = new_global_data; - } - return Val_unit; -} - -value realloc_coq_atom_tbl(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_atom_tbl; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_atom_tbl); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_atom_tbl = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i)); - for (i = actual_size; i < requested_size; i++) - Field (new_atom_tbl, i) = Val_long (0); - coq_atom_tbl = new_atom_tbl; - } - return Val_unit; -} - value coq_set_drawinstr(value unit) { drawinstr = 1; diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index cec34f566..9375b15de 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -20,7 +20,6 @@ #define Coq_stack_size (4096 * sizeof(value)) #define Coq_stack_threshold (256 * sizeof(value)) -#define Coq_global_data_Size (4096 * sizeof(value)) #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 @@ -34,9 +33,7 @@ extern value * coq_stack_threshold; /* global_data */ -extern value coq_global_data; extern int coq_all_transp; -extern value coq_atom_tbl; extern int drawinstr; /* interp state */ @@ -53,10 +50,6 @@ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ void realloc_coq_stack(asize_t required_space); -value get_coq_global_data(value unit); /* ML */ -value realloc_coq_global_data(value size); /* ML */ -value get_coq_atom_tbl(value unit); /* ML */ -value realloc_coq_atom_tbl(value size); /* ML */ value coq_set_transp_value(value transp); /* ML */ value get_coq_transp_value(value unit); /* ML */ #endif /* _COQ_MEMORY_ */ 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/csymtable.ml b/kernel/csymtable.ml index 012948954..4f3cbf289 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -26,7 +26,9 @@ open Cbytegen module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" +external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode" + +type global_data = { mutable glob_len : int; mutable glob_val : values array } (*******************) (* Linkage du code *) @@ -37,21 +39,28 @@ external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" (* [global_data] contient les valeurs des constantes globales (axiomes,definitions), les annotations des switch et les structured constant *) -external global_data : unit -> values array = "get_coq_global_data" +let global_data = { + glob_len = 0; + glob_val = Array.make 4096 crazy_val; +} -(* [realloc_global_data n] augmente de n la taille de [global_data] *) -external realloc_global_data : int -> unit = "realloc_coq_global_data" +let get_global_data () = Vmvalues.vm_global global_data.glob_val -let check_global_data n = - if n >= Array.length (global_data()) then realloc_global_data n +let realloc_global_data n = + let n = min (2 * n + 0x100) Sys.max_array_length in + let ans = Array.make n crazy_val in + let src = global_data.glob_val in + let () = Array.blit src 0 ans 0 (Array.length src) in + global_data.glob_val <- ans -let num_global = ref 0 +let check_global_data n = + if n >= Array.length global_data.glob_val then realloc_global_data n let set_global v = - let n = !num_global in + let n = global_data.glob_len in check_global_data n; - (global_data()).(n) <- v; - incr num_global; + global_data.glob_val.(n) <- v; + global_data.glob_len <- global_data.glob_len + 1; n (* table pour les structured_constant et les annotations des switchs *) @@ -164,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) = in let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in - eval_tcode tc vm_env + eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env and val_of_constr env c = match compile ~fail_on_error:true env c with diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 19b2b8b50..d32cfba36 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -18,3 +18,5 @@ val val_of_constr : env -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit + +val get_global_data : unit -> Vmvalues.vm_global diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 370185a72..5d270125a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,6 +43,6 @@ Subtyping Mod_typing Nativelibrary Safe_typing -Vm Csymtable +Vm Vconv 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/kernel/vm.ml b/kernel/vm.ml index 14aeb732f..d7eedc226 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -42,8 +42,11 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) -external interprete : tcode -> values -> vm_env -> int -> values = - "coq_interprete_ml" +external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -> int -> values = + "coq_interprete_byte" "coq_interprete_ml" + +let interprete code v env k = + coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k (* Functions over arguments *) @@ -184,6 +187,6 @@ let apply_whd k whd = push_val v; interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> - apply_stack (val_of_atom a) stk v + apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 0e0cb4e58..6a41efac2 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -43,6 +43,7 @@ let fix_val v = (Obj.magic v : values) let cofix_upd_val v = (Obj.magic v : values) type vm_env +type vm_global let fun_env v = (Obj.magic v : vm_env) let fix_env v = (Obj.magic v : vm_env) let cofix_env v = (Obj.magic v : vm_env) @@ -51,6 +52,8 @@ type vstack = values array let fun_of_val v = (Obj.magic v : vfun) +let vm_global (v : values array) = (Obj.magic v : vm_global) + (*******************************************) (* Machine code *** ************************) (*******************************************) @@ -407,13 +410,20 @@ let check_fix f1 f2 = else false else false -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" +let atom_rel : atom array ref = + let init i = Aid (RelKey i) in + ref (Array.init 40 init) + +let get_atom_rel () = !atom_rel + +let realloc_atom_rel n = + let n = min (2 * n + 0x100) Sys.max_array_length in + let init i = Aid (RelKey i) in + let ans = Array.init n init in + atom_rel := ans let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; + let len = Array.length !atom_rel in ref (Array.init len mkAccuCode) let relaccu_code i = @@ -422,9 +432,7 @@ let relaccu_code i = else begin realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; + let nl = Array.length !atom_rel in relaccu_tbl := Array.init nl (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index c6e342a96..550791b2c 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -15,6 +15,7 @@ open Cbytecodes type values type vm_env +type vm_global type vprod type vfun type vfix @@ -33,6 +34,8 @@ val fix_env : vfix -> vm_env val cofix_env : vcofix -> vm_env val cofix_upd_env : to_update -> vm_env +val vm_global : values array -> vm_global + (** Cast a value known to be a function, unsafe in general *) val fun_of_val : values -> vfun @@ -69,6 +72,9 @@ type atom = | Aind of inductive | Asort of Sorts.t +val get_atom_rel : unit -> atom array +(** Global table of rels *) + (** Zippers *) type zipper = 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/intf/decl_kinds.ml b/library/decl_kinds.ml index 0d3285311..0d3285311 100644 --- a/intf/decl_kinds.ml +++ b/library/decl_kinds.ml diff --git a/library/declaremods.ml b/library/declaremods.ml index 762efc5e3..1d5df49cf 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,11 +17,25 @@ open Entries open Libnames open Libobject open Mod_subst -open Vernacexpr open Misctypes (** {6 Inlining levels} *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function diff --git a/library/declaremods.mli b/library/declaremods.mli index fd8d29614..4aee7feae 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -9,10 +9,24 @@ (************************************************************************) open Names -open Vernacexpr (** {6 Modules } *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t diff --git a/library/library.mllib b/library/library.mllib index e43bfb5a1..1c0368847 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -4,7 +4,9 @@ Libobject Summary Nametab Global +Decl_kinds Lib +Misctypes Declaremods Loadpath Library diff --git a/intf/misctypes.ml b/library/misctypes.ml index 72db3b31c..72db3b31c 100644 --- a/intf/misctypes.ml +++ b/library/misctypes.ml diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 593dcbf58..2dbd624c2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -17,6 +17,7 @@ open Constrexpr open Constrexpr_ops open Extend open Decl_kinds +open Declaremods open Declarations open Misctypes open Tok (* necessary for camlp5 *) 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..a1d7d9b1a 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: 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/tacexpr.ml b/plugins/ltac/tacexpr.ml index 3baa475ab..37abfeee9 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -36,6 +36,7 @@ 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 = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 3baa475ab..37abfeee9 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -36,6 +36,7 @@ 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 = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6a4bf577b..84049d4ed 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2010,7 +2010,8 @@ let interp_redexp env sigma r = let _ = let eval lfun env sigma ty tac = - let ist = { lfun = lfun; extra = TacStore.empty; } in + let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in + let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in (EConstr.of_constr c, sigma) 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/intf/constrexpr.ml b/pretyping/constrexpr.ml index fda31756a..fda31756a 100644 --- a/intf/constrexpr.ml +++ b/pretyping/constrexpr.ml 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/intf/extend.ml b/pretyping/extend.ml index 734b859f6..734b859f6 100644 --- a/intf/extend.ml +++ b/pretyping/extend.ml diff --git a/intf/genredexpr.ml b/pretyping/genredexpr.ml index 80697461a..80697461a 100644 --- a/intf/genredexpr.ml +++ b/pretyping/genredexpr.ml diff --git a/intf/glob_term.ml b/pretyping/glob_term.ml index 84be15552..84be15552 100644 --- a/intf/glob_term.ml +++ b/pretyping/glob_term.ml diff --git a/intf/locus.ml b/pretyping/locus.ml index 95a2e495b..95a2e495b 100644 --- a/intf/locus.ml +++ b/pretyping/locus.ml diff --git a/intf/pattern.ml b/pretyping/pattern.ml index 76367b612..76367b612 100644 --- a/intf/pattern.ml +++ b/pretyping/pattern.ml 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/pretyping.mllib b/pretyping/pretyping.mllib index ae4ad0be7..d98026bc6 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,5 +1,5 @@ Geninterp -Ltac_pretype +Locus Locusops Pretype_errors Reductionops @@ -16,12 +16,19 @@ Evarsolve Recordops Evarconv Typing +Constrexpr +Genredexpr Miscops +Glob_term +Ltac_pretype Glob_ops Redops +Pattern Patternops Constr_matching Tacred +Extend +Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/intf/vernacexpr.ml b/pretyping/vernacexpr.ml index 06f969f19..548689205 100644 --- a/intf/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -22,6 +22,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation 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 = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -281,20 +282,22 @@ type bullet = (** Rigid / flexible module signature *) -type 'a module_signature = +type 'a module_signature = 'a Declaremods.module_signature = | Enforce of 'a (** ... : T *) | Check of 'a list (** ... <: T1 <: T2, possibly empty *) +[@@ocaml.deprecated "please use [Declaremods.module_signature]."] (** Which module inline annotations should we honor, either None or the ones whose level is less or equal to the given integer *) -type inline = +type inline = Declaremods.inline = | NoInline | DefaultInline | InlineAt of int +[@@ocaml.deprecated "please use [Declaremods.inline]."] -type module_ast_inl = module_ast * inline +type module_ast_inl = module_ast * Declaremods.inline type module_binder = bool option * lident list * module_ast_inl (** [Some b] if locally enabled/disabled according to [b], [None] if @@ -333,7 +336,7 @@ type nonrec vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * - inline * (ident_decl list * constr_expr) with_coercion list + Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list @@ -373,7 +376,7 @@ type nonrec vernac_expr = | VernacDeclareModule of bool option * lident * module_binder list * module_ast_inl | VernacDefineModule of bool option * lident * module_binder list * - module_ast_inl module_signature * module_ast_inl list + module_ast_inl Declaremods.module_signature * module_ast_inl list | VernacDeclareModuleType of lident * module_binder list * module_ast_inl list * module_ast_inl list | VernacInclude of module_ast_inl list diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7eb8396ac..83c875707 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -16,12 +16,13 @@ open Util open CAst open Extend -open Vernacexpr -open Pputils open Libnames +open Decl_kinds open Constrexpr open Constrexpr_ops -open Decl_kinds +open Vernacexpr +open Declaremods +open Pputils open Ppconstr diff --git a/proofs/logic.ml b/proofs/logic.ml index e5294715e..4934afa83 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -289,7 +289,15 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | (App _| Case _) -> Constr.fold (collrec deep) acc c + | Case(ci,p,c,br) -> + (* Hack assuming only two situations: the legacy one that branches, + if with Metas, are Meta, and the new one with eta-let-expanded + branches *) + let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in + Array.fold_left (collrec deep) + (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c) + br + | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c in @@ -387,12 +395,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma, rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -440,12 +443,7 @@ and mk_hdgoals sigma goal goalacc trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -497,6 +495,50 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') +and treat_case sigma goal ci lbrty lf acc' = + let rec strip_outer_cast c = match kind c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c in + let decompose_app_vect c = match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) in + let env = Goal.V82.env sigma goal in + Array.fold_left3 + (fun (lacc,sigma,bacc) ty fi l -> + if isMeta (strip_outer_cast fi) then + (* Support for non-eta-let-expanded Meta as found in *) + (* destruct/case with an non eta-let expanded elimination scheme *) + let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in + r,s,(fi'::bacc) + else + (* Deal with a branch in expanded form of the form + Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as + if it were not so, so as to preserve compatibility with when + destruct/case generated schemes of the form + Case(ci,p,c,[|Meta;...;Meta|]; + CAUTION: it does not deal with the general case of eta-zeta + reduced branches having a form different from Meta, as it + would be theoretically the case with third-party code *) + let n = List.length l in + let ctx, body = Term.decompose_lam_n_decls n fi in + let head, args = decompose_app_vect body in + (* Strip cast because clenv_cast_meta adds a cast when the branch is + eta-expanded but when not when the branch has the single-meta + form [Meta] *) + let head = strip_outer_cast head in + if isMeta head then begin + assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); + let head' = lift (-n) head in + let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in + let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in + (r,s,fi'::bacc) + end + else + (* Supposed to be meta-free *) + let sigma, t'ty = goal_type_of env sigma fi in + let sigma = check_conv_leq_goal env sigma fi t'ty ty in + (lacc,sigma,fi::bacc)) + (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index abda04ff1..62a38fa32 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -101,6 +101,18 @@ let solve ?with_end_tac gi info_lvl tac pr = | Some _ -> Proofview.Trace.record_info_trace tac in let tac = match gi with + | Vernacexpr.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 + | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index e22d382f7..d6f7c0e93 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -212,6 +212,7 @@ let pr_range_selector (i, j) = else Pp.(int i ++ str "-" ++ int j) let pr_goal_selector = function + | Vernacexpr.SelectAlreadyFocused -> Pp.str "!" | Vernacexpr.SelectAll -> Pp.str "all" | Vernacexpr.SelectNth i -> Pp.int i | Vernacexpr.SelectList l -> @@ -221,9 +222,10 @@ let pr_goal_selector = function | Vernacexpr.SelectId id -> Names.Id.print id let parse_goal_selector = function + | "!" -> Vernacexpr.SelectAlreadyFocused | "all" -> Vernacexpr.SelectAll | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in + let err_msg = "The default selector must be \"all\" or \"!\" 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); diff --git a/stm/stm.ml b/stm/stm.ml index 326b6d1c2..cbd324f5c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -92,11 +92,11 @@ let execution_error ?loc state_id msg = module Hooks = struct let state_computed, state_computed_hook = Hook.make - ~default:(fun state_id ~in_cache -> + ~default:(fun ~doc:_ state_id ~in_cache -> feedback ~id:state_id Processed) () let state_ready, state_ready_hook = Hook.make - ~default:(fun state_id -> ()) () + ~default:(fun ~doc:_ state_id -> ()) () let forward_feedback, forward_feedback_hook = let m = Mutex.create () in @@ -106,7 +106,7 @@ let forward_feedback, forward_feedback_hook = with e -> Mutex.unlock m; raise e) () let unreachable_state, unreachable_state_hook = Hook.make - ~default:(fun _ _ -> ()) () + ~default:(fun ~doc:_ _ _ -> ()) () include Hook @@ -578,7 +578,7 @@ end = struct (* {{{ *) | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- s; - if async_proofs_is_master !cur_opt then Hooks.(call state_ready id) + if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -770,6 +770,7 @@ module State : sig Warning: an optimization in installed_cached requires that state modifying functions are always executed using this wrapper. *) val define : + doc:doc -> ?safe_id:Stateid.t -> ?redefine:bool -> ?cache:Summary.marshallable -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit @@ -919,7 +920,7 @@ end = struct (* {{{ *) let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in e1 == e2 - let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) + let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id = feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id); @@ -938,7 +939,7 @@ end = struct (* {{{ *) stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then - Hooks.(call state_computed id ~in_cache:false); + Hooks.(call state_computed ~doc id ~in_cache:false); VCS.reached id; if Proof_global.there_are_pending_proofs () then VCS.goals id (Proof_global.get_open_goals ()) @@ -954,7 +955,7 @@ end = struct (* {{{ *) | Some _, None -> (e, info) | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in if cache = `Yes || cache = `Shallow then freeze_invalid id ie; - Hooks.(call unreachable_state id ie); + Hooks.(call unreachable_state ~doc id ie); Exninfo.iraise ie let init_state = ref None @@ -1352,6 +1353,7 @@ module rec ProofTask : sig and type request := request val build_proof_here : + doc:doc -> ?loc:Loc.t -> drop_pt:bool -> Stateid.t * Stateid.t -> Stateid.t -> @@ -1466,11 +1468,12 @@ end = struct (* {{{ *) execution_error start (Pp.strbrk s); feedback (InProgress ~-1) - let build_proof_here ?loc ~drop_pt (id,valid) eop = + let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop = Future.create (State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in - if VCS.is_interactive () = `No then Reach.known_state ~cache:`No eop - else Reach.known_state ~cache:`Shallow eop; + if VCS.is_interactive () = `No + then Reach.known_state ~doc ~cache:`No eop + else Reach.known_state ~doc ~cache:`Shallow eop; let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); @@ -1484,7 +1487,7 @@ end = struct (* {{{ *) VCS.print (); let proof, future_proof, time = let wall_clock = Unix.gettimeofday () in - let fp = build_proof_here ?loc ~drop_pt:drop exn_info stop in + let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in let proof = Future.force fp in proof, fp, Unix.gettimeofday () -. wall_clock in (* We typecheck the proof with the kernel (in the worker) to spot @@ -1577,7 +1580,7 @@ end = struct (* {{{ *) msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ "The system state could not be sent to the worker process. "^ "Falling back to local, lazy, evaluation.")); - t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop)); + t_assign(`Comp(build_proof_here ~doc:dummy_doc (* XXX should be stored in a closure, it is the same doc that was used to generate the task *) ?loc:t_loc ~drop_pt t_exn_info t_stop)); feedback (InProgress ~-1) end (* }}} *) @@ -1587,6 +1590,7 @@ and Slaves : sig (* (eventually) remote calls *) val build_proof : + doc:doc -> ?loc:Loc.t -> drop_pt:bool -> exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * AsyncTaskQueue.cancel_switch @@ -1634,7 +1638,7 @@ end = struct (* {{{ *) with VCS.Expired -> cur in aux stop in try - Reach.known_state ~cache:`No stop; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop; if drop then let _proof = Proof_global.return_proof ~allow_partial:true () in `OK_ADMITTED @@ -1647,7 +1651,7 @@ end = struct (* {{{ *) Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) - Reach.known_state ~cache:`No start; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; (* STATE SPEC: * - start: First non-expired state! [This looks very fishy] * - end : start + qed @@ -1754,7 +1758,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = + let build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then @@ -1769,7 +1773,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch; f, cancel_switch end else - ProofTask.build_proof_here ?loc ~drop_pt t_exn_info block_stop, cancel_switch + ProofTask.build_proof_here ~doc ?loc ~drop_pt t_exn_info block_stop, cancel_switch else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in @@ -1892,7 +1896,7 @@ end = struct (* {{{ *) let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try - Reach.known_state ~cache:`No id; + Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id; stm_purify (fun () -> let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in @@ -2047,7 +2051,7 @@ end = struct (* {{{ *) let perform { r_where; r_doc; r_what; r_for } = VCS.restore r_doc; VCS.print (); - Reach.known_state ~cache:`No r_where; + Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where; (* STATE *) let st = Vernacstate.freeze_interp_state `No in try @@ -2092,7 +2096,8 @@ end (* }}} *) and Reach : sig val known_state : - ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit + doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable -> + Stateid.t -> unit end = struct (* {{{ *) @@ -2250,7 +2255,7 @@ let log_processing_sync id name reason = log_string Printf.(sprintf let wall_clock_last_fork = ref 0.0 -let known_state ?(redefine_qed=false) ~cache id = +let known_state ~doc ?(redefine_qed=false) ~cache id = let error_absorbing_tactic id blockname exn = (* We keep the static/dynamic part of block detection separate, since @@ -2345,7 +2350,7 @@ let known_state ?(redefine_qed=false) ~cache id = and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin - Hooks.(call state_computed id ~in_cache:true); + Hooks.(call state_computed ~doc id ~in_cache:true); stm_prerr_endline (fun () -> "reached (cache)"); State.install_cached id end else @@ -2426,7 +2431,7 @@ let known_state ?(redefine_qed=false) ~cache id = ^" proof. Reprocess the command declaring " ^"the proof's statement to avoid that.")); let fp, cancel = - Slaves.build_proof + Slaves.build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in Future.replace ofp fp; qed.fproof <- Some (fp, cancel); @@ -2438,10 +2443,10 @@ let known_state ?(redefine_qed=false) ~cache id = reach ~cache:`Shallow block_start; let fp, cancel = if delegate then - Slaves.build_proof + Slaves.build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name else - ProofTask.build_proof_here ?loc + ProofTask.build_proof_here ~doc ?loc ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (fp, cancel); @@ -2511,7 +2516,7 @@ let known_state ?(redefine_qed=false) ~cache id = let cache_step = if !cur_opt.async_proofs_cache = Some Force then `Yes else cache_step in - State.define ?safe_id + State.define ~doc ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id @@ -2600,7 +2605,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = load_objs require_libs; (* We record the state at this point! *) - State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; + State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); if async_proofs_is_master !cur_opt then begin @@ -2621,7 +2626,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = let observe ~doc id = let vcs = VCS.backup () in try - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.print (); doc with e -> @@ -2714,7 +2719,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; VCS.delete_branch brname; VCS.gc (); - let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in + let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> @@ -2766,7 +2771,7 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok -let process_transaction ?(newtip=Stateid.fresh ()) +let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2871,11 +2876,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in - let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *) + let _st : unit = Reach.known_state ~doc ~cache:`Yes head_id in (* ensure it is ok *) let step () = VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in - let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in + let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) @@ -2901,7 +2906,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) end; VCS.checkout_shallowest_proof_branch (); end in - State.define ~safe_id:head_id ~cache:`Yes step id; + State.define ~doc ~safe_id:head_id ~cache:`Yes step id; Backtrack.record (); `Ok | VtUnknown, VtLater -> @@ -3015,7 +3020,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in - match process_transaction ?newtip aast clas with + match process_transaction ~doc ?newtip aast clas with | `Ok -> doc, VCS.cur_tip (), `NewTip | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ()) @@ -3030,7 +3035,7 @@ type focus = { let query ~doc ~at ~route s = stm_purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) - else Reach.known_state ~cache:`Yes at; + else Reach.known_state ~doc ~cache:`Yes at; try while true do let { CAst.loc; v=ast } = parse_sentence ~doc at s in @@ -3092,7 +3097,7 @@ let edit_at ~doc id = VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); VCS.delete_boxes_of id; cancel_switch := true; - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `Focus { stop = qed_id; start = master_id; tip } in let no_edit = function @@ -3115,7 +3120,7 @@ let edit_at ~doc id = VCS.gc (); VCS.print (); if not !cur_opt.async_proofs_full then - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try @@ -3144,7 +3149,7 @@ let edit_at ~doc id = | true, None, _ -> if on_cur_branch id then begin VCS.reset_branch (VCS.current_branch ()) id; - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip end else if is_ancestor_of_cur_branch id then begin @@ -3207,4 +3212,9 @@ let forward_feedback_hook = Hooks.forward_feedback_hook let unreachable_state_hook = Hooks.unreachable_state_hook let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +type document = VCS.vcs +let backup () = VCS.backup () +let restore d = VCS.restore d + + (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index 7a720aa72..aed7274d0 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -263,11 +263,12 @@ val register_proof_block_delimiter : * the alternative toploop for the worker can be selected by changing * the name of the Task(s) above) *) -val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t -val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t +val state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t +val unreachable_state_hook : + (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t (* ready means that master has it at hand *) -val state_ready_hook : (Stateid.t -> unit) Hook.t +val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t @@ -283,3 +284,7 @@ val get_all_proof_names : doc:doc -> Id.t list (** Enable STM debugging *) val stm_debug : bool ref + +type document +val backup : unit -> document +val restore : document -> unit diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 5445925b1..5130b019a 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -17,9 +17,9 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let loop init _coq_args extra_args = +let loop init coq_args extra_args = let args = parse extra_args in Flags.quiet := true; init (); CoqworkmgrApi.init !async_proofs_worker_priority; - args + coq_args, args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index f02edb9bb..37ec6dacc 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -11,4 +11,6 @@ (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list +val loop : + (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> + Coqargs.coq_cmdopts * string list 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..82b178388 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -496,7 +496,9 @@ module New = struct | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | Vernacexpr.SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index aae4bc088..3a20c3fc4 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 -> @@ -3007,8 +3015,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 +4953,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/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/toplevel/coqtop.ml b/toplevel/coqtop.ml index eb6e23202..e60382f2c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -368,7 +368,7 @@ let init_color color_mode = let toploop_init = ref begin fun opts x -> let () = init_color opts.color in let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - x + opts, x end let print_style_tags opts = @@ -454,7 +454,7 @@ let init_toplevel arglist = 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; - let extras = !toploop_init opts extras in + let opts, extras = !toploop_init opts extras in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 056279bbd..fcc569ca0 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -18,5 +18,6 @@ val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts val start : unit -> unit (* For other toploops *) -val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref +val toploop_init : + (Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list) ref val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref diff --git a/vernac/classes.ml b/vernac/classes.ml index 3c133f317..2e1bd6970 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -196,7 +196,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 @@ -289,7 +289,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 @@ -365,7 +365,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 = @@ -425,7 +425,7 @@ let context poly l = let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl - Vernacexpr.NoInline (CAst.make id)) + Declaremods.NoInline (CAst.make id)) | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 6a590758f..26a46a752 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -20,7 +20,6 @@ open Constrintern open Impargs open Decl_kinds open Pretyping -open Vernacexpr open Entries (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) @@ -66,7 +65,7 @@ match local with | Global | Local | Discharge -> let do_instance = should_axiom_into_instance local in let local = DeclareDef.get_locality ident ~kind:"axiom" local in - let inl = match nl with + let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 56e324376..a2d20a1d1 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -19,7 +19,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool + Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) @@ -32,5 +32,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind -> val declare_assumption : coercion_flag -> assumption_kind -> types in_constant_universes_entry -> Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t -> + bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> global_reference * Univ.Instance.t * bool 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/vernacentries.ml b/vernac/vernacentries.ml index a9d1631ba..564c0965b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -672,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Enforce mty_ast) [] + id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); @@ -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 @@ -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 |