--- a/etc/options Sun Aug 10 21:09:45 2025 +0200
+++ b/etc/options Sun Aug 10 21:44:42 2025 +0200
@@ -161,6 +161,9 @@
option profiling : string = "" (standard "time") for build
-- "ML profiling (possible values: time, time_thread, allocations)"
+option profiling_dir : string = "" for content
+ -- "output directory for \"isabelle profiling\" tool"
+
option system_log : string = "" (standard "-") for build
-- "output for system messages (log file or \"-\" for console progress)"
--- a/src/Pure/Tools/profiling.scala Sun Aug 10 21:09:45 2025 +0200
+++ b/src/Pure/Tools/profiling.scala Sun Aug 10 21:44:42 2025 +0200
@@ -82,11 +82,10 @@
val eval_args =
List("--eval", "use_thy " + ML_Syntax.print_string_bytes("~~/src/Tools/Profiling"))
Isabelle_System.with_tmp_dir("profiling") { dir =>
- val putenv = List("ISABELLE_PROFILING" -> dir.implode)
File.write(dir + Path.explode("args.yxml"), YXML.string_of_body(encode_args(args)))
+ val ml_options = store.options + Options.Spec("profiling_dir", Some(dir.implode))
val session_heaps = store.session_heaps(session_background, logic = session_name)
- ML_Process(store.options, session_background, session_heaps, args = eval_args,
- env = Isabelle_System.Settings.env(putenv)).result().check
+ ML_Process(ml_options, session_background, session_heaps, args = eval_args).result().check
decode_result(YXML.parse_body(Bytes.read(dir + Path.explode("result.yxml"))))
}
}
--- a/src/Tools/Profiling.thy Sun Aug 10 21:09:45 2025 +0200
+++ b/src/Tools/Profiling.thy Sun Aug 10 21:44:42 2025 +0200
@@ -183,7 +183,7 @@
in
fun main () =
- (case getenv "ISABELLE_PROFILING" of
+ (case Options.default_string \<^system_option>\<open>profiling_dir\<close> of
"" => ()
| dir_name =>
let