--- a/NEWS Mon Jun 16 12:18:26 2025 +0200
+++ b/NEWS Mon Jun 16 12:19:23 2025 +0200
@@ -322,6 +322,10 @@
isabelle build -o ML_system_64 -b HOL
isabelle jedit -o ML_system_64
+* System option "ML_platform" specifies the underlying Poly/ML platform
+identifier explicitly: it takes precedence over all other options and
+settings to determine the ML_PLATFORM (see above).
+
* 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/etc/options Mon Jun 16 12:18:26 2025 +0200
+++ b/etc/options Mon Jun 16 12:19:23 2025 +0200
@@ -180,6 +180,9 @@
public option ML_debugger : bool = false
-- "ML debugger instrumentation for newly compiled code"
+public option ML_platform : string = "" for build build_sync
+ -- "explicit ML platform identifier"
+
public option ML_system_64 : bool = false for build build_sync
-- "prefer native 64bit platform (change requires restart)"
--- a/src/Pure/ML/ml_settings.scala Mon Jun 16 12:18:26 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala Mon Jun 16 12:19:23 2025 +0200
@@ -15,6 +15,7 @@
override def polyml_home: Path = Path.variable("POLYML_HOME").expand_env(env)
override def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM", env = env)
override def ml_platform: String = {
+ proper_string(options.string("ML_platform")) orElse
proper_string(Isabelle_System.getenv("ML_PLATFORM", env = env)) getOrElse {
val platform_64 =
Isabelle_Platform.make(env = env)