[sphinx] Add links to other versions of the refman

3 files changed, 78 insertions, 7 deletions

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.