Merge pull request #162 from Zimmi48/coq-platform-update

Website simplification and Coq platform update.

incl/macros.html

@@ -1,9 +1,3 @@
-<#def RELEASES>https://github.com/coq/coq/releases</#def>
-<#def BASEURL>https://github.com/coq/coq/releases/tag/</#def>
-
-<#def CURRENTMAJORVERSION>8.13</#def>
 <#def CURRENTVERSION>8.13.1</#def>
-<#def CURRENTVERSIONDATE>February 2021</#def>
-<#def CURRENTVERSIONTAG>V8.13.1</#def>
-<#def CURRENTVERSIONURL><#BASEURL><#CURRENTVERSIONTAG></#def>
+<#def CURRENTVERSIONTAG>V<#CURRENTVERSION></#def>
 <#def CURRENTCREDITSURL>https://github.com/coq/coq/blob/<#CURRENTVERSIONTAG>/CREDITS</#def>

pages/about-coq.html

@@ -12,7 +12,7 @@
       <li>to state mathematical theorems and software specifications;</li>
       <li>to interactively develop formal proofs of these theorems;</li>
       <li>to machine-check these proofs by a relatively small certification "kernel";</li>
-      <li>to extract certified programs to languages like Objective Caml, Haskell or Scheme.</li>
+      <li>to extract certified programs to languages like OCaml, Haskell or Scheme.</li>
     </ul>
 
    <p>As a proof development system, Coq provides interactive proof
@@ -63,28 +63,26 @@
 <div class="frameworklabel">Credits</div>
 <div class="frameworkcontent">
 
-    <p>Coq is the result of about 30 years of research. It started in
+    <p>Coq is the result of more than 30 years of research. It started in
     1984 from an implementation of the Calculus of Constructions at
     INRIA-Rocquencourt by Thierry Coquand and Gérard Huet. In 1991,
     Christine Paulin extended it to the Calculus of Inductive
     Constructions.
 
