--- a/NEWS Thu Mar 02 15:55:20 2023 +0100
+++ b/NEWS Thu Mar 02 16:09:22 2023 +0100
@@ -259,6 +259,10 @@
scalable, and supports most options from "isabelle build". Partial
builds are supported as well, e.g. "isabelle update -n -a".
+* System option "ML_process_policy" has been renamed to
+"process_policy", as it may affect other processes as well (notably in
+"isabelle build").
+
* Isabelle/Scala provides generic support for XZ and Zstd compression,
via Compress.Options and Compress.Cache. Bytes.uncompress automatically
detects the compression scheme.
--- a/etc/options Thu Mar 02 15:55:20 2023 +0100
+++ b/etc/options Thu Mar 02 16:09:22 2023 +0100
@@ -132,6 +132,9 @@
option timeout_build : bool = true
-- "observe timeout for session build"
+option process_policy : string = ""
+ -- "command prefix for underlying process, notably ML with NUMA policy"
+
option process_output_tail : int = 40
-- "build process output tail shown to user (in lines, 0 = unlimited)"
@@ -165,9 +168,6 @@
public option ML_system_apple : bool = true
-- "prefer native Apple/ARM64 platform (change requires restart)"
-public option ML_process_policy : string = ""
- -- "ML process command prefix (process policy)"
-
section "Build Process"
--- a/src/Doc/JEdit/JEdit.thy Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Mar 02 16:09:22 2023 +0100
@@ -243,7 +243,7 @@
-l NAME logic image name
-m MODE add print mode for output
-n no build of session image on startup
- -p CMD ML process command prefix (process policy)
+ -p CMD command prefix for ML process (e.g. NUMA policy)
-s system build mode for session image (system_heaps=true)
-u user build mode for session image (system_heaps=false)
@@ -308,7 +308,7 @@
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
- option @{system_option_ref ML_process_policy} for ML processes started by
+ option @{system_option_ref process_policy} for ML processes started by
the Prover IDE, e.g. to control CPU affinity on multiprocessor systems.
The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different server
--- a/src/Pure/ML/ml_process.scala Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Pure/ML/ml_process.scala Thu Mar 02 16:09:22 2023 +0100
@@ -117,7 +117,7 @@
bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
- val process_policy = options.string("ML_process_policy")
+ val process_policy = options.string("process_policy")
val process_prefix = if_proper(process_policy, process_policy + " ")
Bash.process(process_prefix + "\"$POLYML_EXE\" -q " + Bash.strings(bash_args),
--- a/src/Pure/System/host.scala Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Pure/System/host.scala Thu Mar 02 16:09:22 2023 +0100
@@ -54,7 +54,7 @@
def process_policy_options(options: Options, numa_node: Option[Int]): Options =
numa_node match {
case None => options
- case Some(n) => options.string("ML_process_policy") = process_policy(n)
+ case Some(n) => options.string("process_policy") = process_policy(n)
}
def perhaps_process_policy_options(options: Options): Options = {
--- a/src/Tools/VSCode/src/vscode_main.scala Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala Thu Mar 02 16:09:22 2023 +0100
@@ -203,7 +203,7 @@
-m MODE add print mode for output
-n no build of session image on startup
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -p CMD ML process command prefix (process policy)
+ -p CMD command prefix for ML process (e.g. NUMA policy)
-s system build mode for session image (system_heaps=true)
-u user build mode for session image (system_heaps=false)
-v verbose logging of language server
@@ -226,7 +226,7 @@
"m:" -> (arg => modes = modes ::: List(arg)),
"n" -> (_ => no_build = true),
"o:" -> add_option,
- "p:" -> (arg => add_option("ML_process_policy=" + arg)),
+ "p:" -> (arg => add_option("process_policy=" + arg)),
"s" -> (_ => add_option("system_heaps=true")),
"u" -> (_ => add_option("system_heaps=false")),
"v" -> (_ => verbose = true))
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Mar 02 16:09:22 2023 +0100
@@ -28,7 +28,7 @@
echo " -l NAME logic session name"
echo " -m MODE add print mode for output"
echo " -n no build of session image on startup"
- echo " -p CMD ML process command prefix (process policy)"
+ echo " -p CMD command prefix for ML process (e.g. NUMA policy)"
echo " -s system build mode for session image (system_heaps=true)"
echo " -u user build mode for session image (system_heaps=false)"
echo
@@ -56,7 +56,7 @@
BUILD_ONLY=false
BUILD_OPTIONS=""
-ML_PROCESS_POLICY=""
+PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_INCLUDE_SESSIONS=""
@@ -119,7 +119,7 @@
JEDIT_NO_BUILD="true"
;;
p)
- ML_PROCESS_POLICY="$OPTARG"
+ PROCESS_POLICY="$OPTARG"
;;
s)
JEDIT_BUILD_MODE="system"
@@ -163,7 +163,7 @@
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
- export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
+ export JEDIT_PROCESS_POLICY="$PROCESS_POLICY"
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
"${JAVA_ARGS[@]}" isabelle.jedit.JEdit_Main "${ARGS[@]}"
fi
--- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Mar 02 15:55:20 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Mar 02 16:09:22 2023 +0100
@@ -28,9 +28,9 @@
}
val options2 =
- Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
+ Isabelle_System.getenv("JEDIT_PROCESS_POLICY") match {
case "" => options1
- case s => options1.string.update("ML_process_policy", s)
+ case s => options1.string.update("process_policy", s)
}
options2