Merge PR #12286: [sphinx] Add links to other versions of the refman

Reviewed-by: Zimmi48

4 files changed, 80 insertions, 7 deletions

diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index ceb390c02c..340b66bbd0 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -96,6 +96,8 @@ in time.
 - [ ] Delay non-blocking issues to the appropriate milestone and ensure
   blocking issues are solved. If required to solve some blocking issues,
   it is possible to revert some feature PRs in the version branch only.
+- [ ] Add a new link to the ``'versions'`` list of the refman (in
+      ``html_context`` in ``doc/sphinx/conf.py``).
 
 ## Before the beta release date ##
 
diff --git a/doc/LICENSE b/doc/LICENSE
index 9f3a6b3f4c..a327156144 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -6,13 +6,16 @@ copyright (c) 1999-2019, Inria, CNRS and contributors, with the
 exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright
 2010,2011 Canonical Ltd and licensed under the Ubuntu font license,
 version 1.0
-(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and
+(https://www.ubuntu.com/legal/terms-and-policies/font-licence), 
 its derivative CoqNotations.ttf distributed under the same
-license. The material connected to the Reference Manual may be
-distributed only subject to the terms and conditions set forth in the
-Open Publication License, v1.0 or later (the latest version is
-presently available at http://www.opencontent.org/openpub/).  Options
-A and B are *not* elected.
+license, and the _templates/versions.html file derived from
+sphinx_rtd_theme, which is Copyright 2013-2018 Dave Snider, Read the
+Docs, Inc. & contributors and distributed under the MIT License
+included in that file. The material connected to the Reference Manual
+may be distributed only subject to the terms and conditions set forth in
+the Open Publication License, v1.0 or later (the latest version is
+presently available at http://www.opencontent.org/openpub/).  Options A
+and B are *not* elected.
 
 The Coq Standard Library is a collective work from the Coq Development
 Team whose members are listed in the file CREDITS of the Coq source
diff --git a/doc/sphinx/_templates/versions.html b/doc/sphinx/_templates/versions.html
new file mode 100644
index 0000000000..967d00d2bf
--- /dev/null
+++ b/doc/sphinx/_templates/versions.html
@@ -0,0 +1,48 @@
+{# Forked from versions.html in sphinx_rtd_theme 0.4.3 #}
+
+{#
+The MIT License (MIT)
+
+Copyright (c) 2013-2018 Dave Snider, Read the Docs, Inc. & contributors
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software is furnished to do so,
+subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+#}
+
+{% if not READTHEDOCS %}
+  <div class="rst-versions" data-toggle="rst-versions" role="note" aria-label="versions">
+    <span class="rst-current-version" data-toggle="rst-current-version">
+      <span class="fa fa-book"> Other versions</span>
+      v: {{ version }}
+      <span class="fa fa-caret-down"></span>
+    </span>
+    <div class="rst-other-versions">
+      <dl>
+        <dt>{{ _('Versions') }}</dt>
+        {% for slug, url in versions %}
+          <dd><a href="{{ url }}">{{ slug }}</a></dd>
+        {% endfor %}
+      </dl>
+      <dl>
+        <dt>{{ _('Downloads') }}</dt>
+        {% for type, url in downloads %}
+          <dd><a href="{{ url }}">{{ type }}</a></dd>
+        {% endfor %}
+      </dl>
+    </div>
+  </div>
+{% endif %}
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index dbe582df95..4136b406de 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -202,6 +202,7 @@ html_theme = 'sphinx_rtd_theme'
 # Theme options are theme-specific and customize the look and feel of a theme
 # further.  For a list of options available for each theme, see the
 # documentation.
+PDF_URL = "https://github.com/coq/coq/releases/download/V{version}/coq-{version}-reference-manual.pdf"
 html_theme_options = {
     'collapse_navigation': False
 }
@@ -210,7 +211,26 @@ html_context = {
     'github_user': 'coq',
     'github_repo': 'coq',
     'github_version': 'master',
-    'conf_py_path': '/doc/sphinx/'
+    'conf_py_path': '/doc/sphinx/',
+    # Versions and downloads listed in the versions menu (see _templates/versions.html)
+    'versions': [
+        ("master", "https://coq.github.io/doc/master/refman/"),
+        ("stable", "https://coq.inria.fr/distrib/current/refman/"),
+        ("v8.11", "https://coq.github.io/doc/v8.11/refman/"),
+        ("v8.10", "https://coq.github.io/doc/v8.10/refman/"),
+        ("v8.9", "https://coq.github.io/doc/v8.9/refman/"),
+        ("8.8", "https://coq.inria.fr/distrib/V8.8.2/refman/"),
+        ("8.7", "https://coq.inria.fr/distrib/V8.7.2/refman/"),
+        ("8.6", "https://coq.inria.fr/distrib/V8.6.1/refman/"),
+        ("8.5", "https://coq.inria.fr/distrib/V8.5pl3/refman/"),
+        ("8.4", "https://coq.inria.fr/distrib/V8.4pl6/refman/"),
+        ("8.3", "https://coq.inria.fr/distrib/V8.3pl5/refman/"),
+        ("8.2", "https://coq.inria.fr/distrib/V8.2pl3/refman/"),
+        ("8.1", "https://coq.inria.fr/distrib/V8.1pl6/refman/"),
+        ("8.0", "https://coq.inria.fr/distrib/V8.0/doc/")
+    ],
+    'downloads': ([("PDF", PDF_URL.format(version=version))]
+                  if coq_config.is_a_released_version else [])
 }
 
 # Add any paths that contain custom themes here, relative to this directory.