-    All in all, more than a hundred people contributed to the
-    development of Coq features (see
+    All in all, more than 200 people have contributed to the
+    development of Coq (see
     our <a href="<#CURRENTCREDITSURL>">credits</a> file,
     the <a href="/refman/history.html">history</a>
     and <a href="/refman/changes.html">recent changes</a> chapters in
     the Coq Reference Manual or the
     synthetic <a href="/who-did-what-in-coq">who did what</a>
     table).</p>
 
-    <p>The development is coordinated by the ADT Coq (Action for Technological Development), that gathers the teams involved in the implementation of the Coq Proof Assistant. The teams registered in the ADT are the <a href="http://www.inria.fr">INRIA</a> projects <a href="http://www.pps.univ-paris-diderot.fr/pi.r2/">πr²</a> and <a href="http://www-sop.inria.fr/marelle/">Marelle</a>, and the team <a href="http://cedric.cnam.fr/AfficheEquipe.php?id=7&amp;lang=fr">CPR</a> from <a href="http://www.cnam.fr">CNAM</a>.
-</p>
-
-
-    <p> Coq is written in the <a href="https://ocaml.org/index.fr.html">OCaml</a> language, with a bit of C. It is
-    distributed under the <a href="http://www.gnu.org/licenses/old-licenses/lgpl-2.1.html">GNU Lesser General Public Licence Version
-    2.1</a> (LGPL).</p>
+    <p> Coq is written
+    in <a href="https://ocaml.org/index.fr.html">OCaml</a>. It is
+    distributed under
+    the <a href="http://www.gnu.org/licenses/old-licenses/lgpl-2.1.html">GNU
+    Lesser General Public Licence Version 2.1</a> (LGPL).</p>
 </div>
 </div>
 

pages/documentation.html

@@ -12,7 +12,11 @@
 <ul>
 
 <li>the <a href="/distrib/current/refman/">Reference Manual</a>, which
-is the complete, authoritative source of documentation for Coq;</li>
+is the authoritative source of documentation for Coq.  It
+contains
+a <a href="/distrib/current/refman/changes.html">changelog</a>
+describing updates to Coq,
+which we recommend you read when you upgrade Coq;</li>
 
 <li>the documentation of
 the <a href="/distrib/current/stdlib/">Standard Library</a> distributed
@@ -21,7 +25,8 @@
 </ul>
 
 <p>A PDF version of the reference manual can be downloaded from the
-the <a href="<#CURRENTVERSIONURL>">release page</a>.</p>
+the <a href="https://github.com/coq/coq/releases/latest">release
+page</a>.</p>
 
 <p>Note that this reference documentation is not the recommended way to start
 using Coq. See below for more appropriate documentation for beginners.</p>
@@ -32,6 +37,7 @@
   <ul>
     <li><a href="/distrib/current/refman/">Reference Manual</a></li>
     <li><a href="/distrib/current/stdlib/">Standard Library</a></li>
+    <li><a href="/distrib/current/refman/changes.html">Changelog</a></li>
   </ul>
 </div>
 
@@ -119,7 +125,7 @@
 <div class="frameworkcontent">
 
 <p>The following provide shorter introductions to Coq or specific
-topics, and may be targetted to beginners or more advanced users:</p>
+topics, and may be targeted to beginners or more advanced users:</p>
 
 <ul>
 
@@ -174,7 +180,7 @@
 <div class="frameworklabel">Other documentation</div>
 
 <div class="frameworkcontent">
-<p>Some additional ressources:</p>
+<p>Some additional resources:</p>
 
 <ul>
 

pages/download.html

@@ -1,54 +1,68 @@
 <#include "incl/macros.html">
-<#def TITLE>Coq <#CURRENTVERSION></#def>
+<#def TITLE>Install Coq</#def>
 <#include "incl/header.html">
 
 <div class="framework">
-<div class="frameworklabel">The current version: Coq <#CURRENTVERSION>
+<div class="frameworklabel">The Coq platform
 </div>
 <div class="frameworkcontent">
 
-<p>For downloads (in particular to get installers for Windows and Mac OS, the PDF
-  manual, or a tarball of the sources), please go to
-  <a href="<#CURRENTVERSIONURL>">the release page on GitHub</a>.</p>
+<p>Coq has a rich ecosystem of external packages (libraries and
+plugins) that extend it and make it more powerful.
+The <a href="https://github.com/coq/platform">Coq platform</a>
+provides an easy way to install Coq and a consistent set of packages
+on Windows, macOS and many Linux distributions.</p>
+
+<p>Beginners are encouraged to use one of the binary installers: we
+provide <a href="https://github.com/coq/coq/releases/latest">binary
+installers</a> for Windows and
+a <a href="https://snapcraft.io/coq-prover">Snap package</a>
+compatible with many Linux distributions. A macOS installer for the
+platform is in the works. In the meantime, a macOS installer for just
+Coq + CoqIDE is provided.</p>
+
+<p>Experienced users are advised to run the scripts provided by
+the <a href="https://github.com/coq/platform">Coq platform</a> to
+install from sources as this will allow them to add additional
+packages by <a href="/opam-using.html">using opam</a>.</p>
 
 </div>
 <div class="frameworklinks">
 <ul>
-<li><a href="<#CURRENTVERSIONURL>">Stable release (<#CURRENTVERSION>)</a></li>
-<#ifdef UPCOMINGVERSION>
-<li><a href="<#UPCOMINGVERSIONURL>">Testing release (<#UPCOMINGVERSION>)</a></li>
-</#ifdef>
+<li><a href="https://github.com/coq/coq/releases/latest">Binary installers (Windows and macOS)</a></li>
+<li><a href="https://snapcraft.io/coq-prover">Snap package</a></li>
+<li><a href="https://github.com/coq/platform">Platform scripts</a>
 </ul>
 </div>
 </div>
 
+
 <div class="framework">
-<div class="frameworklabel">How to install Coq on various systems</div>
+<div class="frameworklabel">Other installation methods
+</div>
 <div class="frameworkcontent">
 
-<p>
-The Coq wiki contains three helpful pages detailing various ways of
-installing Coq for the three most standard operating systems:
-</p>
+<p>Coq is available
+through <a href="https://repology.org/metapackage/coq/versions">many
+package managers</a>, including most Linux distribution package
+managers.  However, in many cases, the available version is not
+the latest version.  More importantly, these distributions might
+provide only a fraction of all the external packages available for
+Coq, thus requiring some manual compilation and installation to add
+additional packages.</p>
 
-<ul>
-<li><a href="https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Linux">Linux</a>
-<li><a href="https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Windows">Windows</a>
-<li><a href="https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Mac">MacOS</a>
-</ul>
+<p>Advanced users who want to install Coq and extend it with external
+packages can rely on <a href="/opam-using.html">opam</a>
+or <a href="https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq">Nix</a>.</p>
 
-<p>
-The Coq website also contains a page with instructions on
-<a href="/opam-using.html">how to install Coq and related packages via opam</a>.
-</p>
+<p>Coq is also available as a <a href="https://hub.docker.com/r/coqorg/coq/">Docker image</a>.</p>
 
 </div>
 <div class="frameworklinks">
 <ul>
-<li><a class="extlink" href="https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Linux">Linux</a></li>
-<li><a class="extlink" href="https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Windows">Windows</a></li>
-<li><a class="extlink" href="https://github.com/coq/coq/wiki/Installation%20of%20Coq%20on%20Mac">MacOS</a></li>
-<li><a href="/opam-using.html">opam</a></li>
+<li><a href="/opam-using.html">Using opam</a></li>
+<li><a href="https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq">Nixpkgs manual section on Coq</a></li>
+<li><a href="https://hub.docker.com/r/coqorg/coq/">Docker images</a></li>
 </ul>
 </div>
 </div>
@@ -57,20 +71,24 @@
 <div class="frameworklabel">Previous and development versions of Coq </div>
 <div class="frameworkcontent">
 
-<p>The development version of Coq is <a href="https://github.com/coq/coq">browsable</a>
-and downloadable from our Git repository using command:
-<tt>git clone https://github.com/coq/coq.git</tt>.
+<p>The development version of Coq and its development history can be
+browsed in its <a href="https://github.com/coq/coq">GitHub
+repository</a>.
 </p>
 
-<p>Most of the previous versions of Coq are available <a href="<#RELEASES>">on
-GitHub</a> or <a href="/distrib/">here</a>.</p>
+<p>When you upgrade your version of Coq, be sure to read
+the <a href="/distrib/current/refman/changes.html">changelog</a>.
+
+<p>Most previous versions of Coq are
+available <a href="https://github.com/coq/coq/releases">on GitHub</a>
+or <a href="/distrib/">here</a>.</p>
 
 </div>
 <div class="frameworklinks">
 <ul>
 <li><a class="extlink" href="https://github.com/coq/coq">GitHub repository</a></li>
-<li><a class="extlink" href="<#RELEASES>">All GitHub releases</a></li>
-<li><a href="/distrib/">Old releases</a></li>
+<li><a class="extlink" href="https://github.com/coq/coq/releases">All GitHub releases</a></li>
+<li><a href="/distrib/">Very old releases</a></li>
 </ul>
 </div>
 </div>