--- a/NEWS Tue Oct 18 23:47:33 2016 +0200
+++ b/NEWS Wed Oct 19 14:43:11 2016 +0200
@@ -1037,6 +1037,9 @@
exhaust the small 32-bit address space of the ML process (which is used
by default).
+* System option "profiling" specifies the mode for global ML profiling
+in "isabelle build". Possible values are "time", "allocations".
+
* System option "ML_process_policy" specifies an optional command prefix
for the underlying ML process, e.g. to control CPU affinity on
multiprocessor systems. The "isabelle jedit" tool allows to override the
--- a/etc/options Tue Oct 18 23:47:33 2016 +0200
+++ b/etc/options Wed Oct 19 14:43:11 2016 +0200
@@ -108,6 +108,9 @@
option checkpoint : bool = false
-- "checkpoint for theories during build process (heap compression)"
+option profiling : string = ""
+ -- "ML profiling (possible values: time, allocations)"
+
section "ML System"
--- a/src/Doc/System/Sessions.thy Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Doc/System/Sessions.thy Wed Oct 19 14:43:11 2016 +0200
@@ -215,6 +215,11 @@
Isabelle/Scala. Thus it is relatively reliable in canceling processes that
get out of control, even if there is a deadlock without CPU time usage.
+ \<^item> @{system_option_def "profiling"} specifies a mode for global ML
+ profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
+ @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
+ Results appear near the bottom of the session log file.
+
The @{tool_def options} tool prints Isabelle system options. Its
command-line usage is:
@{verbatim [display]
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Wed Oct 19 14:43:11 2016 +0200
@@ -53,7 +53,7 @@
fun make_cmd command options problem_path proof_path =
space_implode " "
- ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ ("(exec 2>&1;" :: map Bash.string (command () @ options) @
[File.bash_path problem_path, ")", ">", File.bash_path proof_path])
fun trace_and ctxt msg f x =
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Oct 19 14:43:11 2016 +0200
@@ -1028,7 +1028,7 @@
val outcome =
let
val code =
- Isabelle_System.bash ("cd " ^ File.bash_string temp_dir ^ ";\n\
+ Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
\\"$KODKODI/bin/kodkodi\"" ^
(if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Oct 19 14:43:11 2016 +0200
@@ -49,7 +49,7 @@
local
fun make_command command options problem_path proof_path =
- "(exec 2>&1;" :: map File.bash_string (command () @ options) @
+ "(exec 2>&1;" :: map Bash.string (command () @ options) @
[File.bash_path problem_path, ")", ">", File.bash_path proof_path]
|> space_implode " "
--- a/src/Pure/Admin/build_history.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Admin/build_history.scala Wed Oct 19 14:43:11 2016 +0200
@@ -96,7 +96,7 @@
/** build_history **/
private val default_rev = "tip"
- private val default_threads = 1
+ private val default_multicore = (1, 1)
private val default_heap = 1000
private val default_isabelle_identifier = "build_history"
@@ -109,12 +109,13 @@
fresh: Boolean = false,
nonfree: Boolean = false,
multicore_base: Boolean = false,
- threads_list: List[Int] = List(default_threads),
+ multicore_list: List[(Int, Int)] = List(default_multicore),
arch_64: Boolean = false,
heap: Int = default_heap,
max_heap: Option[Int] = None,
more_settings: List[String] = Nil,
verbose: Boolean = false,
+ build_tags: List[String] = Nil,
build_args: List[String] = Nil): List[(Process_Result, Path)] =
{
/* sanity checks */
@@ -122,7 +123,10 @@
if (File.eq(Path.explode("~~"), hg.root))
error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
- for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
+ for ((threads, _) <- multicore_list if threads < 1)
+ error("Bad threads value < 1: " + threads)
+ for ((_, processes) <- multicore_list if processes < 1)
+ error("Bad processes value < 1: " + processes)
if (heap < 100) error("Bad heap value < 100: " + heap)
@@ -146,11 +150,12 @@
/* main */
+ val build_host = Isabelle_System.hostname()
val build_history_date = Date.now()
- val build_host = Isabelle_System.hostname()
+ val build_group_id = build_host + ":" + build_history_date.time.ms
var first_build = true
- for (threads <- threads_list) yield
+ for ((threads, processes) <- multicore_list) yield
{
/* init settings */
@@ -183,27 +188,34 @@
Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
val build_start = Date.now()
- val res =
- other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
+ val build_args1 = List("-v", "-j" + processes) ::: build_args
+ val build_result =
+ other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose)
val build_end = Date.now()
-
- /* output log */
-
val log_path =
other_isabelle.isabelle_home_user +
Build_Log.log_subdir(build_history_date) +
- Build_Log.log_filename(
- BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads)
+ Build_Log.log_filename(BUILD_HISTORY, build_history_date,
+ List(build_host, ml_platform, "M" + threads) ::: build_tags)
- val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
+ val build_info =
+ Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
+
+
+ /* output log */
val meta_info =
- List(Build_Log.Field.build_engine -> BUILD_HISTORY,
- Build_Log.Field.build_host -> build_host,
- Build_Log.Field.build_start -> Build_Log.print_date(build_start),
- Build_Log.Field.build_end -> Build_Log.print_date(build_end),
- Build_Log.Field.isabelle_version -> isabelle_version)
+ Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
+ Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args1) :::
+ List(
+ Build_Log.Prop.build_group_id -> build_group_id,
+ Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
+ Build_Log.Prop.build_engine -> BUILD_HISTORY,
+ Build_Log.Prop.build_host -> build_host,
+ Build_Log.Prop.build_start -> Build_Log.print_date(build_start),
+ Build_Log.Prop.build_end -> Build_Log.print_date(build_end),
+ Build_Log.Prop.isabelle_version -> isabelle_version)
val ml_statistics =
build_info.finished_sessions.flatMap(session_name =>
@@ -228,7 +240,7 @@
Isabelle_System.mkdirs(log_path.dir)
File.write_xz(log_path.ext("xz"),
terminate_lines(
- Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
+ Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
heap_sizes), XZ.options(6))
@@ -242,13 +254,26 @@
first_build = false
- (res, log_path.ext("xz"))
+ (build_result, log_path.ext("xz"))
}
}
/* command line entry point */
+ private object Multicore
+ {
+ private val Pat1 = """^(\d+)$""".r
+ private val Pat2 = """^(\d+)x(\d+)$""".r
+
+ def parse(s: String): (Int, Int) =
+ s match {
+ case Pat1(Value.Int(x)) => (x, 1)
+ case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
+ case _ => error("Bad multicore configuration: " + quote(s))
+ }
+ }
+
def main(args: Array[String])
{
Command_Line.tool0 {
@@ -256,13 +281,14 @@
var components_base = ""
var heap: Option[Int] = None
var max_heap: Option[Int] = None
- var threads_list = List(default_threads)
+ var multicore_list = List(default_multicore)
var isabelle_identifier = default_isabelle_identifier
var more_settings: List[String] = Nil
var fresh = false
var arch_64 = false
var nonfree = false
var rev = default_rev
+ var build_tags = List.empty[String]
var verbose = false
val getopts = Getopts("""
@@ -272,7 +298,7 @@
-B first multicore build serves as base for scheduling information
-C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
- -M THREADS multicore configurations (comma-separated list, default: """ + default_threads + """)
+ -M MULTICORE multicore configurations (see below)
-N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
-U SIZE maximal ML heap in MB (default: unbounded)
-e TEXT additional text for generated etc/settings
@@ -280,15 +306,19 @@
-m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-n include nonfree components
-r REV update to revision (default: """ + default_rev + """)
+ -t TAG free-form build tag (multiple occurrences possible)
-v verbose
Build Isabelle sessions from the history of another REPOSITORY clone,
passing ARGS directly to its isabelle build tool.
+
+ Each MULTICORE configuration consists of one or two numbers (default 1):
+ THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
""",
"B" -> (_ => multicore_base = true),
"C:" -> (arg => components_base = arg),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
- "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
+ "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
"N:" -> (arg => isabelle_identifier = arg),
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
"e:" -> (arg => more_settings = more_settings ::: List(arg)),
@@ -301,6 +331,7 @@
},
"n" -> (_ => nonfree = true),
"r:" -> (arg => rev = arg),
+ "t:" -> (arg => build_tags = build_tags ::: List(arg)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -315,10 +346,10 @@
val results =
build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
components_base = components_base, fresh = fresh, nonfree = nonfree,
- multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
+ multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
max_heap = max_heap, more_settings = more_settings, verbose = verbose,
- build_args = build_args)
+ build_tags = build_tags, build_args = build_args)
for ((_, log_path) <- results)
Output.writeln(log_path.implode, stdout = true)
@@ -342,7 +373,7 @@
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
- val isabelle_admin = ssh.remote_path(isabelle_repos_self + Path.explode("Admin"))
+ val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
/* prepare repository clones */
@@ -353,19 +384,19 @@
if (self_update) {
isabelle_hg.pull()
isabelle_hg.update(clean = true)
- ssh.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
+ ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
}
Mercurial.setup_repository(
- ssh.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
+ ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
/* Admin/build_history */
val result =
ssh.execute(
- File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
- File.bash_string(ssh.remote_path(isabelle_repos_other)) + " " + args,
+ ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
+ ssh.bash_path(isabelle_repos_other) + " " + args,
progress_stderr = progress.echo(_)).check
for (line <- result.out_lines; log = Path.explode(line))
--- a/src/Pure/Admin/build_log.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Admin/build_log.scala Wed Oct 19 14:43:11 2016 +0200
@@ -18,36 +18,32 @@
object Build_Log
{
- /** directory content **/
+ /** content **/
+
+ /* properties */
- /* file names */
+ object Prop
+ {
+ val separator = '\u000b'
+
+ def multiple(name: String, args: List[String]): Properties.T =
+ if (args.isEmpty) Nil
+ else List(name -> args.mkString(separator.toString))
- def log_date(date: Date): String =
- String.format(Locale.ROOT, "%s.%05d",
- DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
- new java.lang.Long((date.time - date.midnight.time).ms / 1000))
-
- def log_subdir(date: Date): Path =
- Path.explode("log") + Path.explode(date.rep.getYear.toString)
-
- def log_filename(engine: String, date: Date, more: String*): Path =
- Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
+ val build_tags = "build_tags" // multiple
+ val build_args = "build_args" // multiple
+ val build_group_id = "build_group_id"
+ val build_id = "build_id"
+ val build_engine = "build_engine"
+ val build_host = "build_host"
+ val build_start = "build_start"
+ val build_end = "build_end"
+ val isabelle_version = "isabelle_version"
+ val afp_version = "afp_version"
+ }
- /* log file collections */
-
- def is_log(file: JFile): Boolean =
- List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
-
- def isatest_files(dir: Path): List[JFile] =
- File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
-
- def afp_test_files(dir: Path): List[JFile] =
- File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
-
-
-
- /** settings **/
+ /* settings */
object Settings
{
@@ -78,6 +74,32 @@
}
+ /* file names */
+
+ def log_date(date: Date): String =
+ String.format(Locale.ROOT, "%s.%05d",
+ DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
+ new java.lang.Long((date.time - date.midnight.time).ms / 1000))
+
+ def log_subdir(date: Date): Path =
+ Path.explode("log") + Path.explode(date.rep.getYear.toString)
+
+ def log_filename(engine: String, date: Date, more: List[String] = Nil): Path =
+ Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log"))
+
+
+ /* log file collections */
+
+ def is_log(file: JFile): Boolean =
+ List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
+
+ def isatest_files(dir: Path): List[JFile] =
+ File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
+
+ def afp_test_files(dir: Path): List[JFile] =
+ File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
+
+
/** log file **/
@@ -245,16 +267,6 @@
/** meta info **/
- object Field
- {
- val build_engine = "build_engine"
- val build_host = "build_host"
- val build_start = "build_start"
- val build_end = "build_end"
- val isabelle_version = "isabelle_version"
- val afp_version = "afp_version"
- }
-
object Meta_Info
{
val empty: Meta_Info = Meta_Info(Nil, Nil)
@@ -303,23 +315,28 @@
def parse(engine: String, host: String, start: Date,
End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
{
- val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
- val build_host = if (host == "") Nil else List(Field.build_host -> host)
+ val build_id =
+ {
+ val prefix = if (host != "") host else if (engine != "") engine else ""
+ (if (prefix == "") "build" else prefix) + ":" + start.time.ms
+ }
+ val build_engine = if (engine == "") Nil else List(Prop.build_engine -> engine)
+ val build_host = if (host == "") Nil else List(Prop.build_host -> host)
- val start_date = List(Field.build_start -> start.toString)
+ val start_date = List(Prop.build_start -> start.toString)
val end_date =
log_file.lines.last match {
case End(log_file.Strict_Date(end_date)) =>
- List(Field.build_end -> end_date.toString)
+ List(Prop.build_end -> end_date.toString)
case _ => Nil
}
val isabelle_version =
- log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
+ log_file.find_match(Isabelle_Version).map(Prop.isabelle_version -> _)
val afp_version =
- log_file.find_match(AFP_Version).map(Field.afp_version -> _)
+ log_file.find_match(AFP_Version).map(Prop.afp_version -> _)
- Meta_Info(build_engine ::: build_host :::
+ Meta_Info((Prop.build_id -> build_id) :: build_engine ::: build_host :::
start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
log_file.get_settings(Settings.all_settings))
}
--- a/src/Pure/Admin/build_release.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Admin/build_release.scala Wed Oct 19 14:43:11 2016 +0200
@@ -76,8 +76,8 @@
progress.bash(
"isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
(if (official_release) " -O" else "") +
- (if (release_name != "") " -r " + File.bash_string(release_name) else "") +
- (if (rev != "") " " + File.bash_string(rev) else ""),
+ (if (release_name != "") " -r " + Bash.string(release_name) else "") +
+ (if (rev != "") " " + Bash.string(rev) else ""),
echo = true).check
}
Library.trim_line(File.read(isabelle_ident_file))
@@ -98,8 +98,8 @@
progress.echo("\nApplication bundle for " + platform_family + ": " + bundle_archive.implode)
progress.bash(
"isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
- " " + File.bash_string(platform_family) +
- (if (remote_mac == "") "" else " " + File.bash_string(remote_mac)),
+ " " + Bash.string(platform_family) +
+ (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
echo = true).check
}
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 19 14:43:11 2016 +0200
@@ -97,19 +97,21 @@
host: String,
user: String = "",
port: Int = SSH.default_port,
- shared_home: Boolean = false,
+ shared_home: Boolean = true,
options: String = "",
args: String = "-o timeout=10800 -a")
private val remote_builds =
List(
- Remote_Build("lxbroy10", options = "-m32 -M4 -N", shared_home = true),
+ Remote_Build("lxbroy10", options = "-m32 -M4 -N"),
Remote_Build("macbroy2", options = "-m32 -M4"),
Remote_Build("macbroy30", options = "-m32 -M2"),
Remote_Build("macbroy31", options = "-m32 -M2"))
private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
- Logger_Task("build_history-" + r.host, logger =>
+ {
+ val task_name = "build_history-" + r.host
+ Logger_Task(task_name, logger =>
{
using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
ssh =>
@@ -120,12 +122,14 @@
isabelle_repos.ext(r.host),
isabelle_repos_source = isabelle_dev_source,
self_update = !r.shared_home,
- options = r.options + " -f -r " + File.bash_string(rev),
+ options =
+ r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
args = r.args)
for ((log, bytes) <- results)
Bytes.write(logger.log_dir + Path.explode(log), bytes)
})
})
+ }
@@ -167,7 +171,9 @@
val err =
res match {
case Exn.Res(_) => None
- case Exn.Exn(exn) => Some(Exn.message(exn))
+ case Exn.Exn(exn) =>
+ val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
+ Some(first_line)
}
logger.log_end(end_date, err)
}
--- a/src/Pure/Admin/other_isabelle.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Admin/other_isabelle.scala Wed Oct 19 14:43:11 2016 +0200
@@ -16,7 +16,7 @@
def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
progress.bash(
- "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
+ "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" + script,
env = null, cwd = isabelle_home.file, redirect = redirect)
def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
--- a/src/Pure/Admin/remote_dmg.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Admin/remote_dmg.scala Wed Oct 19 14:43:11 2016 +0200
@@ -13,13 +13,13 @@
{
ssh.with_tmp_dir(remote_dir =>
{
- val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; "
+ val cd = "cd " + ssh.bash_path(remote_dir) + "; "
ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
ssh.execute(
cd + "hdiutil create -srcfolder root" +
- (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
+ (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) +
" dmg.dmg").check
ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
})
--- a/src/Pure/General/file.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/General/file.ML Wed Oct 19 14:43:11 2016 +0200
@@ -8,8 +8,6 @@
sig
val standard_path: Path.T -> string
val platform_path: Path.T -> string
- val bash_string: string -> string
- val bash_args: string list -> string
val bash_path: Path.T -> string
val full_path: Path.T -> Path.T -> Path.T
val tmp_path: Path.T -> Path.T
@@ -46,26 +44,7 @@
val standard_path = Path.implode o Path.expand;
val platform_path = ML_System.platform_path o standard_path;
-fun bash_string "" = "\"\""
- | bash_string str =
- str |> translate_string (fn ch =>
- let val c = ord ch in
- (case ch of
- "\t" => "$'\\t'"
- | "\n" => "$'\\n'"
- | "\f" => "$'\\f'"
- | "\r" => "$'\\r'"
- | _ =>
- if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
- exists_string (fn c => c = ch) "-./:_" then ch
- else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
- else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
- else "\\" ^ ch)
- end);
-
-val bash_args = space_implode " " o map bash_string;
-
-val bash_path = bash_string o standard_path;
+val bash_path = Bash_Syntax.string o standard_path;
(* full_path *)
--- a/src/Pure/General/file.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/General/file.scala Wed Oct 19 14:43:11 2016 +0200
@@ -108,33 +108,8 @@
/* bash path */
- private def bash_chr(c: Byte): String =
- {
- val ch = c.toChar
- ch match {
- case '\t' => "$'\\t'"
- case '\n' => "$'\\n'"
- case '\f' => "$'\\f'"
- case '\r' => "$'\\r'"
- case _ =>
- if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
- Symbol.ascii(ch)
- else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
- else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
- else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
- else "\\" + ch
- }
- }
-
- def bash_string(s: String): String =
- if (s == "") "\"\""
- else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
-
- def bash_args(args: List[String]): String =
- args.iterator.map(bash_string(_)).mkString(" ")
-
- def bash_path(path: Path): String = bash_string(standard_path(path))
- def bash_path(file: JFile): String = bash_string(standard_path(file))
+ def bash_path(path: Path): String = Bash.string(standard_path(path))
+ def bash_path(file: JFile): String = Bash.string(standard_path(file))
/* directory entries */
--- a/src/Pure/General/mercurial.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/General/mercurial.scala Wed Oct 19 14:43:11 2016 +0200
@@ -16,7 +16,7 @@
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
- if (s == "") "" else " " + prefix + " " + File.bash_string(s)
+ if (s == "") "" else " " + prefix + " " + Bash.string(s)
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
@@ -40,7 +40,7 @@
case None => Isabelle_System.mkdirs(hg.root.dir)
case Some(ssh) => ssh.mkdirs(hg.root.dir)
}
- hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
+ hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
hg
}
--- a/src/Pure/General/name_space.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/General/name_space.ML Wed Oct 19 14:43:11 2016 +0200
@@ -120,7 +120,7 @@
(* internal names *)
-type internals = (string list * string list) Change_Table.T;
+type internals = (string list * string list) Change_Table.T; (*xname -> visible, hidden*)
fun map_internals f xname : internals -> internals =
Change_Table.map_default (xname, ([], [])) f;
@@ -132,13 +132,15 @@
fun hide_name name = map_internals (apsnd (update (op =) name)) name;
+(* external accesses *)
+
+type accesses = (xstring list * xstring list); (*input / output fragments*)
+type entries = (accesses * entry) Change_Table.T; (*name -> accesses, entry*)
+
+
(* datatype T *)
-datatype T =
- Name_Space of
- {kind: string,
- internals: internals, (*xname -> visible, hidden*)
- entries: (xstring list * entry) Change_Table.T}; (*name -> externals, entry*)
+datatype T = Name_Space of {kind: string, internals: internals, entries: entries};
fun make_name_space (kind, internals, entries) =
Name_Space {kind = kind, internals = internals, entries = entries};
@@ -200,12 +202,13 @@
fun get_accesses (Name_Space {entries, ...}) name =
(case Change_Table.lookup entries name of
- NONE => []
- | SOME (externals, _) => externals);
+ NONE => ([], [])
+ | SOME (accesses, _) => accesses);
-fun valid_accesses (Name_Space {internals, ...}) name =
- Change_Table.fold (fn (xname, (names, _)) =>
- if not (null names) andalso hd names = name then cons xname else I) internals [];
+fun is_valid_access (Name_Space {internals, ...}) name xname =
+ (case Change_Table.lookup internals xname of
+ SOME (name' :: _, _) => name = name'
+ | _ => false);
(* extern *)
@@ -234,7 +237,7 @@
in
if names_long then name
else if names_short then Long_Name.base_name name
- else ext (get_accesses space name)
+ else ext (#2 (get_accesses space name))
end;
fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
@@ -426,7 +429,7 @@
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
-fun accesses naming binding =
+fun make_accesses naming binding =
(case name_spec naming binding of
{restriction = SOME true, ...} => ([], [])
| {restriction, spec, ...} =>
@@ -443,12 +446,13 @@
space |> map_name_space (fn (kind, internals, entries) =>
let
val _ = the_entry space name;
- val names = valid_accesses space name;
+ val (accs, accs') = get_accesses space name;
+ val xnames = filter (is_valid_access space name) accs;
val internals' = internals
|> hide_name name
|> fold (del_name name)
- (if fully then names else inter (op =) [Long_Name.base_name name] names)
- |> fold (del_name_extra name) (get_accesses space name);
+ (if fully then xnames else inter (op =) [Long_Name.base_name name] xnames)
+ |> fold (del_name_extra name) accs';
in (kind, internals', entries) end);
@@ -458,10 +462,12 @@
space |> map_name_space (fn (kind, internals, entries) =>
let
val _ = the_entry space name;
- val (accs, accs') = accesses naming binding;
- val internals' = internals |> fold (add_name name) accs;
+ val (more_accs, more_accs') = make_accesses naming binding;
+ val internals' = internals |> fold (add_name name) more_accs;
val entries' = entries
- |> Change_Table.map_entry name (apfst (fold_rev (update op =) accs'));
+ |> Change_Table.map_entry name (apfst (fn (accs, accs') =>
+ (fold_rev (update op =) more_accs accs,
+ fold_rev (update op =) more_accs' accs')))
in (kind, internals', entries') end);
@@ -497,7 +503,7 @@
val naming = naming_of context;
val Naming {group, theory_name, ...} = naming;
val {concealed, spec, ...} = name_spec naming binding;
- val (accs, accs') = accesses naming binding;
+ val accesses = make_accesses naming binding;
val name = Long_Name.implode (map fst spec);
val _ = name = "" andalso error (Binding.bad binding);
@@ -512,10 +518,10 @@
val space' =
space |> map_name_space (fn (kind, internals, entries) =>
let
- val internals' = internals |> fold (add_name name) accs;
+ val internals' = internals |> fold (add_name name) (#1 accesses);
val entries' =
(if strict then Change_Table.update_new else Change_Table.update)
- (name, (accs', entry)) entries
+ (name, (accesses, entry)) entries
handle Change_Table.DUP dup =>
err_dup kind (dup, #2 (the (Change_Table.lookup entries dup)))
(name, entry) (#pos entry);
--- a/src/Pure/General/ssh.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/General/ssh.scala Wed Oct 19 14:43:11 2016 +0200
@@ -243,6 +243,7 @@
}
def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
+ def bash_path(path: Path): String = Bash.string(remote_path(path))
def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
@@ -323,8 +324,10 @@
/* tmp dirs */
+ def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
+
def rm_tree(remote_dir: String): Unit =
- execute("rm -r -f " + File.bash_string(remote_dir)).check
+ execute("rm -r -f " + Bash.string(remote_dir)).check
def tmp_dir(): String =
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
--- a/src/Pure/ROOT.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/ROOT.ML Wed Oct 19 14:43:11 2016 +0200
@@ -67,6 +67,7 @@
ML_file "PIDE/xml.ML";
ML_file "General/path.ML";
ML_file "General/url.ML";
+ML_file "System/bash_syntax.ML";
ML_file "General/file.ML";
ML_file "General/long_name.ML";
ML_file "General/binding.ML";
--- a/src/Pure/System/bash.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/System/bash.ML Wed Oct 19 14:43:11 2016 +0200
@@ -6,6 +6,8 @@
signature BASH =
sig
+ val string: string -> string
+ val strings: string list -> string
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
@@ -14,6 +16,9 @@
structure Bash: BASH =
struct
+val string = Bash_Syntax.string;
+val strings = Bash_Syntax.strings;
+
val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
@@ -105,6 +110,9 @@
structure Bash: BASH =
struct
+val string = Bash_Syntax.string;
+val strings = Bash_Syntax.strings;
+
val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
--- a/src/Pure/System/bash.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/System/bash.scala Wed Oct 19 14:43:11 2016 +0200
@@ -13,6 +13,36 @@
object Bash
{
+ /* concrete syntax */
+
+ private def bash_chr(c: Byte): String =
+ {
+ val ch = c.toChar
+ ch match {
+ case '\t' => "$'\\t'"
+ case '\n' => "$'\\n'"
+ case '\f' => "$'\\f'"
+ case '\r' => "$'\\r'"
+ case _ =>
+ if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
+ Symbol.ascii(ch)
+ else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
+ else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
+ else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
+ else "\\" + ch
+ }
+ }
+
+ def string(s: String): String =
+ if (s == "") "\"\""
+ else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+
+ def strings(ss: List[String]): String =
+ ss.iterator.map(Bash.string(_)).mkString(" ")
+
+
+ /* process and result */
+
private class Limited_Progress(proc: Process, progress_limit: Option[Long])
{
private var count = 0L
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/bash_syntax.ML Wed Oct 19 14:43:11 2016 +0200
@@ -0,0 +1,35 @@
+(* Title: Pure/System/bash_syntax.ML
+ Author: Makarius
+
+Syntax for GNU bash (see also Pure/System/bash.ML).
+*)
+
+signature BASH_SYNTAX =
+sig
+ val string: string -> string
+ val strings: string list -> string
+end;
+
+structure Bash_Syntax: BASH_SYNTAX =
+struct
+
+fun string "" = "\"\""
+ | string str =
+ str |> translate_string (fn ch =>
+ let val c = ord ch in
+ (case ch of
+ "\t" => "$'\\t'"
+ | "\n" => "$'\\n'"
+ | "\f" => "$'\\f'"
+ | "\r" => "$'\\r'"
+ | _ =>
+ if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+ exists_string (fn c => c = ch) "-./:_" then ch
+ else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else "\\" ^ ch)
+ end);
+
+val strings = space_implode " " o map string;
+
+end;
--- a/src/Pure/System/isabelle_system.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Oct 19 14:43:11 2016 +0200
@@ -318,7 +318,7 @@
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
- bash("exec \"$ISABELLE_OPEN\" " + File.bash_string(arg) + " >/dev/null 2>/dev/null &")
+ bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
--- a/src/Pure/System/isabelle_tool.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala Wed Oct 19 14:43:11 2016 +0200
@@ -89,7 +89,7 @@
(args: List[String]) =>
{
val tool = dir + Path.basic(name)
- val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
+ val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
sys.exit(result.print_stdout.rc)
}
})
--- a/src/Pure/Tools/build.ML Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Tools/build.ML Wed Oct 19 14:43:11 2016 +0200
@@ -114,6 +114,12 @@
symbols = symbols,
last_timing = last_timing,
master_dir = master_dir}
+ |>
+ (case Options.string options "profiling" of
+ "" => I
+ | "time" => profile_time
+ | "allocations" => profile_allocations
+ | bad => error ("Bad profiling option: " ^ quote bad))
|> Unsynchronized.setmp print_mode
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
else
--- a/src/Pure/Tools/ml_process.scala Tue Oct 18 23:47:33 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala Wed Oct 19 14:43:11 2016 +0200
@@ -107,7 +107,7 @@
Bash.process(
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
- File.bash_args(bash_args),
+ Bash.strings(bash_args),
cwd = cwd,
env =
Isabelle_System.library_path(env ++ env_options ++ env_tmp,