From d41bb0c5e15442da6f6b7333e2b1e73a8091292a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 Nov 2020 16:44:26 +0100
Subject: Bump version numbers
---
META.coq.in | 86 ++++++++++++++++++++++++++++++------------------------------
configure.ml | 8 +++---
2 files changed, 47 insertions(+), 47 deletions(-)
diff --git a/META.coq.in b/META.coq.in
index 29b3ecbcb3..68ab0733ee 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.13"
+version = "8.14"
directory = ""
requires = ""
@@ -9,7 +9,7 @@ requires = ""
package "config" (
description = "Coq Configuration Variables"
- version = "8.13"
+ version = "8.14"
directory = "config"
@@ -19,7 +19,7 @@ package "config" (
package "clib" (
description = "Base General Coq Library"
- version = "8.13"
+ version = "8.14"
directory = "clib"
requires = "str, unix, threads"
@@ -31,7 +31,7 @@ package "clib" (
package "lib" (
description = "Base Coq-Specific Library"
- version = "8.13"
+ version = "8.14"
directory = "lib"
@@ -45,7 +45,7 @@ package "lib" (
package "vm" (
description = "Coq VM"
- version = "8.13"
+ version = "8.14"
directory = "kernel/byterun"
@@ -64,7 +64,7 @@ package "vm" (
package "kernel" (
description = "Coq's Kernel"
- version = "8.13"
+ version = "8.14"
directory = "kernel"
@@ -78,7 +78,7 @@ package "kernel" (
package "library" (
description = "Coq Libraries (vo) support"
- version = "8.13"
+ version = "8.14"
requires = "coq.kernel"
@@ -92,7 +92,7 @@ package "library" (
package "engine" (
description = "Coq Tactic Engine"
- version = "8.13"
+ version = "8.14"
requires = "coq.library"
directory = "engine"
@@ -105,7 +105,7 @@ package "engine" (
package "pretyping" (
description = "Coq Pretyper"
- version = "8.13"
+ version = "8.14"
requires = "coq.engine"
directory = "pretyping"
@@ -118,7 +118,7 @@ package "pretyping" (
package "interp" (
description = "Coq Term Interpretation"
- version = "8.13"
+ version = "8.14"
requires = "zarith, coq.pretyping"
directory = "interp"
@@ -131,7 +131,7 @@ package "interp" (
package "proofs" (
description = "Coq Proof Engine"
- version = "8.13"
+ version = "8.14"
requires = "coq.interp"
directory = "proofs"
@@ -144,7 +144,7 @@ package "proofs" (
package "gramlib" (
description = "Coq Grammar Engine"
- version = "8.13"
+ version = "8.14"
requires = "coq.lib"
directory = "gramlib/.pack"
@@ -156,7 +156,7 @@ package "gramlib" (
package "parsing" (
description = "Coq Parsing Engine"
- version = "8.13"
+ version = "8.14"
requires = "coq.gramlib, coq.proofs"
directory = "parsing"
@@ -169,7 +169,7 @@ package "parsing" (
package "printing" (
description = "Coq Printing Engine"
- version = "8.13"
+ version = "8.14"
requires = "coq.parsing"
directory = "printing"
@@ -182,7 +182,7 @@ package "printing" (
package "tactics" (
description = "Coq Basic Tactics"
- version = "8.13"
+ version = "8.14"
requires = "coq.printing"
directory = "tactics"
@@ -195,7 +195,7 @@ package "tactics" (
package "vernac" (
description = "Coq Vernacular Interpreter"
- version = "8.13"
+ version = "8.14"
requires = "coq.tactics"
directory = "vernac"
@@ -208,7 +208,7 @@ package "vernac" (
package "stm" (
description = "Coq State Transactional Machine"
- version = "8.13"
+ version = "8.14"
requires = "coq.vernac"
directory = "stm"
@@ -221,7 +221,7 @@ package "stm" (
package "toplevel" (
description = "Coq Toplevel"
- version = "8.13"
+ version = "8.14"
requires = "coq.stm"
directory = "toplevel"
@@ -234,7 +234,7 @@ package "toplevel" (
package "idetop" (
description = "Coq IDE Libraries"
- version = "8.13"
+ version = "8.14"
requires = "coq.toplevel"
directory = "ide"
@@ -247,7 +247,7 @@ package "idetop" (
package "ide" (
description = "Coq IDE Libraries"
- version = "8.13"
+ version = "8.14"
requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3"
directory = "ide"
@@ -260,7 +260,7 @@ package "ide" (
package "ideprotocol" (
description = "Coq IDE protocol"
- version = "8.13"
+ version = "8.14"
requires = "coq.toplevel"
directory = "ide/protocol"
@@ -273,14 +273,14 @@ package "ideprotocol" (
package "plugins" (
description = "Coq built-in plugins"
- version = "8.13"
+ version = "8.14"
directory = "plugins"
package "ltac" (
description = "Coq LTAC Plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.stm"
directory = "ltac"
@@ -295,7 +295,7 @@ package "plugins" (
package "tauto" (
description = "Coq tauto plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "ltac"
@@ -310,7 +310,7 @@ package "plugins" (
package "omega" (
description = "Coq omega plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "omega"
@@ -325,7 +325,7 @@ package "plugins" (
package "micromega" (
description = "Coq micromega plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "micromega"
@@ -340,7 +340,7 @@ package "plugins" (
package "zify" (
description = "Coq Zify plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "micromega"
@@ -355,7 +355,7 @@ package "plugins" (
package "ring" (
description = "Coq ring plugin"
- version = "8.13"
+ version = "8.14"
requires = ""
directory = "ring"
@@ -370,7 +370,7 @@ package "plugins" (
package "extraction" (
description = "Coq extraction plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "extraction"
@@ -385,7 +385,7 @@ package "plugins" (
package "cc" (
description = "Coq cc plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "cc"
@@ -400,7 +400,7 @@ package "plugins" (
package "firstorder" (
description = "Coq ground plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "firstorder"
@@ -415,7 +415,7 @@ package "plugins" (
package "rtauto" (
description = "Coq rtauto plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "rtauto"
@@ -430,7 +430,7 @@ package "plugins" (
package "btauto" (
description = "Coq btauto plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "btauto"
@@ -445,7 +445,7 @@ package "plugins" (
package "funind" (
description = "Coq recdef plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.extraction"
directory = "funind"
@@ -460,7 +460,7 @@ package "plugins" (
package "nsatz" (
description = "Coq nsatz plugin"
- version = "8.13"
+ version = "8.14"
requires = "zarith, coq.plugins.ltac"
directory = "nsatz"
@@ -475,7 +475,7 @@ package "plugins" (
package "rsyntax" (
description = "Coq rsyntax plugin"
- version = "8.13"
+ version = "8.14"
requires = ""
directory = "syntax"
@@ -490,7 +490,7 @@ package "plugins" (
package "int63syntax" (
description = "Coq int63syntax plugin"
- version = "8.13"
+ version = "8.14"
requires = ""
directory = "syntax"
@@ -505,7 +505,7 @@ package "plugins" (
package "string_notation" (
description = "Coq string_notation plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.vernac"
directory = "syntax"
@@ -519,7 +519,7 @@ package "plugins" (
package "numeral_notation" (
description = "Coq numeral notation plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.vernac"
directory = "numeral_notation"
@@ -534,7 +534,7 @@ package "plugins" (
package "derive" (
description = "Coq derive plugin"
- version = "8.13"
+ version = "8.14"
requires = ""
directory = "derive"
@@ -549,7 +549,7 @@ package "plugins" (
package "ssrmatching" (
description = "Coq ssrmatching plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "ssrmatching"
@@ -564,7 +564,7 @@ package "plugins" (
package "ssreflect" (
description = "Coq ssreflect plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ssrmatching"
directory = "ssr"
@@ -579,7 +579,7 @@ package "plugins" (
package "ltac2" (
description = "Coq Ltac2 Plugin"
- version = "8.13"
+ version = "8.14"
requires = "coq.plugins.ltac"
directory = "../user-contrib/Ltac2"
diff --git a/configure.ml b/configure.ml
index e32f780a3d..40d77ed109 100644
--- a/configure.ml
+++ b/configure.ml
@@ -12,11 +12,11 @@
#load "str.cma"
open Printf
-let coq_version = "8.13+alpha"
-let coq_macos_version = "8.12.90" (** "[...] should be a string comprised of
+let coq_version = "8.14+alpha"
+let coq_macos_version = "8.13.90" (** "[...] should be a string comprised of
three non-negative, period-separated integers [...]" *)
-let vo_magic = 81291
-let state_magic = 581291
+let vo_magic = 81391
+let state_magic = 581391
let is_a_released_version = false
let distributed_exec =
["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
--
cgit v1.2.3
From 17da7c41b17da3280cb2c182387685ad4be6022f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 Nov 2020 16:47:06 +0100
Subject: Update compat infrastructure for 8.14
---
doc/stdlib/index-list.html.template | 1 +
test-suite/success/CompatCurrentFlag.v | 4 ++--
test-suite/success/CompatOldFlag.v | 4 ++--
test-suite/success/CompatOldOldFlag.v | 6 ++++++
test-suite/success/CompatPreviousFlag.v | 4 ++--
test-suite/tools/update-compat/run.sh | 2 +-
theories/Compat/Coq813.v | 2 ++
theories/Compat/Coq814.v | 11 +++++++++++
toplevel/coqargs.ml | 1 +
9 files changed, 28 insertions(+), 7 deletions(-)
create mode 100644 test-suite/success/CompatOldOldFlag.v
create mode 100644 theories/Compat/Coq814.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7201dc6a0e..8ab4265b15 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -709,6 +709,7 @@ through the Require Import command.
theories/Compat/Coq811.v
theories/Compat/Coq812.v
theories/Compat/Coq813.v
+ theories/Compat/Coq814.v
Array:
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 97b4e39168..f1dad301fd 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.13") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.14") -*- *)
(** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq813.
+Import Coq.Compat.Coq814.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index c06dd6e450..a737e0c98e 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq814.
Import Coq.Compat.Coq813.
Import Coq.Compat.Coq812.
-Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..f4cf703ec7
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq814.
+Import Coq.Compat.Coq813.
+Import Coq.Compat.Coq812.
+Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 83010f2149..07d5fcd3ab 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.13") -*- *)
(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq814.
Import Coq.Compat.Coq813.
-Import Coq.Compat.Coq812.
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/Coq813.v b/theories/Compat/Coq813.v
index 92544c6ed9..fe7431dcd3 100644
--- a/theories/Compat/Coq813.v
+++ b/theories/Compat/Coq813.v
@@ -9,3 +9,5 @@
(************************************************************************)
(** Compatibility file for making Coq act similar to Coq v8.13 *)
+
+Require Export Coq.Compat.Coq814.
diff --git a/theories/Compat/Coq814.v b/theories/Compat/Coq814.v
new file mode 100644
index 0000000000..94948dd280
--- /dev/null
+++ b/theories/Compat/Coq814.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* ""
let get_compat_file = function
+ | "8.14" -> "Coq.Compat.Coq814"
| "8.13" -> "Coq.Compat.Coq813"
| "8.12" -> "Coq.Compat.Coq812"
| "8.11" -> "Coq.Compat.Coq811"
--
cgit v1.2.3
From f29decccfc51850fe067633fcf759a481a210bca Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Nov 2020 10:46:29 +0100
Subject: update default.nix
---
default.nix | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/default.nix b/default.nix
index 7f9e62b28c..0b23bdb48c 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.13-git"
+, coq-version ? "8.14-git"
}:
with pkgs;
--
cgit v1.2.3