# HG changeset patch # User wenzelm # Date 1705752651 -3600 # Node ID 3225f823b337377134a0fb958f402d813dbf9059 # Parent 4d82b743c5e1319693ba922ad378a5dc0a57e042 more accurate Isabelle versions; diff -r 4d82b743c5e1 -r 3225f823b337 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Jan 20 13:01:30 2024 +0100 +++ b/src/Doc/JEdit/JEdit.thy Sat Jan 20 13:10:51 2024 +0100 @@ -304,7 +304,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>\Isabelle2022\). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\Isabelle2023\). 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 4d82b743c5e1 -r 3225f823b337 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Sat Jan 20 13:01:30 2024 +0100 +++ b/src/Doc/System/Environment.thy Sat Jan 20 13:10:51 2024 +0100 @@ -56,7 +56,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/Isabelle2022\. + usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2023\. Thus individual users may override the site-wide defaults. Typically, a user settings file contains only a few lines, with some assignments that @@ -135,7 +135,7 @@ of the @{executable isabelle} executable. \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\\<^sup>*\] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2022\''. + Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2024Isabelle2023\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] diff -r 4d82b743c5e1 -r 3225f823b337 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Sat Jan 20 13:01:30 2024 +0100 +++ b/src/Doc/System/Misc.thy Sat Jan 20 13:10:51 2024 +0100 @@ -71,7 +71,7 @@ \<^medskip> Option \<^verbatim>\-B\ specifies the Docker image taken as starting point for the Isabelle installation: it needs to be a suitable version of Ubuntu Linux, - see also \<^url>\https://hub.docker.com/_/ubuntu\. The default for Isabelle2022 + see also \<^url>\https://hub.docker.com/_/ubuntu\. The default for Isabelle2023 is \<^verbatim>\ubuntu:22.04\, but other versions often work as well, after some experimentation with packages. @@ -106,22 +106,22 @@ Produce a Dockerfile (without image) from a remote Isabelle distribution: @{verbatim [display] \ isabelle docker_build -E -n -o Dockerfile - https://isabelle.in.tum.de/website-Isabelle2022/dist/Isabelle2022_linux.tar.gz\} + https://isabelle.in.tum.de/website-Isabelle2023/dist/Isabelle2023_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 docker_build -E -t test/isabelle:Isabelle2022 Isabelle2022_linux.tar.gz\} +\ isabelle docker_build -E -t test/isabelle:Isabelle2023 Isabelle2023_linux.tar.gz\} Invoke the raw Isabelle/ML process within that image: @{verbatim [display] -\ docker run test/isabelle:Isabelle2022 process -e "Session.welcome ()"\} +\ docker run test/isabelle:Isabelle2023 process -e "Session.welcome ()"\} Invoke a Linux command-line tool within the contained Isabelle system environment: @{verbatim [display] -\ docker run test/isabelle:Isabelle2022 env uname -a\} +\ docker run test/isabelle:Isabelle2023 env uname -a\} The latter should always report a Linux operating system, even when running on Windows or macOS. \ @@ -454,7 +454,7 @@ \<^medskip> The default is to output the full version string of the Isabelle - distribution, e.g.\ ``\<^verbatim>\Isabelle2022: October 2022\. + distribution, e.g.\ ``\<^verbatim>\Isabelle2023: September 2023\. \<^medskip> Option \<^verbatim>\-i\ produces a short identification derived from the Mercurial id