--- a/etc/settings Fri Jan 24 17:53:17 2025 +0000
+++ b/etc/settings Fri Jan 24 21:24:42 2025 +0000
@@ -16,8 +16,8 @@
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
-ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 17 -target 17"
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -java-output-version 17 -source 3.3 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m"
+ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 21 -target 21"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -java-output-version 21 -source 3.3 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m"
ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar"
--- a/src/Pure/Admin/component_hol_light.scala Fri Jan 24 17:53:17 2025 +0000
+++ b/src/Pure/Admin/component_hol_light.scala Fri Jan 24 21:24:42 2025 +0000
@@ -35,6 +35,8 @@
if (!only_offline) {
Linux.check_system()
+ Isabelle_System.require_command("bzip2")
+ Isabelle_System.require_command("m4")
Isabelle_System.require_command("patch")
Isabelle_System.require_command("zstd")
}
@@ -121,7 +123,7 @@
Isabelle_System.copy_dir(hol_import_dir + offline_path, offline_dir, direct = true)
- progress.bash("ocamlopt offline.ml -o offline",
+ progress.bash("ocamlc.opt offline.ml -o offline",
cwd = offline_dir, echo = progress.verbose).check
Isabelle_System.copy_file(offline_dir + offline_exe, platform_dir + offline_exe)
File.set_executable(platform_dir + offline_exe)
@@ -231,6 +233,9 @@
isabelle component_hol_light_import -L Logic/make.ml
isabelle component_hol_light_import -L 100/thales.ml -L 100/ceva.ml
+
+ The HOL Light build process uses OCaml/OPAM from Isabelle; this requires
+ C development tools with libgmp-dev.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"L:" -> (arg => load_more = load_more ::: List(Path.explode(arg))),
--- a/src/Pure/ROOT.ML Fri Jan 24 17:53:17 2025 +0000
+++ b/src/Pure/ROOT.ML Fri Jan 24 21:24:42 2025 +0000
@@ -1,6 +1,6 @@
(* Title: Pure/ROOT.ML
Author: Makarius
- UUID: 3d6bbaf8-645c-4431-ba30-9b864c20b009
+ UUID: d6fc404b-eeef-4ad0-964d-14b9310ea78f
Main entry point for the Isabelle/Pure bootstrap process.
--- a/src/Pure/ROOT.scala Fri Jan 24 17:53:17 2025 +0000
+++ b/src/Pure/ROOT.scala Fri Jan 24 21:24:42 2025 +0000
@@ -1,6 +1,6 @@
/* Title: Pure/ROOT.scala
Author: Makarius
- UUID: 3d6bbaf8-645c-4431-ba30-9b864c20b009
+ UUID: d6fc404b-eeef-4ad0-964d-14b9310ea78f
Root of isabelle package.
*/
--- a/src/Tools/jEdit/jedit_base/plugin.props Fri Jan 24 17:53:17 2025 +0000
+++ b/src/Tools/jEdit/jedit_base/plugin.props Fri Jan 24 21:24:42 2025 +0000
@@ -13,5 +13,5 @@
plugin.isabelle.jedit_base.Plugin.usePluginHome=false
#dependencies
-plugin.isabelle.jedit_base.Plugin.depend.0=jdk 17
-plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
+plugin.isabelle.jedit_base.Plugin.depend.0=jdk 21
+plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.06.00.00
--- a/src/Tools/jEdit/jedit_main/plugin.props Fri Jan 24 17:53:17 2025 +0000
+++ b/src/Tools/jEdit/jedit_main/plugin.props Fri Jan 24 21:24:42 2025 +0000
@@ -5,7 +5,7 @@
#identification
plugin.isabelle.jedit_main.Plugin.name=Isabelle
plugin.isabelle.jedit_main.Plugin.author=Johannes H\u00F6lzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
-plugin.isabelle.jedit_main.Plugin.version=11.3
+plugin.isabelle.jedit_main.Plugin.version=12.0
plugin.isabelle.jedit_main.Plugin.description=Isabelle/jEdit main plugin
#system parameters
@@ -13,7 +13,7 @@
plugin.isabelle.jedit_main.Plugin.usePluginHome=false
#dependencies
-plugin.isabelle.jedit_main.Plugin.depend.0=jdk 17
+plugin.isabelle.jedit_main.Plugin.depend.0=jdk 21
plugin.isabelle.jedit_main.Plugin.depend.1=jedit 05.06.00.00
plugin.isabelle.jedit_main.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
plugin.isabelle.jedit_main.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.4.0