# HG changeset patch # User wenzelm # Date 1476880991 -7200 # Node ID 1bde86d1001331e1ce1e1e3cfa2522a85af8a08c # Parent 256298544491784db82bacd5d7a8b63591123957# Parent b00508facb4fb5620d29021f3a324c47a5983222 merged diff -r 256298544491 -r 1bde86d10013 NEWS --- 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 diff -r 256298544491 -r 1bde86d10013 etc/options --- 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" diff -r 256298544491 -r 1bde86d10013 src/Doc/System/Sessions.thy --- 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>\time\ for + @{ML profile_time} and \<^verbatim>\allocations\ 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] diff -r 256298544491 -r 1bde86d10013 src/HOL/Library/Old_SMT/old_smt_solver.ML --- 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 = diff -r 256298544491 -r 1bde86d10013 src/HOL/Tools/Nitpick/kodkod.ML --- 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 "") ^ diff -r 256298544491 -r 1bde86d10013 src/HOL/Tools/SMT/smt_solver.ML --- 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 " " diff -r 256298544491 -r 1bde86d10013 src/Pure/Admin/build_history.scala --- 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)) diff -r 256298544491 -r 1bde86d10013 src/Pure/Admin/build_log.scala --- 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)) } diff -r 256298544491 -r 1bde86d10013 src/Pure/Admin/build_release.scala --- 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 } } diff -r 256298544491 -r 1bde86d10013 src/Pure/Admin/isabelle_cronjob.scala --- 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) } diff -r 256298544491 -r 1bde86d10013 src/Pure/Admin/other_isabelle.scala --- 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 = diff -r 256298544491 -r 1bde86d10013 src/Pure/Admin/remote_dmg.scala --- 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) }) diff -r 256298544491 -r 1bde86d10013 src/Pure/General/file.ML --- 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 *) diff -r 256298544491 -r 1bde86d10013 src/Pure/General/file.scala --- 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 */ diff -r 256298544491 -r 1bde86d10013 src/Pure/General/mercurial.scala --- 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 } diff -r 256298544491 -r 1bde86d10013 src/Pure/General/name_space.ML --- 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); diff -r 256298544491 -r 1bde86d10013 src/Pure/General/ssh.scala --- 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 diff -r 256298544491 -r 1bde86d10013 src/Pure/ROOT.ML --- 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"; diff -r 256298544491 -r 1bde86d10013 src/Pure/System/bash.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; diff -r 256298544491 -r 1bde86d10013 src/Pure/System/bash.scala --- 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 diff -r 256298544491 -r 1bde86d10013 src/Pure/System/bash_syntax.ML --- /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; diff -r 256298544491 -r 1bde86d10013 src/Pure/System/isabelle_system.scala --- 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 &") diff -r 256298544491 -r 1bde86d10013 src/Pure/System/isabelle_tool.scala --- 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) } }) diff -r 256298544491 -r 1bde86d10013 src/Pure/Tools/build.ML --- 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 diff -r 256298544491 -r 1bde86d10013 src/Pure/Tools/ml_process.scala --- 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,