--- a/.hgtags Fri Apr 26 13:25:44 2024 +0200
+++ b/.hgtags Fri May 03 00:07:51 2024 +0200
@@ -45,3 +45,4 @@
98f009f56400c7317d26d96cf7d904cc984b1d46 Isabelle2024-RC0
1231a7fb251017c2acec4bda2bb036d4f052542c Isabelle2024-RC1
ef2134570abb6090fa65107661ec8c3f4ffc06e0 Isabelle2024-RC2
+007e6af8a02082e82a6a642a3d5b1649628a50c2 Isabelle2024-RC3
--- a/Admin/components/bundled Fri Apr 26 13:25:44 2024 +0200
+++ b/Admin/components/bundled Fri May 03 00:07:51 2024 +0200
@@ -1,2 +1,2 @@
#additional components to be bundled for release
-#naproche-20230902
+naproche-20240502
--- a/Admin/components/components.sha1 Fri Apr 26 13:25:44 2024 +0200
+++ b/Admin/components/components.sha1 Fri May 03 00:07:51 2024 +0200
@@ -98,7 +98,9 @@
813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz
6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz
a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz
+8744880925dbc95c3977f58b7d6da64a3bd6de6a e-3.0.03-1.tar.gz
230d01c2c7274a17b6410535eb41665b16b41ae6 e-3.0.03.tar.gz
+4e436e450775bd971b3247c97d4bba7943ae4762 e-3.1.tar.gz
239e7b8bebbfc29a1c5151e8fb261ffad44877f1 easychair-3.5.tar.gz
4a3b4b4e0441c4498a0c71dc348f3538be589a15 eptcs-1.7.0.tar.gz
6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
@@ -239,6 +241,7 @@
258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz
+fbfd1d8a117a5bd844f230903d561cb88d3e5189 jedit-20240425.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
@@ -334,6 +337,8 @@
c66f5ce13d429ea9c8dcc0d33d34b7abf178da5d naproche-20221024.tar.gz
8e6cb32312336abcfe488b718bdc621461a7f132 naproche-20230711.tar.gz
3a310253f003f1759b575823f2a2e116ff6edeac naproche-20230902.tar.gz
+f1a9ff4c08c1d226eb1994509254a0b9624f4c52 naproche-20240501.tar.gz
+91ac689e9f7fbd69dd49089bc82904b7f5a290cf naproche-20240502.tar.gz
d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
--- a/Admin/components/main Fri Apr 26 13:25:44 2024 +0200
+++ b/Admin/components/main Fri May 03 00:07:51 2024 +0200
@@ -4,7 +4,7 @@
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
-e-3.0.03
+e-3.0.03-1
easychair-3.5
eptcs-1.7.0
flatlaf-2.6
@@ -14,7 +14,7 @@
isabelle_setup-20240327
javamail-20240109
jdk-21.0.3
-jedit-20231120
+jedit-20240425
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.17.2
--- a/src/Doc/JEdit/JEdit.thy Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri May 03 00:07:51 2024 +0200
@@ -304,7 +304,7 @@
The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
different server name. The default server name is the official distribution
- name (e.g.\ \<^verbatim>\<open>Isabelle2023\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2024\<close>). Thus @{tool jedit_client} can connect to the
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
--- a/src/Doc/System/Environment.thy Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Doc/System/Environment.thy Fri May 03 00:07:51 2024 +0200
@@ -56,7 +56,7 @@
\<^enum> The file \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close> (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>\<open>$USER_HOME/.isabelle/Isabelle2023\<close>.
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2024\<close>.
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}\<open>\<^sup>*\<close>] refers to the name of this
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2024Isabelle2023\<close>''.
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2024\<close>''.
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
@@ -174,7 +174,7 @@
is \<^path>\<open>$ISABELLE_HOME/heaps\<close>. See also \secref{sec:tool-build}.
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
- is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
+ is given explicitly by the user. The default value is \<^verbatim>\<open>HOL\<close>.
\<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
@{tool_ref console} interface.
@@ -449,6 +449,75 @@
\<close>
+section \<open>System registry via TOML\<close>
+
+text \<open>
+ Tools implemented in Isabelle/Scala may refer to a global registry of
+ hierarchically structured values, which is based on a collection of TOML
+ files. TOML is conceptually similar to JSON, but aims at human-readable
+ syntax.
+
+ The recursive structure of a TOML \<^emph>\<open>value\<close> is defined as follows:
+ \<^enum> atom: string, integer, float, bool, date (ISO-8601)
+ \<^enum> array: sequence of \<^emph>\<open>values\<close> \<open>t\<close>, written \<^verbatim>\<open>[\<close>\<open>t\<^sub>1\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>,\<close>\<open>t\<^sub>n\<close>\<^verbatim>\<open>]\<close>
+ \<^enum> table: mapping from \<^emph>\<open>names\<close> \<open>a\<close> to \<^emph>\<open>values\<close> \<open>t\<close>, written
+ \<^verbatim>\<open>{\<close>\<open>a\<^sub>1\<close>\<^verbatim>\<open>=\<close>\<open>t\<^sub>1\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>,\<close>\<open>a\<^sub>n\<close>\<^verbatim>\<open>=\<close>\<open>t\<^sub>n\<close>\<^verbatim>\<open>}\<close>
+
+ There are various alternative syntax forms for convenience, e.g. to
+ construct a table of tables, using \<^emph>\<open>header syntax\<close> that resembles
+ traditional \<^verbatim>\<open>.INI\<close>-file notation. For example:
+ @{verbatim [display, indent = 2]
+ \<open>[point.A]
+x = 1
+y = 1
+description = "one point"
+
+[point.B]
+x = 2
+y = -2
+description = "another point"
+
+[point.C]
+x = 3
+y = 7
+description = "yet another point"
+\<close>}
+
+ Or alternatively like this:
+ @{verbatim [display, indent = 2]
+ \<open>point.A.x = 1
+point.A.y = 1
+point.A.description = "one point"
+
+point.B.x = 2
+point.B.y = -2
+point.B.description = "another point"
+
+point.C.x = 3
+point.C.y = 7
+point.C.description = "yet another point"
+\<close>}
+
+ The TOML website\<^footnote>\<open>\<^url>\<open>https://toml.io/en/v1.0.0\<close>\<close> provides many examples,
+ together with the full language specification. Note that the Isabelle/Scala
+ implementation of TOML uses the default ISO date/time format of
+ Java.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/time/format/DateTimeFormatter.html\<close>\<close>
+
+ \<^medskip>
+ The overall system registry is collected from \<^verbatim>\<open>registry.toml\<close> files in
+ directories specified via the settings variable @{setting
+ "ISABELLE_REGISTRY"}: this refers to \<^path>\<open>$ISABELLE_HOME\<close> and
+ \<^path>\<open>$ISABELLE_HOME_USER\<close> by default, but further directories may be
+ specified via the GNU bash function \<^bash_function>\<open>isabelle_registry\<close>
+ within \<^path>\<open>etc/settings\<close> of Isabelle components.
+
+ The result is available as Isabelle/Scala object
+ \<^scala>\<open>isabelle.Registry.global\<close>. That is empty by default, unless users
+ populate \<^path>\<open>$ISABELLE_HOME_USER/etc/registry.toml\<close> or provide other
+ component \<^path>\<open>etc/registry.toml\<close> files.
+\<close>
+
+
section \<open>YXML versus XML \label{sec:yxml-vs-xml}\<close>
text \<open>
--- a/src/Doc/System/Misc.thy Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Doc/System/Misc.thy Fri May 03 00:07:51 2024 +0200
@@ -71,18 +71,19 @@
\<^medskip>
Option \<^verbatim>\<open>-B\<close> 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>\<open>https://hub.docker.com/_/ubuntu\<close>. The default for Isabelle2023
- is \<^verbatim>\<open>ubuntu:22.04\<close>, but other versions often work as well, after some
- experimentation with packages.
+ see also \<^url>\<open>https://hub.docker.com/_/ubuntu\<close>. The default for Isabelle2024
+ is \<^verbatim>\<open>ubuntu:22.04\<close>, but \<^verbatim>\<open>ubuntu:20.04\<close> and \<^verbatim>\<open>ubuntu:24.04\<close> should work as
+ well. Other versions might require experimentation with the package
+ selection.
Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as
- provided by \<^verbatim>\<open>isabelle docker_build\<close> (assuming Ubuntu 22.04 LTS). This
- imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will
- only provide remote X11 support according to the modest GUI quality
- standards of the late 1990-ies.
+ provided by \<^verbatim>\<open>isabelle docker_build\<close> (assuming Ubuntu 20.04/22.04/24.04
+ LTS). This imposes extra weight on the resulting Docker images. Note that
+ \<^verbatim>\<open>X11\<close> will only provide remote X11 support according to the modest GUI
+ quality standards of the late 1990-ies.
\<^medskip>
Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close>
@@ -106,22 +107,22 @@
Produce a Dockerfile (without image) from a remote Isabelle distribution:
@{verbatim [display]
\<open> isabelle docker_build -E -n -o Dockerfile
- https://isabelle.in.tum.de/website-Isabelle2023/dist/Isabelle2023_linux.tar.gz\<close>}
+ https://isabelle.in.tum.de/website-Isabelle2024/dist/Isabelle2024_linux.tar.gz\<close>}
Build a standard Isabelle Docker image from a local Isabelle distribution,
with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
@{verbatim [display]
-\<open> isabelle docker_build -E -t test/isabelle:Isabelle2023 Isabelle2023_linux.tar.gz\<close>}
+\<open> isabelle docker_build -E -t test/isabelle:Isabelle2024 Isabelle2024_linux.tar.gz\<close>}
Invoke the raw Isabelle/ML process within that image:
@{verbatim [display]
-\<open> docker run test/isabelle:Isabelle2023 process -e "Session.welcome ()"\<close>}
+\<open> docker run test/isabelle:Isabelle2024 process -e "Session.welcome ()"\<close>}
Invoke a Linux command-line tool within the contained Isabelle system
environment:
@{verbatim [display]
-\<open> docker run test/isabelle:Isabelle2023 env uname -a\<close>}
+\<open> docker run test/isabelle:Isabelle2024 env uname -a\<close>}
The latter should always report a Linux operating system, even when running
on Windows or macOS.
\<close>
@@ -454,7 +455,7 @@
\<^medskip>
The default is to output the Isabelle distribution name, e.g.\
- ``\<^verbatim>\<open>Isabelle2023\<close>''.
+ ``\<^verbatim>\<open>Isabelle2024\<close>''.
\<^medskip>
Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id
--- a/src/HOL/Tools/etc/options Fri Apr 26 13:25:44 2024 +0200
+++ b/src/HOL/Tools/etc/options Fri May 03 00:07:51 2024 +0200
@@ -32,7 +32,7 @@
public option sledgehammer_timeout : int = 30
-- "provers will be interrupted after this time (in seconds)"
-public option SystemOnTPTP : string = "https://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
+public option SystemOnTPTP : string = "https://tptp.org/cgi-bin/SystemOnTPTPFormReply"
-- "URL for SystemOnTPTP service"
public option MaSh : string = "sml"
--- a/src/Pure/Admin/build_release.scala Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Pure/Admin/build_release.scala Fri May 03 00:07:51 2024 +0200
@@ -759,6 +759,10 @@
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
+ execute(isabelle_target,
+ """find . -type d -not -perm """ +
+ (if (Platform.is_macos) "+" else "/") + """222 -exec chmod +w "{}" ";" """)
+
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
--- a/src/Pure/Admin/component_e.scala Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Pure/Admin/component_e.scala Fri May 03 00:07:51 2024 +0200
@@ -10,7 +10,7 @@
object Component_E {
/* build E prover */
- val default_version = "3.0.03"
+ val default_version = "3.1"
val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
def build_e(
@@ -19,6 +19,8 @@
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
+ Isabelle_System.require_command("patch")
+
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
/* component */
@@ -84,11 +86,11 @@
File.write(component_dir.README,
"This is E prover " + version + " from\n" + archive_url + """
-The distribution has been built like this:
+* The distribution has been built like this:
cd src && """ + build_script + """
-Only a few executables from PROVERS/ have been moved to the platform-specific
+* Some executables from PROVERS/ have been moved to the platform-specific
Isabelle component directory: x86_64-linux etc.
--- a/src/Pure/Build/build.scala Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Pure/Build/build.scala Fri May 03 00:07:51 2024 +0200
@@ -121,7 +121,7 @@
def build_options(options: Options, build_cluster: Boolean = false): Options = {
val options1 = options + "completion_limit=0" + "editor_tracing_messages=0"
- if (build_cluster) options1 + "build_database" + "build_log_verbose" else options1
+ if (build_cluster) options1 + "build_database" + "build_database_server" + "build_log_verbose" else options1 // FIXME tmp: build_database_server
}
final def build_store(options: Options,
--- a/src/Pure/System/linux.scala Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Pure/System/linux.scala Fri May 03 00:07:51 2024 +0200
@@ -42,6 +42,7 @@
def is_ubuntu: Boolean = id == "Ubuntu"
def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04"
def is_ubuntu_22_04: Boolean = is_ubuntu && release == "22.04"
+ def is_ubuntu_24_04: Boolean = is_ubuntu && release == "24.04"
}
--- a/src/Tools/jEdit/patches/extended_styles_brackets Fri Apr 26 13:25:44 2024 +0200
+++ b/src/Tools/jEdit/patches/extended_styles_brackets Fri May 03 00:07:51 2024 +0200
@@ -1,6 +1,6 @@
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-04-25 12:56:22.208257322 +0200
@@ -332,9 +332,9 @@
//{{{ Package private members
@@ -24,6 +24,18 @@
private GlyphData glyphData;
//}}}
+@@ -926,6 +926,11 @@
+ }
+
+ @Override
++ public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
++ synchronized (this) { return super.computeIfAbsent(key, f); }
++ }
++
++ @Override
+ protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
+ {
+ return size() > capacity;
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2023-11-20 15:31:55.825519645 +0100