diff options
45 files changed, 471 insertions, 120 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d566d56331..f17e06b520 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -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 @@ -699,3 +729,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 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..88bc3f912b 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"; @@ -919,16 +919,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..de21b17f9f 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}" @@ -200,6 +207,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/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/doc/changelog/07-commands-and-options/11187-remove-addpath.rst b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst new file mode 100644 index 0000000000..283c44fda6 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst @@ -0,0 +1,5 @@ +- 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). 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/changes.rst b/doc/sphinx/changes.rst index 80a24b997c..01db9da03b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -568,7 +568,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 +765,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/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/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/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/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/complexity/pattern.v b/test-suite/complexity/pattern.v new file mode 100644 index 0000000000..fb5bf5a00b --- /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 < 0.75s *) +(* 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/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/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/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/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/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/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 5b97e06b2b..8d6724c3b1 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 -> @@ -938,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) *) 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 *) |