diff options
author | Théo Zimmermann <theo.zimmermann@inria.fr> | 2020-05-18 09:28:58 (GMT) |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2020-05-18 14:57:43 (GMT) |
commit | f1238742f931269167e7c2704b53bb285d05f39d (patch) | |
tree | a5e02dcc797d17c09bac5ddc22e9d803828198df | |
parent | b456cf69eaac3e73f0c63c81ab2dbb58ca5e73b2 (diff) | |
download | coq-f1238742f931269167e7c2704b53bb285d05f39d.zip coq-f1238742f931269167e7c2704b53bb285d05f39d.tar.gz coq-f1238742f931269167e7c2704b53bb285d05f39d.tar.bz2 |
Update to 8.13.V8.13+alpharefs/pull/12346/head
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
-rw-r--r-- | .gitlab-ci.yml | 2 | ||||
-rw-r--r-- | META.coq.in | 84 | ||||
-rw-r--r-- | configure.ml | 8 | ||||
-rw-r--r-- | default.nix | 2 | ||||
-rw-r--r-- | dev/doc/changes.md | 2 | ||||
-rw-r--r-- | doc/stdlib/index-list.html.template | 1 | ||||
-rw-r--r-- | test-suite/success/CompatCurrentFlag.v | 4 | ||||
-rw-r--r-- | test-suite/success/CompatOldFlag.v | 4 | ||||
-rw-r--r-- | test-suite/success/CompatOldOldFlag.v | 6 | ||||
-rw-r--r-- | test-suite/success/CompatPreviousFlag.v | 4 | ||||
-rwxr-xr-x | test-suite/tools/update-compat/run.sh | 2 | ||||
-rw-r--r-- | theories/Compat/Coq812.v | 2 | ||||
-rw-r--r-- | theories/Compat/Coq813.v | 11 | ||||
-rw-r--r-- | toplevel/coqargs.ml | 1 |
14 files changed, 78 insertions, 55 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e8ee0c5..f26804e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -371,7 +371,7 @@ pkg:opam: - opam pin add --kind=path coqide.$COQ_VERSION . - set +e variables: - COQ_VERSION: "8.12" + COQ_VERSION: "8.13" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" only: *full-ci diff --git a/META.coq.in b/META.coq.in index 377dbd9..095f54d 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.12" +version = "8.13" directory = "" requires = "" @@ -9,7 +9,7 @@ requires = "" package "config" ( description = "Coq Configuration Variables" - version = "8.12" + version = "8.13" directory = "config" @@ -19,7 +19,7 @@ package "config" ( package "clib" ( description = "Base General Coq Library" - version = "8.12" + version = "8.13" directory = "clib" requires = "str, unix, threads" @@ -31,7 +31,7 @@ package "clib" ( package "lib" ( description = "Base Coq-Specific Library" - version = "8.12" + version = "8.13" directory = "lib" @@ -45,7 +45,7 @@ package "lib" ( package "vm" ( description = "Coq VM" - version = "8.12" + version = "8.13" directory = "kernel/byterun" @@ -64,7 +64,7 @@ package "vm" ( package "kernel" ( description = "Coq's Kernel" - version = "8.12" + version = "8.13" directory = "kernel" @@ -78,7 +78,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.12" + version = "8.13" requires = "coq.kernel" @@ -92,7 +92,7 @@ package "library" ( package "engine" ( description = "Coq Tactic Engine" - version = "8.12" + version = "8.13" requires = "coq.library" directory = "engine" @@ -105,7 +105,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.12" + version = "8.13" requires = "coq.engine" directory = "pretyping" @@ -118,7 +118,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.12" + version = "8.13" requires = "coq.pretyping" directory = "interp" @@ -131,7 +131,7 @@ package "interp" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.12" + version = "8.13" requires = "coq.interp" directory = "proofs" @@ -144,7 +144,7 @@ package "proofs" ( package "gramlib" ( description = "Coq Grammar Engine" - version = "8.12" + version = "8.13" requires = "coq.lib" directory = "gramlib/.pack" @@ -156,7 +156,7 @@ package "gramlib" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.12" + version = "8.13" requires = "coq.gramlib, coq.proofs" directory = "parsing" @@ -169,7 +169,7 @@ package "parsing" ( package "printing" ( description = "Coq Printing Engine" - version = "8.12" + version = "8.13" requires = "coq.parsing" directory = "printing" @@ -182,7 +182,7 @@ package "printing" ( package "tactics" ( description = "Coq Basic Tactics" - version = "8.12" + version = "8.13" requires = "coq.printing" directory = "tactics" @@ -195,7 +195,7 @@ package "tactics" ( package "vernac" ( description = "Coq Vernacular Interpreter" - version = "8.12" + version = "8.13" requires = "coq.tactics" directory = "vernac" @@ -208,7 +208,7 @@ package "vernac" ( package "stm" ( description = "Coq State Transactional Machine" - version = "8.12" + version = "8.13" requires = "coq.vernac" directory = "stm" @@ -221,7 +221,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.12" + version = "8.13" requires = "num, coq.stm" directory = "toplevel" @@ -234,7 +234,7 @@ package "toplevel" ( package "idetop" ( description = "Coq IDE Libraries" - version = "8.12" + version = "8.13" requires = "coq.toplevel" directory = "ide" @@ -247,7 +247,7 @@ package "idetop" ( package "ide" ( description = "Coq IDE Libraries" - version = "8.12" + version = "8.13" requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" @@ -260,7 +260,7 @@ package "ide" ( package "ideprotocol" ( description = "Coq IDE protocol" - version = "8.12" + version = "8.13" requires = "coq.toplevel" directory = "ide/protocol" @@ -273,14 +273,14 @@ package "ideprotocol" ( package "plugins" ( description = "Coq built-in plugins" - version = "8.12" + version = "8.13" directory = "plugins" package "ltac" ( description = "Coq LTAC Plugin" - version = "8.12" + version = "8.13" requires = "coq.stm" directory = "ltac" @@ -295,7 +295,7 @@ package "plugins" ( package "tauto" ( description = "Coq tauto plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "ltac" @@ -310,7 +310,7 @@ package "plugins" ( package "omega" ( description = "Coq omega plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "omega" @@ -325,7 +325,7 @@ package "plugins" ( package "micromega" ( description = "Coq micromega plugin" - version = "8.12" + version = "8.13" requires = "num,coq.plugins.ltac" directory = "micromega" @@ -340,7 +340,7 @@ package "plugins" ( package "zify" ( description = "Coq Zify plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "micromega" @@ -355,7 +355,7 @@ package "plugins" ( package "setoid_ring" ( description = "Coq newring plugin" - version = "8.12" + version = "8.13" requires = "" directory = "setoid_ring" @@ -370,7 +370,7 @@ package "plugins" ( package "extraction" ( description = "Coq extraction plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "extraction" @@ -385,7 +385,7 @@ package "plugins" ( package "cc" ( description = "Coq cc plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "cc" @@ -400,7 +400,7 @@ package "plugins" ( package "firstorder" ( description = "Coq ground plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "firstorder" @@ -415,7 +415,7 @@ package "plugins" ( package "rtauto" ( description = "Coq rtauto plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "rtauto" @@ -430,7 +430,7 @@ package "plugins" ( package "btauto" ( description = "Coq btauto plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "btauto" @@ -445,7 +445,7 @@ package "plugins" ( package "funind" ( description = "Coq recdef plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.extraction" directory = "funind" @@ -460,7 +460,7 @@ package "plugins" ( package "nsatz" ( description = "Coq nsatz plugin" - version = "8.12" + version = "8.13" requires = "num,coq.plugins.ltac" directory = "nsatz" @@ -475,7 +475,7 @@ package "plugins" ( package "rsyntax" ( description = "Coq rsyntax plugin" - version = "8.12" + version = "8.13" requires = "" directory = "syntax" @@ -490,7 +490,7 @@ package "plugins" ( package "int63syntax" ( description = "Coq int63syntax plugin" - version = "8.12" + version = "8.13" requires = "" directory = "syntax" @@ -505,7 +505,7 @@ package "plugins" ( package "string_notation" ( description = "Coq string_notation plugin" - version = "8.12" + version = "8.13" requires = "" directory = "syntax" @@ -520,7 +520,7 @@ package "plugins" ( package "derive" ( description = "Coq derive plugin" - version = "8.12" + version = "8.13" requires = "" directory = "derive" @@ -535,7 +535,7 @@ package "plugins" ( package "ssrmatching" ( description = "Coq ssrmatching plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "ssrmatching" @@ -550,7 +550,7 @@ package "plugins" ( package "ssreflect" ( description = "Coq ssreflect plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ssrmatching" directory = "ssr" @@ -565,7 +565,7 @@ package "plugins" ( package "ltac2" ( description = "Coq Ltac2 Plugin" - version = "8.12" + version = "8.13" requires = "coq.plugins.ltac" directory = "../user-contrib/Ltac2" diff --git a/configure.ml b/configure.ml index 75c11da..9cfa9d4 100644 --- a/configure.ml +++ b/configure.ml @@ -12,11 +12,11 @@ #load "str.cma" open Printf -let coq_version = "8.12+alpha" -let coq_macos_version = "8.11.90" (** "[...] should be a string comprised of +let coq_version = "8.13+alpha" +let coq_macos_version = "8.12.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 81191 -let state_magic = 581191 +let vo_magic = 81291 +let state_magic = 581291 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; diff --git a/default.nix b/default.nix index 841bccb..6b0e396 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.12-git" +, coq-version ? "8.13-git" }: with pkgs; diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9498ab8..ae4c632 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,5 @@ +## Changes between Coq 8.12 and Coq 8.13 + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 1a02d6e..ab615d5 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -707,5 +707,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq810.v theories/Compat/Coq811.v theories/Compat/Coq812.v + theories/Compat/Coq813.v </dd> </dl> diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index c865484..97b4e39 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq812. +Import Coq.Compat.Coq813. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index a1c1209..c06dd6e 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000..f408e95 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. +Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 00f4747..83010f2 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571..61273c4 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/Coq812.v b/theories/Compat/Coq812.v index ee4bac3..f52b559 100644 --- a/theories/Compat/Coq812.v +++ b/theories/Compat/Coq812.v @@ -9,4 +9,6 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.12 *) + +Require Export Coq.Compat.Coq813. Set Firstorder Solver auto with *. diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v new file mode 100644 index 0000000..92544c6 --- /dev/null +++ b/theories/Compat/Coq813.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.13 *) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index c7ad5ed..eb386ea 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -263,6 +263,7 @@ let get_native_name s = with _ -> "" let get_compat_file = function + | "8.13" -> "Coq.Compat.Coq813" | "8.12" -> "Coq.Compat.Coq812" | "8.11" -> "Coq.Compat.Coq811" | "8.10" -> "Coq.Compat.Coq810" |