Merge PR #10085: Do not include unreleased changelog in released versions.

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: vbgl

7 files changed, 50 insertions, 8 deletions

diff --git a/configure.ml b/configure.ml
index 5b99851f83..57f31fec4c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -17,6 +17,7 @@ let coq_macos_version = "8.9.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
 let vo_magic = 8991
 let state_magic = 58991
+let is_a_released_version = false
 let distributed_exec =
   ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt";
    "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"]
@@ -1205,8 +1206,8 @@ let write_configpy f =
   safe_remove f;
   let o = open_out f in
   let pr s = fprintf o s in
-  let pr_s = pr "%s = '%s'\n" in
   pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure\n";
-  pr_s "version" coq_version
+  pr "version = '%s'\n" coq_version;
+  pr "is_a_released_version = %s\n" (if is_a_released_version then "True" else "False")
 
 let _ = write_configpy "config/coq_config.py"
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 60c0886896..189d6f9fa5 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -84,10 +84,18 @@
   Coq has been tagged.
 - [ ] Have some people test the recently auto-generated Windows and MacOS
   packages.
-- [ ] Change the version name from alpha to beta1 (see
+- [ ] In a PR:
+  - Change the version name from alpha to beta1 (see
   [#7009](https://github.com/coq/coq/pull/7009/files)).
-  We generally do not update the magic numbers at this point.
+  - We generally do not update the magic numbers at this point.
+  - Set `is_a_released_version` to `true` in `configure.ml`.
 - [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+- [ ] Check using `git push --tags --dry-run` that you are not
+  pushing anything else than the new tag. If needed, remove spurious
+  tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+  (if you forget about it, you'll be reminded whenever you try to
+  backport a PR with a changelog entry).
 
 ### These steps are the same for all releases (beta, final, patch-level) ###
 
@@ -112,9 +120,17 @@
 
 ## At the final release time ##
 
-- [ ] Change the version name to X.X.0 and the magic numbers (see
+- [ ] In a PR:
+  - Change the version name from X.X.0 and the magic numbers (see
   [#7271](https://github.com/coq/coq/pull/7271/files)).
+  - Set `is_a_released_version` to `true` in `configure.ml`.
 - [ ] Put the `VX.X.0` tag.
+- [ ] Check using `git push --tags --dry-run` that you are not
+  pushing anything else than the new tag. If needed, remove spurious
+  tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+  (if you forget about it, you'll be reminded whenever you try to
+  backport a PR with a changelog entry).
 
 Repeat the generic process documented above for all releases.
 
diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst
index 1113782180..dd873cfdd5 100644
--- a/doc/changelog/12-misc/09964-changes.rst
+++ b/doc/changelog/12-misc/09964-changes.rst
@@ -8,6 +8,7 @@
   `#9668 <https://github.com/coq/coq/pull/9668>`_,
   `#9939 <https://github.com/coq/coq/pull/9939>`_,
   `#9964 <https://github.com/coq/coq/pull/9964>`_,
+  and `#10085 <https://github.com/coq/coq/pull/10085>`_,
   by Théo Zimmermann,
-  with help and ideas from Emilio Jesús Gallego Arias,
-  Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
+  with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
+  Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 5704587ae0..574b943a78 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -2,7 +2,9 @@
 Recent changes
 --------------
 
-.. include:: ../unreleased.rst
+.. ifconfig:: not coq_config.is_a_released_version
+
+   .. include:: ../unreleased.rst
 
 Version 8.10
 ------------
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 972a53ae36..ec3343dac6 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -53,6 +53,7 @@ needs_sphinx = '1.7.8'
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
+    'sphinx.ext.ifconfig',
     'sphinx.ext.mathjax',
     'sphinx.ext.todo',
     'sphinxcontrib.bibtex',
@@ -100,6 +101,7 @@ def copy_formatspecific_files(app):
 
 def setup(app):
     app.connect('builder-inited', copy_formatspecific_files)
+    app.add_config_value('coq_config', coq_config, 'env')
 
 # The master toctree document.
 # We create this file in `copy_master_doc` above.
diff --git a/test-suite/dune b/test-suite/dune
index c430400ba5..cd33319fa4 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -20,6 +20,8 @@
    ../dev/header.ml
    ../dev/tools/update-compat.py
    ../doc/stdlib/index-list.html.template
+   ; For the changelog test
+   ../config/coq_config.py
    (package coq)
    ; For fake_ide
    (package coqide-server)
diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh
new file mode 100755
index 0000000000..8b4a49e577
--- /dev/null
+++ b/test-suite/misc/changelog.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+while read line; do
+  if [ "$line" = "is_a_released_version = False" ]; then
+    echo "This is not a released version: nothing to test."
+    exit 0
+  fi
+done < ../config/coq_config.py
+
+for d in ../doc/changelog/*; do
+  if [ -d "$d" ]; then
+    if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then
+      echo "Fatal: unreleased changelog entries remain in ${d#../}/"
+      echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/"
+      exit 1
+    fi
+  fi
+done