--- a/NEWS Sat Jun 14 14:37:34 2025 +0200
+++ b/NEWS Sat Jun 14 17:10:18 2025 +0200
@@ -302,6 +302,11 @@
*** System ***
+* The traditional ML system settings have been reconsidered: this
+affects ML_IDENTIFIER (discontinued). Potential INCOMPATIBILITY for old
+shell scripts --- better use Isabelle/Scala operations from module
+ML_Process or Store.
+
* System option "record_theories" tells "isabelle build" to record
intermediate theory commands and results, at the cost of approx. 5 times
larger ML heap images. This allows to retrieve fine-grained semantic
--- a/lib/scripts/getsettings Sat Jun 14 14:37:34 2025 +0200
+++ b/lib/scripts/getsettings Sat Jun 14 17:10:18 2025 +0200
@@ -103,13 +103,6 @@
;;
esac
-#ML system identifier
-if [ -z "$ML_PLATFORM" ]; then
- ML_IDENTIFIER="$ML_SYSTEM"
-else
- ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
-fi
-
#enforce ISABELLE_OCAMLFIND
if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then
ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind"
--- a/src/Doc/System/Environment.thy Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Doc/System/Environment.thy Sat Jun 14 17:10:18 2025 +0200
@@ -138,18 +138,13 @@
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2025\<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>]
- specify the underlying ML system to be used for Isabelle. There is only a
- fixed set of admissable @{setting ML_SYSTEM} names (see the
- \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
+ ML_OPTIONS}, @{setting_def ML_PLATFORM}] specify the underlying ML system of
+ Isabelle.
The actual compiler binary will be run from the directory @{setting
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
- images, which is useful for cross-platform installations. The value of
- @{setting ML_IDENTIFIER} is automatically obtained by composing the values
- of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
- values.
+ images, which is useful for cross-platform installations.
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development
Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. Note that
--- a/src/Pure/Admin/build_history.scala Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Jun 14 17:10:18 2025 +0200
@@ -204,9 +204,7 @@
File.write(other_isabelle.etc_preferences,
cat_lines("build_log_verbose = true" :: more_preferences))
- val isabelle_output =
- other_isabelle.expand_path(
- Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER"))
+ val isabelle_output = other_isabelle.user_output_dir
val isabelle_output_log = isabelle_output + Path.explode("log")
val isabelle_base_log = isabelle_output + Path.explode("../base_log")
--- a/src/Pure/Build/build.scala Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/Build/build.scala Sat Jun 14 17:10:18 2025 +0200
@@ -31,7 +31,6 @@
engine: Engine = Engine.Default,
afp_root: Option[Path] = None,
build_hosts: List[Build_Cluster.Host] = Nil,
- ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
hostname: String = Isabelle_System.hostname(),
numa_shuffling: Boolean = false,
numa_nodes: List[Int] = Nil,
@@ -47,6 +46,8 @@
) {
def build_options: Options = store.options
+ def ml_platform: String = store.ml_platform
+
def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure
def worker: Boolean = jobs > 0
--- a/src/Pure/Build/store.scala Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/Build/store.scala Sat Jun 14 17:10:18 2025 +0200
@@ -14,8 +14,9 @@
def apply(
options: Options,
build_cluster: Boolean = false,
- cache: Term.Cache = Term.Cache.make()
- ): Store = new Store(options, build_cluster, cache)
+ cache: Term.Cache = Term.Cache.make(),
+ other_ml_platform: Option[String] = None
+ ): Store = new Store(options, build_cluster, cache, other_ml_platform)
/* file names */
@@ -277,17 +278,25 @@
class Store private(
val options: Options,
val build_cluster: Boolean,
- val cache: Term.Cache
+ val cache: Term.Cache,
+ other_ml_platform: Option[String]
) {
store =>
override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
+ /* ML system */
+
+ def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM")
+ def ml_platform: String = other_ml_platform getOrElse Isabelle_System.getenv_strict("ML_PLATFORM")
+ def ml_identifier: String = ml_system + "_" + ml_platform
+
+
/* directories */
- val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
- val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
+ val system_output_dir: Path = Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_identifier)
+ val user_output_dir: Path = Path.variable("ISABELLE_HEAPS") + Path.basic(ml_identifier)
def system_heaps: Boolean = options.bool("system_heaps")
--- a/src/Pure/ML/ml_process.scala Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/ML/ml_process.scala Sat Jun 14 17:10:18 2025 +0200
@@ -14,7 +14,8 @@
/* settings */
def ml_identifier(env: Isabelle_System.Settings = Isabelle_System.Settings()): String =
- Isabelle_System.getenv("ML_IDENTIFIER", env = env)
+ Isabelle_System.getenv_strict("ML_SYSTEM", env = env) + "_" +
+ Isabelle_System.getenv_strict("ML_PLATFORM", env = env)
/* heaps */
--- a/src/Pure/System/other_isabelle.scala Sat Jun 14 14:37:34 2025 +0200
+++ b/src/Pure/System/other_isabelle.scala Sat Jun 14 17:10:18 2025 +0200
@@ -73,8 +73,12 @@
def expand_path(path: Path): Path = path.expand_env(settings)
def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
+ def ml_identifier: String = ML_Process.ml_identifier(env = settings)
+
val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
+ def user_output_dir: Path = isabelle_home_user + Path.basic("heaps") + Path.basic(ml_identifier)
+
def host_db: Path = isabelle_home_user + Path.explode("host.db")
def etc: Path = isabelle_home_user + Path.explode("etc")