# HG changeset patch # User wenzelm # Date 1610981195 -3600 # Node ID c9a836122739cfc54a08fc193a7f5331e083fce7 # Parent bdc8cd6f5e6e6987ae9ad4070261e3d0e3bc74dd updated for release; diff -r bdc8cd6f5e6e -r c9a836122739 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Mon Jan 18 15:22:17 2021 +0100 +++ b/src/Doc/JEdit/JEdit.thy Mon Jan 18 15:46:35 2021 +0100 @@ -305,7 +305,7 @@ The \<^verbatim>\-n\ option reports the server name, and the \<^verbatim>\-s\ option provides a different server name. The default server name is the official distribution - name (e.g.\ \<^verbatim>\Isabelle2020\). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\Isabelle2021\). Thus @{tool jedit_client} can connect to the Isabelle desktop application without further options. The \<^verbatim>\-p\ option allows to override the implicit default of the system diff -r bdc8cd6f5e6e -r c9a836122739 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Mon Jan 18 15:22:17 2021 +0100 +++ b/src/Doc/System/Environment.thy Mon Jan 18 15:46:35 2021 +0100 @@ -58,7 +58,7 @@ \<^enum> The file \<^path>\$ISABELLE_HOME_USER/etc/settings\ (if it exists) is run in the same way as the site default settings. Note that the variable @{setting ISABELLE_HOME_USER} has already been set before --- - usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2020\. + usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2021\. Thus individual users may override the site-wide defaults. Typically, a user settings file contains only a few lines, with some assignments that @@ -148,7 +148,7 @@ of the @{executable isabelle} executable. \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\\<^sup>*\] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2020\''. + Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2021\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] diff -r bdc8cd6f5e6e -r c9a836122739 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Mon Jan 18 15:22:17 2021 +0100 +++ b/src/Doc/System/Misc.thy Mon Jan 18 15:46:35 2021 +0100 @@ -71,7 +71,7 @@ Isabelle installation: it needs to be a suitable version of Ubuntu Linux. The default \<^verbatim>\ubuntu\ refers to the latest LTS version provided by Canonical as the official Ubuntu vendor\<^footnote>\\<^url>\https://hub.docker.com/_/ubuntu\\. For - Isabelle2020 this should be Ubuntu 18.04 LTS. + Isabelle2021 this should be Ubuntu 20.04 LTS. Option \<^verbatim>\-p\ includes additional Ubuntu packages, using the terminology of \<^verbatim>\apt-get install\ within the underlying Linux distribution. @@ -98,22 +98,22 @@ Produce a Dockerfile (without image) from a remote Isabelle distribution: @{verbatim [display] \ isabelle build_docker -E -n -o Dockerfile - https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020_linux.tar.gz\} + https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz\} Build a standard Isabelle Docker image from a local Isabelle distribution, with \<^verbatim>\bin/isabelle\ as executable entry point: @{verbatim [display] -\ isabelle build_docker -E -t test/isabelle:Isabelle2020 Isabelle2020_linux.tar.gz\} +\ isabelle build_docker -E -t test/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz\} Invoke the raw Isabelle/ML process within that image: @{verbatim [display] -\ docker run test/isabelle:Isabelle2020 process -e "Session.welcome ()"\} +\ docker run test/isabelle:Isabelle2021 process -e "Session.welcome ()"\} Invoke a Linux command-line tool within the contained Isabelle system environment: @{verbatim [display] -\ docker run test/isabelle:Isabelle2020 env uname -a\} +\ docker run test/isabelle:Isabelle2021 env uname -a\} The latter should always report a Linux operating system, even when running on Windows or macOS. \ @@ -357,7 +357,7 @@ \<^medskip> The default is to output the full version string of the Isabelle - distribution, e.g.\ ``\<^verbatim>\Isabelle2020: April 2020\. + distribution, e.g.\ ``\<^verbatim>\Isabelle2021: February 2021\. The \<^verbatim>\-i\ option produces a short identification derived from the Mercurial id of the @{setting ISABELLE_HOME} directory.