diff options
148 files changed, 1402 insertions, 837 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d566d56331..49e1361407 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-11-05-V01" + CACHEKEY: "bionic_coq-V2019-11-25-V01" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -323,7 +323,7 @@ pkg:opam: - opam pin add --kind=path coqide.$COQ_VERSION . - set +e variables: - COQ_VERSION: "8.11" + COQ_VERSION: "8.12" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci @@ -562,7 +562,11 @@ library:ci-argosy: extends: .ci-template library:ci-bedrock2: - extends: .ci-template + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci library:ci-color: extends: .ci-template-flambda @@ -577,6 +581,20 @@ library:ci-color: library:ci-compcert: extends: .ci-template-flambda +library:ci-coqprime: + stage: stage-3 + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci + needs: + - build:edge+flambda + - plugin:ci-bignums + dependencies: + - build:edge+flambda + - plugin:ci-bignums + library:ci-coquelicot: extends: .ci-template @@ -588,6 +606,18 @@ library:ci-fcsl-pcm: library:ci-fiat-crypto: extends: .ci-template-flambda + stage: stage-4 + needs: + - build:edge+flambda + - library:ci-bedrock2 + - library:ci-coqprime + - plugin:ci-bignums + - plugin:ci-rewriter + dependencies: + - build:edge+flambda + - library:ci-bedrock2 + - library:ci-coqprime + - plugin:ci-rewriter library:ci-fiat-crypto-legacy: extends: .ci-template-flambda @@ -634,7 +664,6 @@ library:ci-math-comp: library:ci-sf: extends: .ci-template - allow_failure: true # Waiting for integration of the fix for #10476 library:ci-stdlib2: extends: .ci-template-flambda @@ -699,3 +728,10 @@ plugin:ci-quickchick: plugin:ci-relation_algebra: extends: .ci-template + +plugin:ci-rewriter: + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 07008f42d6..e26103cedd 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -483,7 +483,7 @@ We have a linter that checks a few different things: to build every commit, and in principle even the test-suite should pass on every commit (but this isn't tested in CI because it would take too long). A good way to test this is to use `git rebase - master --exec "make -f Makefile.dune check`. + master --exec "make -f Makefile.dune check"`. - **No tabs or end-of-line spaces on updated lines**. We are trying to get rid of all tabs and all end-of-line spaces from the code base (except in some very special files that need them). This checks not @@ -152,6 +152,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). c.f. https://caml.inria.fr/mantis/view.php?id=7630 + If you want your build to be reproducible, ensure that the + SOURCE_DATE_EPOCH environment variable is set as documented in + https://reproducible-builds.org/specs/source-date-epoch/ + 4- Still in the root directory, do make diff --git a/META.coq.in b/META.coq.in index 9869e7f575..49bdea6d9c 100644 --- a/META.coq.in +++ b/META.coq.in @@ -1,7 +1,7 @@ # TODO: Generate automatically with Dune description = "The Coq Proof Assistant Plugin API" -version = "8.11" +version = "8.12" directory = "" requires = "" @@ -9,7 +9,7 @@ requires = "" package "config" ( description = "Coq Configuration Variables" - version = "8.11" + version = "8.12" directory = "config" @@ -19,7 +19,7 @@ package "config" ( package "clib" ( description = "Base General Coq Library" - version = "8.11" + version = "8.12" directory = "clib" requires = "str, unix, threads" @@ -31,7 +31,7 @@ package "clib" ( package "lib" ( description = "Base Coq-Specific Library" - version = "8.11" + version = "8.12" directory = "lib" @@ -45,7 +45,7 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.11" + version = "8.12" directory = "kernel/byterun" @@ -64,7 +64,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.11" + version = "8.12" directory = "kernel" @@ -78,7 +78,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.11" + version = "8.12" requires = "coq.kernel" @@ -92,7 +92,7 @@ package "library" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.11" + version = "8.12" requires = "coq.library" directory = "engine" @@ -105,7 +105,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.11" + version = "8.12" requires = "coq.engine" directory = "pretyping" @@ -118,7 +118,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.11" + version = "8.12" requires = "coq.pretyping" directory = "interp" @@ -131,7 +131,7 @@ package "interp" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.11" + version = "8.12" requires = "coq.interp" directory = "proofs" @@ -144,7 +144,7 @@ package "proofs" ( package "gramlib" ( description = "Coq Grammar Engine" - version = "8.11" + version = "8.12" requires = "coq.lib" directory = "gramlib/.pack" @@ -156,7 +156,7 @@ package "gramlib" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.11" + version = "8.12" requires = "coq.gramlib, coq.proofs" directory = "parsing" @@ -169,7 +169,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.11" + version = "8.12" requires = "coq.parsing" directory = "printing" @@ -182,7 +182,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.11" + version = "8.12" requires = "coq.printing" directory = "tactics" @@ -195,7 +195,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.11" + version = "8.12" requires = "coq.tactics" directory = "vernac" @@ -208,7 +208,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.11" + version = "8.12" requires = "coq.vernac" directory = "stm" @@ -221,7 +221,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.11" + version = "8.12" requires = "num, coq.stm" directory = "toplevel" @@ -234,7 +234,7 @@ package "toplevel" ( package "idetop" ( description = "Coq IDE Libraries" - version = "8.11" + version = "8.12" requires = "coq.toplevel" directory = "ide" @@ -247,7 +247,7 @@ package "idetop" ( package "ide" ( description = "Coq IDE Libraries" - version = "8.11" + version = "8.12" requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" @@ -260,7 +260,7 @@ package "ide" ( package "ideprotocol" ( description = "Coq IDE protocol" - version = "8.11" + version = "8.12" requires = "coq.toplevel" directory = "ide/protocol" @@ -273,14 +273,14 @@ package "ideprotocol" ( package "plugins" ( description = "Coq built-in plugins" - version = "8.11" + version = "8.12" directory = "plugins" package "ltac" ( description = "Coq LTAC Plugin" - version = "8.11" + version = "8.12" requires = "coq.stm" directory = "ltac" @@ -295,7 +295,7 @@ package "plugins" ( package "tauto" ( description = "Coq tauto plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "ltac" @@ -310,7 +310,7 @@ package "plugins" ( package "omega" ( description = "Coq omega plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "omega" @@ -325,7 +325,7 @@ package "plugins" ( package "micromega" ( description = "Coq micromega plugin" - version = "8.11" + version = "8.12" requires = "num,coq.plugins.ltac" directory = "micromega" @@ -340,7 +340,7 @@ package "plugins" ( package "zify" ( description = "Coq Zify plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "micromega" @@ -355,7 +355,7 @@ package "plugins" ( package "setoid_ring" ( description = "Coq newring plugin" - version = "8.11" + version = "8.12" requires = "" directory = "setoid_ring" @@ -370,7 +370,7 @@ package "plugins" ( package "extraction" ( description = "Coq extraction plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "extraction" @@ -385,7 +385,7 @@ package "plugins" ( package "cc" ( description = "Coq cc plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "cc" @@ -400,7 +400,7 @@ package "plugins" ( package "firstorder" ( description = "Coq ground plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "firstorder" @@ -415,7 +415,7 @@ package "plugins" ( package "rtauto" ( description = "Coq rtauto plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "rtauto" @@ -430,7 +430,7 @@ package "plugins" ( package "btauto" ( description = "Coq btauto plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "btauto" @@ -445,7 +445,7 @@ package "plugins" ( package "funind" ( description = "Coq recdef plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.extraction" directory = "funind" @@ -460,7 +460,7 @@ package "plugins" ( package "nsatz" ( description = "Coq nsatz plugin" - version = "8.11" + version = "8.12" requires = "num,coq.plugins.ltac" directory = "nsatz" @@ -475,7 +475,7 @@ package "plugins" ( package "rsyntax" ( description = "Coq rsyntax plugin" - version = "8.11" + version = "8.12" requires = "" directory = "syntax" @@ -490,7 +490,7 @@ package "plugins" ( package "int63syntax" ( description = "Coq int63syntax plugin" - version = "8.11" + version = "8.12" requires = "" directory = "syntax" @@ -505,7 +505,7 @@ package "plugins" ( package "string_notation" ( description = "Coq string_notation plugin" - version = "8.11" + version = "8.12" requires = "" directory = "syntax" @@ -520,7 +520,7 @@ package "plugins" ( package "derive" ( description = "Coq derive plugin" - version = "8.11" + version = "8.12" requires = "" directory = "derive" @@ -535,7 +535,7 @@ package "plugins" ( package "ssrmatching" ( description = "Coq ssrmatching plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ltac" directory = "ssrmatching" @@ -550,7 +550,7 @@ package "plugins" ( package "ssreflect" ( description = "Coq ssreflect plugin" - version = "8.11" + version = "8.12" requires = "coq.plugins.ssrmatching" directory = "ssr" diff --git a/Makefile.ci b/Makefile.ci index e9f7fa2db5..8315c16c64 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -19,6 +19,7 @@ CI_TARGETS= \ ci-coquelicot \ ci-corn \ ci-cross-crypto \ + ci-coqprime \ ci-elpi \ ci-ext-lib \ ci-equations \ @@ -38,6 +39,7 @@ CI_TARGETS= \ ci-perennial \ ci-quickchick \ ci-relation_algebra \ + ci-rewriter \ ci-sf \ ci-simple-io \ ci-stdlib2 \ @@ -56,10 +58,14 @@ ci-all: $(CI_TARGETS) ci-color: ci-bignums +ci-coqprime: ci-bignums + ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-fiat-crypto: ci-bedrock2 ci-coqprime ci-rewriter + ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io @@ -103,7 +103,7 @@ used, and include a complete source example leading to the bug. Guidelines for contributing to Coq in various ways are listed in the [contributor's guide](CONTRIBUTING.md). -Information about the next release is at https://github.com/coq/coq/wiki/Release-Plan +Information about release plans is at https://github.com/coq/coq/wiki/Release-Plan ## Supporting Coq diff --git a/configure.ml b/configure.ml index 60ba8b1101..89d9ed9d2a 100644 --- a/configure.ml +++ b/configure.ml @@ -12,11 +12,11 @@ #load "str.cma" open Printf -let coq_version = "8.11+alpha" -let coq_macos_version = "8.10.90" (** "[...] should be a string comprised of +let coq_version = "8.12+alpha" +let coq_macos_version = "8.11.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 81091 -let state_magic = 581091 +let vo_magic = 81191 +let state_magic = 581191 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; @@ -194,6 +194,12 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false +let build_date = + try + float_of_string (Sys.getenv "SOURCE_DATE_EPOCH") + with + Not_found -> Unix.time () + (** * Date *) (** The short one is displayed when starting coqtop, @@ -204,7 +210,7 @@ let months = "July";"August";"September";"October";"November";"December" |] let get_date () = - let now = Unix.localtime (Unix.time ()) in + let now = Unix.gmtime build_date in let year = 1900+now.Unix.tm_year in let month = months.(now.Unix.tm_mon) in sprintf "%s %d" month year, @@ -919,16 +925,16 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s let cflags_dflt = "-Wall -Wno-unused -g -O2 -fexcess-precision=standard" -let cflags_sse2 = ["-msse2"; "-mfpmath=sse"] +let cflags_sse2 = "-msse2 -mfpmath=sse" let cflags, sse2_math = let _, slurp = (* Test SSE2_MATH support <https://stackoverflow.com/a/45667927> *) - tryrun "cc" (["-march=native"; "-dM"; "-E"] - @ cflags_sse2 - @ [coqtop/"kernel/byterun/coq_interp.h"] (* any file *)) in + tryrun camlexec.find + ["ocamlc"; "-ccopt"; cflags_dflt ^ " -march=native -dM -E " ^ cflags_sse2; + "-c"; coqtop/"dev/header.c"] in (* any file *) if List.exists (fun line -> starts_with line "#define __SSE2_MATH__ 1") slurp - then (cflags_dflt ^ " " ^ String.concat " " cflags_sse2, true) + then (cflags_dflt ^ " " ^ cflags_sse2, true) else (cflags_dflt, false) (** Test at configure time that no harmful double rounding seems to diff --git a/default.nix b/default.nix index 19afc2bd1b..6a7a98aa5e 100644 --- a/default.nix +++ b/default.nix @@ -29,7 +29,7 @@ , shell ? false # We don't use lib.inNixShell because that would also apply # when in a nix-shell of some package depending on this one. -, coq-version ? "8.11-git" +, coq-version ? "8.12-git" }: with pkgs; diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5139113083..87122e0fb5 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -144,6 +144,13 @@ : "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" ######################################################################## +# rewriter +######################################################################## +: "${rewriter_CI_REF:=master}" +: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}" +: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}" + +######################################################################## # fiat_parsers ######################################################################## : "${fiat_parsers_CI_REF:=master}" @@ -179,13 +186,6 @@ : "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" ######################################################################## -# SF -######################################################################## -: "${sf_lf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz}" -: "${sf_plf_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz}" -: "${sf_vfa_CI_TARURL:=https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz}" - -######################################################################## # TLC ######################################################################## : "${tlc_CI_REF:=master-for-coq-ci}" @@ -200,6 +200,13 @@ : "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" ######################################################################## +# coqprime +######################################################################## +: "${coqprime_CI_REF:=master}" +: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}" +: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" + +######################################################################## # bedrock2 ######################################################################## : "${bedrock2_CI_REF:=master}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 2ac78d3c2b..8570c34194 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install ) diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh new file mode 100755 index 0000000000..a4fd296896 --- /dev/null +++ b/dev/ci/ci-coqprime.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqprime + +( cd "${CI_BUILD_DIR}/coqprime" && make && make install) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index e8c8d22678..000c418137 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,8 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 -fiat_crypto_CI_TARGETS1="c-files printlite lite" -fiat_crypto_CI_TARGETS2="coq" +fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1" +fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite" +fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s 32768 && \ diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh new file mode 100755 index 0000000000..235482ffeb --- /dev/null +++ b/dev/ci/ci-rewriter.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download rewriter + +( cd "${CI_BUILD_DIR}/rewriter" && make && make install) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 60436e672c..2b1d2298f2 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,10 +3,18 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" || exit 1 -wget -qO- "${sf_lf_CI_TARURL}" | tar xvz -wget -qO- "${sf_plf_CI_TARURL}" | tar xvz -wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz +CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2 +data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) + +mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" + +sf_lf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "lf.tgz") | .url') +sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url') +sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url') + +wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz +wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz +wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz ( cd lf && make clean && make ) ( cd plf && make clean && make ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 1cad46cd89..e80f96362b 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-11-05-V01" +# CACHEKEY: "bionic_coq-V2019-11-25-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -8,7 +8,7 @@ ENV DEBIAN_FRONTEND="noninteractive" RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of the image, the test-suite and external projects - m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \ + m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \ # Dependencies of lablgtk (for CoqIDE) libgtksourceview-3.0-dev \ # Dependencies of stdlib and sphinx doc diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 8ab00c6fd8..7d394c3401 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,5 @@ +## Changes between Coq 8.11 and Coq 8.12 + ## Changes between Coq 8.10 and Coq 8.11 ### ML API diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 0631b3ad59..67becb251a 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -120,7 +120,17 @@ Universes risk: unlikely to be activated by chance (requires a plugin) component: template polymorphism - summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though) + summary: template polymorphism not collecting side constrains on the + universe level of a parameter; this is a general form of the + previous issue about template polymorphism exploiting other ways to + generate untracked constraints + introduced: morally at the introduction of template polymorphism, 23 + May 2006, 9c2d70b, r8845, Herbelin + impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, + V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory + also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found + there yet (an exploit using a plugin to force sharing of universe + level is in principle possible though) impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit) fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau) @@ -129,6 +139,22 @@ Universes GH issue number: #9294 risk: moderate risk to be activated by chance + component: template polymorphism + summary: using the same universe in the parameters and the + constructor arguments of a template polymorphic inductive (using + named universes in modern Coq, or unification tricks in older Coq) + produces implicit equality constraints not caught by the previous + template polymorphism fix. + introduced: same as the previous template polymorphism bug, morally + from V8.1, first verified impacted version V8.5 (the universe + unification is sufficiently different in V8.4 to prevent our trick + from working) + fixed in: expected in 8.10.2, 8.11+beta, master (#11128, Nov 2019, Gilbert) + found by: Gilbert + exploit: test-suite/bugs/closed/bug_11039.v + GH issue number: #11039 + risk: moderate risk (found by investigating #10504) + component: universe polymorphism, asynchronous proofs summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh index dbb60359cb..e1aed4560d 100755 --- a/dev/tools/make-changelog.sh +++ b/dev/tools/make-changelog.sh @@ -3,7 +3,7 @@ printf "PR number? " read -r PR -printf "Where? (type a prefix)\n" +printf "Category? (type a prefix)\n" (cd doc/changelog && ls -d */) read -r where @@ -11,11 +11,25 @@ where="doc/changelog/$where" if ! [ -d "$where" ]; then where=$(echo "$where"*); fi where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst" +printf "Type? (type first letter)\n" +printf "[A]dded \t[C]hanged \t[D]eprecated \t[F]ixed \t[R]emoved\n" +read -r type_first_letter + +case "$type_first_letter" in + [Aa]) type_full="Added";; + [Cc]) type_full="Changed";; + [Dd]) type_full="Deprecated";; + [Ff]) type_full="Fixed";; + [Rr]) type_full="Removed";; + *) printf "Invalid input!\n" + exit 1;; +esac + # shellcheck disable=SC2016 # the ` are regular strings, this is intended # use %s for the leading - to avoid looking like an option (not sure # if necessary but doesn't hurt) -printf '%s bla bla (`#%s <https://github.com/coq/coq/pull/%s>`_, by %s).' - "$PR" "$PR" "$(git config user.name)" > "$where" +printf '%s **%s:**\n Bla bla\n (`#%s <https://github.com/coq/coq/pull/%s>`_,\n by %s).' - "$type_full" "$PR" "$PR" "$(git config user.name)" > "$where" printf "Name of created changelog file:\n" printf "$where\n" diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index c7bb36b6d3..7312c2a5af 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,6 +1,8 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python3 from __future__ import with_statement +from __future__ import print_function import os, re, sys, subprocess +from io import open # When passed `--release`, this script sets up Coq to support three # `-compat` flag arguments. If executed manually, this would consist @@ -84,17 +86,25 @@ BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *) (* It is autogenerated by %s. *) """ % os.path.relpath(os.path.realpath(__file__), ROOT_PATH) +def get_file_lines(file_name): + with open(file_name, 'rb') as f: + lines = f.readlines() + return [line.decode('utf-8') for line in lines] + +def get_file(file_name): + return ''.join(get_file_lines(file_name)) + def get_header(): - with open(HEADER_PATH, 'r') as f: return f.read() + return get_file(HEADER_PATH) HEADER = get_header() -def break_or_continue(): - msg = 'Press ENTER to continue, or Ctrl+C to break...' - try: - raw_input(msg) - except NameError: # we must be running python3 - input(msg) +def fatal_error(msg): + if hasattr(sys.stderr, 'buffer'): + sys.stderr.buffer.write(msg.encode("utf-8")) + else: + sys.stderr.write(msg.encode("utf-8")) + sys.exit(1) def maybe_git_add(local_path, suggest_add=True, **args): if args['git_add']: @@ -114,11 +124,10 @@ def maybe_git_rm(local_path, **args): def get_version(cur_version=None): if cur_version is not None: return cur_version - with open(CONFIGURE_PATH, 'r') as f: - for line in f.readlines(): - found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line) - if len(found) > 0: - return found[0] + for line in get_file_lines(CONFIGURE_PATH): + found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line) + if len(found) > 0: + return found[0] raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH)) def compat_name_to_version_name(compat_file_name): @@ -132,8 +141,7 @@ def version_name_to_compat_name(v, ext='.v'): # returns (lines of compat files, lines of not compat files def get_doc_index_lines(): - with open(DOC_INDEX_PATH, 'r') as f: - lines = f.readlines() + lines = get_file_lines(DOC_INDEX_PATH) return (tuple(line for line in lines if 'theories/Compat/Coq' in line), tuple(line for line in lines if 'theories/Compat/Coq' not in line)) @@ -183,7 +191,7 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su if contents is None or contents != new_contents: if not assert_unchanged: print('Updating %s...' % os.path.relpath(path, ROOT_PATH)) - with open(path, 'w') as f: + with open(path, 'w', encoding='utf-8') as f: f.write(new_contents) maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args) else: @@ -226,8 +234,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args) else: # print('Checking %s...' % compat_file) - with open(compat_path, 'r') as f: - contents = f.read() + contents = get_file(compat_path) header = HEADER + (EXTRA_HEADER % v) if not contents.startswith(HEADER): raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH))) @@ -323,13 +330,13 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath): raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath)) def update_flags_mli(old_versions, new_versions, **args): - with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read() + contents = get_file(FLAGS_MLI_PATH) new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args) def update_flags_ml(old_versions, new_versions, **args): - with open(FLAGS_ML_PATH, 'r') as f: contents = f.read() + contents = get_file(FLAGS_ML_PATH) new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) @@ -337,13 +344,13 @@ def update_flags_ml(old_versions, new_versions, **args): update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args) def update_coqargs_ml(old_versions, new_versions, **args): - with open(COQARGS_ML_PATH, 'r') as f: contents = f.read() + contents = get_file(COQARGS_ML_PATH) new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args) def update_g_vernac(old_versions, new_versions, **args): - with open(G_VERNAC_PATH, 'r') as f: contents = f.read() + contents = get_file(G_VERNAC_PATH) new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args) check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, G_VERNAC_PATH, **args) @@ -361,7 +368,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES contents = None suggest_add = False if os.path.exists(path): - with open(path, 'r') as f: contents = f.read() + contents = get_file(path) else: suggest_add = True if '%s' in descr: descr = descr % v @@ -376,7 +383,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES remove_if_exists(path, assert_unchanged=assert_unchanged, **args) def update_doc_index(new_versions, **args): - with open(DOC_INDEX_PATH, 'r') as f: contents = f.read() + contents = get_file(DOC_INDEX_PATH) firstline = ' theories/Compat/AdmitAxiom.v' new_contents = ''.join(DOC_INDEX_LINES) if firstline not in new_contents: @@ -386,7 +393,7 @@ def update_doc_index(new_versions, **args): update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args) def update_test_suite_run(**args): - with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read() + contents = get_file(TEST_SUITE_RUN_PATH) new_contents = r'''#!/usr/bin/env bash # allow running this script from any directory by basing things on where the script lives @@ -410,7 +417,7 @@ def update_compat_notations(old_versions, new_versions, **args): for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')): for fname in files: if not fname.endswith('.v'): continue - with open(os.path.join(root, fname), 'r') as f: contents = f.read() + contents = get_file(os.path.join(root, fname)) new_contents = update_compat_notations_in(old_versions, new_versions, contents) update_if_changed(contents, new_contents, os.path.join(root, fname), **args) @@ -435,9 +442,8 @@ def parse_args(argv): 'git_add': False, } if '--master' not in argv and '--release' not in argv: - print(r'''WARNING: You should pass either --release (sometime before branching) + fatal_error(r'''ERROR: You should pass either --release (sometime before branching) or --master (right after branching and updating the version number in version.ml)''') - if '--assert-unchanged' not in args: break_or_continue() for arg in argv[1:]: if arg == '--assert-unchanged': args['assert_unchanged'] = True diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst deleted file mode 100644 index 56b5fc747a..0000000000 --- a/doc/changelog/01-kernel/09867-floats.rst +++ /dev/null @@ -1,13 +0,0 @@ -- A built-in support of floating-point arithmetic was added, allowing - one to devise efficient reflection tactics involving numerical - computation. Primitive floats are added in the language of terms, - following the binary64 format of the IEEE 754 standard, and the - related operations are implemented for the different reduction - engines of Coq by using the corresponding processor operators in - rounding-to-nearest-even. The properties of these operators are - axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part - of the library :g:`Coq.Floats.Floats`. - See Section :ref:`primitive-floats` - (`#9867 <https://github.com/coq/coq/pull/9867>`_, - closes `#8276 <https://github.com/coq/coq/issues/8276>`_, - by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md deleted file mode 100644 index e0573a2c74..0000000000 --- a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md +++ /dev/null @@ -1,4 +0,0 @@ -- Internal definitions generated by abstract-like tactics are now inlined - inside universe Qed-terminated polymorphic definitions, similarly to what - happens for their monomorphic counterparts, - (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst deleted file mode 100644 index bac08d12ea..0000000000 --- a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Section data is now part of the kernel. Solves a soundness issue - in interactive mode where global monomorphic universe constraints would be - dropped when forcing a delayed opaque proof inside a polymorphic section. Also - relaxes the nesting criterion for sections, as polymorphic sections can now - appear inside a monomorphic one - (#10664, <https://github.com/coq/coq/pull/10664> by Pierre-Marie Pédrot). diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst deleted file mode 100644 index 349c44c205..0000000000 --- a/doc/changelog/01-kernel/10811-sprop-default-on.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Using ``SProp`` is now allowed by default, without needing to pass - ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 - <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst deleted file mode 100644 index 279bb9272a..0000000000 --- a/doc/changelog/02-specification-language/10049-bidi-app.rst +++ /dev/null @@ -1,6 +0,0 @@ -- New annotation in `Arguments` for bidirectionality hints: it is now possible - to tell type inference to use type information from the context once the `n` - first arguments of an application are known. The syntax is: - `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` - (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with - help from Enrico Tassi). diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst deleted file mode 100644 index 0a902079b9..0000000000 --- a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Record fields can be annotated to prevent them from being used as canonical projections; - see :ref:`canonicalstructures` for details - (`#10076 <https://github.com/coq/coq/pull/10076>`_, - by Vincent Laporte). diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst deleted file mode 100644 index 2d17e569d3..0000000000 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ /dev/null @@ -1,12 +0,0 @@ -- Require parentheses around nested disjunctive patterns, so that pattern and - term syntax are consistent; match branch patterns no longer require - parentheses for notation at level 100 or more. Incompatibilities: - - + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be - omitted around :n:`0|1`. - + notation :g:`(p | q)` now potentially clashes with core pattern syntax, - and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. - - See :ref:`extendedpatternmatching` for details - (`#10167 <https://github.com/coq/coq/pull/10167>`_, - by Georges Gonthier). diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst deleted file mode 100644 index 71b10aaaf4..0000000000 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ /dev/null @@ -1,11 +0,0 @@ -- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` - annotation, see :ref:`advanced-recursive-functions` for the updated - documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, - by Enrico Tassi). - -- The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used - inside a module type. In order to declare a module type parameter that - happens to be a morphism, use :cmd:`Declare Morphism`. See - :ref:`deprecated_syntax_for_generalized_rewriting` for the updated - documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, - by Enrico Tassi). diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst deleted file mode 100644 index 7f0345d946..0000000000 --- a/doc/changelog/02-specification-language/10441-static-poly-section.rst +++ /dev/null @@ -1,11 +0,0 @@ -- The universe polymorphism setting now applies from the opening of a section. - In particular, it is not possible anymore to mix polymorphic and monomorphic - definitions in a section when there are no variables nor universe constraints - defined in this section. This makes the behaviour consistent with the - documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, - by Pierre-Marie Pédrot) - -- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In - addition to setting the section universe polymorphism, it also locally sets - the universe polymorphic option inside the section. - (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst deleted file mode 100644 index 4cce26aedc..0000000000 --- a/doc/changelog/02-specification-language/10758-fix-10757.rst +++ /dev/null @@ -1,5 +0,0 @@ -- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes - involving ``Prop`` types (`#10758 - <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing - `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by - Xavier Leroy). diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst deleted file mode 100644 index 1e05b0b0fe..0000000000 --- a/doc/changelog/02-specification-language/10985-about-arguments.rst +++ /dev/null @@ -1,5 +0,0 @@ -- The output of the :cmd:`Print` and :cmd:`About` commands has - changed. Arguments meta-data is now displayed as the corresponding - :cmd:`Arguments <Arguments (implicits)>` command instead of the - human-targeted prose used in previous Coq versions. (`#10985 - <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst deleted file mode 100644 index cd1a692f54..0000000000 --- a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Added ``#[refine]`` attribute for :cmd:`Instance`, a more - predictable version of the old ``Refine Instance Mode`` which - unconditionally opens a proof (`#10996 - <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst deleted file mode 100644 index 43a748b365..0000000000 --- a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst +++ /dev/null @@ -1,3 +0,0 @@ -- The unsupported attribute error is now an error-by-default warning, - meaning it can be disabled (`#10997 - <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst deleted file mode 100644 index f8298cdbdd..0000000000 --- a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst +++ /dev/null @@ -1,13 +0,0 @@ -- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments - in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_ - (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin). - - .. example:: - - The following features an implicit argument after a local - definition. It was wrongly rejected. - - .. coqtop:: in - - Definition f := fix f (o := true) {n : nat} m {struct m} := - match m with 0 => 0 | S m' => f (n:=n+1) m' end. diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst deleted file mode 100644 index abc5a516ae..0000000000 --- a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Numeral Notations now support sorts in the input to printing - functions (e.g., numeral notations can be defined for terms - containing things like `@cons Set nat nil`). (`#9883 - <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst deleted file mode 100644 index bce5db5865..0000000000 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` - attribute. The former `compat` annotation for notations is - deprecated, and its semantics changed. It is now made equivalent to using - a `deprecated` attribute, and is no longer connected with the `-compat` - command-line flag - (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst deleted file mode 100644 index 327a39bdb6..0000000000 --- a/doc/changelog/03-notations/10963-simplify-parser.rst +++ /dev/null @@ -1,6 +0,0 @@ -- A simplification of parsing rules could cause a slight change of - parsing precedences for the very rare users who defined notations - with `constr` at level strictly between 100 and 200 and used these - notations on the right-hand side of a cast operator (`:`, `:>`, - `:>>`) (`#10963 <https://github.com/coq/coq/pull/10963>`_, by Théo - Zimmermann, simplification initially noticed by Jim Fehrle). diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst deleted file mode 100644 index 0cb669778c..0000000000 --- a/doc/changelog/04-tactics/09288-injection-as.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as - an alternative to :n:`injection @term as {+ @simple_intropattern}` using - the standard :n:`@injection_intropattern` syntax (`#9288 - <https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/09856-zify.rst b/doc/changelog/04-tactics/09856-zify.rst deleted file mode 100644 index 6b9143c77b..0000000000 --- a/doc/changelog/04-tactics/09856-zify.rst +++ /dev/null @@ -1,7 +0,0 @@ -- Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. - It can also be extended by redefining the tactic ``zify_post_hook``. - (`#9856 <https://github.com/coq/coq/pull/9856>`_ fixes - `#8898 <https://github.com/coq/coq/issues/8898>`_, - `#7886 <https://github.com/coq/coq/issues/7886>`_, - `#9848 <https://github.com/coq/coq/issues/9848>`_ and - `#5155 <https://github.com/coq/coq/issues/5155>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst deleted file mode 100644 index b4f991316e..0000000000 --- a/doc/changelog/04-tactics/10318-select-only-error.rst +++ /dev/null @@ -1,4 +0,0 @@ -- The goal selector tactical ``only`` now checks that the goal range - it is given is valid instead of ignoring goals out of the focus - range (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan - Gilbert). diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst deleted file mode 100644 index 12d8f68e63..0000000000 --- a/doc/changelog/04-tactics/10765-micromega-caches.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. - (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case) - (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson). diff --git a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst deleted file mode 100644 index ed46cb101e..0000000000 --- a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst +++ /dev/null @@ -1,3 +0,0 @@ -- The :tacn:`zify` tactic is now aware of `Z.to_N`. - (`#10774 <https://github.com/coq/coq/pull/10774>`_ fixes - `#9162 <https://github.com/coq/coq/issues/9162>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst deleted file mode 100644 index 09bef82c80..0000000000 --- a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst +++ /dev/null @@ -1,11 +0,0 @@ -- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now - only run their tactic argument once, even if it has multiple - successes. This prevents blow-up and looping from using - multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 - <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 - <https://github.com/coq/coq/issues/10965>`_, by Jason Gross). - -- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now - behave correctly when their tactic fully solves the goal. (`#10966 - <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 - <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst index 3ec526f0a9..c72d085687 100644 --- a/doc/changelog/04-tactics/10998-zify-complements.rst +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -1,4 +1,5 @@ -- The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, +- **Added:** + The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`. Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`) diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst deleted file mode 100644 index 6d62f11eff..0000000000 --- a/doc/changelog/05-tactic-language/10002-ltac2.rst +++ /dev/null @@ -1,9 +0,0 @@ -- Ltac2, a new version of the tactic language Ltac, that doesn't - preserve backward compatibility, has been integrated in the main Coq - distribution. It is still experimental, but we already recommend - users of advanced Ltac to start using it and report bugs or request - enhancements. See its documentation in the :ref:`dedicated chapter - <ltac2>` (`#10002 <https://github.com/coq/coq/pull/10002>`_, plugin - authored by Pierre-Marie Pédrot, with contributions by various - users, integration by Maxime Dénès, help on integrating / improving - the documentation by Théo Zimmermann and Jim Fehrle). diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst deleted file mode 100644 index bd1c0c42e8..0000000000 --- a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Ltac2 tactic notations with “constr” arguments can specify the - interpretation scope for these arguments; - see :ref:`ltac2_notations` for details - (`#10289 <https://github.com/coq/coq/pull/10289>`_, - by Vincent Laporte). diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst deleted file mode 100644 index fba09f5e87..0000000000 --- a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst +++ /dev/null @@ -1,5 +0,0 @@ -- White spaces are forbidden in the “&ident” syntax for ltac2 references - that are described in :ref:`ltac2_built-in-quotations` - (`#10324 <https://github.com/coq/coq/pull/10324>`_, - fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, - authored by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst deleted file mode 100644 index 5e005742fd..0000000000 --- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst +++ /dev/null @@ -1,28 +0,0 @@ -- Generalize tactics :tacn:`under` and :tacn:`over` for any registered - relation. More precisely, assume the given context lemma has type - `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The - first step performed by :tacn:`under` (since Coq 8.10) amounts to - calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which - itself relies on :tacn:`setoid_rewrite` if need be. So this step was - already compatible with a double implication or setoid equality for - the conclusion head symbol `R2`. But a further step consists in - tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from - unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)` - that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second - (convenience) step was only performed when `R1` was Leibniz' `eq` or - `iff`. Now, it is also performed for any relation `R1` which has a - ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance - being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` - goal by instantiating the hidden evar.) Also, it is now possible to - manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` - is a `PreOrder` relation or so, thanks to extra instances proving - that `Under_rel` preserves the properties of the `R1` relation. - These two features generalizing support for setoid-like relations is - enabled as soon as we do both ``Require Import ssreflect.`` and - ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been - added if one wants to "unprotect" the evar, and instantiate it - manually with another rule than reflexivity (i.e., without using the - :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section - :ref:`under_ssr` (`#10022 <https://github.com/coq/coq/pull/10022>`_, - by Erik Martin-Dorel, with suggestions and review by Enrico Tassi - and Cyril Cohen). diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst deleted file mode 100644 index 7366ef1190..0000000000 --- a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`) - (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de - Amorim). diff --git a/doc/changelog/06-ssreflect/11136-inj_compr.rst b/doc/changelog/06-ssreflect/11136-inj_compr.rst deleted file mode 100644 index b546fcde6b..0000000000 --- a/doc/changelog/06-ssreflect/11136-inj_compr.rst +++ /dev/null @@ -1,2 +0,0 @@ -- Added lemma :g:`inj_compr` to :g:`ssr.ssrfun` - (`#11136 <https://github.com/coq/coq/pull/11136>`_, by Cyril Cohen). diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst deleted file mode 100644 index 1c91800c65..0000000000 --- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Deprecated flag `Refine Instance Mode` has been removed. - (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes - `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 - <https://github.com/coq/coq/issues/3890>`_ and `#4638 - <https://github.com/coq/coq/issues/4638>`_ - by Maxime Dénès, review by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst deleted file mode 100644 index c69cda9656..0000000000 --- a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst +++ /dev/null @@ -1,2 +0,0 @@ -- Remove undocumented :n:`Instance : !@type` syntax - (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst deleted file mode 100644 index 7fdeb632b4..0000000000 --- a/doc/changelog/07-commands-and-options/10277-no-show-script.rst +++ /dev/null @@ -1,2 +0,0 @@ -- Remove ``Show Script`` command (deprecated since 8.10) - (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst deleted file mode 100644 index ef7adde801..0000000000 --- a/doc/changelog/07-commands-and-options/10291-typing-flags.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Adding unsafe commands to enable/disable guard checking, positivity checking - and universes checking (providing a local `-type-in-type`). - See :ref:`controlling-typing-flags`. - (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). diff --git a/doc/changelog/07-commands-and-options/10476-fix-export.rst b/doc/changelog/07-commands-and-options/10476-fix-export.rst deleted file mode 100644 index ba71e1c337..0000000000 --- a/doc/changelog/07-commands-and-options/10476-fix-export.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Fix two bugs in `Export`. This can have an impact on the behavior of the - `Import` command on libraries. `Import A` when `A` imports `B` which exports - `C` was importing `C`, whereas `Import` is not transitive. Also, after - `Import A B`, the import of `B` was sometimes incomplete. - (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst deleted file mode 100644 index 580e808baa..0000000000 --- a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst +++ /dev/null @@ -1,7 +0,0 @@ -- Update output generated by :flag:`Printing Dependent Evars Line` flag - used by the Prooftree tool in Proof General. - (`#10489 <https://github.com/coq/coq/pull/10489>`_, - closes `#4504 <https://github.com/coq/coq/issues/4504>`_, - `#10399 <https://github.com/coq/coq/issues/10399>`_ and - `#10400 <https://github.com/coq/coq/issues/10400>`_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst deleted file mode 100644 index c1df728c5c..0000000000 --- a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Optionally highlight the differences between successive proof steps in the - :cmd:`Show Proof` command. Experimental; only available in coqtop - and Proof General for now, may be supported in other IDEs - in the future. - (`#10494 <https://github.com/coq/coq/pull/10494>`_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst new file mode 100644 index 0000000000..9fc09c4189 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst @@ -0,0 +1,3 @@ +- **Removed:** ``Typeclasses Axioms Are Instances`` flag, deprecated since 8.10. + Use :cmd:`Declare Instance` for axioms which should be instances + (`#11185 <https://github.com/coq/coq/pull/11185>`_, by Théo Zimmermann). diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst deleted file mode 100644 index f612096880..0000000000 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ /dev/null @@ -1,7 +0,0 @@ -- `coqc` now provides the ability to generate compiled interfaces. - Use `coqc -vos foo.v` to skip all opaque proofs during the - compilation of `foo.v`, and output a file called `foo.vos`. - This feature is experimental. It enables working on a Coq file without the need to - first compile the proofs contained in its dependencies - (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by - Maxime Dénès and Emilio Gallego). diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst deleted file mode 100644 index 54417077f5..0000000000 --- a/doc/changelog/08-tools/10245-require-command-line.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Add command line options `-require-import`, `-require-export`, - `-require-import-from` and `-require-export-from`, as well as their - shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate - confusing command line option `-require` - (`#10245 <https://github.com/coq/coq/pull/10245>`_ - by Hugo Herbelin, review by Emilio Gallego). diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst deleted file mode 100644 index f620b32cb8..0000000000 --- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` - utility, where `<CoqMakefile>` is the name of the output file given by the - `-o` option. In this way two generated makefiles can coexist in the same - directory. - (`#10947 <https://github.com/coq/coq/pull/10947>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/08-tools/11068-coqbin-noslash.rst b/doc/changelog/08-tools/11068-coqbin-noslash.rst deleted file mode 100644 index c2c8f4df31..0000000000 --- a/doc/changelog/08-tools/11068-coqbin-noslash.rst +++ /dev/null @@ -1,3 +0,0 @@ -- ``coq_makefile`` now supports environment variable ``COQBIN`` with - no ending ``/`` character (`#11068 - <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst deleted file mode 100644 index 7babcdb6f1..0000000000 --- a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Moved the `auto` hints of the `OrderedType` module into a new `ordered_type` - database - (`#9772 <https://github.com/coq/coq/pull/9772>`_, - by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst deleted file mode 100644 index ab625b9e03..0000000000 --- a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Removes deprecated modules `Coq.ZArith.Zlogarithm` - and `Coq.ZArith.Zsqrt_compat` - (#9881 <https://github.com/coq/coq/pull/9811> - by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst deleted file mode 100644 index d69056fc2f..0000000000 --- a/doc/changelog/10-standard-library/10445-constructive-reals.rst +++ /dev/null @@ -1,12 +0,0 @@ -- New module `Reals.ConstructiveCauchyReals` defines constructive real numbers - by Cauchy sequences of rational numbers. Classical real numbers are now defined - as a quotient of these constructive real numbers, which significantly reduces - the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`), - while preserving backward compatibility. - - Futhermore, the new axioms for classical real numbers include the limited - principle of omniscience (`sig_forall_dec`), which is a logical principle - instead of an ad hoc property of the real numbers. - - See `#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria, - with the help and review of Guillaume Melquiond and Bas Spitters. diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst deleted file mode 100644 index 864c4e6a7e..0000000000 --- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst +++ /dev/null @@ -1,6 +0,0 @@ -- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and - :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the - :g:`List` module. - - See `#10651 <https://github.com/coq/coq/pull/10651>`_, and - `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash. diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst deleted file mode 100644 index 5d8467025b..0000000000 --- a/doc/changelog/10-standard-library/10827-dedekind-reals.rst +++ /dev/null @@ -1,11 +0,0 @@ -- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers - as boolean-values functions along with 3 logical axioms: limited principle - of omniscience, excluded middle of negations and functional extensionality. - The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those - Dedekind reals, hidden behind an opaque module. - Classical Dedekind reals are a quotient of constructive reals, which allows - to transport many constructive proofs to the classical case. - - See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, - based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, - code review by Hugo Herbelin. diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst deleted file mode 100644 index 6e87ff93c7..0000000000 --- a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst +++ /dev/null @@ -1 +0,0 @@ -- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). diff --git a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst deleted file mode 100644 index 8bfd01d7a0..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Coq now officially supports OCaml 4.08. - - see INSTALL files for details - (`#10471 <https://github.com/coq/coq/pull/10471>`_, - by Emilio Jesús Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst new file mode 100644 index 0000000000..5c08e2b0ea --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst @@ -0,0 +1,5 @@ +- **Added:** + Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). diff --git a/doc/changelog/README.md b/doc/changelog/README.md index 3e0970a656..05bf710f89 100644 --- a/doc/changelog/README.md +++ b/doc/changelog/README.md @@ -15,12 +15,12 @@ entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). ## How to add an entry? ## Run `./dev/tools/make-changelog.sh`: it will ask you for your PR -number, and to choose among the predefined categories. Afterward, -fill in the automatically generated entry with a short description of -your change (which should describe any compatibility issues in -particular). You may also add a reference to the relevant fixed -issue, and credit reviewers, co-authors, and anyone who helped advance -the PR. +number, and to choose among the predefined categories, and the +predefined types of changes. Afterward, fill in the automatically +generated entry with a short description of your change (which should +describe any compatibility issues in particular). You may also add a +reference to the relevant fixed issue, and credit reviewers, +co-authors, and anyone who helped advance the PR. The format for changelog entries is the same as in the reference manual. In particular, you may reference the documentation you just @@ -31,10 +31,18 @@ manual for details. Here is a summary of the structure of a changelog entry: ``` rst -- Description of the changes, with possible link to +- **Added / Changed / Deprecated / Fixed / Removed:** + Description of the changes, with possible link to :ref:`relevant-section` of the updated documentation (`#PRNUM <https://github.com/coq/coq/pull/PRNUM>`_, [fixes `#ISSUE1 <https://github.com/coq/coq/issues/ISSUE1>`_ [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],] by Full Name[, with help / review of Full Name]). ``` + +The first line indicates the type of change. Available types come +from the [Keep a Changelog +1.0.0](https://keepachangelog.com/en/1.0.0/) specification. We +exclude the "Security" type for now because of the absence of a +process for handling critical bugs (proof of False) as security +vulnerabilities. diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md index 6d142a9af8..e0cedb0487 100644 --- a/doc/plugin_tutorial/README.md +++ b/doc/plugin_tutorial/README.md @@ -3,13 +3,21 @@ How to write plugins in Coq # Working environment In addition to installing OCaml and Coq, it can help to install several tools for development. - - ## Merlin + + ## Tuareg and Merlin These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) ```shell opam install merlin # prints instructions for vim and emacs +opam install tuareg # syntax highlighting for OCaml +opam user-setup install # automatically configures editors for merlin +``` + + Adding this line to your .emacs helps Tuareg recognize the .mlg extension: + +```shell +(add-to-list 'auto-mode-alist '("\\.mlg$" . tuareg-mode) t) ``` ## This tutorial @@ -23,7 +31,7 @@ make # build # tuto0 : basics of project organization - package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + package an mlg file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - Example of function call to print a simple message - Example of function call to print a simple warning diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index ca5b5e54a7..9f5741f72a 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -9,7 +9,7 @@ This chapter presents the extension of several equality related tactics to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities. Actually, the tactics have also been generalized to -relations weaker then equivalences (e.g. rewriting systems). The +relations weaker than equivalences (e.g. rewriting systems). The toolbox also extends the automatic rewriting capabilities of the system, allowing the specification of custom strategies for rewriting. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 661aa88082..57a2254100 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -576,14 +576,6 @@ Settings of goals. Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this option to 0 turns that flag off. -.. flag:: Typeclasses Axioms Are Instances - - .. deprecated:: 8.10 - - This flag (off by default since 8.8) automatically declares axioms - whose type is a typeclass at declaration time as instances of that - class. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 80a24b997c..1d0c937792 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -6,6 +6,512 @@ Recent changes .. include:: ../unreleased.rst +Version 8.11 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +The main changes brought by |Coq| version 8.11 are: + +- `Ltac2`__, a new tactic language for writing more robust larger scale + tactics, with built-in support for datatypes and the multi-goal tactic monad. +- `Primitive floats`__ are integrated in terms and follow the binary64 format + of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library. +- `Cleanups`__ of the section mechanism, delayed proofs and further + restrictions of template polymorphism to fix soundness issues related to + universes. +- New `unsafe flags`__ to disable locally guard, positivity and universe + checking. Reliance on these flags is always printed by + :g:`Print Assumptions`. +- `Fixed bugs`__ of :g:`Export` and :g:`Import` that can have a + significant impact on user developments (**common source of + incompatibility!**). +- New interactive development method based on `vos` `interface files`__, + allowing to work on a file without recompiling the proof parts of their + dependencies. +- New :g:`Arguments` annotation for `bidirectional type inference`__ + configuration for reference (e.g. constants, inductive) applications. +- New `refine attribute`__ for :cmd:`Instance` can be used instead of + the removed ``Refine Instance Mode``. +- Generalization of the :g:`under` and :g:`over` tactics__ of SSReflect to + arbitrary relations. +- `Revision`__ of the :g:`Coq.Reals` library, its axiomatisation and + instances of the constructive and classical real numbers. + +__ 811Ltac2_ +__ 811PrimitiveFloats_ +__ 811Sections_ +__ 811UnsafeFlags_ +__ 811ExportBug_ +__ 811vos_ +__ 811BidirArguments_ +__ 811RefineInstance_ +__ 811SSRUnderOver_ +__ 811Reals_ + +The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| +and affected releases. See the `Changes in 8.11+beta1`_ section for the +detailed list of changes, including potentially breaking changes marked with +**Changed**. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop, Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + +Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of +the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference +manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of +the standard library). + +The OPAM repository for |Coq| packages has been maintained by +Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions +from many users. A list of packages is available at +https://coq.inria.fr/opam/www/. + +The 61 contributors to this version are Michael D. Adams, Guillaume +Allais, Helge Bahmann, Langston Barrett, Guillaume Bertholon, Frédéric +Besson, Simon Boulier, Michele Caci, Tej Chajed, Arthur Charguéraud, +Cyril Cohen, Frédéric Dabrowski, Arthur Azevedo de Amorim, Maxime +Dénès, Nikita Eshkeev, Jim Fehrle, Emilio Jesús Gallego Arias, +Paolo G. Giarrusso, Gaëtan Gilbert, Georges Gonthier, Jason Gross, +Samuel Gruetter, Armaël Guéneau, Hugo Herbelin, Florent Hivert, Jasper +Hugunin, Shachar Itzhaky, Jan-Oliver Kaiser, Robbert Krebbers, Vincent +Laporte, Olivier Laurent, Samuel Lelièvre, Nicholas Lewycky, Yishuai +Li, Jose Fernando Lopez Fernandez, Andreas Lynge, Kenji Maillard, Erik +Martin-Dorel, Guillaume Melquiond, Alexandre Moine, Oliver Nash, +Wojciech Nawrocki, Antonio Nikishaev, Pierre-Marie Pédrot, Clément +Pit-Claudel, Lars Rasmusson, Robert Rand, Talia Ringer, JP Rodi, +Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, +Matthieu Sozeau, spanjel, Claude Stolze, Enrico Tassi, Laurent Théry, +James R. Wilcox, Xia Li-yao, Théo Zimmermann + +Many power users helped to improve the design of the new features via +the issue and pull request system, the |Coq| development mailing list, +the coq-club@inria.fr mailing list or the `Discourse forum +<https://coq.discourse.group/>`_. It would be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.11 is the sixth release of |Coq| developed on a time-based +development cycle. Its development spanned 3 months from the release of +|Coq| 8.10. Pierre-Marie Pédrot is the release manager and maintainer of this +release, assisted by Matthieu Sozeau. This release is the result of 2000+ +commits and 300+ PRs merged, closing 75+ issues. + +| Paris, November 2019, +| Matthieu Sozeau for the |Coq| development team +| + + +Changes in 8.11+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + + .. _811PrimitiveFloats: + +- **Added:** + A built-in support of floating-point arithmetic, allowing + one to devise efficient reflection tactics involving numerical + computation. Primitive floats are added in the language of terms, + following the binary64 format of the IEEE 754 standard, and the + related operations are implemented for the different reduction + engines of Coq by using the corresponding processor operators in + rounding-to-nearest-even. The properties of these operators are + axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part + of the library :g:`Coq.Floats.Floats`. + See Section :ref:`primitive-floats` + (`#9867 <https://github.com/coq/coq/pull/9867>`_, + closes `#8276 <https://github.com/coq/coq/issues/8276>`_, + by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). +- **Changed:** + Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined + inside universe :cmd:`Qed`\-terminated polymorphic definitions, similarly to what + happens for their monomorphic counterparts, + (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). + + .. _811Sections: + +- **Fixed:** + Section data is now part of the kernel. Solves a soundness issue + in interactive mode where global monomorphic universe constraints would be + dropped when forcing a delayed opaque proof inside a polymorphic section. Also + relaxes the nesting criterion for sections, as polymorphic sections can now + appear inside a monomorphic one + (`#10664, <https://github.com/coq/coq/pull/10664>`_ by Pierre-Marie Pédrot). +- **Changed:** + Using ``SProp`` is now allowed by default, without needing to pass + ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 + <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + + .. _811BidirArguments: + +- **Added:** + Annotation in `Arguments` for bidirectionality hints: it is now possible + to tell type inference to use type information from the context once the `n` + first arguments of an application are known. The syntax is: + `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` + (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with + help from Enrico Tassi). +- **Added:** + Record fields can be annotated to prevent them from being used as canonical projections; + see :ref:`canonicalstructures` for details + (`#10076 <https://github.com/coq/coq/pull/10076>`_, + by Vincent Laporte). +- **Changed:** + Require parentheses around nested disjunctive patterns, so that pattern and + term syntax are consistent; match branch patterns no longer require + parentheses for notation at level 100 or more. + + .. warning:: Incompatibilities + + + In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + Notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + + See :ref:`extendedpatternmatching` for details + (`#10167 <https://github.com/coq/coq/pull/10167>`_, + by Georges Gonthier). +- **Changed:** + :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). +- **Changed:** + The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used + inside a module type. In order to declare a module type parameter that + happens to be a morphism, use :cmd:`Declare Morphism`. See + :ref:`deprecated_syntax_for_generalized_rewriting` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). +- **Changed:** + The universe polymorphism setting now applies from the opening of a section. + In particular, it is not possible anymore to mix polymorphic and monomorphic + definitions in a section when there are no variables nor universe constraints + defined in this section. This makes the behaviour consistent with the + documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, + by Pierre-Marie Pédrot) +- **Added:** + The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + addition to setting the section universe polymorphism, it also locally sets + the universe polymorphic option inside the section. + (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) +- **Fixed:** + ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes + involving ``Prop`` types (`#10758 + <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing + `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by + Xavier Leroy). +- **Changed:** + Output of the :cmd:`Print` and :cmd:`About` commands. + Arguments meta-data is now displayed as the corresponding + :cmd:`Arguments <Arguments (implicits)>` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). + + .. _811RefineInstance: + +- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more + predictable version of the old ``Refine Instance Mode`` which + unconditionally opens a proof (`#10996 + <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). +- **Changed:** + The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). +- **Fixed:** Bugs sometimes preventing to define valid (co)fixpoints with implicit arguments + in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_ + (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin). + + .. example:: + + The following features an implicit argument after a local + definition. It was wrongly rejected. + + .. coqtop:: in + + Definition f := fix f (o := true) {n : nat} m {struct m} := + match m with 0 => 0 | S m' => f (n:=n+1) m' end. + +**Notations** + +- **Added:** + Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). +- **Added:** + The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). +- **Deprecated:** + The former `compat` annotation for notations is + deprecated, and its semantics changed. It is now made equivalent to using + a `deprecated` attribute, and is no longer connected with the `-compat` + command-line flag + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). +- **Changed:** + A simplification of parsing rules could cause a slight change of + parsing precedences for the very rare users who defined notations + with `constr` at level strictly between 100 and 200 and used these + notations on the right-hand side of a cast operator (`:`, `:>`, + `:>>`) (`#10963 <https://github.com/coq/coq/pull/10963>`_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). + +**Tactics** + +- **Added:** + Syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#9288 + <https://github.com/coq/coq/pull/9288>`_, by Hugo Herbelin). +- **Changed:** + Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. + It can also be extended by redefining the tactic ``zify_post_hook``. + (`#9856 <https://github.com/coq/coq/pull/9856>`_, fixes + `#8898 <https://github.com/coq/coq/issues/8898>`_, + `#7886 <https://github.com/coq/coq/issues/7886>`_, + `#9848 <https://github.com/coq/coq/issues/9848>`_ and + `#5155 <https://github.com/coq/coq/issues/5155>`_, by Frédéric Besson). +- **Changed:** + The goal selector tactical ``only`` now checks that the goal range + it is given is valid instead of ignoring goals out of the focus + range (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan + Gilbert). +- **Added:** + Flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (`#10765 <https://github.com/coq/coq/pull/10765>`_, by Frédéric Besson, + see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case). +- **Added:** + The :tacn:`zify` tactic is now aware of `Z.to_N`. + (`#10774 <https://github.com/coq/coq/pull/10774>`_, grants + `#9162 <https://github.com/coq/coq/issues/9162>`_, by Kazuhiko Sakaguchi). +- **Changed:** + The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + only run their tactic argument once, even if it has multiple + successes. This prevents blow-up and looping from using + multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 + <https://github.com/coq/coq/issues/10965>`_, by Jason Gross). +- **Fixed:** + The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + behave correctly when their tactic fully solves the goal. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 + <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). + +**Tactic language** + + .. _811Ltac2: + +- **Added:** + Ltac2, a new version of the tactic language Ltac, that doesn't + preserve backward compatibility, has been integrated in the main Coq + distribution. It is still experimental, but we already recommend + users of advanced Ltac to start using it and report bugs or request + enhancements. See its documentation in the :ref:`dedicated chapter + <ltac2>` (`#10002 <https://github.com/coq/coq/pull/10002>`_, plugin + authored by Pierre-Marie Pédrot, with contributions by various + users, integration by Maxime Dénès, help on integrating / improving + the documentation by Théo Zimmermann and Jim Fehrle). +- **Added:** + Ltac2 tactic notations with “constr” arguments can specify the + interpretation scope for these arguments; + see :ref:`ltac2_notations` for details + (`#10289 <https://github.com/coq/coq/pull/10289>`_, + by Vincent Laporte). +- **Changed:** + White spaces are forbidden in the :n:`&@ident` syntax for ltac2 references + that are described in :ref:`ltac2_built-in-quotations` + (`#10324 <https://github.com/coq/coq/pull/10324>`_, + fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, + authored by Pierre-Marie Pédrot). + +**SSReflect** + + .. _811SSRUnderOver: + +- **Added:** + Generalize tactics :tacn:`under` and :tacn:`over` for any registered + relation. More precisely, assume the given context lemma has type + `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The + first step performed by :tacn:`under` (since Coq 8.10) amounts to + calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which + itself relies on :tacn:`setoid_rewrite` if need be. So this step was + already compatible with a double implication or setoid equality for + the conclusion head symbol `R2`. But a further step consists in + tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from + unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)` + that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second + (convenience) step was only performed when `R1` was Leibniz' `eq` or + `iff`. Now, it is also performed for any relation `R1` which has a + ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance + being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` + goal by instantiating the hidden evar.) Also, it is now possible to + manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` + is a `PreOrder` relation or so, thanks to extra instances proving + that `Under_rel` preserves the properties of the `R1` relation. + These two features generalizing support for setoid-like relations is + enabled as soon as we do both ``Require Import ssreflect.`` and + ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been + added if one wants to "unprotect" the evar, and instantiate it + manually with another rule than reflexivity (i.e., without using the + :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section + :ref:`under_ssr` (`#10022 <https://github.com/coq/coq/pull/10022>`_, + by Erik Martin-Dorel, with suggestions and review by Enrico Tassi + and Cyril Cohen). +- **Added:** + A :g:`void` notation for the standard library empty type (:g:`Empty_set`) + (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de + Amorim). +- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun` + (`#11136 <https://github.com/coq/coq/pull/11136>`_, by Cyril Cohen). + +**Commands and options** + +- **Removed:** + Deprecated flag `Refine Instance Mode` + (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes + `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 + <https://github.com/coq/coq/issues/3890>`_ and `#4638 + <https://github.com/coq/coq/issues/4638>`_ + by Maxime Dénès, review by Gaëtan Gilbert). +- **Removed:** + Undocumented :n:`Instance : !@type` syntax + (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). +- **Removed:** + Deprecated ``Show Script`` command + (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). + + .. _811UnsafeFlags: + +- **Added:** + Unsafe commands to enable/disable guard checking, positivity checking + and universes checking (providing a local `-type-in-type`). + See :ref:`controlling-typing-flags` + (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). + + .. _811ExportBug: + +- **Fixed:** + Two bugs in :cmd:`Export`. This can have an impact on the behavior of the + :cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports + `C` was importing `C`, whereas :cmd:`Import` is not transitive. Also, after + `Import A B`, the import of `B` was sometimes incomplete + (`#10476 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès). + + .. warning:: + + This is a common source of incompatibilities in projects + migrating to Coq 8.11. + +- **Changed:** + Output generated by :flag:`Printing Dependent Evars Line` flag + used by the Prooftree tool in Proof General. + (`#10489 <https://github.com/coq/coq/pull/10489>`_, + closes `#4504 <https://github.com/coq/coq/issues/4504>`_, + `#10399 <https://github.com/coq/coq/issues/10399>`_ and + `#10400 <https://github.com/coq/coq/issues/10400>`_, + by Jim Fehrle). +- **Added:** + Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 <https://github.com/coq/coq/pull/10494>`_, + by Jim Fehrle). +- **Removed:** Legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath`` + which were undocumented, broken variants of :cmd:`Add LoadPath`, + :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath` + (`#11187 <https://github.com/coq/coq/pull/11187>`_, + by Maxime Dénès and Théo Zimmermann). + +**Tools** + + .. _811vos: + +- **Added:** + `coqc` now provides the ability to generate compiled interfaces. + Use `coqc -vos foo.v` to skip all opaque proofs during the + compilation of `foo.v`, and output a file called `foo.vos`. + This feature is experimental. It enables working on a Coq file without the need to + first compile the proofs contained in its dependencies + (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by + Maxime Dénès and Emilio Gallego). +- **Added:** + Command-line options `-require-import`, `-require-export`, + `-require-import-from` and `-require-export-from`, as well as their + shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate + confusing command line option `-require` + (`#10245 <https://github.com/coq/coq/pull/10245>`_ + by Hugo Herbelin, review by Emilio Gallego). +- **Changed:** + Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` + utility, where `<CoqMakefile>` is the name of the output file given by the + `-o` option. In this way two generated makefiles can coexist in the same + directory. + (`#10947 <https://github.com/coq/coq/pull/10947>`_, by Kazuhiko Sakaguchi). +- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with + no ending ``/`` character (`#11068 + <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert). + +**Standard library** + +- **Changed:** + Moved the :tacn:`auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 <https://github.com/coq/coq/pull/9772>`_, + by Vincent Laporte). +- **Removed:** + Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` + (`#9881 <https://github.com/coq/coq/pull/9811>`_, + by Vincent Laporte). + + .. _811Reals: + +- **Added:** + Module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers + (`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters). +- **Added:** + New module `Reals.ClassicalDedekindReals` defines Dedekind real + numbers as boolean-valued functions along with 3 logical axioms: + limited principle of omniscience, excluded middle of negations, and + functional extensionality. The exposed type :g:`R` in module + :g:`Reals.Rdefinitions` now corresponds to these Dedekind reals, + hidden behind an opaque module, which significantly reduces the + number of axioms needed (see `Reals.Rdefinitions` and + `Reals.Raxioms`), while preserving backward compatibility. + Classical Dedekind reals are a quotient of constructive reals, which + allows to transport many constructive proofs to the classical case + (`#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin). +- **Added:** + New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists + (`#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash). +- **Changed:** + The lemma :g:`filter_app` was moved to the :g:`List` module + (`#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash). +- **Added:** + Standard equivalence between weak excluded-middle and the + classical instance of De Morgan's law, in module :g:`ClassicalFacts` + (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). + +**Infrastructure and dependencies** + +- **Changed:** + Coq now officially supports OCaml 4.08. + See `INSTALL` file for details + (`#10471 <https://github.com/coq/coq/pull/10471>`_, + by Emilio Jesús Gallego Arias). + Version 8.10 ------------ @@ -568,7 +1074,7 @@ Other changes in 8.10+beta1 - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which don't use `-noinit` into files which do - (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilert). + (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilbert). - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an ordered type, using lexical order @@ -765,6 +1271,51 @@ A few bug fixes and documentation improvements, in particular: fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, by Helge Bahmann). +Changes in 8.10.2 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- Fixed a critical bug of template polymorphism and nonlinear universes + (`#11128 <https://github.com/coq/coq/pull/11128>`_, + fixes `#11039 <https://github.com/coq/coq/issues/11039>`_, + by Gaëtan Gilbert). + +- Fixed an anomaly “Uncaught exception Constr.DestKO” on :g:`Inductive` + (`#11052 <https://github.com/coq/coq/pull/11052>`_, + fixes `#11048 <https://github.com/coq/coq/issues/11048>`_, + by Gaëtan Gilbert). + +- Fixed an anomaly “not enough abstractions in fix body” + (`#11014 <https://github.com/coq/coq/pull/11014>`_, + fixes `#8459 <https://github.com/coq/coq/issues/8459>`_, + by Gaëtan Gilbert). + +**Notations** + +- Fixed an 8.10 regression related to the printing of coercions associated to notations + (`#11090 <https://github.com/coq/coq/pull/11090>`_, + fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). + +**CoqIDE** + +- Fixed uneven dimensions of CoqIDE panels when window has been resized + (`#11070 <https://github.com/coq/coq/pull/11070>`_, + fixes 8.10-regression `#10956 <https://github.com/coq/coq/issues/10956>`_, + by Guillaume Melquiond). + +- Do not include final stops in queries + (`#11069 <https://github.com/coq/coq/pull/11069>`_, + fixes 8.10-regression `#11058 <https://github.com/coq/coq/issues/11058>`_, + by Guillaume Melquiond). + +**Infrastructure and dependencies** + +- Enable building of executables when they are running + (`#11000 <https://github.com/coq/coq/pull/11000>`_, + fixes 8.9-regression `#10728 <https://github.com/coq/coq/issues/10728>`_, + by Gaëtan Gilbert). + Version 8.9 ----------- diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 62d4aa704f..81e50c0834 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2824,11 +2824,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as <-`. .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident @@ -3281,11 +3285,13 @@ the conversion in hypotheses :n:`{+ @ident}`. defined transparent constant or local definition (see :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of - the constant to which :n:`@qualid` refers in the current goal and - then replaces it with its :math:`\beta`:math:`\iota`-normal form. + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence + of the constant to which :n:`@qualid` refers in the current goal + and then replaces it with its :math:`\beta\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. - .. exn:: @qualid does not denote an evaluable constant. + .. exn:: Cannot coerce @qualid to an evaluable reference. This error is frequent when trying to unfold something that has defined as an inductive type (or constructor) and not as a @@ -4893,6 +4899,8 @@ Performance-oriented tactic variants .. tacv:: convert_concl_no_check @term :name: convert_concl_no_check + .. deprecated:: 8.11 + Deprecated old name for :tacn:`change_no_check`. Does not support any of its variants. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 21b5678a85..ac611926b3 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -642,5 +642,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq89.v theories/Compat/Coq810.v theories/Compat/Coq811.v + theories/Compat/Coq812.v </dd> </dl> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0c247e2660..c85f4f2cf7 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -721,15 +721,27 @@ let extern_possible_prim_token (custom,scopes) r = | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) -let extern_possible extern r = - try Some (extern r) with No_match -> None - -let extern_optimal extern r r' = - let c = extern_possible extern r in - let c' = if r==r' then None else extern_possible extern r' in - match c,c' with - | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n - | _ -> raise No_match +let filter_fully_applied r l = + let nargs = match DAst.get r with + | GApp (f,args) -> List.length args + | _ -> assert false in + List.filter (fun (keyrule,pat,n as _rule) -> n = Some nargs) l + +let extern_optimal extern extern_fully_applied r r' = + if r==r' then + (* No coercion: we look for a notation for r or a partial application of it *) + extern r + else + (* A coercion is removed: we prefer in order: + - a notation w/o a delimiter for the expression w/o coercions (or a partial application of it), if any + - a notation for the fully-applied expression with coercions, if any + - a notation with a delimiter for the expression w/o coercions (or a partial applied of it), if any *) + try + let c' = extern r' in + match c' with + | { CAst.v = CDelimiters _} -> (try extern_fully_applied r with No_match -> c') + | _ -> c' + with No_match -> extern_fully_applied r (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -798,13 +810,15 @@ let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token scopes) r r' + let extern_fun = extern_possible_prim_token scopes in + extern_optimal extern_fun extern_fun r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal (fun r -> extern_notation scopes vars r (uninterp_notations r)) + (fun r -> extern_notation scopes vars r (filter_fully_applied r (uninterp_notations r))) r r'' with No_match -> let loc = r'.CAst.loc in diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 06d2e1bb21..c91cb39fe2 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -253,10 +253,11 @@ let unbounded_from_below u cstrs = (starting from the most recent and ignoring let-definitions) is not contributing to the inductive type's sort or is Some u_k if its level is u_k and is contributing. *) -let template_polymorphic_univs ~template_check uctx paramsctxt concl = +let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = let check_level l = if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && - unbounded_from_below l (Univ.ContextSet.constraints uctx) then + unbounded_from_below l (Univ.ContextSet.constraints uctx) && + not (Univ.LSet.mem l ctor_levels) then Some l else None in @@ -302,10 +303,31 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in - let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + Array.fold_left + (fun levels (d,c) -> + let levels = + List.fold_left (fun levels d -> + Context.Rel.Declaration.fold_constr add_levels d levels) + levels d + in + add_levels c levels) + param_levels + splayed_lc + in + let param_levels, concl_levels = + template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + in if template_check && List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then - CErrors.anomaly ~label:"polymorphic_template_ind" + CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") else TemplateArity {template_param_levels = param_levels; template_level = min_univ} diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8da4e2885c..5c04e860a2 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -38,6 +38,7 @@ val typecheck_inductive : env -> mutual_inductive_entry -> of a template polymorphic inductive *) val template_polymorphic_univs : template_check:bool -> + ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f2cb9a8aec..b7bd4eef9a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -302,7 +302,7 @@ let unfold_ref_with_args infos tab fl v = type conv_tab = { cnv_inf : clos_infos; - relevances : Sorts.relevance list; + relevances : Sorts.relevance Range.t; lft_tab : clos_tab; rgt_tab : clos_tab; } @@ -313,16 +313,16 @@ type conv_tab = { passed to each respective side of the conversion function below. *) let push_relevance infos r = - { infos with relevances = r.Context.binder_relevance :: infos.relevances } + { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances } let push_relevances infos nas = - { infos with relevances = Array.fold_left (fun l x -> x.Context.binder_relevance :: l) infos.relevances nas } + { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas } let rec skip_pattern infos relevances n c1 c2 = if Int.equal n 0 then {infos with relevances}, c1, c2 else match kind c1, kind c2 with | Lambda (x, _, c1), Lambda (_, _, c2) -> - skip_pattern infos (x.Context.binder_relevance :: relevances) (pred n) c1 c2 + skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2 | _ -> raise IrregularPatternShape let skip_pattern infos n c1 c2 = @@ -705,7 +705,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let infos = create_clos_infos ~evars reds env in let infos = { cnv_inf = infos; - relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env); + relevances = Range.empty; lft_tab = create_tab (); rgt_tab = create_tab (); } in diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml index 5c15257511..6a1b36ea94 100644 --- a/kernel/retypeops.ml +++ b/kernel/retypeops.ml @@ -39,16 +39,10 @@ let relevance_of_projection env p = let mib = lookup_mind mind env in Declareops.relevance_of_projection_repr mib (Projection.repr p) -let rec relevance_of_rel_extra env extra n = - match extra with - | [] -> relevance_of_rel env n - | r :: _ when Int.equal n 1 -> r - | _ :: extra -> relevance_of_rel_extra env extra (n-1) - -let relevance_of_flex env extra lft = function +let relevance_of_flex env = function | ConstKey (c,_) -> relevance_of_constant env c | VarKey x -> relevance_of_var env x - | RelKey p -> relevance_of_rel_extra env extra (Esubst.reloc_rel p lft) + | RelKey p -> relevance_of_rel env p let rec relevance_of_fterm env extra lft f = let open CClosure in @@ -57,9 +51,9 @@ let rec relevance_of_fterm env extra lft f = | KnownI -> Sorts.Irrelevant | Unknown -> let r = match fterm_of f with - | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft) + | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1) | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c - | FFlex key -> relevance_of_flex env extra lft key + | FFlex key -> relevance_of_flex env key | FInt _ | FFloat _ -> Sorts.Relevant | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) | FConstruct (c,_) -> relevance_of_constructor env c @@ -69,12 +63,12 @@ let rec relevance_of_fterm env extra lft f = | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance | FCaseT (ci, _, _, _, _) -> ci.ci_relevance | FLambda (len, tys, bdy, e) -> - let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in + let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in let lft = Esubst.el_liftn len lft in let e = Esubst.subs_liftn len e in relevance_of_term_extra env extra lft e bdy | FLetIn (x, _, _, bdy, e) -> - relevance_of_term_extra env (x.binder_relevance :: extra) + relevance_of_term_extra env (Range.cons x.binder_relevance extra) (Esubst.el_lift lft) (Esubst.subs_lift e) bdy | FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f | FCLOS (c, e) -> relevance_of_term_extra env extra lft e c @@ -88,16 +82,18 @@ let rec relevance_of_fterm env extra lft f = and relevance_of_term_extra env extra lft subs c = match kind c with | Rel n -> - (match Esubst.expand_rel n subs with + begin match Esubst.expand_rel n subs with | Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f - | Inr (n, _) -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)) + | Inr (n, None) -> Range.get extra (Esubst.reloc_rel n lft - 1) + | Inr (_, Some p) -> relevance_of_rel env p + end | Var x -> relevance_of_var env x | Sort _ | Ind _ | Prod _ -> Sorts.Relevant (* types are always relevant *) | Cast (c, _, _) -> relevance_of_term_extra env extra lft subs c | Lambda ({binder_relevance=r;_}, _, bdy) -> - relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy | LetIn ({binder_relevance=r;_}, _, _, bdy) -> - relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy | App (c, _) -> relevance_of_term_extra env extra lft subs c | Const (c,_) -> relevance_of_constant env c | Construct (c,_) -> relevance_of_constructor env c @@ -115,5 +111,5 @@ let relevance_of_fterm env extra lft c = let relevance_of_term env c = if Environ.sprop_allowed env - then relevance_of_term_extra env [] Esubst.el_id (Esubst.subs_id 0) c + then relevance_of_term_extra env Range.empty Esubst.el_id (Esubst.subs_id 0) c else Sorts.Relevant diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli index f4497be44b..dd4513959f 100644 --- a/kernel/retypeops.mli +++ b/kernel/retypeops.mli @@ -14,14 +14,14 @@ val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance -val relevance_of_fterm : Environ.env -> Sorts.relevance list -> +val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t -> Esubst.lift -> CClosure.fconstr -> Sorts.relevance (** Helpers *) open Names -val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance +val relevance_of_rel : Environ.env -> int -> Sorts.relevance val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance diff --git a/lib/flags.ml b/lib/flags.ml index 83588779e5..27ca8e9596 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -62,7 +62,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_9 | V8_10 | Current +type compat_version = V8_9 | V8_10 | V8_11 | Current let compat_version = ref Current @@ -73,6 +73,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_10, V8_10 -> 0 | V8_10, _ -> -1 | _, V8_10 -> 1 + | V8_11, V8_11 -> 0 + | V8_11, _ -> -1 + | _, V8_11 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -81,6 +84,7 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_9 -> "8.9" | V8_10 -> "8.10" + | V8_11 -> "8.11" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index 5df07399c5..36a996401d 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,7 +52,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_9 | V8_10 | Current +type compat_version = V8_9 | V8_10 | V8_11 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index 3ad5bc9f2d..4a603f2c52 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Ring Omega Lia. +Require Import Bool PArith DecidableClass Ring Lia. Ltac bool := repeat match goal with @@ -359,8 +359,8 @@ intros k p var1 var2 Hvar Hv; revert var1 var2 Hvar. induction Hv; intros var1 var2 Hvar; simpl; [now auto|]. rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2). + erewrite (IHHv2 var1 var2); [ring|]. - intros; apply Hvar; zify; omega. - + intros; apply Hvar; zify; omega. + intros; apply Hvar; lia. + + intros; apply Hvar; lia. Qed. End Evaluation. @@ -424,7 +424,7 @@ match goal with apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => apply Pos.max_case_strong; intros; lia -| _ => zify; omega +| _ => lia end : core. Hint Resolve Pos.le_max_r Pos.le_max_l : core. @@ -472,8 +472,8 @@ intros k i p H; induction H; simpl poly_mul_mon; case_decide; intuition. - match goal with [ H : null ?p |- _ ] => solve[inversion H] end. + apply (valid_le_compat k); auto; constructor; intuition. - assert (X := poly_mul_mon_null_compat); intuition eauto. - - cutrewrite <- (Pos.max (Pos.succ i) i0 = i0); intuition. - - cutrewrite <- (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0); intuition. + - enough (Pos.max (Pos.succ i) i0 = i0) as <-; intuition. + - enough (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0) as <-; intuition. Qed. Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr -> @@ -488,7 +488,7 @@ induction Hl; intros kr pr Hr; simpl. { apply (valid_le_compat (Pos.max i kr)); auto. } { apply poly_add_valid_compat; auto. now apply poly_mul_mon_valid_compat; intuition. } - - repeat apply Pos.max_case_strong; zify; omega. + - repeat apply Pos.max_case_strong; lia. Qed. (* Compatibility of linearity wrt to linear operations *) @@ -497,7 +497,7 @@ Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr linear (Pos.max kl kr) (poly_add pl pr). Proof. intros kl kr pl pr Hl; revert kr pr; induction Hl; intros kr pr Hr; simpl. -+ apply (linear_le_compat kr); [|apply Pos.max_case_strong; zify; omega]. ++ apply (linear_le_compat kr); [|apply Pos.max_case_strong; lia]. now induction Hr; constructor; auto. + apply (linear_le_compat (Pos.max kr (Pos.succ i))); [|now auto]. induction Hr; simpl. @@ -527,17 +527,17 @@ inversion Hv; case_decide; subst. destruct (list_nth k var false); ring_simplify; [|now auto]. rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p3)). rewrite <- IHp2; auto; rewrite <- IHp1; [ring|]. - apply (valid_le_compat k); [now auto|zify; omega]. + apply (valid_le_compat k); [now auto|lia]. + remember (list_nth k var false) as b; destruct b; ring_simplify; [|now auto]. case_decide; simpl. - rewrite <- (IHp2 p2); [inversion H|now auto]; simpl. replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k). { rewrite <- Heqb; ring. } - { apply (valid_le_compat p2); [auto|zify; omega]. } + { apply (valid_le_compat p2); [auto|lia]. } - rewrite (IHp2 p2); [|now auto]. replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring). rewrite <- (IHp1 k); [rewrite <- Heqb; ring|]. - apply (valid_le_compat p2); [auto|zify; omega]. + apply (valid_le_compat p2); [auto|lia]. Qed. (* Reduction preserves evaluation by boolean assignations *) @@ -555,10 +555,10 @@ Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive -> reduce_aux l p = reduce_aux k p. Proof. intros k l p; revert k l; induction p; intros k l H Hle; simpl; auto. -inversion H; subst; repeat case_decide; subst; try (exfalso; zify; omega). -+ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|zify; omega]. +inversion H; subst; repeat case_decide; subst; try lia. ++ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|lia]. + f_equal; apply IHp1; auto. - now eapply valid_le_compat; [eauto|zify; omega]. + now eapply valid_le_compat; [eauto|lia]. Qed. (* Reduce projects valid polynomials into linear ones *) @@ -569,13 +569,13 @@ intros i p; revert i; induction p; intros i Hp; simpl. + constructor. + inversion Hp; subst; case_decide; subst. - rewrite <- (Pos.max_id i) at 1; apply poly_add_linear_compat. - { apply IHp1; eapply valid_le_compat; [eassumption|zify; omega]. } + { apply IHp1; eapply valid_le_compat; [eassumption|lia]. } { intuition. } - case_decide. - { apply IHp1; eapply valid_le_compat; [eauto|zify; omega]. } - { constructor; try (zify; omega); auto. - erewrite (reduce_aux_le_compat p2); [|assumption|zify; omega]. - apply IHp1; eapply valid_le_compat; [eauto|]; zify; omega. } + { apply IHp1; eapply valid_le_compat; [eauto|lia]. } + { constructor; try lia; auto. + erewrite (reduce_aux_le_compat p2); [|assumption|lia]. + apply IHp1; eapply valid_le_compat; [eauto|]; lia. } Qed. Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p). @@ -583,7 +583,7 @@ Proof. intros k p H; induction H; simpl. + now constructor. + case_decide. - - eapply linear_le_compat; [eauto|zify; omega]. + - eapply linear_le_compat; [eauto|lia]. - constructor; auto. apply linear_reduce_aux; auto. Qed. diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 98f5ab067a..867fe69550 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith Omega. +Require Import Bool DecidableClass Algebra Ring PArith Lia. Section Bool. @@ -80,7 +80,7 @@ Qed. Hint Extern 5 => change 0 with (min 0 0) : core. Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. Local Hint Constructors valid : core. -Hint Extern 5 => zify; omega : core. +Hint Extern 5 => lia : core. (* Compatibility with validity *) @@ -203,7 +203,7 @@ intros A n; induction n using Pos.peano_rect; intros i x def Hd; + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def). induction i using Pos.peano_case. - rewrite list_nth_base; reflexivity. - - rewrite list_nth_succ; apply IHn; zify; omega. + - rewrite list_nth_succ; apply IHn; lia. Qed. Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x. @@ -226,7 +226,7 @@ intros var; induction var; intros i j x Hd; simpl. - rewrite Pos.peano_rect_succ. induction i using Pos.peano_rect. { rewrite 2list_nth_base; reflexivity. } - { rewrite 2list_nth_succ; apply IHvar; zify; omega. } + { rewrite 2list_nth_succ; apply IHvar; lia. } Qed. Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x. @@ -251,10 +251,10 @@ intros k p Hl Hp; induction Hl; simpl. assert (Hrw : b = true); [|rewrite Hrw; reflexivity] end. erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto]. - now intros j Hd; apply list_replace_nth_1; zify; omega. + now intros j Hd; apply list_replace_nth_1; lia. rewrite list_replace_nth_2, xorb_false_r. erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto]. - now intros j Hd; apply list_replace_nth_1; zify; omega. + now intros j Hd; apply list_replace_nth_1; lia. Qed. (* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 2bc79d45d4..8946587a02 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -47,20 +47,6 @@ let ()= declare_int_option gdopt -let ()= - let congruence_depth=ref 100 in - let gdopt= - { optdepr=true; (* noop *) - optname="Congruence Depth"; - optkey=["Congruence";"Depth"]; - optread=(fun ()->Some !congruence_depth); - optwrite= - (function - None->congruence_depth:=0 - | Some i->congruence_depth:=(max i 0))} - in - declare_int_option gdopt - let default_intuition_tac = let tac _ _ = Auto.h_auto None [] None in let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index a9e5271e81..6c63a891e8 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -203,10 +203,6 @@ TACTIC EXTEND dependent_rewrite -> { rewriteInHyp b c id } END -(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to - "replace u with t" or "enough (t=u) as <-" and - "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) - TACTIC EXTEND cut_rewrite | [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5618fd7bc3..2998e1c767 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1944,12 +1944,7 @@ let default_morphism sign m = let evars, mor = resolve_one_typeclass env (goalevars evars) morph in mor, proper_projection env sigma mor morph -let warn_add_setoid_deprecated = - CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> - Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) - let add_setoid atts binders a aeq t n = - warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in @@ -1966,10 +1961,6 @@ let make_tactic name = let tacqid = Libnames.qualid_of_string name in TacArg (CAst.make @@ (TacCall (CAst.make (tacqid, [])))) -let warn_add_morphism_deprecated = - CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> - Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) - let add_morphism_as_parameter atts m n : unit = init_setoid (); let instance_id = add_suffix n "_Proper" in @@ -1986,7 +1977,6 @@ let add_morphism_as_parameter atts m n : unit = declare_projection n instance_id (GlobRef.ConstRef cst) let add_morphism_interactive atts m n : Lemmas.t = - warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in let env = Global.env () in diff --git a/plugins/micromega/ZifyComparison.v b/plugins/micromega/ZifyComparison.v index 8a8b40ded8..df75cf2c05 100644 --- a/plugins/micromega/ZifyComparison.v +++ b/plugins/micromega/ZifyComparison.v @@ -9,7 +9,8 @@ (************************************************************************) Require Import Bool ZArith. -Require Import ZifyClasses. +Require Import Zify ZifyClasses. +Require Import Lia. Local Open Scope Z_scope. (** [Z_of_comparison] is the injection function for comparison *) @@ -64,11 +65,11 @@ Proof. intros. destruct (x ?= y) eqn:C; simpl. - rewrite Z.compare_eq_iff in C. - intuition. + lia. - rewrite Z.compare_lt_iff in C. - intuition. + lia. - rewrite Z.compare_gt_iff in C. - intuition. + lia. Qed. Instance ZcompareSpec : BinOpSpec ZcompareZ := diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 58d01c125c..896ee303cc 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -31,6 +31,7 @@ Require Export Ncring_tac. Require Export Integral_domain. Require Import DiscrR. Require Import ZArith. +Require Import Lia. Declare ML Module "nsatz_plugin". @@ -413,7 +414,7 @@ Ltac nsatz_generic radicalmax info lparam lvar := try exact integral_domain_minus_one_zero || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation, one, one_notation, multiplication, mul_notation, zero, zero_notation; - discrR || omega]) + discrR || lia ]) || ((*simpl*) idtac) || idtac "could not prove discrimination result" ] ] @@ -502,7 +503,7 @@ reflexivity. exact Qplus_opp_r. Defined. Lemma Q_one_zero: not (Qeq 1%Q 0%Q). -unfold Qeq. simpl. auto with *. Qed. +Proof. unfold Qeq. simpl. lia. Qed. Instance Qcri: (Cring (Rr:=Qri)). red. exact Qmult_comm. Defined. @@ -513,8 +514,7 @@ exact Qmult_integral. exact Q_one_zero. Defined. (* Integers *) Lemma Z_one_zero: 1%Z <> 0%Z. -omega. -Qed. +Proof. lia. Qed. Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index a0901202f7..8a51bcea02 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -17,8 +17,7 @@ Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. Lemma Z_one_zero: 1%Z <> 0%Z. -omega. -Qed. +Proof. discriminate. Qed. Instance Zdi : (Integral_domain (Rcr:=Zcri)). constructor. diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 376410658a..475859fcc2 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -290,7 +290,7 @@ Require Import ssreflect ssrfun. r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. T or t -- boolean truth, as in andbT: right_id true andb. U -- predicate union, as in predU. - W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. **) + W -- weakening, as in in1W : (forall x, P) -> {in D, forall x, P}. **) Set Implicit Arguments. @@ -1184,7 +1184,6 @@ Notation xpreim := (fun f (p : pred _) x => p (f x)). (** The packed class interface for pred-like types. **) -#[universes(template)] Structure predType T := PredType {pred_sort :> Type; topred : pred_sort -> pred T}. diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e07fec6b43..f0e73bdb29 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -31,7 +31,6 @@ open Classops open Evarutil open Evarconv open Evd -open Termops open Globnames let get_use_typeclasses_for_conversion = @@ -151,7 +150,7 @@ let mu env evdref t = | None -> (None, v) in aux t -and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) +let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) : (EConstr.constr -> EConstr.constr) option = let open Context.Rel.Declaration in @@ -361,8 +360,8 @@ let app_coercion env evdref coercion v = let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in let coercion = coerce ?loc env evdref t c1 in - let t = Option.map (app_coercion env evdref coercion) v in - !evdref, t + let t = app_coercion env evdref coercion v in + !evdref, t let saturate_evd env evd = Typeclasses.resolve_typeclasses @@ -370,27 +369,25 @@ let saturate_evd env evd = (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = - try - let j,t,evd = - List.fold_left - (fun (ja,typ_cl,sigma) i -> - let isid = i.coe_is_identity in - let isproj = i.coe_is_projection in - let sigma, c = new_global sigma i.coe_value in - let typ = Retyping.get_type_of env sigma c in - let fv = make_judge c typ in - let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in - let sigma, jres = - apply_coercion_args env sigma true isproj argl fv - in - (if isid then - { uj_val = ja.uj_val; uj_type = jres.uj_type } - else - jres), - jres.uj_type,sigma) + let j,t,evd = + List.fold_left + (fun (ja,typ_cl,sigma) i -> + let isid = i.coe_is_identity in + let isproj = i.coe_is_projection in + let sigma, c = new_global sigma i.coe_value in + let typ = Retyping.get_type_of env sigma c in + let fv = make_judge c typ in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in + let sigma, jres = + apply_coercion_args env sigma true isproj argl fv + in + (if isid then + { uj_val = ja.uj_val; uj_type = jres.uj_type } + else + jres), + jres.uj_type,sigma) (hj,typ_cl,sigma) p - in evd, j - with NoCoercion as e -> raise e + in evd, j (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core ~program_mode env evd j = @@ -474,17 +471,15 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 = let evd, v', t' = try let t2,t1,p = lookup_path_between env evd (t,c1) in - match v with - | Some v -> - let evd,j = - apply_coercion env evd p - {uj_val = v; uj_type = t} t2 in - evd, Some j.uj_val, j.uj_type - | None -> evd, None, t + let evd,j = + apply_coercion env evd p + {uj_val = v; uj_type = t} t2 + in + evd, j.uj_val, j.uj_type with Not_found -> raise NoCoercion in - try (unify_leq_delay ~flags env evd t' c1, v') - with UnableToUnify _ -> raise NoCoercion + try (unify_leq_delay ~flags env evd t' c1, v') + with UnableToUnify _ -> raise NoCoercion let default_flags_of env = default_flags_of TransparentState.full @@ -512,25 +507,22 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = inh_conv_coerce_to_fail ?loc env1 evd rigidonly - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in - let v1 = Option.get v1 in - let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in - let t2 = match v2 with - | None -> subst_term evd' v1 t2 - | Some v2 -> Retyping.get_type_of env1 evd' v2 in + (mkRel 1) (lift 1 u1) (lift 1 t1) in + let v2 = beta_applist evd' (lift 1 v,[v1]) in + let t2 = Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') + (evd'', mkLambda (name, u1, v2')) | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if program_mode then - coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t + coerce_itf ?loc env evd cj.uj_val cj.uj_type t else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> @@ -541,21 +533,13 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd if evd' == evd then error_actual_type ?loc env best_failed_evd cj t e else - inh_conv_coerce_to_fail ?loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> error_actual_type ?loc env best_failed_evd cj t e in - let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = val'; uj_type = t }) + (evd',{ uj_val = val'; uj_type = t }) let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env evd - -let inh_conv_coerces_to ?loc env evd ?(flags=default_flags_of env) t t' = - try - fst (inh_conv_coerce_to_fail ?loc env evd ~flags true None t t') - with NoCoercion -> - evd (* Maybe not enough information to unify *) - diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 3b24bcec8b..fe93a26f4f 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -54,13 +54,6 @@ val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> unsafe_judgment -> types -> evar_map * unsafe_judgment -(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] - is coercible to an object of type [t'] adding evar constraints if needed; - it fails if no coercion exists *) -val inh_conv_coerces_to : ?loc:Loc.t -> - env -> evar_map -> ?flags:Evarconv.unify_flags -> - types -> types -> evar_map - (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; raises [Not_found] if no coercion found *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f089b242a2..d2af957b54 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -264,16 +264,19 @@ let relevance_of_term env sigma c = if Environ.sprop_allowed env then let rec aux rels c = match kind sigma c with - | Rel n -> Retypeops.relevance_of_rel_extra env rels n + | Rel n -> + let len = Range.length rels in + if n <= len then Range.get rels (n - 1) + else Retypeops.relevance_of_rel env (n - len) | Var x -> Retypeops.relevance_of_var env x | Sort _ -> Sorts.Relevant | Cast (c, _, _) -> aux rels c | Prod ({binder_relevance=r}, _, codom) -> - aux (r::rels) codom + aux (Range.cons r rels) codom | Lambda ({binder_relevance=r}, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | LetIn ({binder_relevance=r}, _, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | App (c, _) -> aux rels c | Const (c,_) -> Retypeops.relevance_of_constant env c | Ind _ -> Sorts.Relevant @@ -287,7 +290,7 @@ let relevance_of_term env sigma c = | Meta _ | Evar _ -> Sorts.Relevant in - aux [] c + aux Range.empty c else Sorts.Relevant let relevance_of_type env sigma t = diff --git a/tactics/equality.ml b/tactics/equality.ml index fc37d5a254..96b61b6994 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1648,7 +1648,14 @@ let cutSubstClause l2r eqn cls = | None -> cutSubstInConcl l2r eqn | Some id -> cutSubstInHyp l2r eqn id -let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls) +let warn_deprecated_cutrewrite = + CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated" + (fun () -> strbrk"\"cutrewrite\" is deprecated. See documentation for proposed replacement.") + +let cutRewriteClause l2r eqn cls = + warn_deprecated_cutrewrite (); + try_rewrite (cutSubstClause l2r eqn cls) + let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None diff --git a/test-suite/Makefile b/test-suite/Makefile index 1744138d29..609a61226b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -543,13 +543,15 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) res=`echo "$$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`; \ true "find expected time * 100"; \ exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \ + true "compute corrected effective time, rounded up"; \ + rescorrected=`expr \( $$res \* $(bogomips) \+ 6120 \- 1 \) \/ 6120`; \ ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \ if [ "$$ok" = 1 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " $<...Error! (should run faster)"; \ + echo " $<...Error! (should run faster ($$rescorrected >= $$exp))"; \ $(FAIL); \ fi; \ fi; \ diff --git a/test-suite/bugs/closed/bug_10504.v b/test-suite/bugs/closed/bug_10504.v new file mode 100644 index 0000000000..6e66a6a90a --- /dev/null +++ b/test-suite/bugs/closed/bug_10504.v @@ -0,0 +1,14 @@ +Inductive any_list {A} := +| nil : @any_list A +| cons : forall X, A -> @any_list X -> @any_list A. + +Arguments nil {A}. +Arguments cons {A X}. + +Notation "[]" := (@nil Type). +Notation "hd :: tl" := (cons hd tl). + +Definition xs := true :: 2137 :: false :: 0 :: []. +Fail Definition ys := xs :: xs. + +(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *) diff --git a/test-suite/bugs/closed/bug_11039.v b/test-suite/bugs/closed/bug_11039.v new file mode 100644 index 0000000000..f02a3ef177 --- /dev/null +++ b/test-suite/bugs/closed/bug_11039.v @@ -0,0 +1,26 @@ +(* this bug was a proof of False *) + +(* when we require template poly Coq recognizes that it's not allowed *) +Fail #[universes(template)] + Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A. + +(* variants with letin *) +Fail #[universes(template)] + Inductive foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A. + +Fail #[universes(template)] + Record foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }. + + +(* no implicit template poly, no explicit universe annotations *) +Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty. +Arguments nonempty {_}. + +Fail Check foo nat : Type@{foo.u0}. +(* template poly didn't activate *) + +Definition U := Type. +Definition A : U := foo nat. + +Fail Definition down : U -> A := fun u => bar nat u nonempty. +(* this is the one where it's important that it fails *) diff --git a/test-suite/bugs/closed/bug_11161.v b/test-suite/bugs/closed/bug_11161.v new file mode 100644 index 0000000000..22a075e096 --- /dev/null +++ b/test-suite/bugs/closed/bug_11161.v @@ -0,0 +1,10 @@ +(* Ensure that evars are properly normalized in the instance path. + Problems with this can cause eg #11161. *) + +Class Foo (n:nat) := {x : bool}. + +Instance bar n : Foo n. Admitted. + +Instance bar' n : Foo n. split. abstract exact true. Qed. + +Instance bar'' n : Foo n. split. abstract exact true. Defined. diff --git a/test-suite/bugs/closed/bug_2083.v b/test-suite/bugs/closed/bug_2083.v index f33e96cea6..40fda71e66 100644 --- a/test-suite/bugs/closed/bug_2083.v +++ b/test-suite/bugs/closed/bug_2083.v @@ -13,15 +13,15 @@ Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) error end. -Require Import Omega. +Require Import Lia. -Solve Obligations with program_simpl ; auto with *; try omega. +Solve Obligations with program_simpl ; auto with *; lia. Next Obligation. - apply H. simpl. omega. + apply H. simpl. lia. Defined. Next Obligation. - case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. + case (le_lt_dec p i) ; intros. assert(i = p) by lia. subst. revert H0. clear_subset_proofs. auto. apply H. simpl. assumption. Defined. diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v index 915cfcac27..b21a4d939c 100644 --- a/test-suite/bugs/closed/bug_3652.v +++ b/test-suite/bugs/closed/bug_3652.v @@ -1,6 +1,7 @@ Require Setoid. Require ZArith. Import ZArith. +Require Import Lia. Inductive Erasable(A : Set) : Prop := erasable: A -> Erasable A. @@ -87,12 +88,12 @@ Proof. unfold zotval. unfold mp2a1s. ring_simplify'. - replace 2 with (2*1) at 2 7 by omega. + replace 2 with (2*1) at 2 7 by lia. rewrite <-?Z.mul_assoc. rewrite <-?Z.mul_add_distr_l. rewrite <-Z.mul_sub_distr_l. - rewrite Z.mul_cancel_l by omega. - replace 1 with (2-1) at 1 by omega. + rewrite Z.mul_cancel_l by lia. + replace 1 with (2-1) at 1 by lia. rewrite Z.add_sub_assoc. rewrite Z.sub_cancel_r. Unshelve. diff --git a/test-suite/bugs/closed/bug_4280.v b/test-suite/bugs/closed/bug_4280.v index fd7897509e..31524e5dcf 100644 --- a/test-suite/bugs/closed/bug_4280.v +++ b/test-suite/bugs/closed/bug_4280.v @@ -1,11 +1,11 @@ -Require Import ZArith. +Require Import ZArith Lia. Require Import Eqdep_dec. Local Open Scope Z_scope. Definition t := { n: Z | n > 1 }. Program Definition two : t := 2. -Next Obligation. omega. Qed. +Next Obligation. lia. Qed. Program Definition t_eq (x y: t) : {x=y} + {x<>y} := if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _. diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v index f1bce04451..1ad84f9bb5 100644 --- a/test-suite/bugs/closed/bug_4306.v +++ b/test-suite/bugs/closed/bug_4306.v @@ -1,7 +1,7 @@ Require Import List. Require Import Arith. Require Import Recdef. -Require Import Omega. +Require Import Lia. Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := match xys with @@ -14,9 +14,7 @@ Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) end end. Proof. - intros; simpl; omega. - intros; simpl; omega. - intros; simpl; omega. + all: simpl; lia. Qed. Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v index 7685552725..0c26d4de32 100644 --- a/test-suite/bugs/closed/bug_4456.v +++ b/test-suite/bugs/closed/bug_4456.v @@ -10,7 +10,7 @@ Tactic Notation "admit" := case proof_admitted. Require Coq.Program.Program. Require Coq.Strings.String. -Require Coq.omega.Omega. +Require Coq.micromega.Lia. Module Export Fiat_DOT_Common. Module Export Fiat. Module Common. @@ -489,7 +489,8 @@ Defined. End app. Import Coq.Lists.List. -Import Coq.omega.Omega. +Import Coq.Arith.Arith. +Import Coq.micromega.Lia. Import Fiat_DOT_Common.Fiat.Common. Import Fiat.Parsers.ContextFreeGrammar.Valid. Local Open Scope string_like_scope. @@ -585,8 +586,8 @@ Defined. | _ => discriminate | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) | _ => solve [ eauto with nocore ] - | _ => solve [ apply Min.min_case_strong; omega ] - | _ => omega + | _ => solve [ apply Min.min_case_strong; lia ] + | _ => lia | [ H : production_valid (_::_) |- _ ] => let H' := fresh in pose proof H as H'; diff --git a/test-suite/bugs/closed/bug_4852.v b/test-suite/bugs/closed/bug_4852.v index e2e00f05d3..cdc8cd8b20 100644 --- a/test-suite/bugs/closed/bug_4852.v +++ b/test-suite/bugs/closed/bug_4852.v @@ -2,7 +2,7 @@ Require Import Coq.Lists.List. Import ListNotations. -Require Import Omega. +Require Import Lia. Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf. @@ -16,7 +16,7 @@ Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) := Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws. -Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega. +Ltac solve_nat := autorewrite with app_rws in *; cbn in *; lia. Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'"). diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 27cb731151..89410047b2 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -1,7 +1,7 @@ Require Import Relations. Require Import FSets. Require Import Arith. -Require Import Omega. +Require Import Lia. Set Keyed Unification. @@ -147,14 +147,14 @@ Module MessageSpi. Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z). unfold lt. induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros. - omega. + lia. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). unfold eq;unfold lt. induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate H0);injection H0;intros. - elim (lt_irrefl n);try omega. + elim (lt_irrefl n); lia. Qed. Definition compare : forall (x y:t),(Compare lt eq x y). diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v new file mode 100644 index 0000000000..2101535be7 --- /dev/null +++ b/test-suite/complexity/pattern.v @@ -0,0 +1,38 @@ +(** Testing the performance of [pattern]. For not regressing on COQBUG(https://github.com/coq/coq/issues/11150) and COQBUG(https://github.com/coq/coq/issues/6502) *) +(* Expected time < 1.65s *) +(* reference: 0.673s after adjustment *) +Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v +:= let x := v in f x. + +Fixpoint big (a : nat) (sz : nat) : nat + := match sz with + | O => a + | S sz' => Let_In (a * a) (fun a' => big a' sz') + end. + +Ltac do_time n := + try ( + once (assert (exists e, e = big 1 n); + [ lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big]; + time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat)) + | ]); + fail). + +Ltac do_time_to n := + lazymatch (eval vm_compute in n) with + | O => idtac + | ?n' => do_time_to (Nat.div2 n'); idtac n'; do_time n' + end. + +Local Set Warnings "-abstract-large-number". + +(* Don't spend lots of time printing *) +Notation hide := (_ = _). + +Goal True. +Proof. + (* do_time_to 16384. *) (* should be linear, not quadratic *) + assert (exists e, e = big 1 16384). + lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big]. + Timeout 15 Time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat)). +Abort. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index be33104918..4c0ee1b5bd 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -35,8 +35,8 @@ Module Pair (X: PO) (Y: PO) <: PO. destruct p2. unfold le. intuition. - cutrewrite (t = t1). - cutrewrite (t0 = t2). + enough (t = t1) as ->. + enough (t0 = t2) as ->. reflexivity. info auto. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 6704337f80..f889da4e98 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,7 +1,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch +Arguments Nat.sub (_ _)%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub @@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub !_%nat_scope !_%nat_scope / +Arguments Nat.sub (!_ !_)%nat_scope / The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent @@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub !_%nat_scope !_%nat_scope +Arguments Nat.sub (!_ !_)%nat_scope The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor Nat.sub is transparent @@ -43,14 +43,14 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never +Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic -Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / +Arguments fcomp {A B C}%type_scope _ _ _ / The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp @@ -78,7 +78,7 @@ Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent @@ -86,7 +86,7 @@ Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 53d5624f6f..5093e785de 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,21 +13,21 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A%type_scope} -Arguments eq_refl {B%type_scope} {y}, [B] _ +Arguments eq {A}%type_scope +Arguments eq_refl {B}%type_scope {y}, [B] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments eq_refl {B%type_scope} {y}, [B] _ +Arguments eq_refl {B}%type_scope {y}, [B] _ Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope -Arguments myrefl {C%type_scope} x : rename +Arguments myrefl {C}%type_scope x : rename myrefl : forall (B : Type) (x : A), B -> myEq B x x myrefl is not universe polymorphic -Arguments myrefl {C%type_scope} x : rename +Arguments myrefl {C}%type_scope x : rename Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -37,11 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -51,12 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x -Arguments myEq _%type_scope _%type_scope -Arguments myrefl A%type_scope {C%type_scope} x : rename +Arguments myEq (_ _)%type_scope +Arguments myrefl A%type_scope {C}%type_scope x : rename myrefl : forall (A B : Type) (x : A), B -> myEq A B x x myrefl is not universe polymorphic -Arguments myrefl A%type_scope {C%type_scope} x : rename +Arguments myrefl A%type_scope {C}%type_scope x : rename Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -68,11 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 7489b8987e..e84ac85aa8 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Arguments t_rect _%function_scope _%function_scope +Arguments t_rect (_ _)%function_scope = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Arguments proj _%nat_scope _%nat_scope _%function_scope +Arguments proj (_ _)%nat_scope _%function_scope foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..398528de72 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -16,7 +16,7 @@ Check end in f 0. -Require Import ZArith_base Omega. +Require Import ZArith_base Lia. Open Scope Z_scope. Inductive even: Z -> Prop := @@ -35,13 +35,13 @@ Proof. fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). intros. destruct H. - omega. + lia. apply odd_pos_even_pos in H. - omega. + lia. intros. destruct H. apply even_pos_odd_pos in H. - omega. + lia. Qed. CoInductive Inf := S { projS : Inf }. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index d65d2a8f55..5f22eb5d7c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x%nat_scope] [x0%nat_scope] +Arguments d2 [x x0]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index ce058a6d34..da255e86cd 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,8 +1,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} -Arguments sig2 [A%type_scope] _%type_scope _%type_scope -Arguments exist2 [A%type_scope] _%function_scope _%function_scope +Arguments sig2 [A]%type_scope (_ _)%type_scope +Arguments exist2 [A]%type_scope (_ _)%function_scope exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index ba4ac5a8f9..32120a9674 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -59,3 +59,5 @@ where |- Type] (pat, p0, p cannot be used) fun '{| |} => true : R -> bool +b = a + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4b9d0abd95..d3433949d1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -140,3 +140,17 @@ Record R := { n : nat }. Check fun '{|n:=x|} => true. End EmptyRecordSyntax. + +Module L. + +(* Testing regression #11053 *) + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. +End Test. + +End L. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 2952b6d94b..4f09f00c56 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,7 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments swap {A%type_scope} {B%type_scope} +Arguments swap {A B}%type_scope fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 7d0d81a3e8..71d162c314 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,24 +1,24 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Arguments existT [A%type_scope] _%function_scope +Arguments existT [A]%type_scope _%function_scope Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} -Arguments sigT [A%type_scope] _%type_scope -Arguments existT [A%type_scope] _%function_scope +Arguments sigT [A]%type_scope _%type_scope +Arguments existT [A]%type_scope _%function_scope existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A%type_scope} -Arguments eq_refl {A%type_scope} {x}, [A] _ +Arguments eq {A}%type_scope +Arguments eq_refl {A}%type_scope {x}, [A] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments eq_refl {A%type_scope} {x}, [A] _ +Arguments eq_refl {A}%type_scope {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall (A : Type) (x : A), x = x @@ -34,11 +34,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Arguments Nat.add _%nat_scope _%nat_scope +Arguments Nat.add (_ _)%nat_scope Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic -Arguments Nat.add _%nat_scope _%nat_scope +Arguments Nat.add (_ _)%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add Nat.add : nat -> nat -> nat @@ -52,9 +52,9 @@ Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m -Arguments le _%nat_scope _%nat_scope +Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope -Arguments le_S {n%nat_scope} [m%nat_scope] +Arguments le_S {n}%nat_scope [m]%nat_scope comparison : Set comparison is not universe polymorphic @@ -80,8 +80,8 @@ Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A%type_scope} -Arguments eq_refl {A%type_scope} {x}, {A} _ +Arguments eq {A}%type_scope +Arguments eq_refl {A}%type_scope {x}, {A} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 298a0789c4..525ca48bee 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -33,7 +33,7 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -Arguments wrap {A%type_scope} {Wrap} +Arguments wrap {A}%type_scope {Wrap} bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index fd6101bf89..c86548440b 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq811. +Import Coq.Compat.Coq812. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index f774cef44f..a1c1209db6 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..dd259988ac --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 1c5ccc1a92..00f4747e3e 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v index 22fb09526d..d944036112 100644 --- a/test-suite/success/LocalDefinition.v +++ b/test-suite/success/LocalDefinition.v @@ -26,28 +26,12 @@ Module TestAdmittedVisibility. Fail Check d2. End TestAdmittedVisibility. -(* Test consistent behavior of Local Definition wrt automatic declaration of instances *) - Module TestVariableAsInstances. - Module Test1. - Set Typeclasses Axioms Are Instances. - Class U. - Local Parameter b : U. - Definition testU := _ : U. (* _ resolved *) - - Class T. - Variable a : T. (* warned to be the same as "Local Parameter" *) - Definition testT := _ : T. (* _ resolved *) - End Test1. - - Module Test2. - Unset Typeclasses Axioms Are Instances. - Class U. - Local Parameter b : U. - Fail Definition testU := _ : U. (* _ unresolved *) + Class U. + Local Parameter b : U. + Fail Definition testU := _ : U. (* _ unresolved *) - Class T. - Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) - Fail Definition testT := _ : T. (* used to succeed *) - End Test2. + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) + Fail Definition testT := _ : T. (* used to succeed *) End TestVariableAsInstances. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 736d05fefc..3f96bf2c35 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -241,13 +241,8 @@ Module IterativeDeepening. End IterativeDeepening. -Module AxiomsAreInstances. - Set Typeclasses Axioms Are Instances. - Class TestClass1 := {}. - Axiom testax1 : TestClass1. - Definition testdef1 : TestClass1 := _. +Module AxiomsAreNotInstances. - Unset Typeclasses Axioms Are Instances. Class TestClass2 := {}. Axiom testax2 : TestClass2. Fail Definition testdef2 : TestClass2 := _. @@ -256,4 +251,4 @@ Module AxiomsAreInstances. Existing Instance testax2. Definition testdef2 : TestClass2 := _. -End AxiomsAreInstances. +End AxiomsAreNotInstances. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq811.v b/theories/Compat/Coq811.v index 4a9a041d4e..4d28e4f708 100644 --- a/theories/Compat/Coq811.v +++ b/theories/Compat/Coq811.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.11 *) + +Require Export Coq.Compat.Coq812. diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v new file mode 100644 index 0000000000..5d2fbc56d5 --- /dev/null +++ b/theories/Compat/Coq812.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.12 *) diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index e777f10411..303acf7ae2 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -17,7 +17,7 @@ [mem x s=true] instead of [In x s], [equal s s'=true] instead of [Equal s s'], etc. *) -Require Import MSetProperties Zerob Sumbool Omega DecidableTypeEx. +Require Import MSetProperties Zerob Sumbool Lia DecidableTypeEx. Module WEqPropertiesOn (Import E:DecidableType)(M:WSetsOn E). Module Import MP := WPropertiesOn E M. @@ -845,19 +845,19 @@ unfold sum. intros f g Hf Hg. assert (fc : compat_opL (fun x:elt =>plus (f x))) by (repeat red; intros; rewrite Hf; auto). -assert (ft : transposeL (fun x:elt =>plus (f x))) by (red; intros; omega). +assert (ft : transposeL (fun x:elt =>plus (f x))) by (red; intros; lia). assert (gc : compat_opL (fun x:elt => plus (g x))) by (repeat red; intros; rewrite Hg; auto). -assert (gt : transposeL (fun x:elt =>plus (g x))) by (red; intros; omega). +assert (gt : transposeL (fun x:elt =>plus (g x))) by (red; intros; lia). assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))) by (repeat red; intros; rewrite Hf,Hg; auto). -assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))) by (red; intros; omega). +assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))) by (red; intros; lia). intros s;pattern s; apply set_rec. intros. rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto. -intros. do 3 (rewrite fold_add; auto with *). +intros. do 3 (rewrite fold_add; auto with fset). lia. do 3 rewrite fold_empty;auto. Qed. @@ -869,7 +869,7 @@ assert (st : Equivalence (@Logic.eq nat)) by (split; congruence). assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))) by (repeat red; intros; rewrite Hf; auto). assert (ct : transposeL (fun x => plus (if f x then 1 else 0))) by - (red; intros; omega). + (red; intros; lia). intros s;pattern s; apply set_rec. intros. change elt with E.t. @@ -919,7 +919,7 @@ Lemma sum_compat : forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s. intros. unfold sum; apply (@fold_compat _ (@Logic.eq nat)); - repeat red; auto with *. + repeat red; auto with *; lia. Qed. End Sum. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index b09a7d3264..c5165662e5 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -257,7 +257,6 @@ Ltac blocked t := block_goal ; t ; unblock_goal. be used by the [equations] resolver. It is especially useful to register the dependent elimination principles for things in [Prop] which are not automatically generated. *) -#[universes(template)] Class DependentEliminationPackage (A : Type) := { elim_type : Type ; elim : elim_type }. diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 8e8f05dabc..4feeb9bfff 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega. +Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Lia. Set Implicit Arguments. @@ -85,7 +85,7 @@ Section Perm. rewrite multiplicity_NoDup in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_In. - destruct 3; omega. + destruct 3; lia. Qed. (** Permutation is compatible with In. *) diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 90c82b677b..234063f14f 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Omega Relations Multiset SetoidList. +Require Import Lia Relations Multiset SetoidList. (** This file is deprecated, use [Permutation.v] instead. @@ -189,7 +189,7 @@ Lemma permut_conv_inv : forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2. Proof. intros e l1 l2; unfold permutation, meq; simpl; intros H a; - generalize (H a); apply plus_reg_l. + generalize (H a); lia. Qed. Lemma permut_app_inv1 : @@ -199,9 +199,7 @@ Proof. intros H a; generalize (H a); clear H. do 2 rewrite list_contents_app. simpl. - intros; apply plus_reg_l with (multiplicity (list_contents l) a). - rewrite plus_comm; rewrite H; rewrite plus_comm. - trivial. + lia. Qed. (** we can use [multiplicity] to define [InA] and [NoDupA]. *) @@ -220,8 +218,7 @@ Proof. intros H a; generalize (H a); clear H. do 2 rewrite list_contents_app. simpl. - intros; apply plus_reg_l with (multiplicity (list_contents l) a). - trivial. + lia. Qed. Lemma permut_remove_hd_eq : @@ -230,13 +227,9 @@ Lemma permut_remove_hd_eq : Proof. unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0. specialize H with a0. - rewrite list_contents_app in *; simpl in *. - apply plus_reg_l with (if eqA_dec a a0 then 1 else 0). - rewrite H; clear H. - symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal. - rewrite plus_comm. - destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha; - decide (eqA_dec b a0) with Ha; reflexivity. + rewrite list_contents_app in *. simpl in *. + destruct (eqA_dec a _) as [Ha|Ha]; rewrite Heq in Ha; revert H; + decide (eqA_dec b a0) with Ha; lia. Qed. Lemma permut_remove_hd : @@ -342,9 +335,9 @@ Proof. rewrite multiplicity_InA. specialize (H a). rewrite if_eqA_refl in H. - clear IHl; omega. + clear IHl; lia. rewrite IHl; intros. - specialize (H a0). omega. + specialize (H a0). lia. Qed. (** Permutation is compatible with InA. *) @@ -395,14 +388,14 @@ Proof. apply permut_length_1. red; red; intros. specialize (P a). simpl in *. - rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega. + rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. lia. right. inversion_clear H0; [|inversion H]. split; auto. apply permut_length_1. red; red; intros. specialize (P a); simpl in *. - rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega. + rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. lia. Qed. (** Permutation is compatible with length. *) @@ -434,7 +427,7 @@ Proof. rewrite multiplicity_NoDupA in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_InA. - destruct 3; omega. + destruct 3; lia. Qed. End Permut. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index f8f046ae75..3e8cafc417 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -34,7 +34,7 @@ let rec print_prefix_list sep = function let usage_coq_makefile () = output_string stderr "Usage summary:\ \n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\ncoq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\ \n ... [any] ... [-extra[-phony] result dependencies command]\ \n ... [-I dir] ... [-R physicalpath logicalpath]\ \n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ @@ -45,7 +45,7 @@ let usage_coq_makefile () = \nFull list of options:\ \n\ \n[file.v]: Coq file to be compiled\ -\n[file.ml[i4]?]: Objective Caml file to be compiled\ +\n[file.ml[ig]?]: Objective Caml file to be compiled\ \n[file.ml{lib,pack}]: ocamlbuild-style file that describes a Objective Caml\ \n library/module\ \n[any] : subdirectory that should be \"made\" and has a Makefile itself\ diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 717c06a868..ae1e1c6ed3 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -30,7 +30,7 @@ let build_table l = let is_keyword = build_table - [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint"; + [ "About"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "From"; "Function"; "Generalizable"; "Global"; "Grammar"; "Guarded"; "Goal"; "Hint"; "Debug"; "On"; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 8dd1c45024..e3116550d9 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -178,7 +178,8 @@ let add_compat_require opts v = match v with | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) + | Flags.V8_11 -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) + | Flags.Current -> add_vo_require opts "Coq.Compat.Coq812" None (Some false) let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 737e0427ec..15077298aa 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -60,7 +60,7 @@ let warn_arguments_assert = (* [nargs_for_red] is the number of arguments required to trigger reduction, [args] is the main list of arguments statuses, [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = +let vernac_arguments ~section_local reference args more_implicits flags = let env = Global.env () in let sigma = Evd.from_env env in let assert_flag = List.mem `Assert flags in @@ -83,6 +83,23 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red if clear_implicits_flag && default_implicits_flag then err_incompat "clear implicits" "default implicits"; + let args, nargs_for_red, nargs_before_bidi, _i = + List.fold_left (fun (args,red,bidi,i) arg -> + match arg with + | RealArg arg -> (arg::args,red,bidi,i+1) + | VolatileArg -> + if Option.has_some red + then CErrors.user_err Pp.(str "The \"/\" modifier may only occur once."); + (args,Some i,bidi,i) + | BidiArg -> + if Option.has_some bidi + then CErrors.user_err Pp.(str "The \"&\" modifier may only occur once."); + (args,red,Some i,i)) + ([],None,None,0) + args + in + let args = List.rev args in + let sr = smart_global reference in let inf_names = let ty, _ = Typeops.type_of_global_in_context env sr in diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index f78e01a11f..71effddf67 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -13,7 +13,5 @@ val vernac_arguments -> Libnames.qualid Constrexpr.or_by_notation -> Vernacexpr.vernac_argument_status list -> (Names.Name.t * Impargs.implicit_kind) list list - -> int option - -> int option -> Vernacexpr.arguments_modifier list -> unit diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e5db6146ca..a001420f74 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -22,24 +22,6 @@ open Entries module RelDecl = Context.Rel.Declaration (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let axiom_into_instance = ref false - -let () = - let open Goptions in - declare_bool_option - { optdepr = true; - optname = "automatically declare axioms whose type is a typeclass as instances"; - optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; - optread = (fun _ -> !axiom_into_instance); - optwrite = (:=) axiom_into_instance; } - -let should_axiom_into_instance = let open Decls in function - | Context -> - (* The typeclass behaviour of Variable and Context doesn't depend - on section status *) - true - | Definitional | Logical | Conjectural -> !axiom_into_instance - let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in let decl = Declare.SectionLocalAssum {typ; impl} in @@ -58,7 +40,12 @@ let instance_of_univ_entry = function | Monomorphic_entry _ -> Univ.Instance.empty let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = - let do_instance = should_axiom_into_instance kind in + let do_instance = let open Decls in match kind with + | Context -> true + (* The typeclass behaviour of Variable and Context doesn't depend + on section status *) + | Definitional | Logical | Conjectural -> false + in let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 80fcb7bc45..2aee9bd47f 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -323,7 +323,7 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate env uctx params concl = +let template_polymorphism_candidate env ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in @@ -331,7 +331,9 @@ let template_polymorphism_candidate env uctx params concl = else let template_check = Environ.check_template env in let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in + let params, conclunivs = + IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu + in not (template_check && Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -376,14 +378,24 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> let template_candidate () = - templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in + templatearity || + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty ctx_params + in + List.fold_left (fun levels c -> add_levels c levels) + param_levels ctypes + in + template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl + in let template = match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "Inductive " ++ Id.print indname ++ - str" cannot be made template polymorphic."); template | None -> should_auto_template indname (template_candidate ()) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 45e539b1e4..ef05b213d8 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -77,12 +77,18 @@ val should_auto_template : Id.t -> bool -> bool automatically use template polymorphism. [x] is the name of the inductive under consideration. *) -val template_polymorphism_candidate : - Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env uctx params conclsort] is - [true] iff an inductive with params [params] and conclusion - [conclsort] would be definable as template polymorphic. It should - have at least one universe in its monomorphic universe context that - can be made parametric in its conclusion sort, if one is given. - If the [Template Check] flag is false we just check that the conclusion sort - is not small. *) +val template_polymorphism_candidate + : Environ.env + -> ctor_levels:Univ.LSet.t + -> Entries.universes_entry + -> Constr.rel_context + -> Sorts.t option + -> bool +(** [template_polymorphism_candidate env ~ctor_levels uctx params + conclsort] is [true] iff an inductive with params [params], + conclusion [conclsort] and universe levels appearing in the + constructor arguments [ctor_levels] would be definable as template + polymorphic. It should have at least one universe in its + monomorphic universe context that can be made parametric in its + conclusion sort, if one is given. If the [Template Check] flag is + false we just check that the conclusion sort is not small. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 0515e88a15..5f088379ca 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -63,7 +63,8 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.11" -> Current + | "8.12" -> Current + | "8.11" -> V8_11 | "8.10" -> V8_10 | "8.9" -> V8_9 | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> @@ -781,25 +782,8 @@ GRAMMAR EXTEND Gram ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] -> { let mods = match mods with None -> [] | Some l -> List.flatten l in - let slash_position = ref None in - let ampersand_position = ref None in - let rec parse_args i = function - | [] -> [] - | `Id x :: args -> x :: parse_args (i+1) args - | `Slash :: args -> - if Option.is_empty !slash_position then - (slash_position := Some i; parse_args i args) - else - user_err Pp.(str "The \"/\" modifier can occur only once") - | `Ampersand :: args -> - if Option.is_empty !ampersand_position then - (ampersand_position := Some i; parse_args i args) - else - user_err Pp.(str "The \"&\" modifier can occur only once") - in - let args = parse_args 0 (List.flatten args) in let more_implicits = Option.default [] more_implicits in - VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) } + VernacArguments (qid, List.flatten args, more_implicits, mods) } | IDENT "Implicit"; "Type"; bl = reserv_list -> { VernacReserve bl } @@ -843,17 +827,17 @@ GRAMMAR EXTEND Gram argument_spec_block: [ [ item = argument_spec -> { let name, recarg_like, notation_scope = item in - [`Id { name=name; recarg_like=recarg_like; + [RealArg { name=name; recarg_like=recarg_like; notation_scope=notation_scope; implicit_status = NotImplicit}] } - | "/" -> { [`Slash] } - | "&" -> { [`Ampersand] } + | "/" -> { [VolatileArg] } + | "&" -> { [BidiArg] } | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; + RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = NotImplicit}) items } | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> @@ -861,7 +845,7 @@ GRAMMAR EXTEND Gram | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; + RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = Implicit}) items } | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> @@ -869,7 +853,7 @@ GRAMMAR EXTEND Gram | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; + RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = MaximallyImplicit}) items } ] @@ -955,15 +939,7 @@ GRAMMAR EXTEND Gram | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> { VernacRemoveLoadPath dir } - (* For compatibility *) - | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath -> - { VernacAddLoadPath (false, dir, alias) } - | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath -> - { VernacAddLoadPath (true, dir, alias) } - | IDENT "DelPath"; dir = ne_string -> - { VernacRemoveLoadPath dir } - - (* Type-Checking (pas dans le refman) *) + (* Type-Checking *) | "Type"; c = lconstr -> { VernacGlobalCheck c } (* Printing (careful factorization of entries) *) @@ -1027,7 +1003,7 @@ GRAMMAR EXTEND Gram | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> - { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) } + { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } (* compatibility: SearchAbout *) | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 3dbf7afb78..1aa9a4e0f5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -161,6 +161,8 @@ open Pputils | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> + keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + | Search sl -> keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b let pr_option_ref_value = function @@ -1068,39 +1070,52 @@ let string_of_definition_object_kind = let open Decls in function | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) -> + | VernacArguments (q, args, more_implicits, mods) -> return ( hov 2 ( keyword "Arguments" ++ spc() ++ pr_smart_global q ++ let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in let pr_if b x = if b then x else str "" in - let pr_br imp x = match imp with - | Impargs.Implicit -> str "[" ++ x ++ str "]" - | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}" - | Impargs.NotImplicit -> x in - let rec print_arguments n nbidi l = - match n, nbidi, l with - | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l - | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l - | None, None, [] -> mt() - | _, _, [] -> - let dummy = {name=Anonymous; recarg_like=false; - notation_scope=None; implicit_status=Impargs.NotImplicit} - in - print_arguments n nbidi [dummy] - | n, nbidi, { name = id; recarg_like = k; + let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in + let pr_br imp force x = + let left,right = + match imp with + | Impargs.Implicit -> str "[", str "]" + | Impargs.MaximallyImplicit -> str "{", str "}" + | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt() + in + left ++ x ++ right + in + let get_arguments_like s imp tl = + if s = None && imp = Impargs.NotImplicit then [], tl + else + let rec fold extra = function + | RealArg arg :: tl when + Option.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s + && arg.implicit_status = imp -> + fold ((arg.name,arg.recarg_like) :: extra) tl + | args -> List.rev extra, args + in + fold [] tl + in + let rec print_arguments = function + | [] -> mt() + | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l + | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l + | RealArg { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> - spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ - print_arguments (Option.map pred n) (Option.map pred nbidi) tl + let extra, tl = get_arguments_like s imp tl in + spc() ++ pr_br imp (extra<>[]) (prlist_with_sep spc pr_one_arg ((id,k)::extra)) ++ + pr_s s ++ print_arguments tl in let rec print_implicits = function | [] -> mt () | (name, impl) :: rest -> - spc() ++ pr_br impl (Name.print name) ++ print_implicits rest + spc() ++ pr_br impl false (Name.print name) ++ print_implicits rest in - print_arguments nargs nargs_before_bidi args ++ + print_arguments args ++ if not (List.is_empty more_implicits) then prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 5ebc89892c..ea49cae9db 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -259,6 +259,13 @@ let implicit_kind_of_status = function | None -> Anonymous, NotImplicit | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit +let dummy = { + Vernacexpr.implicit_status = NotImplicit; + name = Anonymous; + recarg_like = false; + notation_scope = None; +} + let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit @@ -287,6 +294,20 @@ let rec main_implicits i renames recargs scopes impls = then [] (* we may have a trail of dummies due to eg "clear scopes" *) else status :: rest +let rec insert_fake_args volatile bidi impls = + let open Vernacexpr in + match volatile, bidi with + | Some 0, _ -> VolatileArg :: insert_fake_args None bidi impls + | _, Some 0 -> BidiArg :: insert_fake_args volatile None impls + | None, None -> List.map (fun a -> RealArg a) impls + | _, _ -> + let hd, tl = match impls with + | impl :: impls -> impl, impls + | [] -> dummy, [] + in + let f = Option.map pred in + RealArg hd :: insert_fake_args (f volatile) (f bidi) tl + let print_arguments ref = let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in let flags, recargs, nargs_for_red = @@ -312,12 +333,13 @@ let print_arguments ref = let impls = main_implicits 0 renames recargs scopes impls in let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in let bidi = Pretyping.get_bidirectionality_hint ref in - if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then [] + let impls = insert_fake_args nargs_for_red bidi impls in + if impls = [] && moreimpls = [] && flags = [] then [] else let open Constrexpr in let open Vernacexpr in [Ppvernac.pr_vernac_expr - (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))] + (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))] let print_name_infos ref = let type_info_for_implicit = diff --git a/vernac/record.ml b/vernac/record.ml index 49a73271f0..d85b71df44 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -429,15 +429,31 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let type_constructor = it_mkProd_or_LetIn ind fields in let template = let template_candidate () = - ComInductive.template_polymorphism_candidate (Global.env ()) univs params + (* we use some dummy values for the arities in the rel_context + as univs_of_constr doesn't care about localassums and + getting the real values is too annoying *) + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + let ctor_levels = List.fold_left + (fun univs d -> + let univs = + RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs + in + univs) + param_levels fields + in + ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with | Some template, _ -> (* templateness explicitly requested *) if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "record cannot be made template polymorphic on any universe"); template | None, template -> (* auto detect template *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b53302e1d7..de7695791f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,6 +1785,10 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } +let warn_deprecated_search_about = + CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" + (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") + let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1815,6 +1819,10 @@ let vernac_search ~pstate ~atts s gopt r = | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchAbout sl -> + warn_deprecated_search_about (); + (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + Search.prioritize_search) pr_search + | Search sl -> (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search @@ -2166,10 +2174,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) - | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> + | VernacArguments (qid, args, more_implicits, flags) -> VtDefault(fun () -> with_section_locality ~atts - (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags)) + (ComArguments.vernac_arguments qid args more_implicits flags)) | VernacReserve bl -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 564c55670d..bec6a0d2bb 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -70,6 +70,7 @@ type searchable = | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr | SearchAbout of (bool * search_about_item) list + | Search of (bool * search_about_item) list type locatable = | LocateAny of qualid or_by_notation @@ -250,13 +251,17 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative (** {6 The type of vernacular expressions} *) -type vernac_argument_status = { +type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; implicit_status : Impargs.implicit_kind; } +type vernac_argument_status = + | VolatileArg | BidiArg + | RealArg of vernac_one_argument_status + type arguments_modifier = [ `Assert | `ClearBidiHint @@ -383,8 +388,6 @@ type nonrec vernac_expr = qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * - int option (* Number of args to trigger reduction *) * - int option (* Number of args before bidirectional typing *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |