diff --git a/src/HOL/Tools/Nitpick/kodkod.scala b/src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala
+++ b/src/HOL/Tools/Nitpick/kodkod.scala
@@ -1,178 +1,178 @@
/* Title: HOL/Tools/Nitpick/kodkod.scala
Author: Makarius
Scala interface for Kodkod.
*/
package isabelle.nitpick
import isabelle._
import java.util.concurrent.{TimeUnit, LinkedBlockingQueue, ThreadPoolExecutor}
import org.antlr.runtime.{ANTLRInputStream, RecognitionException}
import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
object Kodkod
{
/** result **/
sealed case class Result(rc: Int, out: String, err: String)
{
- def ok: Boolean = rc == 0
+ def ok: Boolean = rc == Process_Result.RC.ok
def check: String =
if (ok) out else error(if (err.isEmpty) "Error" else err)
def encode: XML.Body =
{
import XML.Encode._
triple(int, string, string)((rc, out, err))
}
}
/** execute **/
def execute(source: String,
solve_all: Boolean = false,
prove: Boolean = false,
max_solutions: Int = Integer.MAX_VALUE,
cleanup_inst: Boolean = false,
timeout: Time = Time.zero,
max_threads: Int = 0): Result =
{
/* executor */
val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
val executor: ThreadPoolExecutor =
new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS,
new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy)
val executor_killed = Synchronized(false)
def executor_kill(): Unit =
executor_killed.change(b =>
if (b) b else { Isabelle_Thread.fork() { executor.shutdownNow() }; true })
/* system context */
class Exit extends Exception("EXIT")
class Exec_Context extends Context
{
- private var rc = 0
+ private var rc = Process_Result.RC.ok
private val out = new StringBuilder
private val err = new StringBuilder
def return_code(i: Int): Unit = synchronized { rc = rc max i}
override def output(s: String): Unit = synchronized {
Exn.Interrupt.expose()
out ++= s
out += '\n'
}
override def error(s: String): Unit = synchronized {
Exn.Interrupt.expose()
err ++= s
err += '\n'
}
override def exit(i: Int): Unit =
synchronized {
return_code(i)
executor_kill()
throw new Exit
}
def result(): Result = synchronized { Result(rc, out.toString, err.toString) }
}
val context = new Exec_Context
/* main */
try {
val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream()))
val parser =
KodkodiParser.create(context, executor,
false, solve_all, prove, max_solutions, cleanup_inst, lexer)
val timeout_request =
if (timeout.is_zero) None
else {
Some(Event_Timer.request(Time.now() + timeout) {
context.error("Ran out of time")
- context.return_code(2)
+ context.return_code(Process_Result.RC.failure)
executor_kill()
})
}
try { parser.problems() }
catch { case exn: RecognitionException => parser.reportError(exn) }
timeout_request.foreach(_.cancel())
if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
context.error("Error: trailing tokens")
- context.exit(1)
+ context.exit(Process_Result.RC.error)
}
if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) {
- context.exit(1)
+ context.exit(Process_Result.RC.error)
}
}
catch {
case _: Exit =>
case exn: Throwable =>
val message = exn.getMessage
context.error(if (message.isEmpty) exn.toString else "Error: " + message)
context.return_code(1)
}
executor.shutdownNow()
context.result()
}
/** protocol handler **/
def warmup(): String =
execute(
"solver: \"MiniSat\"\n" +
File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
class Handler extends Session.Protocol_Handler
{
override def init(session: Session): Unit = warmup()
}
/** scala function **/
object Fun extends Scala.Fun_String("kodkod", thread = true)
{
val here = Scala_Project.here
def apply(args: String): String =
{
val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) =
{
import XML.Decode._
pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args))
}
val result =
execute(kki,
solve_all = solve_all,
max_solutions = max_solutions,
timeout = Time.ms(timeout),
max_threads = max_threads)
YXML.string_of_body(result.encode)
}
}
}
class Scala_Functions extends Scala.Functions(Kodkod.Fun)
diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala
+++ b/src/Pure/Admin/build_history.scala
@@ -1,624 +1,624 @@
/* Title: Pure/Admin/build_history.scala
Author: Makarius
Build other history versions.
*/
package isabelle
object Build_History
{
/* log files */
val engine = "build_history"
val log_prefix = engine + "_"
/* augment settings */
def augment_settings(
other_isabelle: Other_Isabelle,
threads: Int,
arch_64: Boolean,
heap: Int,
max_heap: Option[Int],
more_settings: List[String]): String =
{
val (ml_platform, ml_settings) =
{
val cygwin_32 = "x86-cygwin"
val windows_32 = "x86-windows"
val windows_64 = "x86_64-windows"
val windows_64_32 = "x86_64_32-windows"
val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-")
val polyml_home =
try { Path.explode(other_isabelle.getenv("ML_HOME")).dir }
catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
def err(platform: String): Nothing =
error("Platform " + platform + " unavailable on this machine")
def check_dir(platform: String): Boolean =
platform != "" && ml_home(platform).is_dir
val ml_platform =
if (Platform.is_windows && arch_64) {
if (check_dir(windows_64)) windows_64 else err(windows_64)
}
else if (Platform.is_windows && !arch_64) {
if (check_dir(windows_64_32)) windows_64_32
else if (check_dir(cygwin_32)) cygwin_32
else if (check_dir(windows_32)) windows_32
else err(windows_32)
}
else if (arch_64) {
if (check_dir(platform_64)) platform_64 else err(platform_64)
}
else if (check_dir(platform_64_32)) platform_64_32
else platform_32
val ml_options =
"--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
" --gcthreads " + threads +
(if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
(ml_platform,
List(
"ML_HOME=" + File.bash_path(ml_home(ml_platform)),
"ML_PLATFORM=" + quote(ml_platform),
"ML_OPTIONS=" + quote(ml_options)))
}
val thread_settings =
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
"ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
val settings =
List(ml_settings, thread_settings) :::
(if (more_settings.isEmpty) Nil else List(more_settings))
File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
ml_platform
}
/** build_history **/
private val default_user_home = Path.USER_HOME
private val default_rev = "tip"
private val default_multicore = (1, 1)
private val default_heap = 1500
private val default_isabelle_identifier = "build_history"
def build_history(
options: Options,
root: Path,
user_home: Path = default_user_home,
progress: Progress = new Progress,
rev: String = default_rev,
afp_rev: Option[String] = None,
afp_partition: Int = 0,
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
fresh: Boolean = false,
hostname: String = "",
multicore_base: Boolean = false,
multicore_list: List[(Int, Int)] = List(default_multicore),
arch_64: Boolean = false,
heap: Int = default_heap,
max_heap: Option[Int] = None,
init_settings: List[String] = Nil,
more_settings: List[String] = Nil,
more_preferences: List[String] = Nil,
verbose: Boolean = false,
build_tags: List[String] = Nil,
build_args: List[String] = Nil): List[(Process_Result, Path)] =
{
/* sanity checks */
if (File.eq(Path.ISABELLE_HOME, root))
error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand)
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)
if (max_heap.isDefined && max_heap.get < heap)
error("Bad max_heap value < heap: " + max_heap.get)
System.getenv("ISABELLE_SETTINGS_PRESENT") match {
case null | "" =>
case _ => error("Cannot run build_history within existing Isabelle settings environment")
}
/* checkout Isabelle + AFP repository */
def checkout(dir: Path, version: String): String =
{
val hg = Mercurial.repository(dir)
hg.update(rev = version, clean = true)
progress.echo_if(verbose, hg.log(version, options = "-l1"))
hg.id(rev = version)
}
val isabelle_version = checkout(root, rev)
val afp_repos = root + Path.explode("AFP")
val afp_version = afp_rev.map(checkout(afp_repos, _))
val (afp_build_args, afp_sessions) =
if (afp_rev.isEmpty) (Nil, Nil)
else {
val (opt, sessions) = {
if (afp_partition == 0) ("-d", Nil)
else {
try {
val afp = AFP.init(options, afp_repos)
("-d", afp.partition(afp_partition))
} catch { case ERROR(_) => ("-D", Nil) }
}
}
(List(opt, "~~/AFP/thys"), sessions)
}
/* main */
val other_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = progress)
val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
val build_history_date = Date.now()
val build_group_id = build_host + ":" + build_history_date.time.ms
var first_build = true
for ((threads, processes) <- multicore_list) yield
{
/* init settings */
val component_settings =
other_isabelle.init_components(
component_repository = component_repository,
components_base = components_base,
catalogs = List("main", "optional"))
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
val ml_platform =
augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
val isabelle_output =
other_isabelle.isabelle_home_user + Path.explode("heaps") +
Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
val isabelle_output_log = isabelle_output + Path.explode("log")
val isabelle_base_log = isabelle_output + Path.explode("../base_log")
if (first_build) {
other_isabelle.resolve_components(echo = verbose)
if (fresh)
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
other_isabelle.bash(
"env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
"bin/isabelle jedit -b", redirect = true, echo = verbose).check
for {
tool <- List("ghc_setup", "ocaml_setup")
if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
(other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
} other_isabelle(tool, echo = verbose)
Isabelle_System.rm_tree(isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.make_directory(isabelle_output)
val log_path =
other_isabelle.isabelle_home_user +
Build_Log.log_subdir(build_history_date) +
Build_Log.log_filename(Build_History.engine, build_history_date,
List(build_host, ml_platform, "M" + threads) ::: build_tags)
Isabelle_System.make_directory(log_path.dir)
val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
val build_out_progress = new File_Progress(build_out)
build_out.file.delete
/* build */
if (multicore_base && !first_build && isabelle_base_log.is_dir)
Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
val build_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = build_out_progress)
val build_result =
build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions),
redirect = true, echo = true, strict = false)
val build_end = Date.now()
val build_info: Build_Log.Build_Info =
Build_Log.Log_File(log_path.file_name, build_result.out_lines).
parse_build_info(ml_statistics = true)
/* output log */
val store = Sessions.store(options + "build_database_server=false")
val meta_info =
Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
List(
Build_Log.Prop.build_group_id.name -> build_group_id,
Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
Build_Log.Prop.build_engine.name -> Build_History.engine,
Build_Log.Prop.build_host.name -> build_host,
Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
build_out_progress.echo("Reading session build info ...")
val session_build_info =
build_info.finished_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
if (database.is_file) {
using(SQLite.open_database(database))(db =>
{
val theory_timings =
try {
store.read_theory_timings(db, session_name).map(ps =>
Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
}
catch { case ERROR(_) => Nil }
val session_sources =
store.read_build(db, session_name).map(_.sources) match {
case Some(sources) if sources.length == SHA1.digest_length =>
List("Sources " + session_name + " " + sources)
case _ => Nil
}
theory_timings ::: session_sources
})
}
else Nil
})
build_out_progress.echo("Reading ML statistics ...")
val ml_statistics =
build_info.finished_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
val log_gz = isabelle_output + store.log_gz(session_name)
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
store.read_ml_statistics(db, session_name))
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
}
else Nil
val trimmed_properties =
if (ml_statistics_step <= 0) Nil
else if (ml_statistics_step == 1) properties
else {
(for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
yield ps).toList
}
trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
})
build_out_progress.echo("Reading error messages ...")
val session_errors =
build_info.failed_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
val errors =
if (database.is_file) {
try {
using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
} // column "errors" could be missing
catch { case _: java.sql.SQLException => Nil }
}
else Nil
errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
})
build_out_progress.echo("Reading heap sizes ...")
val heap_sizes =
build_info.finished_sessions.flatMap(session_name =>
{
val heap = isabelle_output + Path.explode(session_name)
if (heap.is_file)
Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
else None
})
build_out_progress.echo("Writing log file " + log_path.xz + " ...")
File.write_xz(log_path.xz,
terminate_lines(
Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
session_build_info :::
ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
session_errors.map(Protocol.Error_Message_Marker.apply) :::
heap_sizes), XZ.options(6))
/* next build */
if (multicore_base && first_build && isabelle_output_log.is_dir)
Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
Isabelle_System.rm_tree(isabelle_output)
first_build = false
(build_result, log_path.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]): Unit =
{
Command_Line.tool {
var afp_rev: Option[String] = None
var multicore_base = false
var components_base: Path = Components.default_components_base
var heap: Option[Int] = None
var max_heap: Option[Int] = None
var multicore_list = List(default_multicore)
var isabelle_identifier = default_isabelle_identifier
var afp_partition = 0
var component_repository = Components.default_component_repository
var more_settings: List[String] = Nil
var more_preferences: List[String] = Nil
var fresh = false
var hostname = ""
var init_settings: List[String] = Nil
var arch_64 = false
var output_file = ""
var rev = default_rev
var ml_statistics_step = 1
var build_tags = List.empty[String]
var user_home = default_user_home
var verbose = false
var exit_code = false
val getopts = Getopts("""
Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
Options are:
-A REV include $ISABELLE_HOME/AFP repository at given revision
-B first multicore build serves as base for scheduling information
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
default_heap * 2 + """ for x86_64)
-M MULTICORE multicore configurations (see below)
-N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
-P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted)
-R URL remote repository for Isabelle components (default: """ +
Components.default_component_repository + """)
-U SIZE maximal ML heap in MB (default: unbounded)
-e TEXT additional text for generated etc/settings
-f fresh build of Isabelle/Scala components (recommended)
-h NAME override local hostname
-i TEXT initial text for generated etc/settings
-m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-o FILE output file for log names (default: stdout)
-p TEXT additional text for generated etc/preferences
-r REV update to revision (default: """ + default_rev + """)
-s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1)
-t TAG free-form build tag (multiple occurrences possible)
-u DIR alternative USER_HOME directory
-v verbose
-x return overall exit code from build processes
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.
""",
"A:" -> (arg => afp_rev = Some(arg)),
"B" -> (_ => multicore_base = true),
"C:" -> (arg => components_base = Path.explode(arg)),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
"M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
"P:" -> (arg => afp_partition = Value.Int.parse(arg)),
"R:" -> (arg => component_repository = arg),
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
"e:" -> (arg => more_settings = more_settings ::: List(arg)),
"f" -> (_ => fresh = true),
"h:" -> (arg => hostname = arg),
"i:" -> (arg => init_settings = init_settings ::: List(arg)),
"m:" ->
{
case "32" | "x86" => arch_64 = false
case "64" | "x86_64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"o:" -> (arg => output_file = arg),
"p:" -> (arg => more_preferences = more_preferences ::: List(arg)),
"r:" -> (arg => rev = arg),
"s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
"t:" -> (arg => build_tags = build_tags ::: List(arg)),
"u:" -> (arg => user_home = Path.explode(arg)),
"v" -> (_ => verbose = true),
"x" -> (_ => exit_code = true))
val more_args = getopts(args)
val (root, build_args) =
more_args match {
case root :: build_args => (Path.explode(root), build_args)
case _ => getopts.usage()
}
val progress = new Console_Progress(stderr = true)
val results =
build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
afp_rev = afp_rev, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
component_repository = component_repository, components_base = components_base,
fresh = fresh, hostname = hostname, 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, init_settings = init_settings, more_settings = more_settings,
more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
build_args = build_args)
if (output_file == "") {
for ((_, log_path) <- results)
Output.writeln(log_path.implode, stdout = true)
}
else {
File.write(Path.explode(output_file),
cat_lines(for ((_, log_path) <- results) yield log_path.implode))
}
- val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
- if (rc != 0 && exit_code) sys.exit(rc)
+ val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc }
+ if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc)
}
}
/** remote build_history -- via command-line **/
def remote_build_history(
ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
isabelle_repository: Mercurial.Server = Isabelle_System.isabelle_repository,
afp_repository: Mercurial.Server = Isabelle_System.afp_repository,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
progress: Progress = new Progress,
rev: String = "",
afp_rev: Option[String] = None,
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
/* Isabelle self repository */
val self_hg =
Mercurial.setup_repository(isabelle_repository.root, isabelle_repos_self, ssh = ssh)
def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
progress_stdout = progress.echo_if(echo, _),
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
if (self_update) {
val hg = Mercurial.repository(Path.ISABELLE_HOME)
hg.push(self_hg.root_url, force = true)
self_hg.update(rev = hg.parent(), clean = true)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("bin/isabelle", "jedit -bf")
}
val rev_id = self_hg.id(rev)
/* Isabelle other + AFP repository */
if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
ssh.rm_tree(isabelle_repos_other)
}
Mercurial.clone_repository(
ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh)
val afp_options =
if (afp_rev.isEmpty) ""
else {
val afp_repos = isabelle_repos_other + Path.explode("AFP")
Mercurial.setup_repository(afp_repository.root, afp_repos, ssh = ssh)
" -A " + Bash.string(afp_rev.get)
}
/* Admin/build_history */
ssh.with_tmp_dir(tmp_dir =>
{
val output_file = tmp_dir + Path.explode("output")
val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)
try {
execute("Admin/build_history",
"-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " +
ssh.bash_path(isabelle_repos_other) + " " + args,
echo = true, strict = false)
}
catch {
case ERROR(msg) =>
cat_error(msg,
"The error(s) above occurred for build_bistory " + rev_options + afp_options)
}
for (line <- split_lines(ssh.read(output_file)))
yield {
val log = Path.explode(line)
val bytes = ssh.read_bytes(log)
ssh.rm(log)
(log.file_name, bytes)
}
})
}
}
diff --git a/src/Pure/Admin/ci_profile.scala b/src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala
+++ b/src/Pure/Admin/ci_profile.scala
@@ -1,170 +1,170 @@
/* Title: Pure/Admin/ci_profile.scala
Author: Lars Hupel
Build profile for continuous integration services.
*/
package isabelle
import java.time.{Instant, ZoneId}
import java.time.format.DateTimeFormatter
import java.util.{Properties => JProperties, Map => JMap}
abstract class CI_Profile extends Isabelle_Tool.Body
{
case class Result(rc: Int)
case object Result
{
- def ok: Result = Result(0)
- def error: Result = Result(1)
+ def ok: Result = Result(Process_Result.RC.ok)
+ def error: Result = Result(Process_Result.RC.error)
}
private def build(options: Options): (Build.Results, Time) =
{
val progress = new Console_Progress(verbose = true)
val start_time = Time.now()
val results = progress.interrupt_handler {
Build.build(
options + "system_heaps",
selection = selection,
progress = progress,
clean_build = clean,
verbose = true,
numa_shuffling = numa,
max_jobs = jobs,
dirs = include,
select_dirs = select)
}
val end_time = Time.now()
(results, end_time - start_time)
}
private def load_properties(): JProperties =
{
val props = new JProperties()
val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
if (file_name != "")
{
val file = Path.explode(file_name).file
if (file.exists())
props.load(new java.io.FileReader(file))
props
}
else
props
}
private def compute_timing(results: Build.Results, group: Option[String]): Timing =
{
val timings = results.sessions.collect {
case session if group.forall(results.info(session).groups.contains(_)) =>
results(session).timing
}
timings.foldLeft(Timing.zero)(_ + _)
}
private def with_documents(options: Options): Options =
{
if (documents)
options
.bool.update("browser_info", true)
.string.update("document", "pdf")
.string.update("document_variants", "document:outline=/proof,/ML")
else
options
}
final def hg_id(path: Path): String =
Mercurial.repository(path).id()
final def print_section(title: String): Unit =
println(s"\n=== $title ===\n")
final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
final val isabelle_id = hg_id(isabelle_home)
final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
override final def apply(args: List[String]): Unit =
{
print_section("CONFIGURATION")
println(Build_Log.Settings.show())
val props = load_properties()
System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props)
val options =
with_documents(Options.init())
.int.update("parallel_proofs", 1)
.int.update("threads", threads)
println(s"jobs = $jobs, threads = $threads, numa = $numa")
print_section("BUILD")
println(s"Build started at $start_time")
println(s"Isabelle id $isabelle_id")
val pre_result = pre_hook(args)
print_section("LOG")
val (results, elapsed_time) = build(options)
print_section("TIMING")
val groups = results.sessions.map(results.info).flatMap(_.groups)
for (group <- groups)
println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
println("Overall: " + total_timing.message_resources)
if (!results.ok) {
print_section("FAILED SESSIONS")
for (name <- results.sessions) {
if (results.cancelled(name)) {
println(s"Session $name: CANCELLED")
}
else {
val result = results(name)
if (!result.ok)
println(s"Session $name: FAILED ${result.rc}")
}
}
}
val post_result = post_hook(results)
System.exit(List(pre_result.rc, results.rc, post_result.rc).max)
}
/* profile */
def threads: Int = Isabelle_System.hostname() match {
case "hpcisabelle" => 8
case "lxcisa1" => 4
case _ => 2
}
def jobs: Int = Isabelle_System.hostname() match {
case "hpcisabelle" => 8
case "lxcisa1" => 10
case _ => 2
}
def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle"
def documents: Boolean = true
def clean: Boolean = true
def include: List[Path]
def select: List[Path]
def pre_hook(args: List[String]): Result
def post_hook(results: Build.Results): Result
def selection: Sessions.Selection
}
diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala
+++ b/src/Pure/General/ssh.scala
@@ -1,524 +1,524 @@
/* Title: Pure/General/ssh.scala
Author: Makarius
SSH client based on JSch (see also http://www.jcraft.com/jsch/examples).
*/
package isabelle
import java.util.{Map => JMap}
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
import scala.collection.mutable
import scala.util.matching.Regex
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS,
JSchException}
object SSH
{
/* target machine: user@host syntax */
object Target
{
val User_Host: Regex = "^([^@]+)@(.+)$".r
def parse(s: String): (String, String) =
s match {
case User_Host(user, host) => (user, host)
case _ => ("", s)
}
def unapplySeq(s: String): Option[List[String]] =
parse(s) match {
case (_, "") => None
case (user, host) => Some(List(user, host))
}
}
val default_port = 22
def make_port(port: Int): Int = if (port > 0) port else default_port
def port_suffix(port: Int): String =
if (port == default_port) "" else ":" + port
def user_prefix(user: String): String =
proper_string(user) match {
case None => ""
case Some(name) => name + "@"
}
def connect_timeout(options: Options): Int =
options.seconds("ssh_connect_timeout").ms.toInt
def alive_interval(options: Options): Int =
options.seconds("ssh_alive_interval").ms.toInt
def alive_count_max(options: Options): Int =
options.int("ssh_alive_count_max")
/* init context */
def init_context(options: Options): Context =
{
val config_dir = Path.explode(options.string("ssh_config_dir"))
if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
val jsch = new JSch
val config_file = Path.explode(options.string("ssh_config_file"))
if (config_file.is_file)
jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
val known_hosts = config_dir + Path.explode("known_hosts")
if (!known_hosts.is_file) known_hosts.file.createNewFile
jsch.setKnownHosts(File.platform_path(known_hosts))
val identity_files =
space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
for (identity_file <- identity_files if identity_file.is_file) {
try { jsch.addIdentity(File.platform_path(identity_file)) }
catch {
case exn: JSchException =>
error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
}
}
new Context(options, jsch)
}
def open_session(options: Options,
host: String, user: String = "", port: Int = 0, actual_host: String = "",
proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
permissive: Boolean = false): Session =
init_context(options).open_session(
host = host, user = user, port = port, actual_host = actual_host,
proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
permissive = permissive)
class Context private[SSH](val options: Options, val jsch: JSch)
{
def update_options(new_options: Options): Context = new Context(new_options, jsch)
private def connect_session(host: String, user: String = "", port: Int = 0,
host_key_permissive: Boolean = false,
nominal_host: String = "",
nominal_user: String = "",
on_close: () => Unit = () => ()): Session =
{
val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
session.setUserInfo(No_User_Info)
session.setServerAliveInterval(alive_interval(options))
session.setServerAliveCountMax(alive_count_max(options))
session.setConfig("MaxAuthTries", "3")
if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no")
if (nominal_host != "") session.setHostKeyAlias(nominal_host)
if (options.bool("ssh_compression")) {
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
session.setConfig("compression_level", "9")
}
session.connect(connect_timeout(options))
new Session(options, session, on_close,
proper_string(nominal_host) getOrElse host,
proper_string(nominal_user) getOrElse user)
}
def open_session(
host: String, user: String = "", port: Int = 0, actual_host: String = "",
proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0,
permissive: Boolean = false): Session =
{
val connect_host = proper_string(actual_host) getOrElse host
if (proxy_host == "") connect_session(host = connect_host, user = user, port = port)
else {
val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
val fw =
try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
catch { case exn: Throwable => proxy.close(); throw exn }
try {
connect_session(host = fw.local_host, port = fw.local_port,
host_key_permissive = permissive,
nominal_host = host, nominal_user = user, user = user,
on_close = () => { fw.close(); proxy.close() })
}
catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
}
}
}
/* logging */
def logging(verbose: Boolean = true, debug: Boolean = false): Unit =
{
JSch.setLogger(if (verbose) new Logger(debug) else null)
}
private class Logger(debug: Boolean) extends JSch_Logger
{
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
def log(level: Int, msg: String): Unit =
{
level match {
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
case JSch_Logger.WARN => Output.warning(msg)
case _ => Output.writeln(msg)
}
}
}
/* user info */
object No_User_Info extends UserInfo
{
def getPassphrase: String = null
def getPassword: String = null
def promptPassword(msg: String): Boolean = false
def promptPassphrase(msg: String): Boolean = false
def promptYesNo(msg: String): Boolean = false
def showMessage(msg: String): Unit = Output.writeln(msg)
}
/* port forwarding */
object Port_Forwarding
{
def open(ssh: Session, ssh_close: Boolean,
local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding =
{
val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port)
}
}
class Port_Forwarding private[SSH](
ssh: SSH.Session,
ssh_close: Boolean,
val local_host: String,
val local_port: Int,
val remote_host: String,
val remote_port: Int) extends AutoCloseable
{
override def toString: String =
local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
def close(): Unit =
{
ssh.session.delPortForwardingL(local_host, local_port)
if (ssh_close) ssh.close()
}
}
/* Sftp channel */
type Attrs = SftpATTRS
sealed case class Dir_Entry(name: String, is_dir: Boolean)
{
def is_file: Boolean = !is_dir
}
/* exec channel */
private val exec_wait_delay = Time.seconds(0.3)
class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable
{
override def toString: String = "exec " + session.toString
def close(): Unit = channel.disconnect
val exit_status: Future[Int] =
Future.thread("ssh_wait") {
while (!channel.isClosed) exec_wait_delay.sleep()
channel.getExitStatus
}
val stdin: OutputStream = channel.getOutputStream
val stdout: InputStream = channel.getInputStream
val stderr: InputStream = channel.getErrStream
// connect after preparing streams
channel.connect(connect_timeout(session.options))
def result(
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
strict: Boolean = true): Process_Result =
{
stdin.close()
def read_lines(stream: InputStream, progress: String => Unit): List[String] =
{
val result = new mutable.ListBuffer[String]
val line_buffer = new ByteArrayOutputStream(100)
def line_flush(): Unit =
{
val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
progress(line)
result += line
line_buffer.reset
}
var c = 0
var finished = false
while (!finished) {
while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
if (c == 10) line_flush()
else if (channel.isClosed) {
if (line_buffer.size > 0) line_flush()
finished = true
}
else exec_wait_delay.sleep()
}
result.toList
}
val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
def terminate(): Unit =
{
close()
out_lines.join
err_lines.join
exit_status.join
}
val rc =
try { exit_status.join }
- catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
+ catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
close()
- if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
+ if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
Process_Result(rc, out_lines.join, err_lines.join)
}
}
/* session */
class Session private[SSH](
val options: Options,
val session: JSch_Session,
on_close: () => Unit,
val nominal_host: String,
val nominal_user: String) extends System
{
def update_options(new_options: Options): Session =
new Session(new_options, session, on_close, nominal_host, nominal_user)
def host: String = if (session.getHost == null) "" else session.getHost
override def hg_url: String =
"ssh://" + user_prefix(nominal_user) + nominal_host + "/"
override def toString: String =
user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
(if (session.isConnected) "" else " (disconnected)")
/* port forwarding */
def port_forwarding(
remote_port: Int, remote_host: String = "localhost",
local_port: Int = 0, local_host: String = "localhost",
ssh_close: Boolean = false): Port_Forwarding =
Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port)
/* sftp channel */
val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
sftp.connect(connect_timeout(options))
override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
val settings: JMap[String, String] =
{
val home = sftp.getHome
JMap.of("HOME", home, "USER_HOME", home)
}
override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
override 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))
def rm(path: Path): Unit = sftp.rm(remote_path(path))
def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
private def test_entry(path: Path, as_dir: Boolean): Boolean =
try {
val is_dir = sftp.stat(remote_path(path)).isDir
if (as_dir) is_dir else !is_dir
}
catch { case _: SftpException => false }
override def is_dir(path: Path): Boolean = test_entry(path, true)
override def is_file(path: Path): Boolean = test_entry(path, false)
def is_link(path: Path): Boolean =
try { sftp.lstat(remote_path(path)).isLink }
catch { case _: SftpException => false }
override def make_directory(path: Path): Path =
{
if (!is_dir(path)) {
execute(
"perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
}
path
}
def read_dir(path: Path): List[Dir_Entry] =
{
if (!is_dir(path)) error("No such directory: " + path.toString)
val dir_name = remote_path(path)
val dir = sftp.ls(dir_name)
(for {
i <- (0 until dir.size).iterator
a = dir.get(i).asInstanceOf[AnyRef]
name = Untyped.get[String](a, "filename")
attrs = Untyped.get[Attrs](a, "attrs")
if name != "." && name != ".."
}
yield {
Dir_Entry(name,
if (attrs.isLink) {
try { sftp.stat(dir_name + "/" + name).isDir }
catch { case _: SftpException => false }
}
else attrs.isDir)
}).toList.sortBy(_.name)
}
def find_files(
start: Path,
pred: Path => Boolean = _ => true,
include_dirs: Boolean = false,
follow_links: Boolean = false): List[Path] =
{
val result = new mutable.ListBuffer[Path]
def check(path: Path): Unit = { if (pred(path)) result += path }
def find(dir: Path): Unit =
{
if (include_dirs) check(dir)
if (follow_links || !is_link(dir)) {
for (entry <- read_dir(dir)) {
val path = dir + Path.basic(entry.name)
if (entry.is_file) check(path) else find(path)
}
}
}
if (is_file(start)) check(start) else find(start)
result.toList
}
def open_input(path: Path): InputStream = sftp.get(remote_path(path))
def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
override def read_file(path: Path, local_path: Path): Unit =
sftp.get(remote_path(path), File.platform_path(local_path))
def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
def read(path: Path): String = using(open_input(path))(File.read_stream)
override def write_file(path: Path, local_path: Path): Unit =
sftp.put(File.platform_path(local_path), remote_path(path))
def write_bytes(path: Path, bytes: Bytes): Unit =
using(open_output(path))(bytes.write_stream)
def write(path: Path, text: String): Unit =
using(open_output(path))(stream => Bytes(text).write_stream(stream))
/* exec channel */
def exec(command: String): Exec =
{
val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
new Exec(this, channel)
}
override def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
settings: Boolean = true,
strict: Boolean = true): Process_Result =
exec(command).result(progress_stdout, progress_stderr, strict)
override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this))
/* tmp dirs */
def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
def rm_tree(remote_dir: String): Unit =
execute("rm -r -f " + Bash.string(remote_dir)).check
def tmp_dir(): String =
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
override def with_tmp_dir[A](body: Path => A): A =
{
val remote_dir = tmp_dir()
try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
}
}
/* system operations */
trait System extends AutoCloseable
{
def close(): Unit = ()
def hg_url: String = ""
def expand_path(path: Path): Path = path.expand
def bash_path(path: Path): String = File.bash_path(path)
def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
settings: Boolean = true,
strict: Boolean = true): Process_Result =
Isabelle_System.bash(command,
progress_stdout = progress_stdout,
progress_stderr = progress_stderr,
env = if (settings) Isabelle_System.settings() else null,
strict = strict)
def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
}
object Local extends System
}
diff --git a/src/Pure/ML/ml_console.scala b/src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala
+++ b/src/Pure/ML/ml_console.scala
@@ -1,84 +1,84 @@
/* Title: Pure/ML/ml_console.scala
Author: Makarius
The raw ML process in interactive mode.
*/
package isabelle
object ML_Console
{
/* command line entry point */
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var dirs: List[Path] = Nil
var include_sessions: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var modes: List[String] = Nil
var no_build = false
var options = Options.init()
var raw_ml_system = false
val getopts = Getopts("""
Usage: isabelle console [OPTIONS]
Options are:
-d DIR include session directory
-i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-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)
-r bootstrap from raw Poly/ML
Build a logic session image and run the raw Isabelle ML process
in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
""",
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"r" -> (_ => raw_ml_system = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val sessions_structure = Sessions.load_structure(options, dirs = dirs)
val store = Sessions.store(options)
// build logic
if (!no_build && !raw_ml_system) {
val progress = new Console_Progress()
val rc =
progress.interrupt_handler {
Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
}
- if (rc != 0) sys.exit(rc)
+ if (rc != Process_Result.RC.ok) sys.exit(rc)
}
// process loop
val process =
ML_Process(options, sessions_structure, store,
logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system,
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(
options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
POSIX_Interrupt.handler { process.interrupt() } {
new TTY_Loop(process.stdin, process.stdout).join()
val rc = process.join()
- if (rc != 0) sys.exit(rc)
+ if (rc != Process_Result.RC.ok) sys.exit(rc)
}
}
}
}
diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala
+++ b/src/Pure/System/bash.scala
@@ -1,396 +1,396 @@
/* Title: Pure/System/bash.scala
Author: Makarius
Support for GNU bash: portable external processes with propagation of
interrupts.
*/
package isabelle
import java.util.{List => JList, Map => JMap}
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
File => JFile, IOException}
import scala.annotation.tailrec
import scala.jdk.OptionConverters._
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 def make_description(description: String): String =
proper_string(description) getOrElse "bash_process"
type Watchdog = (Time, Process => Boolean)
def process(script: String,
description: String = "",
cwd: JFile = null,
env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => ()): Process =
new Process(script, description, cwd, env, redirect, cleanup)
class Process private[Bash](
script: String,
description: String,
cwd: JFile,
env: JMap[String, String],
redirect: Boolean,
cleanup: () => Unit)
{
override def toString: String = make_description(description)
private val timing_file = Isabelle_System.tmp_file("bash_timing")
private val timing = Synchronized[Option[Timing]](None)
def get_timing: Timing = timing.value getOrElse Timing.zero
private val winpid_file: Option[JFile] =
if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None
private val winpid_script =
winpid_file match {
case None => script
case Some(file) =>
"read < /proc/self/winpid > /dev/null 2> /dev/null\n" +
"""echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script
}
private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
File.write(script_file, winpid_script)
private val proc =
isabelle.setup.Environment.process_builder(
JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
File.standard_path(timing_file), "bash", File.standard_path(script_file)),
cwd, env, redirect).start()
// channels
val stdin: BufferedWriter =
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
val stdout: BufferedReader =
new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
val stderr: BufferedReader =
new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
// signals
private val group_pid = stdout.readLine
private def process_alive(pid: String): Boolean =
(for {
p <- Value.Long.unapply(pid)
handle <- ProcessHandle.of(p).toScala
} yield handle.isAlive) getOrElse false
private def root_process_alive(): Boolean =
winpid_file match {
case None => process_alive(group_pid)
case Some(file) =>
file.exists() && process_alive(Library.trim_line(File.read(file)))
}
@tailrec private def signal(s: String, count: Int = 1): Boolean =
{
count <= 0 ||
{
isabelle.setup.Environment.kill_process(group_pid, s)
val running =
root_process_alive() ||
isabelle.setup.Environment.kill_process(group_pid, "0")
if (running) {
Time.seconds(0.1).sleep()
signal(s, count - 1)
}
else false
}
}
def terminate(): Unit = Isabelle_Thread.try_uninterruptible
{
signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL")
proc.destroy()
do_cleanup()
}
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
{
isabelle.setup.Environment.kill_process(group_pid, "INT")
}
// JVM shutdown hook
private val shutdown_hook = Isabelle_Thread.create(() => terminate())
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
// cleanup
private def do_cleanup(): Unit =
{
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
script_file.delete()
winpid_file.foreach(_.delete())
timing.change {
case None =>
if (timing_file.isFile) {
val t =
Word.explode(File.read(timing_file)) match {
case List(Value.Long(elapsed), Value.Long(cpu)) =>
Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
case _ => Timing.zero
}
timing_file.delete
Some(t)
}
else Some(Timing.zero)
case some => some
}
cleanup()
}
// join
def join(): Int =
{
val rc = proc.waitFor()
do_cleanup()
rc
}
// result
def result(
input: String = "",
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
watchdog: Option[Watchdog] = None,
strict: Boolean = true): Process_Result =
{
val in =
if (input.isEmpty) Future.value(stdin.close())
else Future.thread("bash_stdin") { stdin.write(input); stdin.flush(); stdin.close(); }
val out_lines =
Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
val err_lines =
Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
val watchdog_thread =
for ((time, check) <- watchdog)
yield {
Future.thread("bash_watchdog") {
while (proc.isAlive) {
time.sleep()
if (check(this)) interrupt()
}
}
}
val rc =
try { join() }
- catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
+ catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
watchdog_thread.foreach(_.cancel())
in.join
out_lines.join
err_lines.join
- if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
+ if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
Process_Result(rc, out_lines.join, err_lines.join, get_timing)
}
}
/* server */
object Server
{
// input messages
private val RUN = "run"
private val KILL = "kill"
// output messages
private val UUID = "uuid"
private val INTERRUPT = "interrupt"
private val FAILURE = "failure"
private val RESULT = "result"
def start(port: Int = 0, debugging: => Boolean = false): Server =
{
val server = new Server(port, debugging)
server.start()
server
}
}
class Server private(port: Int, debugging: => Boolean)
extends isabelle.Server.Handler(port)
{
server =>
private val _processes = Synchronized(Map.empty[UUID.T, Bash.Process])
override def stop(): Unit =
{
for ((_, process) <- _processes.value) process.terminate()
super.stop()
}
override def handle(connection: isabelle.Server.Connection): Unit =
{
def reply(chunks: List[String]): Unit =
try { connection.write_byte_message(chunks.map(Bytes.apply)) }
catch { case _: IOException => }
def reply_failure(exn: Throwable): Unit =
reply(
if (Exn.is_interrupt(exn)) List(Server.INTERRUPT)
else List(Server.FAILURE, Exn.message(exn)))
def reply_result(result: Process_Result): Unit =
reply(
Server.RESULT ::
result.rc.toString ::
result.timing.elapsed.ms.toString ::
result.timing.cpu.ms.toString ::
result.out_lines.length.toString ::
result.out_lines :::
result.err_lines)
connection.read_byte_message().map(_.map(_.text)) match {
case None =>
case Some(List(Server.KILL, UUID(uuid))) =>
if (debugging) Output.writeln("kill " + uuid)
_processes.value.get(uuid).foreach(_.terminate())
case Some(List(Server.RUN, script, input, cwd, putenv,
Value.Boolean(redirect), Value.Seconds(timeout), description)) =>
val uuid = UUID.random()
val descr = make_description(description)
if (debugging) {
Output.writeln(
"start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")")
}
Exn.capture {
Bash.process(script,
description = description,
cwd =
XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match {
case None => null
case Some(s) => Path.explode(s).file
},
env =
Isabelle_System.settings(
XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))(
YXML.parse_body(putenv))),
redirect= redirect)
}
match {
case Exn.Exn(exn) => reply_failure(exn)
case Exn.Res(process) =>
_processes.change(processes => processes + (uuid -> process))
reply(List(Server.UUID, uuid.toString))
Isabelle_Thread.fork(name = "bash_process") {
@volatile var is_timeout = false
val watchdog: Option[Watchdog] =
if (timeout.is_zero) None else Some((timeout, _ => { is_timeout = true; true }))
Exn.capture { process.result(input = input, watchdog = watchdog, strict = false) }
match {
case Exn.Exn(exn) => reply_failure(exn)
case Exn.Res(res0) =>
val res = if (!res0.ok && is_timeout) res0.timeout_rc else res0
if (debugging) {
Output.writeln(
"stop " + quote(descr) + " (uuid=" + uuid + ", return_code=" + res.rc + ")")
}
reply_result(res)
}
_processes.change(provers => provers - uuid)
}
connection.await_close()
}
case Some(_) => reply_failure(ERROR("Bad protocol message"))
}
}
}
class Handler extends Session.Protocol_Handler
{
private var server: Server = null
override def init(session: Session): Unit =
{
exit()
server = Server.start(debugging = session.session_options.bool("bash_process_debugging"))
}
override def exit(): Unit =
{
if (server != null) {
server.stop()
server = null
}
}
override def prover_options(options: Options): Options =
{
val address = if (server == null) "" else server.address
val password = if (server == null) "" else server.password
options +
("bash_process_address=" + address) +
("bash_process_password=" + password)
}
}
}
diff --git a/src/Pure/System/command_line.scala b/src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala
+++ b/src/Pure/System/command_line.scala
@@ -1,42 +1,42 @@
/* Title: Pure/System/command_line.scala
Author: Makarius
Support for Isabelle/Scala command line tools.
*/
package isabelle
object Command_Line
{
object Chunks
{
private def chunks(list: List[String]): List[List[String]] =
list.indexWhere(_ == "\n") match {
case -1 => List(list)
case i =>
val (chunk, rest) = list.splitAt(i)
chunk :: chunks(rest.tail)
}
def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
}
def tool(body: => Unit): Unit =
{
val thread =
Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
val rc =
- try { body; 0 }
+ try { body; Process_Result.RC.ok }
catch {
case exn: Throwable =>
Output.error_message(Exn.print(exn))
Exn.failure_rc(exn)
}
sys.exit(rc)
}
thread.join()
}
def ML_tool(body: List[String]): String =
"Command_Line.tool (fn () => (" + body.mkString("; ") + "));"
}
diff --git a/src/Pure/System/getopts.scala b/src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala
+++ b/src/Pure/System/getopts.scala
@@ -1,72 +1,72 @@
/* Title: Pure/System/getopts.scala
Author: Makarius
Support for command-line options as in GNU bash.
*/
package isabelle
import scala.annotation.tailrec
object Getopts
{
def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
{
val options =
option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
case (m, (s, f)) =>
val (a, entry) =
if (s.length == 1) (s(0), (false, f))
else if (s.length == 2 && s.endsWith(":")) (s(0), (true, f))
else error("Bad option specification: " + quote(s))
if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
else m + (a -> entry)
}
new Getopts(usage_text, options)
}
}
class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
{
def usage(): Nothing =
{
Output.writeln(usage_text, stdout = true)
- sys.exit(1)
+ sys.exit(Process_Result.RC.error)
}
private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
private def print_option(opt: Char): String = quote("-" + opt.toString)
private def option(opt: Char, opt_arg: List[Char]): Unit =
try { options(opt)._2.apply(opt_arg.mkString) }
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
}
@tailrec private def getopts(args: List[List[Char]]): List[List[Char]] =
args match {
case List('-', '-') :: rest_args => rest_args
case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
case List('-', opt) :: rest_args if is_option0(opt) =>
option(opt, Nil); getopts(rest_args)
case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
option(opt, opt_arg); getopts(rest_args)
case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
option(opt, opt_arg); getopts(rest_args)
case List(List('-', opt)) if is_option1(opt) =>
Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
usage()
case ('-' :: opt :: _) :: _ if !is_option(opt) =>
if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
usage()
case _ => args
}
def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
def apply(args: Array[String]): List[String] = apply(args.toList)
}
diff --git a/src/Pure/System/process_result.scala b/src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala
+++ b/src/Pure/System/process_result.scala
@@ -1,87 +1,97 @@
/* Title: Pure/System/process_result.scala
Author: Makarius
Result of system process.
*/
package isabelle
object Process_Result
{
- def print_return_code(rc: Int): String = "Return code: " + rc + rc_text(rc)
- def print_rc(rc: Int): String = "return code " + rc + rc_text(rc)
+ /* return code */
- def rc_text(rc: Int): String =
- return_code_text.get(rc) match {
- case None => ""
- case Some(text) => " (" + text + ")"
+ object RC
+ {
+ val ok = 0
+ val error = 1
+ val failure = 2
+ val interrupt = 130
+ val timeout = 142
+
+ private def text(rc: Int): String =
+ {
+ val txt =
+ rc match {
+ case `ok` => "OK"
+ case `error` => "ERROR"
+ case `failure` => "FAILURE"
+ case 127 => "COMMAND NOT FOUND"
+ case `interrupt` => "INTERRUPT"
+ case 131 => "QUIT SIGNAL"
+ case 137 => "KILL SIGNAL"
+ case 138 => "BUS ERROR"
+ case 139 => "SEGMENTATION VIOLATION"
+ case `timeout` => "TIMEOUT"
+ case 143 => "TERMINATION SIGNAL"
+ case _ => ""
+ }
+ if (txt.isEmpty) txt else " (" + txt + ")"
}
- val interrupt_rc = 130
- val timeout_rc = 142
-
- private val return_code_text =
- Map(0 -> "OK",
- 1 -> "ERROR",
- 2 -> "FAILURE",
- 127 -> "COMMAND NOT FOUND",
- interrupt_rc -> "INTERRUPT",
- 131 -> "QUIT SIGNAL",
- 137 -> "KILL SIGNAL",
- 138 -> "BUS ERROR",
- 139 -> "SEGMENTATION VIOLATION",
- timeout_rc -> "TIMEOUT",
- 143 -> "TERMINATION SIGNAL")
+ def print_long(rc: Int): String = "Return code: " + rc + text(rc)
+ def print(rc: Int): String = "return code " + rc + text(rc)
+ }
}
final case class Process_Result(
rc: Int,
out_lines: List[String] = Nil,
err_lines: List[String] = Nil,
timing: Timing = Timing.zero)
{
def out: String = Library.trim_line(cat_lines(out_lines))
def err: String = Library.trim_line(cat_lines(err_lines))
def output(outs: List[String]): Process_Result =
copy(out_lines = out_lines ::: outs.flatMap(split_lines))
def errors(errs: List[String]): Process_Result =
copy(err_lines = err_lines ::: errs.flatMap(split_lines))
def error(err: String): Process_Result =
if (err.isEmpty) this else errors(List(err))
- def ok: Boolean = rc == 0
- def interrupted: Boolean = rc == Process_Result.interrupt_rc
+ def ok: Boolean = rc == Process_Result.RC.ok
+ def interrupted: Boolean = rc == Process_Result.RC.interrupt
- def timeout_rc: Process_Result = copy(rc = Process_Result.timeout_rc)
- def timeout: Boolean = rc == Process_Result.timeout_rc
+ def timeout_rc: Process_Result = copy(rc = Process_Result.RC.timeout)
+ def timeout: Boolean = rc == Process_Result.RC.timeout
- def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
+ def error_rc: Process_Result =
+ if (interrupted) this else copy(rc = rc max Process_Result.RC.error)
def errors_rc(errs: List[String]): Process_Result =
if (errs.isEmpty) this else errors(errs).error_rc
def check_rc(pred: Int => Boolean): Process_Result =
if (pred(rc)) this
else if (interrupted) throw Exn.Interrupt()
else Exn.error(err)
- def check: Process_Result = check_rc(_ == 0)
+ def check: Process_Result = check_rc(_ == Process_Result.RC.ok)
- def print_return_code: String = Process_Result.print_return_code(rc)
- def print_rc: String = Process_Result.print_rc(rc)
+ def print_return_code: String = Process_Result.RC.print_long(rc)
+ def print_rc: String = Process_Result.RC.print(rc)
def print: Process_Result =
{
Output.warning(err)
Output.writeln(out)
copy(out_lines = Nil, err_lines = Nil)
}
def print_stdout: Process_Result =
{
Output.warning(err, stdout = true)
Output.writeln(out, stdout = true)
copy(out_lines = Nil, err_lines = Nil)
}
}
diff --git a/src/Pure/Thy/export.scala b/src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala
+++ b/src/Pure/Thy/export.scala
@@ -1,469 +1,469 @@
/* Title: Pure/Thy/export.scala
Author: Makarius
Manage theory exports: compressed blobs.
*/
package isabelle
import scala.annotation.tailrec
import scala.util.matching.Regex
object Export
{
/* artefact names */
val DOCUMENT_ID = "PIDE/document_id"
val FILES = "PIDE/files"
val MARKUP = "PIDE/markup"
val MESSAGES = "PIDE/messages"
val DOCUMENT_PREFIX = "document/"
val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex"
val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
val THEORY_PREFIX: String = "theory/"
val PROOFS_PREFIX: String = "proofs/"
def explode_name(s: String): List[String] = space_explode('/', s)
def implode_name(elems: Iterable[String]): String = elems.mkString("/")
/* SQL data model */
object Data
{
val session_name = SQL.Column.string("session_name").make_primary_key
val theory_name = SQL.Column.string("theory_name").make_primary_key
val name = SQL.Column.string("name").make_primary_key
val executable = SQL.Column.bool("executable")
val compressed = SQL.Column.bool("compressed")
val body = SQL.Column.bytes("body")
val table =
SQL.Table("isabelle_exports",
List(session_name, theory_name, name, executable, compressed, body))
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
"WHERE " + Data.session_name.equal(session_name) +
(if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
(if (name == "") "" else " AND " + Data.name.equal(name))
}
def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
{
val select =
Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
db.using_statement(select)(stmt => stmt.execute_query().next())
}
def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
{
val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res => res.string(Data.name)).toList)
}
def read_theory_names(db: SQL.Database, session_name: String): List[String] =
{
val select =
Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
}
def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
{
val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
(res.string(Data.theory_name), res.string(Data.name))).toList)
}
def message(msg: String, theory_name: String, name: String): String =
msg + " " + quote(name) + " for theory " + quote(theory_name)
def compound_name(a: String, b: String): String =
if (a.isEmpty) b else a + ":" + b
def empty_entry(theory_name: String, name: String): Entry =
Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none)
sealed case class Entry(
session_name: String,
theory_name: String,
name: String,
executable: Boolean,
body: Future[(Boolean, Bytes)],
cache: XML.Cache)
{
override def toString: String = name
def compound_name: String = Export.compound_name(theory_name, name)
def name_has_prefix(s: String): Boolean = name.startsWith(s)
val name_elems: List[String] = explode_name(name)
def name_extends(elems: List[String]): Boolean =
name_elems.startsWith(elems) && name_elems != elems
def text: String = uncompressed.text
def uncompressed: Bytes =
{
val (compressed, bytes) = body.join
if (compressed) bytes.uncompress(cache = cache.xz) else bytes
}
def uncompressed_yxml: XML.Body =
YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
def write(db: SQL.Database): Unit =
{
val (compressed, bytes) = body.join
db.using_statement(Data.table.insert())(stmt =>
{
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
stmt.bool(4) = executable
stmt.bool(5) = compressed
stmt.bytes(6) = bytes
stmt.execute()
})
}
}
def make_regex(pattern: String): Regex =
{
@tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
chs match {
case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
case '*' :: rest => make("[^:/]*" :: result, depth, rest)
case '?' :: rest => make("[^:/]" :: result, depth, rest)
case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
case '{' :: rest => make("(" :: result, depth + 1, rest)
case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
case c :: rest => make(c.toString :: result, depth, rest)
case Nil => result.reverse.mkString.r
}
make(Nil, 0, pattern.toList)
}
def make_matcher(pattern: String): (String, String) => Boolean =
{
val regex = make_regex(pattern)
(theory_name: String, name: String) =>
regex.pattern.matcher(compound_name(theory_name, name)).matches
}
def make_entry(
session_name: String, args: Protocol.Export.Args, bytes: Bytes, cache: XML.Cache): Entry =
{
val body =
if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
else Future.value((false, bytes))
Entry(session_name, args.theory_name, args.name, args.executable, body, cache)
}
def read_entry(db: SQL.Database, cache: XML.Cache,
session_name: String, theory_name: String, name: String): Option[Entry] =
{
val select =
Data.table.select(List(Data.executable, Data.compressed, Data.body),
Data.where_equal(session_name, theory_name, name))
db.using_statement(select)(stmt =>
{
val res = stmt.execute_query()
if (res.next()) {
val executable = res.bool(Data.executable)
val compressed = res.bool(Data.compressed)
val bytes = res.bytes(Data.body)
val body = Future.value(compressed, bytes)
Some(Entry(session_name, theory_name, name, executable, body, cache))
}
else None
})
}
def read_entry(dir: Path, cache: XML.Cache,
session_name: String, theory_name: String, name: String): Option[Entry] =
{
val path = dir + Path.basic(theory_name) + Path.explode(name)
if (path.is_file) {
val executable = File.is_executable(path)
val uncompressed = Bytes.read(path)
val body = Future.value((false, uncompressed))
Some(Entry(session_name, theory_name, name, executable, body, cache))
}
else None
}
/* database consumer thread */
def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer =
new Consumer(db, cache, progress)
class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress)
{
private val errors = Synchronized[List[String]](Nil)
private val consumer =
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
bulk = { case (entry, _) => entry.body.is_finished },
consume =
(args: List[(Entry, Boolean)]) =>
{
val results =
db.transaction {
for ((entry, strict) <- args)
yield {
if (progress.stopped) {
entry.body.cancel()
Exn.Res(())
}
else if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
if (strict) {
val msg = message("Duplicate export", entry.theory_name, entry.name)
errors.change(msg :: _)
}
Exn.Res(())
}
else Exn.capture { entry.write(db) }
}
}
(results, true)
})
def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit =
{
if (!progress.stopped) {
consumer.send(make_entry(session_name, args, body, cache) -> args.strict)
}
}
def shutdown(close: Boolean = false): List[String] =
{
consumer.shutdown()
if (close) db.close()
errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil)
}
}
/* abstract provider */
object Provider
{
def none: Provider =
new Provider {
def apply(export_name: String): Option[Entry] = None
def focus(other_theory: String): Provider = this
override def toString: String = "none"
}
def database_context(
context: Sessions.Database_Context,
sessions: List[String],
theory_name: String): Provider =
new Provider {
def apply(export_name: String): Option[Entry] =
context.read_export(sessions, theory_name, export_name)
def focus(other_theory: String): Provider = this
override def toString: String = context.toString
}
def database(db: SQL.Database, cache: XML.Cache, session_name: String, theory_name: String)
: Provider =
{
new Provider {
def apply(export_name: String): Option[Entry] =
read_entry(db, cache, session_name, theory_name, export_name)
def focus(other_theory: String): Provider =
if (other_theory == theory_name) this
else Provider.database(db, cache, session_name, other_theory)
override def toString: String = db.toString
}
}
def snapshot(snapshot: Document.Snapshot): Provider =
new Provider {
def apply(export_name: String): Option[Entry] =
snapshot.exports_map.get(export_name)
def focus(other_theory: String): Provider =
if (other_theory == snapshot.node_name.theory) this
else {
val node_name =
snapshot.version.nodes.theory_name(other_theory) getOrElse
error("Bad theory " + quote(other_theory))
Provider.snapshot(snapshot.state.snapshot(node_name))
}
override def toString: String = snapshot.toString
}
def directory(dir: Path, cache: XML.Cache, session_name: String, theory_name: String)
: Provider =
{
new Provider {
def apply(export_name: String): Option[Entry] =
read_entry(dir, cache, session_name, theory_name, export_name)
def focus(other_theory: String): Provider =
if (other_theory == theory_name) this
else Provider.directory(dir, cache, session_name, other_theory)
override def toString: String = dir.toString
}
}
}
trait Provider
{
def apply(export_name: String): Option[Entry]
def uncompressed_yxml(export_name: String): XML.Body =
apply(export_name) match {
case Some(entry) => entry.uncompressed_yxml
case None => Nil
}
def focus(other_theory: String): Provider
}
/* export to file-system */
def export_files(
store: Sessions.Store,
session_name: String,
export_dir: Path,
progress: Progress = new Progress,
export_prune: Int = 0,
export_list: Boolean = false,
export_patterns: List[String] = Nil): Unit =
{
using(store.open_database(session_name))(db =>
{
db.transaction {
val export_names = read_theory_exports(db, session_name)
// list
if (export_list) {
(for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
sorted.foreach(progress.echo)
}
// export
if (export_patterns.nonEmpty) {
val exports =
(for {
export_pattern <- export_patterns.iterator
matcher = make_matcher(export_pattern)
(theory_name, name) <- export_names if matcher(theory_name, name)
} yield (theory_name, name)).toSet
for {
(theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
name <- group.map(_._2).sorted
entry <- read_entry(db, store.cache, session_name, theory_name, name)
} {
val elems = theory_name :: space_explode('/', name)
val path =
if (elems.length < export_prune + 1) {
error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
}
else export_dir + Path.make(elems.drop(export_prune))
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
Isabelle_System.make_directory(path.dir)
val bytes = entry.uncompressed
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
File.set_executable(path, entry.executable)
}
}
}
})
}
/* Isabelle tool wrapper */
val default_export_dir: Path = Path.explode("export")
val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports",
Scala_Project.here, args =>
{
/* arguments */
var export_dir = default_export_dir
var dirs: List[Path] = Nil
var export_list = false
var no_build = false
var options = Options.init()
var export_prune = 0
var export_patterns: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle export [OPTIONS] SESSION
Options are:
-O DIR output directory for exported files (default: """ + default_export_dir + """)
-d DIR include session directory
-l list exports
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NUM prune path of exported files by NUM elements
-x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
isabelle build. Option -l or -x is required; option -x may be repeated.
The PATTERN language resembles glob patterns in the shell, with ? and *
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
and variants {pattern1,pattern2,pattern3}.
""",
"O:" -> (arg => export_dir = Path.explode(arg)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l" -> (_ => export_list = true),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => export_prune = Value.Int.parse(arg)),
"x:" -> (arg => export_patterns ::= arg))
val more_args = getopts(args)
val session_name =
more_args match {
case List(session_name) if export_list || export_patterns.nonEmpty => session_name
case _ => getopts.usage()
}
val progress = new Console_Progress()
/* build */
if (!no_build) {
val rc =
progress.interrupt_handler {
Build.build_logic(options, session_name, progress = progress, dirs = dirs)
}
- if (rc != 0) sys.exit(rc)
+ if (rc != Process_Result.RC.ok) sys.exit(rc)
}
/* export files */
val store = Sessions.store(options)
export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
export_list = export_list, export_patterns = export_patterns)
})
}
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,687 +1,687 @@
/* Title: Pure/Tools/build.scala
Author: Makarius
Options: :folding=explicit:
Build and manage Isabelle sessions.
*/
package isabelle
import scala.collection.immutable.SortedSet
import scala.annotation.tailrec
object Build
{
/** auxiliary **/
/* persistent build info */
sealed case class Session_Info(
sources: String,
input_heaps: List[String],
output_heap: Option[String],
return_code: Int)
{
def ok: Boolean = return_code == 0
}
/* queue with scheduling information */
private object Queue
{
type Timings = (List[Properties.T], Double)
def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
{
val no_timings: Timings = (Nil, 0.0)
store.try_open_database(session_name) match {
case None => no_timings
case Some(db) =>
def ignore_error(msg: String) =
{
progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
no_timings
}
try {
val command_timings = store.read_command_timings(db, session_name)
val session_timing =
store.read_session_timing(db, session_name) match {
case Markup.Elapsed(t) => t
case _ => 0.0
}
(command_timings, session_timing)
}
catch {
case ERROR(msg) => ignore_error(msg)
case exn: java.lang.Error => ignore_error(Exn.message(exn))
case _: XML.Error => ignore_error("")
}
finally { db.close() }
}
}
def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
: Map[String, Double] =
{
val maximals = sessions_structure.build_graph.maximals.toSet
def desc_timing(session_name: String): Double =
{
if (maximals.contains(session_name)) timing(session_name)
else {
val descendants = sessions_structure.build_descendants(List(session_name)).toSet
val g = sessions_structure.build_graph.restrict(descendants)
(0.0 :: g.maximals.flatMap(desc => {
val ps = g.all_preds(List(desc))
if (ps.exists(p => !timing.isDefinedAt(p))) None
else Some(ps.map(timing(_)).sum)
})).max
}
}
timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
}
def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
: Queue =
{
val graph = sessions_structure.build_graph
val names = graph.keys
val timings = names.map(name => (name, load_timings(progress, store, name)))
val command_timings =
timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
val session_timing =
make_session_timing(sessions_structure,
timings.map({ case (name, (_, t)) => (name, t) }).toMap)
object Ordering extends scala.math.Ordering[String]
{
def compare(name1: String, name2: String): Int =
session_timing(name2) compare session_timing(name1) match {
case 0 =>
sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
case 0 => name1 compare name2
case ord => ord
}
case ord => ord
}
}
new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
}
}
private class Queue(
graph: Graph[String, Sessions.Info],
order: SortedSet[String],
val command_timings: String => List[Properties.T])
{
def is_inner(name: String): Boolean = !graph.is_maximal(name)
def is_empty: Boolean = graph.is_empty
def - (name: String): Queue =
new Queue(graph.del_node(name), order - name, command_timings)
def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
{
val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
else None
}
}
/** build with results **/
class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
{
def sessions: Set[String] = results.keySet
def infos: List[Sessions.Info] = results.values.map(_._2).toList
def cancelled(name: String): Boolean = results(name)._1.isEmpty
def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
def info(name: String): Sessions.Info = results(name)._2
val rc: Int =
results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
- foldLeft(0)(_ max _)
- def ok: Boolean = rc == 0
+ foldLeft(Process_Result.RC.ok)(_ max _)
+ def ok: Boolean = rc == Process_Result.RC.ok
override def toString: String = rc.toString
}
def session_finished(session_name: String, process_result: Process_Result): String =
"Finished " + session_name + " (" + process_result.timing.message_resources + ")"
def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
{
val props = build_log.session_timing
val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
val timing = Markup.Timing_Properties.parse(props)
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
}
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,
presentation: Presentation.Context = Presentation.Context.none,
progress: Progress = new Progress,
check_unknown_files: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
infos: List[Sessions.Info] = Nil,
numa_shuffling: Boolean = false,
max_jobs: Int = 1,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
fresh_build: Boolean = false,
no_build: Boolean = false,
soft_build: Boolean = false,
verbose: Boolean = false,
export_files: Boolean = false,
session_setup: (String, Session) => Unit = (_, _) => ()): Results =
{
val build_options =
options +
"completion_limit=0" +
"editor_tracing_messages=0" +
"kodkod_scala=false" +
("pide_reports=" + options.bool("build_pide_reports"))
val store = Sessions.store(build_options)
Isabelle_Fonts.init()
/* session selection and dependencies */
val full_sessions =
Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
val full_sessions_selection = full_sessions.imports_selection(selection)
def sources_stamp(deps: Sessions.Deps, session_name: String): String =
{
val digests =
full_sessions(session_name).meta_digest ::
deps.sources(session_name) :::
deps.imported_sources(session_name)
SHA1.digest_set(digests).toString
}
val deps =
{
val deps0 =
Sessions.deps(full_sessions.selection(selection),
progress = progress, inlined_files = true, verbose = verbose,
list_files = list_files, check_keywords = check_keywords).check_errors
if (soft_build && !fresh_build) {
val outdated =
deps0.sessions_structure.build_topological_order.flatMap(name =>
store.try_open_database(name) match {
case Some(db) =>
using(db)(store.read_build(_, name)) match {
case Some(build)
if build.ok && build.sources == sources_stamp(deps0, name) => None
case _ => Some(name)
}
case None => Some(name)
})
Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
progress = progress, inlined_files = true).check_errors
}
else deps0
}
/* check unknown files */
if (check_unknown_files) {
val source_files =
(for {
(_, base) <- deps.session_bases.iterator
(path, _) <- base.sources.iterator
} yield path).toList
val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
val unknown_files =
Mercurial.check_files(source_files)._2.
filterNot(path => exclude_files.contains(path.canonical_file))
if (unknown_files.nonEmpty) {
progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
}
}
/* main build process */
val queue = Queue(progress, deps.sessions_structure, store)
store.prepare_output_dir()
if (clean_build) {
for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
val (relevant, ok) = store.clean_output(name)
if (relevant) {
if (ok) progress.echo("Cleaned " + name)
else progress.echo(name + " FAILED to clean")
}
}
}
// scheduler loop
case class Result(
current: Boolean,
heap_digest: Option[String],
process: Option[Process_Result],
info: Sessions.Info)
{
def ok: Boolean =
process match {
case None => false
- case Some(res) => res.rc == 0
+ case Some(res) => res.ok
}
}
def sleep(): Unit =
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
val log =
build_options.string("system_log") match {
case "" => No_Logger
case "true" => Logger.make(progress)
case log_file => Logger.make(Some(Path.explode(log_file)))
}
val numa_nodes = new NUMA.Nodes(numa_shuffling)
@tailrec def loop(
pending: Queue,
running: Map[String, (List[String], Build_Job)],
results: Map[String, Result]): Map[String, Result] =
{
def used_node(i: Int): Boolean =
running.iterator.exists(
{ case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
if (pending.is_empty) results
else {
if (progress.stopped) {
for ((_, (_, job)) <- running) job.terminate()
}
running.find({ case (_, (_, job)) => job.is_finished }) match {
case Some((session_name, (input_heaps, job))) =>
//{{{ finish job
val (process_result, heap_digest) = job.join
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
val process_result_tail =
{
val tail = job.info.options.int("process_output_tail")
process_result.copy(
out_lines =
"(see also " + store.output_log(session_name).file.toString + ")" ::
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
}
val build_log =
Build_Log.Log_File(session_name, process_result.out_lines).
parse_session_info(
command_timings = true,
theory_timings = true,
ml_statistics = true,
task_statistics = true)
// write log file
if (process_result.ok) {
File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
}
else File.write(store.output_log(session_name), terminate_lines(log_lines))
// write database
using(store.open_database(session_name, output = true))(db =>
store.write_session_info(db, session_name,
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
process_result.rc)))
// messages
process_result.err_lines.foreach(progress.echo)
if (process_result.ok) {
if (verbose) progress.echo(session_timing(session_name, build_log))
progress.echo(session_finished(session_name, process_result))
}
else {
progress.echo(session_name + " FAILED")
if (!process_result.interrupted) progress.echo(process_result_tail.out)
}
loop(pending - session_name, running - session_name,
results +
(session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
//}}}
case None if running.size < (max_jobs max 1) =>
//{{{ check/start next job
pending.dequeue(running.isDefinedAt) match {
case Some((session_name, info)) =>
val ancestor_results =
deps.sessions_structure.build_requirements(List(session_name)).
filterNot(_ == session_name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
val do_store =
build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
val (current, heap_digest) =
{
store.try_open_database(session_name) match {
case Some(db) =>
using(db)(store.read_build(_, session_name)) match {
case Some(build) =>
val heap_digest = store.find_heap_digest(session_name)
val current =
!fresh_build &&
build.ok &&
build.sources == sources_stamp(deps, session_name) &&
build.input_heaps == ancestor_heaps &&
build.output_heap == heap_digest &&
!(do_store && heap_digest.isEmpty)
(current, heap_digest)
case None => (false, None)
}
case None => (false, None)
}
}
val all_current = current && ancestor_results.forall(_.current)
if (all_current)
loop(pending - session_name, running,
results +
(session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
else if (no_build) {
progress.echo_if(verbose, "Skipping " + session_name + " ...")
loop(pending - session_name, running,
results +
(session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
}
else if (ancestor_results.forall(_.ok) && !progress.stopped) {
progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
store.clean_output(session_name)
using(store.open_database(session_name, output = true))(
store.init_session_info(_, session_name))
val numa_node = numa_nodes.next(used_node)
val job =
new Build_Job(progress, session_name, info, deps, store, do_store,
log, session_setup, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
else {
progress.echo(session_name + " CANCELLED")
loop(pending - session_name, running,
results + (session_name -> Result(false, heap_digest, None, info)))
}
case None => sleep(); loop(pending, running, results)
}
///}}}
case None => sleep(); loop(pending, running, results)
}
}
}
/* build results */
val results =
{
val results0 =
if (deps.is_empty) {
progress.echo_warning("Nothing to build")
Map.empty[String, Result]
}
else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
new Results(
(for ((name, result) <- results0.iterator)
yield (name, (result.process, result.info))).toMap)
}
if (export_files) {
for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
val info = results.info(name)
if (info.export_files.nonEmpty) {
progress.echo("Exporting " + info.name + " ...")
for ((dir, prune, pats) <- info.export_files) {
Export.export_files(store, name, info.dir + dir,
progress = if (verbose) progress else new Progress,
export_prune = prune,
export_patterns = pats)
}
}
}
}
- if (results.rc != 0 && (verbose || !no_build)) {
+ if (results.rc != Process_Result.RC.ok && (verbose || !no_build)) {
val unfinished =
(for {
name <- results.sessions.iterator
if !results(name).ok
} yield name).toList.sorted
progress.echo("Unfinished session(s): " + commas(unfinished))
}
/* PDF/HTML presentation */
if (!no_build && !progress.stopped && results.ok) {
val selected = full_sessions_selection.toSet
val presentation_chapters =
(for {
session_name <- deps.sessions_structure.build_topological_order.iterator
info = results.info(session_name)
if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
yield (info.chapter, (session_name, info.description))).toList
if (presentation_chapters.nonEmpty) {
val presentation_dir = presentation.dir(store)
progress.echo("Presentation in " + presentation_dir.absolute)
val resources = Resources.empty
val html_context = Presentation.html_context()
using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
progress.expose_interrupt()
progress.echo("Presenting " + session_name + " ...")
Presentation.session_html(
resources, session_name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
elements = Presentation.elements1, presentation = presentation)
})
val browser_chapters =
presentation_chapters.groupBy(_._1).
map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
for ((chapter, entries) <- browser_chapters)
Presentation.update_chapter_index(presentation_dir, chapter, entries)
if (browser_chapters.nonEmpty) Presentation.make_global_index(presentation_dir)
}
}
results
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
Scala_Project.here, args =>
{
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
var presentation = Presentation.Context.none
var requirements = false
var soft_build = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var build_heap = false
var clean_build = false
var dirs: List[Path] = Nil
var export_files = false
var fresh_build = false
var session_groups: List[String] = Nil
var max_jobs = 1
var check_keywords: Set[String] = Set.empty
var list_files = false
var no_build = false
var options = Options.init(opts = build_options)
var verbose = false
var exclude_sessions: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
-P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b build heap images
-c clean build
-d DIR include session directory
-e export files from session specification into file-system
-f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-k KEYWORD check theory sources for conflicts with proposed keywords
-l list session source files
-n no build -- test dependencies only
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
Build and manage Isabelle sessions, depending on implicit settings:
""" + Library.indent_lines(2, Build_Log.Settings.show()) + "\n",
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
"P:" -> (arg => presentation = Presentation.Context.make(arg)),
"R" -> (_ => requirements = true),
"S" -> (_ => soft_build = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
"b" -> (_ => build_heap = true),
"c" -> (_ => clean_build = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"e" -> (_ => export_files = true),
"f" -> (_ => fresh_build = true),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
"k:" -> (arg => check_keywords = check_keywords + arg),
"l" -> (_ => list_files = true),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
val sessions = getopts(args)
val progress = new Console_Progress(verbose = verbose)
val start_date = Date.now()
if (verbose) {
progress.echo(
"Started at " + Build_Log.print_date(start_date) +
" (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
progress.echo(Build_Log.Settings.show() + "\n")
}
val results =
progress.interrupt_handler {
build(options,
selection = Sessions.Selection(
requirements = requirements,
all_sessions = all_sessions,
base_sessions = base_sessions,
exclude_session_groups = exclude_session_groups,
exclude_sessions = exclude_sessions,
session_groups = session_groups,
sessions = sessions),
presentation = presentation,
progress = progress,
check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
build_heap = build_heap,
clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
fresh_build = fresh_build,
no_build = no_build,
soft_build = soft_build,
verbose = verbose,
export_files = export_files)
}
val end_date = Date.now()
val elapsed_time = end_date.time - start_date.time
if (verbose) {
progress.echo("\nFinished at " + Build_Log.print_date(end_date))
}
val total_timing =
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
copy(elapsed = elapsed_time)
progress.echo(total_timing.message_resources)
sys.exit(results.rc)
})
/* build logic image */
def build_logic(options: Options, logic: String,
progress: Progress = new Progress,
build_heap: Boolean = false,
dirs: List[Path] = Nil,
fresh: Boolean = false,
strict: Boolean = false): Int =
{
val selection = Sessions.Selection.session(logic)
val rc =
if (!fresh && build(options, selection = selection,
- build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
+ build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok
else {
progress.echo("Build started for Isabelle/" + logic + " ...")
Build.build(options, selection = selection, progress = progress,
build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
}
- if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
+ if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc
}
}
diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala
+++ b/src/Pure/Tools/build_job.scala
@@ -1,552 +1,554 @@
/* Title: Pure/Tools/build_job.scala
Author: Makarius
Build job running prover process, with rudimentary PIDE session.
*/
package isabelle
import java.util.HashMap
import scala.collection.mutable
object Build_Job
{
/* theory markup/messages from database */
def read_theory(
db_context: Sessions.Database_Context,
resources: Resources,
session: String,
theory: String,
unicode_symbols: Boolean = false): Option[Command] =
{
def read(name: String): Export.Entry =
db_context.get_export(List(session), theory, name)
def read_xml(name: String): XML.Body =
YXML.parse_body(
Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
cache = db_context.cache)
(read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
case (Value.Long(id), thy_file :: blobs_files) =>
val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
val results =
Command.Results.make(
for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
yield i -> elem)
val blobs =
blobs_files.map(file =>
{
val path = Path.explode(file)
val name = resources.file_node(path)
val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
Command.Blob(name, src_path, None)
})
val blobs_xml =
for (i <- (1 to blobs.length).toList)
yield read_xml(Export.MARKUP + i)
val blobs_info =
Command.Blobs_Info(
for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
yield {
val text = XML.content(xml)
val chunk = Symbol.Text_Chunk(text)
val digest = SHA1.digest(Symbol.encode(text))
Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
})
val thy_xml = read_xml(Export.MARKUP)
val thy_source = XML.content(thy_xml)
val markups_index =
Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
val markups =
Command.Markups.make(
for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
yield index -> Markup_Tree.from_XML(xml))
val command =
Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
blobs_info = blobs_info, results = results, markups = markups)
Some(command)
case _ => None
}
}
/* print messages */
def print_log(
options: Options,
session_name: String,
theories: List[String] = Nil,
verbose: Boolean = false,
progress: Progress = new Progress,
margin: Double = Pretty.default_margin,
breakgain: Double = Pretty.default_breakgain,
metric: Pretty.Metric = Symbol.Metric,
unicode_symbols: Boolean = false): Unit =
{
val store = Sessions.store(options)
val resources = Resources.empty
val session = new Session(options, resources)
using(store.open_database_context())(db_context =>
{
val result =
db_context.input_database(session_name)((db, _) =>
{
val theories = store.read_theories(db, session_name)
val errors = store.read_errors(db, session_name)
store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
})
result match {
case None => error("Missing build database for session " + quote(session_name))
case Some((used_theories, errors, rc)) =>
theories.filterNot(used_theories.toSet) match {
case Nil =>
case bad => error("Unknown theories " + commas_quote(bad))
}
val print_theories =
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
for (thy <- print_theories) {
val thy_heading = "\nTheory " + quote(thy) + ":"
read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
match {
case None => progress.echo(thy_heading + " MISSING")
case Some(command) =>
val snapshot = Document.State.init.snippet(command)
val rendering = new Rendering(snapshot, options, session)
val messages =
rendering.text_messages(Text.Range.full)
.filter(message => verbose || Protocol.is_exported(message.info))
if (messages.nonEmpty) {
val line_document = Line.Document(command.source)
progress.echo(thy_heading)
for (Text.Info(range, elem) <- messages) {
val line = line_document.position(range.start).line1
val pos = Position.Line_File(line, command.node_name.node)
progress.echo(
Protocol.message_text(elem, heading = true, pos = pos,
margin = margin, breakgain = breakgain, metric = metric))
}
}
}
}
if (errors.nonEmpty) {
val msg = Symbol.output(unicode_symbols, cat_lines(errors))
progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
}
- if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
+ if (rc != Process_Result.RC.ok) {
+ progress.echo("\n" + Process_Result.RC.print_long(rc))
+ }
}
})
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
Scala_Project.here, args =>
{
/* arguments */
var unicode_symbols = false
var theories: List[String] = Nil
var margin = Pretty.default_margin
var options = Options.init()
var verbose = false
val getopts = Getopts("""
Usage: isabelle log [OPTIONS] SESSION
Options are:
-T NAME restrict to given theories (multiple options possible)
-U output Unicode symbols
-m MARGIN margin for pretty printing (default: """ + margin + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v print all messages, including information etc.
Print messages from the build database of the given session, without any
checks against current sources: results from a failed build can be
printed as well.
""",
"T:" -> (arg => theories = theories ::: List(arg)),
"U" -> (_ => unicode_symbols = true),
"m:" -> (arg => margin = Value.Double.parse(arg)),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
val session_name =
more_args match {
case List(session_name) => session_name
case _ => getopts.usage()
}
val progress = new Console_Progress()
print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
progress = progress, unicode_symbols = unicode_symbols)
})
}
class Build_Job(progress: Progress,
session_name: String,
val info: Sessions.Info,
deps: Sessions.Deps,
store: Sessions.Store,
do_store: Boolean,
log: Logger,
session_setup: (String, Session) => Unit,
val numa_node: Option[Int],
command_timings0: List[Properties.T])
{
val options: Options = NUMA.policy_options(info.options, numa_node)
private val sessions_structure = deps.sessions_structure
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
val parent = info.parent.getOrElse("")
val base = deps(parent)
val result_base = deps(session_name)
val env = new HashMap(Isabelle_System.settings())
env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString)
val is_pure = Sessions.is_pure(session_name)
val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
val eval_store =
if (do_store) {
(if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
List("ML_Heap.save_child " +
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
}
else Nil
val resources =
new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
val session =
new Session(options, resources) {
override val cache: XML.Cache = store.cache
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
{
result_base.load_commands.get(name.expand) match {
case Some(spans) =>
val syntax = result_base.theory_syntax(name)
Command.build_blobs_info(syntax, name, spans)
case None => Command.Blobs_Info.none
}
}
}
object Build_Session_Errors
{
private val promise: Promise[List[String]] = Future.promise
def result: Exn.Result[List[String]] = promise.join_result
def cancel(): Unit = promise.cancel()
def apply(errs: List[String]): Unit =
{
try { promise.fulfill(errs) }
catch { case _: IllegalStateException => }
}
}
val export_consumer =
Export.consumer(store.open_database(session_name, output = true), store.cache,
progress = progress)
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
val command_timings = new mutable.ListBuffer[Properties.T]
val theory_timings = new mutable.ListBuffer[Properties.T]
val session_timings = new mutable.ListBuffer[Properties.T]
val runtime_statistics = new mutable.ListBuffer[Properties.T]
val task_statistics = new mutable.ListBuffer[Properties.T]
def fun(
name: String,
acc: mutable.ListBuffer[Properties.T],
unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
{
name -> ((msg: Prover.Protocol_Output) =>
unapply(msg.properties) match {
case Some(props) => acc += props; true
case _ => false
})
}
session.init_protocol_handler(new Session.Protocol_Handler
{
override def exit(): Unit = Build_Session_Errors.cancel()
private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
{
val (rc, errors) =
try {
val (rc, errs) =
{
import XML.Decode._
pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
}
val errors =
for (err <- errs) yield {
val prt = Protocol_Message.expose_no_reports(err)
Pretty.string_of(prt, metric = Symbol.Metric)
}
(rc, errors)
}
- catch { case ERROR(err) => (2, List(err)) }
+ catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
session.protocol_command("Prover.stop", rc.toString)
Build_Session_Errors(errors)
true
}
private def loading_theory(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Markup.Loading_Theory(Markup.Name(name)) =>
progress.theory(Progress.Theory(name, session = session_name))
false
case _ => false
}
private def export(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Protocol.Export(args) =>
export_consumer(session_name, args, msg.chunk)
true
case _ => false
}
override val functions =
List(
Markup.Build_Session_Finished.name -> build_session_finished,
Markup.Loading_Theory.name -> loading_theory,
Markup.EXPORT -> export,
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
})
session.command_timings += Session.Consumer("command_timings")
{
case Session.Command_Timing(props) =>
for {
elapsed <- Markup.Elapsed.unapply(props)
elapsed_time = Time.seconds(elapsed)
if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
} command_timings += props.filter(Markup.command_timing_property)
}
session.runtime_statistics += Session.Consumer("ML_statistics")
{
case Session.Runtime_Statistics(props) => runtime_statistics += props
}
session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
{
case snapshot =>
if (!progress.stopped) {
val rendering = new Rendering(snapshot, options, session)
def export(name: String, xml: XML.Body, compress: Boolean = true): Unit =
{
if (!progress.stopped) {
val theory_name = snapshot.node_name.theory
val args =
Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml)))
if (!bytes.is_empty) export_consumer(session_name, args, bytes)
}
}
def export_text(name: String, text: String, compress: Boolean = true): Unit =
export(name, List(XML.Text(text)), compress = compress)
for (command <- snapshot.snippet_command) {
export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
}
export_text(Export.FILES,
cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
export(Export.MARKUP + (i + 1), xml)
}
export(Export.MARKUP, snapshot.xml_markup())
export(Export.MESSAGES, snapshot.messages.map(_._1))
val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations))
}
}
session.all_messages += Session.Consumer[Any]("build_session_output")
{
case msg: Prover.Output =>
val message = msg.message
if (msg.is_system) resources.log(Protocol.message_text(message))
if (msg.is_stdout) {
stdout ++= Symbol.encode(XML.content(message))
}
else if (msg.is_stderr) {
stderr ++= Symbol.encode(XML.content(message))
}
else if (msg.is_exit) {
val err =
"Prover terminated" +
(msg.properties match {
case Markup.Process_Result(result) => ": " + result.print_rc
case _ => ""
})
Build_Session_Errors(List(err))
}
case _ =>
}
session_setup(session_name, session)
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
Isabelle_Process.start(session, options, sessions_structure, store,
logic = parent, raw_ml_system = is_pure,
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
val build_errors =
Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
Exn.capture { process.await_startup() } match {
case Exn.Res(_) =>
val resources_yxml = resources.init_session_yxml
val encode_options: XML.Encode.T[Options] =
options => session.prover_options(options).encode
val args_yxml =
YXML.string_of_body(
{
import XML.Encode._
pair(string, list(pair(encode_options, list(pair(string, properties)))))(
(session_name, info.theories))
})
session.protocol_command("build_session", resources_yxml, args_yxml)
Build_Session_Errors.result
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
}
}
val process_result =
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
session.stop()
val export_errors =
export_consumer.shutdown(close = true).map(Output.error_message_text)
val (document_output, document_errors) =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
using(store.open_database_context())(db_context =>
{
val documents =
Document_Build.build_documents(
Document_Build.context(session_name, deps, db_context, progress = progress),
output_sources = info.document_output,
output_pdf = info.document_output)
db_context.output_database(session_name)(db =>
documents.foreach(_.write(db, session_name)))
(documents.flatMap(_.log_lines), Nil)
})
}
else (Nil, Nil)
}
catch {
case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
}
val result =
{
val theory_timing =
theory_timings.iterator.map(
{ case props @ Markup.Name(name) => name -> props }).toMap
val used_theory_timings =
for { (name, _) <- deps(session_name).used_theories }
yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
val more_output =
Library.trim_line(stdout.toString) ::
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
document_output
process_result.output(more_output)
.error(Library.trim_line(stderr.toString))
.errors_rc(export_errors ::: document_errors)
}
build_errors match {
case Exn.Res(build_errs) =>
val errs = build_errs ::: document_errors
if (errs.nonEmpty) {
result.error_rc.output(
errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
errs.map(Protocol.Error_Message_Marker.apply))
}
- else if (progress.stopped && result.ok) result.copy(rc = Process_Result.interrupt_rc)
+ else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt)
else result
case Exn.Exn(Exn.Interrupt()) =>
- if (result.ok) result.copy(rc = Process_Result.interrupt_rc)
+ if (result.ok) result.copy(rc = Process_Result.RC.interrupt)
else result
case Exn.Exn(exn) => throw exn
}
}
def terminate(): Unit = future_result.cancel()
def is_finished: Boolean = future_result.is_finished
private val timeout_request: Option[Event_Timer.Request] =
{
if (info.timeout_ignored) None
else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
}
def join: (Process_Result, Option[String]) =
{
val result1 = future_result.join
val was_timeout =
timeout_request match {
case None => false
case Some(request) => !request.cancel()
}
val result2 =
if (result1.ok) result1
else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc
else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
else result1
val heap_digest =
if (result2.ok && do_store && store.output_heap(session_name).is_file)
Some(Sessions.write_heap_digest(store.output_heap(session_name)))
else None
(result2, heap_digest)
}
}
diff --git a/src/Pure/Tools/server.scala b/src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala
+++ b/src/Pure/Tools/server.scala
@@ -1,606 +1,606 @@
/* Title: Pure/Tools/server.scala
Author: Makarius
Resident Isabelle servers.
Message formats:
- short message (single line):
NAME ARGUMENT
- long message (multiple lines):
BYTE_LENGTH
NAME ARGUMENT
Argument formats:
- Unit as empty string
- XML.Elem in YXML notation
- JSON.T in standard notation
*/
package isabelle
import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
IOException}
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
object Server
{
/* message argument */
object Argument
{
def is_name_char(c: Char): Boolean =
Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
def split(msg: String): (String, String) =
{
val name = msg.takeWhile(is_name_char)
val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank)
(name, argument)
}
def print(arg: Any): String =
arg match {
case () => ""
case t: XML.Elem => YXML.string_of_tree(t)
case t: JSON.T => JSON.Format(t)
}
def parse(argument: String): Any =
if (argument == "") ()
else if (YXML.detect_elem(argument)) YXML.parse_elem(argument)
else JSON.parse(argument, strict = false)
def unapply(argument: String): Option[Any] =
try { Some(parse(argument)) }
catch { case ERROR(_) => None }
}
/* input command */
type Command_Body = PartialFunction[(Context, Any), Any]
abstract class Command(val command_name: String)
{
def command_body: Command_Body
override def toString: String = command_name
}
class Commands(commands: Command*) extends Isabelle_System.Service
{
def entries: List[Command] = commands.toList
}
private lazy val command_table: Map[String, Command] =
Isabelle_System.make_services(classOf[Commands]).flatMap(_.entries).
foldLeft(Map.empty[String, Command]) {
case (cmds, cmd) =>
val name = cmd.command_name
if (cmds.isDefinedAt(name)) error("Duplicate Isabelle server command: " + quote(name))
else cmds + (name -> cmd)
}
/* output reply */
class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
extends RuntimeException(message)
def json_error(exn: Throwable): JSON.Object.T =
exn match {
case e: Error => Reply.error_message(e.message) ++ e.json
case ERROR(msg) => Reply.error_message(msg)
case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
case _ => JSON.Object.empty
}
object Reply extends Enumeration
{
val OK, ERROR, FINISHED, FAILED, NOTE = Value
def message(msg: String, kind: String = ""): JSON.Object.T =
JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
def error_message(msg: String): JSON.Object.T =
message(msg, kind = Markup.ERROR)
def unapply(msg: String): Option[(Reply.Value, Any)] =
{
if (msg == "") None
else {
val (name, argument) = Argument.split(msg)
for {
reply <-
try { Some(withName(name)) }
catch { case _: NoSuchElementException => None }
arg <- Argument.unapply(argument)
} yield (reply, arg)
}
}
}
/* handler: port, password, thread */
abstract class Handler(port0: Int)
{
val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost)
def port: Int = socket.getLocalPort
def address: String = print_address(port)
val password: String = UUID.random().toString
override def toString: String = print(port, password)
def handle(connection: Server.Connection): Unit
private lazy val thread: Thread =
Isabelle_Thread.fork(name = "server_handler") {
var finished = false
while (!finished) {
Exn.capture(socket.accept) match {
case Exn.Res(client) =>
Isabelle_Thread.fork(name = "client") {
using(Connection(client))(connection =>
if (connection.read_password(password)) handle(connection))
}
case Exn.Exn(_) => finished = true
}
}
}
def start(): Unit = thread
def join(): Unit = thread.join()
def stop(): Unit = { socket.close(); join() }
}
/* socket connection */
object Connection
{
def apply(socket: Socket): Connection =
new Connection(socket)
}
class Connection private(socket: Socket) extends AutoCloseable
{
override def toString: String = socket.toString
def close(): Unit = socket.close()
def set_timeout(t: Time): Unit = socket.setSoTimeout(t.ms.toInt)
private val in = new BufferedInputStream(socket.getInputStream)
private val out = new BufferedOutputStream(socket.getOutputStream)
private val out_lock: AnyRef = new Object
def tty_loop(): TTY_Loop =
new TTY_Loop(
new OutputStreamWriter(out),
new InputStreamReader(in),
writer_lock = out_lock)
def read_password(password: String): Boolean =
try { Byte_Message.read_line(in).map(_.text) == Some(password) }
catch { case _: IOException => false }
def read_line_message(): Option[String] =
try { Byte_Message.read_line_message(in).map(_.text) }
catch { case _: IOException => None }
def read_byte_message(): Option[List[Bytes]] =
try { Byte_Message.read_message(in) }
catch { case _: IOException => None }
def await_close(): Unit =
try { Byte_Message.read(in, 1); socket.close() }
catch { case _: IOException => }
def write_line_message(msg: String): Unit =
out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
def write_byte_message(chunks: List[Bytes]): Unit =
out_lock.synchronized { Byte_Message.write_message(out, chunks) }
def reply(r: Reply.Value, arg: Any): Unit =
{
val argument = Argument.print(arg)
write_line_message(if (argument == "") r.toString else r.toString + " " + argument)
}
def reply_ok(arg: Any): Unit = reply(Reply.OK, arg)
def reply_error(arg: Any): Unit = reply(Reply.ERROR, arg)
def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
reply_error(Reply.error_message(message) ++ more)
def notify(arg: Any): Unit = reply(Reply.NOTE, arg)
}
/* context with output channels */
class Context private[Server](val server: Server, connection: Connection)
extends AutoCloseable
{
context =>
def command_list: List[String] = command_table.keys.toList.sorted
def reply(r: Reply.Value, arg: Any): Unit = connection.reply(r, arg)
def notify(arg: Any): Unit = connection.notify(arg)
def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
notify(Reply.message(msg, kind = kind) ++ more)
def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
def error_message(msg: String, more: JSON.Object.Entry*): Unit =
message(Markup.ERROR, msg, more:_*)
def progress(more: JSON.Object.Entry*): Connection_Progress =
new Connection_Progress(context, more:_*)
override def toString: String = connection.toString
/* asynchronous tasks */
private val _tasks = Synchronized(Set.empty[Task])
def make_task(body: Task => JSON.Object.T): Task =
{
val task = new Task(context, body)
_tasks.change(_ + task)
task
}
def remove_task(task: Task): Unit =
_tasks.change(_ - task)
def cancel_task(id: UUID.T): Unit =
_tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel()); tasks })
def close(): Unit =
{
while(_tasks.change_result(tasks => { tasks.foreach(_.cancel()); (tasks.nonEmpty, tasks) }))
{ _tasks.value.foreach(_.join()) }
}
}
class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
extends Progress
{
override def echo(msg: String): Unit = context.writeln(msg, more:_*)
override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
override def theory(theory: Progress.Theory): Unit =
{
val entries: List[JSON.Object.Entry] =
List("theory" -> theory.theory, "session" -> theory.session) :::
(theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
context.writeln(theory.message, entries ::: more.toList:_*)
}
override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
{
val json =
for ((name, node_status) <- nodes_status.present)
yield name.json + ("status" -> node_status.json)
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
}
override def toString: String = context.toString
}
class Task private[Server](val context: Context, body: Task => JSON.Object.T)
{
task =>
val id: UUID.T = UUID.random()
val ident: JSON.Object.Entry = ("task" -> id.toString)
val progress: Connection_Progress = context.progress(ident)
def cancel(): Unit = progress.stop()
private lazy val thread = Isabelle_Thread.fork(name = "server_task")
{
Exn.capture { body(task) } match {
case Exn.Res(res) =>
context.reply(Reply.FINISHED, res + ident)
case Exn.Exn(exn) =>
val err = json_error(exn)
if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
}
progress.stop()
context.remove_task(task)
}
def start(): Unit = thread
def join(): Unit = thread.join()
}
/* server info */
val localhost_name: String = "127.0.0.1"
def localhost: InetAddress = InetAddress.getByName(localhost_name)
def print_address(port: Int): String = localhost_name + ":" + port
def print(port: Int, password: String): String =
print_address(port) + " (password " + quote(password) + ")"
object Info
{
private val Pattern =
("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r
def parse(s: String): Option[Info] =
s match {
case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password))
case _ => None
}
def apply(name: String, port: Int, password: String): Info =
new Info(name, port, password)
}
class Info private(val name: String, val port: Int, val password: String)
{
def address: String = print_address(port)
override def toString: String =
"server " + quote(name) + " = " + print(port, password)
def connection(): Connection =
{
val connection = Connection(new Socket(localhost, port))
connection.write_line_message(password)
connection
}
def active: Boolean =
try {
using(connection())(connection =>
{
connection.set_timeout(Time.seconds(2.0))
connection.read_line_message() match {
case Some(Reply(Reply.OK, _)) => true
case _ => false
}
})
}
catch {
case _: IOException => false
case _: SocketException => false
case _: SocketTimeoutException => false
}
}
/* per-user servers */
val default_name = "isabelle"
object Data
{
val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
val name = SQL.Column.string("name").make_primary_key
val port = SQL.Column.int("port")
val password = SQL.Column.string("password")
val table = SQL.Table("isabelle_servers", List(name, port, password))
}
def list(db: SQLite.Database): List[Info] =
if (db.tables.contains(Data.table.name)) {
db.using_statement(Data.table.select())(stmt =>
stmt.execute_query().iterator(res =>
Info(
res.string(Data.name),
res.int(Data.port),
res.string(Data.password))).toList.sortBy(_.name))
}
else Nil
def find(db: SQLite.Database, name: String): Option[Info] =
list(db).find(server_info => server_info.name == name && server_info.active)
def init(
name: String = default_name,
port: Int = 0,
existing_server: Boolean = false,
log: Logger = No_Logger): (Info, Option[Server]) =
{
using(SQLite.open_database(Data.database))(db =>
{
db.transaction {
Isabelle_System.chmod("600", Data.database)
db.create_table(Data.table)
list(db).filterNot(_.active).foreach(server_info =>
db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
_.execute()))
}
db.transaction {
find(db, name) match {
case Some(server_info) => (server_info, None)
case None =>
if (existing_server) error("Isabelle server " + quote(name) + " not running")
val server = new Server(port, log)
val server_info = Info(name, server.port, server.password)
db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
db.using_statement(Data.table.insert())(stmt =>
{
stmt.string(1) = server_info.name
stmt.int(2) = server_info.port
stmt.string(3) = server_info.password
stmt.execute()
})
server.start()
(server_info, Some(server))
}
}
})
}
def exit(name: String = default_name): Boolean =
{
using(SQLite.open_database(Data.database))(db =>
db.transaction {
find(db, name) match {
case Some(server_info) =>
using(server_info.connection())(_.write_line_message("shutdown"))
while(server_info.active) { Time.seconds(0.05).sleep() }
true
case None => false
}
})
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("server", "manage resident Isabelle servers", Scala_Project.here, args =>
{
var console = false
var log_file: Option[Path] = None
var operation_list = false
var operation_exit = false
var name = default_name
var port = 0
var existing_server = false
val getopts =
Getopts("""
Usage: isabelle server [OPTIONS]
Options are:
-L FILE logging on FILE
-c console interaction with specified server
-l list servers (alternative operation)
-n NAME explicit server name (default: """ + default_name + """)
-p PORT explicit server port
-s assume existing server, no implicit startup
-x exit specified server (alternative operation)
Manage resident Isabelle servers.
""",
"L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
"c" -> (_ => console = true),
"l" -> (_ => operation_list = true),
"n:" -> (arg => name = arg),
"p:" -> (arg => port = Value.Int.parse(arg)),
"s" -> (_ => existing_server = true),
"x" -> (_ => operation_exit = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
if (operation_list) {
for {
server_info <- using(SQLite.open_database(Data.database))(list)
if server_info.active
} Output.writeln(server_info.toString, stdout = true)
}
else if (operation_exit) {
val ok = Server.exit(name)
- sys.exit(if (ok) 0 else 2)
+ sys.exit(if (ok) Process_Result.RC.ok else Process_Result.RC.failure)
}
else {
val log = Logger.make(log_file)
val (server_info, server) =
init(name, port = port, existing_server = existing_server, log = log)
Output.writeln(server_info.toString, stdout = true)
if (console) {
using(server_info.connection())(connection => connection.tty_loop().join())
}
server.foreach(_.join())
}
})
}
class Server private(port0: Int, val log: Logger) extends Server.Handler(port0)
{
server =>
private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
def add_session(entry: (UUID.T, Headless.Session)): Unit = _sessions.change(_ + entry)
def remove_session(id: UUID.T): Headless.Session =
{
_sessions.change_result(sessions =>
sessions.get(id) match {
case Some(session) => (session, sessions - id)
case None => err_session(id)
})
}
def shutdown(): Unit =
{
server.socket.close()
val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
for ((_, session) <- sessions) {
try {
val result = session.stop()
if (!result.ok) log("Session shutdown failed: " + result.print_rc)
}
catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
}
}
override def join(): Unit = { super.join(); shutdown() }
override def handle(connection: Server.Connection): Unit =
{
using(new Server.Context(server, connection))(context =>
{
connection.reply_ok(
JSON.Object(
"isabelle_id" -> Isabelle_System.isabelle_id(),
"isabelle_name" -> Isabelle_System.isabelle_name()))
var finished = false
while (!finished) {
connection.read_line_message() match {
case None => finished = true
case Some("") => context.notify("Command 'help' provides list of commands")
case Some(msg) =>
val (name, argument) = Server.Argument.split(msg)
Server.command_table.get(name) match {
case Some(cmd) =>
argument match {
case Server.Argument(arg) =>
if (cmd.command_body.isDefinedAt((context, arg))) {
Exn.capture { cmd.command_body((context, arg)) } match {
case Exn.Res(task: Server.Task) =>
connection.reply_ok(JSON.Object(task.ident))
task.start()
case Exn.Res(res) => connection.reply_ok(res)
case Exn.Exn(exn) =>
val err = Server.json_error(exn)
if (err.isEmpty) throw exn else connection.reply_error(err)
}
}
else {
connection.reply_error_message(
"Bad argument for command " + Library.single_quote(name),
"argument" -> argument)
}
case _ =>
connection.reply_error_message(
"Malformed argument for command " + Library.single_quote(name),
"argument" -> argument)
}
case None => connection.reply_error("Bad command " + Library.single_quote(name))
}
}
}
})
}
}
diff --git a/src/Pure/Tools/server_commands.scala b/src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala
+++ b/src/Pure/Tools/server_commands.scala
@@ -1,345 +1,345 @@
/* Title: Pure/Tools/server_commands.scala
Author: Makarius
Miscellaneous Isabelle server commands.
*/
package isabelle
object Server_Commands
{
def default_preferences: String = Options.read_prefs()
object Help extends Server.Command("help")
{
override val command_body: Server.Command_Body =
{ case (context, ()) => context.command_list }
}
object Echo extends Server.Command("echo")
{
override val command_body: Server.Command_Body =
{ case (_, t) => t }
}
object Cancel extends Server.Command("cancel")
{
sealed case class Args(task: UUID.T)
def unapply(json: JSON.T): Option[Args] =
for { task <- JSON.uuid(json, "task") }
yield Args(task)
override val command_body: Server.Command_Body =
{ case (context, Cancel(args)) => context.cancel_task(args.task) }
}
object Shutdown extends Server.Command("shutdown")
{
override val command_body: Server.Command_Body =
{ case (context, ()) => context.server.shutdown() }
}
object Session_Build extends Server.Command("session_build")
{
sealed case class Args(
session: String,
preferences: String = default_preferences,
options: List[String] = Nil,
dirs: List[String] = Nil,
include_sessions: List[String] = Nil,
verbose: Boolean = false)
def unapply(json: JSON.T): Option[Args] =
for {
session <- JSON.string(json, "session")
preferences <- JSON.string_default(json, "preferences", default_preferences)
options <- JSON.strings_default(json, "options")
dirs <- JSON.strings_default(json, "dirs")
include_sessions <- JSON.strings_default(json, "include_sessions")
verbose <- JSON.bool_default(json, "verbose")
}
yield {
Args(session, preferences = preferences, options = options, dirs = dirs,
include_sessions = include_sessions, verbose = verbose)
}
def command(args: Args, progress: Progress = new Progress)
: (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
{
val options = Options.init(prefs = args.preferences, opts = args.options)
val dirs = args.dirs.map(Path.explode)
val base_info =
Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
include_sessions = args.include_sessions).check
val results =
Build.build(options,
selection = Sessions.Selection.session(args.session),
progress = progress,
build_heap = true,
dirs = dirs,
infos = base_info.infos,
verbose = args.verbose)
val sessions_order =
base_info.sessions_structure.imports_topological_order.zipWithIndex.
toMap.withDefaultValue(-1)
val results_json =
JSON.Object(
"ok" -> results.ok,
"return_code" -> results.rc,
"sessions" ->
results.sessions.toList.sortBy(sessions_order).map(session =>
{
val result = results(session)
JSON.Object(
"session" -> session,
"ok" -> result.ok,
"return_code" -> result.rc,
"timeout" -> result.timeout,
"timing" -> result.timing.json)
}))
if (results.ok) (results_json, results, options, base_info)
else {
- throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc),
+ throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc),
results_json)
}
}
override val command_body: Server.Command_Body =
{ case (context, Session_Build(args)) =>
context.make_task(task => Session_Build.command(args, progress = task.progress)._1) }
}
object Session_Start extends Server.Command("session_start")
{
sealed case class Args(
build: Session_Build.Args,
print_mode: List[String] = Nil)
def unapply(json: JSON.T): Option[Args] =
for {
build <- Session_Build.unapply(json)
print_mode <- JSON.strings_default(json, "print_mode")
}
yield Args(build = build, print_mode = print_mode)
def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger)
: (JSON.Object.T, (UUID.T, Headless.Session)) =
{
val (_, _, options, base_info) =
try { Session_Build.command(args.build, progress = progress) }
catch { case exn: Server.Error => error(exn.message) }
val resources = Headless.Resources(options, base_info, log = log)
val session = resources.start_session(print_mode = args.print_mode, progress = progress)
val id = UUID.random()
val res =
JSON.Object(
"session_id" -> id.toString,
"tmp_dir" -> File.path(session.tmp_dir).implode)
(res, id -> session)
}
override val command_body: Server.Command_Body =
{ case (context, Session_Start(args)) =>
context.make_task(task =>
{
val (res, entry) =
Session_Start.command(args, progress = task.progress, log = context.server.log)
context.server.add_session(entry)
res
})
}
}
object Session_Stop extends Server.Command("session_stop")
{
def unapply(json: JSON.T): Option[UUID.T] =
JSON.uuid(json, "session_id")
def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
{
val result = session.stop()
val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
if (result.ok) (result_json, result)
else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)
}
override val command_body: Server.Command_Body =
{ case (context, Session_Stop(id)) =>
context.make_task(_ =>
{
val session = context.server.remove_session(id)
Session_Stop.command(session)._1
})
}
}
object Use_Theories extends Server.Command("use_theories")
{
sealed case class Args(
session_id: UUID.T,
theories: List[String],
master_dir: String = "",
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
export_pattern: String = "",
check_delay: Option[Time] = None,
check_limit: Option[Int] = None,
watchdog_timeout: Option[Time] = None,
nodes_status_delay: Option[Time] = None,
commit_cleanup_delay: Option[Time] = None)
def unapply(json: JSON.T): Option[Args] =
for {
session_id <- JSON.uuid(json, "session_id")
theories <- JSON.strings(json, "theories")
master_dir <- JSON.string_default(json, "master_dir")
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
export_pattern <- JSON.string_default(json, "export_pattern")
check_delay = JSON.seconds(json, "check_delay")
check_limit = JSON.int(json, "check_limit")
watchdog_timeout = JSON.seconds(json, "watchdog_timeout")
nodes_status_delay = JSON.seconds(json, "nodes_status_delay")
commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay")
}
yield {
Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
unicode_symbols = unicode_symbols, export_pattern = export_pattern,
check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout,
nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay)
}
def command(args: Args,
session: Headless.Session,
id: UUID.T = UUID.random(),
progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
{
val result =
session.use_theories(args.theories, master_dir = args.master_dir,
check_delay = args.check_delay.getOrElse(session.default_check_delay),
check_limit = args.check_limit.getOrElse(session.default_check_limit),
watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout),
nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay),
commit_cleanup_delay =
args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
id = id, progress = progress)
def output_text(text: String): String =
Symbol.output(args.unicode_symbols, text)
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
{
val position = "pos" -> Position.JSON(pos)
tree match {
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
case elem: XML.Elem =>
val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
val kind =
Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
Server.Reply.message(output_text(msg), kind = kind) + position
}
}
val result_json =
JSON.Object(
"ok" -> result.ok,
"errors" ->
(for {
(name, status) <- result.nodes if !status.ok
(tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree)
} yield output_message(tree, pos)),
"nodes" ->
(for ((name, status) <- result.nodes) yield {
val snapshot = result.snapshot(name)
name.json +
("status" -> status.json) +
("messages" ->
(for {
(tree, pos) <- snapshot.messages if Protocol.is_exported(tree)
} yield output_message(tree, pos))) +
("exports" ->
(if (args.export_pattern == "") Nil else {
val matcher = Export.make_matcher(args.export_pattern)
for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
yield {
val (base64, body) = entry.uncompressed.maybe_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
}
}))
}))
(result_json, result)
}
override val command_body: Server.Command_Body =
{ case (context, Use_Theories(args)) =>
context.make_task(task =>
{
val session = context.server.the_session(args.session_id)
Use_Theories.command(args, session, id = task.id, progress = task.progress)._1
})
}
}
object Purge_Theories extends Server.Command("purge_theories")
{
sealed case class Args(
session_id: UUID.T,
theories: List[String] = Nil,
master_dir: String = "",
all: Boolean = false)
def unapply(json: JSON.T): Option[Args] =
for {
session_id <- JSON.uuid(json, "session_id")
theories <- JSON.strings_default(json, "theories")
master_dir <- JSON.string_default(json, "master_dir")
all <- JSON.bool_default(json, "all")
}
yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
def command(args: Args, session: Headless.Session)
: (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
{
val (purged, retained) =
session.purge_theories(
theories = args.theories, master_dir = args.master_dir, all = args.all)
val result_json =
JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))
(result_json, (purged, retained))
}
override val command_body: Server.Command_Body =
{ case (context, Purge_Theories(args)) =>
val session = context.server.the_session(args.session_id)
command(args, session)._1
}
}
}
class Server_Commands extends Server.Commands(
Server_Commands.Help,
Server_Commands.Echo,
Server_Commands.Cancel,
Server_Commands.Shutdown,
Server_Commands.Session_Build,
Server_Commands.Session_Start,
Server_Commands.Session_Stop,
Server_Commands.Use_Theories,
Server_Commands.Purge_Theories)
diff --git a/src/Tools/VSCode/src/language_server.scala b/src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala
+++ b/src/Tools/VSCode/src/language_server.scala
@@ -1,562 +1,562 @@
/* Title: Tools/VSCode/src/language_server.scala
Author: Makarius
Server for VS Code Language Server Protocol 2.0/3.0, see also
https://github.com/Microsoft/language-server-protocol
https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
PIDE protocol extensions depend on system option "vscode_pide_extensions".
*/
package isabelle.vscode
import isabelle._
import java.io.{PrintStream, OutputStream, File => JFile}
import scala.annotation.tailrec
import scala.collection.mutable
object Language_Server
{
type Editor = isabelle.Editor[Unit]
/* Isabelle tool wrapper */
private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
val isabelle_tool =
Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", Scala_Project.here, args =>
{
try {
var logic_ancestor: Option[String] = None
var log_file: Option[Path] = None
var logic_requirements = false
var dirs: List[Path] = Nil
var include_sessions: List[String] = Nil
var logic = default_logic
var modes: List[String] = Nil
var options = Options.init()
var verbose = false
val getopts = Getopts("""
Usage: isabelle vscode_server [OPTIONS]
Options are:
-A NAME ancestor session for option -R (default: parent)
-L FILE logging on FILE
-R NAME build image with requirements from other sessions
-d DIR include session directory
-i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose logging
Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
""",
"A:" -> (arg => logic_ancestor = Some(arg)),
"L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
"R:" -> (arg => { logic = arg; logic_requirements = true }),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
"i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val log = Logger.make(log_file)
val channel = new Channel(System.in, System.out, log, verbose)
val server =
new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
include_sessions = include_sessions, session_ancestor = logic_ancestor,
session_requirements = logic_requirements, modes = modes, log = log)
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
try {
System.setOut(new PrintStream(new OutputStream { def write(n: Int): Unit = {} }))
server.start()
}
finally { System.setOut(orig_out) }
}
catch {
case exn: Throwable =>
val channel = new Channel(System.in, System.out, No_Logger)
channel.error_message(Exn.message(exn))
throw(exn)
}
})
}
class Language_Server(
val channel: Channel,
options: Options,
session_name: String = Language_Server.default_logic,
session_dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
session_ancestor: Option[String] = None,
session_requirements: Boolean = false,
modes: List[String] = Nil,
log: Logger = No_Logger)
{
server =>
/* prover session */
private val session_ = Synchronized(None: Option[Session])
def session: Session = session_.value getOrElse error("Server inactive")
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
for {
model <- resources.get_model(new JFile(node_pos.name))
rendering = model.rendering()
offset <- model.content.doc.offset(node_pos.pos)
} yield (rendering, offset)
private val dynamic_output = Dynamic_Output(server)
/* input from client or file-system */
private val file_watcher: File_Watcher =
File_Watcher(sync_documents, options.seconds("vscode_load_delay"))
private val delay_input: Delay =
Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ resources.flush_input(session, channel) }
private val delay_load: Delay =
Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
val (invoke_input, invoke_load) =
resources.resolve_dependencies(session, editor, file_watcher)
if (invoke_input) delay_input.invoke()
if (invoke_load) delay_load.invoke()
}
private def close_document(file: JFile): Unit =
{
if (resources.close_model(file)) {
file_watcher.register_parent(file)
sync_documents(Set(file))
delay_input.invoke()
delay_output.invoke()
}
}
private def sync_documents(changed: Set[JFile]): Unit =
{
resources.sync_models(changed)
delay_input.invoke()
delay_output.invoke()
}
private def change_document(
file: JFile, version: Long, changes: List[LSP.TextDocumentChange]): Unit =
{
val norm_changes = new mutable.ListBuffer[LSP.TextDocumentChange]
@tailrec def norm(chs: List[LSP.TextDocumentChange]): Unit =
{
if (chs.nonEmpty) {
val (full_texts, rest1) = chs.span(_.range.isEmpty)
val (edits, rest2) = rest1.span(_.range.nonEmpty)
norm_changes ++= full_texts
norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse
norm(rest2)
}
}
norm(changes)
norm_changes.foreach(change =>
resources.change_model(session, editor, file, version, change.text, change.range))
delay_input.invoke()
delay_output.invoke()
}
/* caret handling */
private val delay_caret_update: Delay =
Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ session.caret_focus.post(Session.Caret_Focus) }
private def update_caret(caret: Option[(JFile, Line.Position)]): Unit =
{
resources.update_caret(caret)
delay_caret_update.invoke()
delay_input.invoke()
}
/* preview */
private lazy val preview_panel = new Preview_Panel(resources)
private lazy val delay_preview: Delay =
Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (preview_panel.flush(channel)) delay_preview.invoke()
}
private def request_preview(file: JFile, column: Int): Unit =
{
preview_panel.request(file, column)
delay_preview.invoke()
}
/* output to client */
private val delay_output: Delay =
Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (resources.flush_output(channel)) delay_output.invoke()
}
def update_output(changed_nodes: Iterable[JFile]): Unit =
{
resources.update_output(changed_nodes)
delay_output.invoke()
}
def update_output_visible(): Unit =
{
resources.update_output_visible()
delay_output.invoke()
}
private val prover_output =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed =>
update_output(changed.nodes.toList.map(resources.node_file(_)))
}
private val syslog_messages =
Session.Consumer[Prover.Output](getClass.getName) {
case output => channel.log_writeln(resources.output_xml(output.message))
}
/* init and exit */
def init(id: LSP.Id): Unit =
{
def reply_ok(msg: String): Unit =
{
channel.write(LSP.Initialize.reply(id, ""))
channel.writeln(msg)
}
def reply_error(msg: String): Unit =
{
channel.write(LSP.Initialize.reply(id, msg))
channel.error_message(msg)
}
val try_session =
try {
val base_info =
Sessions.base_info(
options, session_name, dirs = session_dirs, include_sessions = include_sessions,
session_ancestor = session_ancestor, session_requirements = session_requirements).check
def build(no_build: Boolean = false): Build.Results =
Build.build(options,
selection = Sessions.Selection.session(base_info.session),
build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
if (!build(no_build = true).ok) {
val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
val fail_msg = "Session build failed -- prover process remains inactive!"
val progress = channel.progress(verbose = true)
progress.echo(start_msg); channel.writeln(start_msg)
if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
}
val resources = new VSCode_Resources(options, base_info, log)
{
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
delay_load.invoke()
}
val session_options = options.bool("editor_output_state") = true
val session = new Session(session_options, resources)
Some((base_info, session))
}
catch { case ERROR(msg) => reply_error(msg); None }
for ((base_info, session) <- try_session) {
session_.change(_ => Some(session))
session.commands_changed += prover_output
session.syslog_messages += syslog_messages
dynamic_output.init()
try {
Isabelle_Process.start(session, options, base_info.sessions_structure,
Sessions.store(options), modes = modes, logic = base_info.session).await_startup()
reply_ok("Welcome to Isabelle/" + base_info.session + Isabelle_System.isabelle_heading())
}
catch { case ERROR(msg) => reply_error(msg) }
}
}
def shutdown(id: LSP.Id): Unit =
{
def reply(err: String): Unit = channel.write(LSP.Shutdown.reply(id, err))
session_.change({
case Some(session) =>
session.commands_changed -= prover_output
session.syslog_messages -= syslog_messages
dynamic_output.exit()
delay_load.revoke()
file_watcher.shutdown()
delay_input.revoke()
delay_output.revoke()
delay_caret_update.revoke()
delay_preview.revoke()
val result = session.stop()
if (result.ok) reply("")
else reply("Prover shutdown failed: " + result.rc)
None
case None =>
reply("Prover inactive")
None
})
}
def exit(): Unit =
{
log("\n")
- sys.exit(if (session_.value.isDefined) 2 else 0)
+ sys.exit(if (session_.value.isDefined) Process_Result.RC.failure else Process_Result.RC.ok)
}
/* completion */
def completion(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
yield rendering.completion(node_pos.pos, offset)) getOrElse Nil
channel.write(LSP.Completion.reply(id, result))
}
/* spell-checker dictionary */
def update_dictionary(include: Boolean, permanent: Boolean): Unit =
{
for {
spell_checker <- resources.spell_checker.get
caret <- resources.get_caret()
rendering = caret.model.rendering()
range = rendering.before_caret_range(caret.offset)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} {
spell_checker.update(word, include, permanent)
update_output_visible()
}
}
def reset_dictionary(): Unit =
{
for (spell_checker <- resources.spell_checker.get)
{
spell_checker.reset()
update_output_visible()
}
}
/* hover */
def hover(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
for {
(rendering, offset) <- rendering_offset(node_pos)
info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1))
} yield {
val range = rendering.model.content.doc.range(info.range)
val contents = info.info.map(t => LSP.MarkedString(resources.output_pretty_tooltip(List(t))))
(range, contents)
}
channel.write(LSP.Hover.reply(id, result))
}
/* goto definition */
def goto_definition(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
channel.write(LSP.GotoDefinition.reply(id, result))
}
/* document highlights */
def document_highlights(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
yield {
val model = rendering.model
rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range)
.map(r => LSP.DocumentHighlight.text(model.content.doc.range(r)))
}) getOrElse Nil
channel.write(LSP.DocumentHighlights.reply(id, result))
}
/* main loop */
def start(): Unit =
{
log("Server started " + Date.now())
def handle(json: JSON.T): Unit =
{
try {
json match {
case LSP.Initialize(id) => init(id)
case LSP.Initialized(()) =>
case LSP.Shutdown(id) => shutdown(id)
case LSP.Exit(()) => exit()
case LSP.DidOpenTextDocument(file, _, version, text) =>
change_document(file, version, List(LSP.TextDocumentChange(None, text)))
delay_load.invoke()
case LSP.DidChangeTextDocument(file, version, changes) =>
change_document(file, version, changes)
case LSP.DidCloseTextDocument(file) => close_document(file)
case LSP.Completion(id, node_pos) => completion(id, node_pos)
case LSP.Include_Word(()) => update_dictionary(true, false)
case LSP.Include_Word_Permanently(()) => update_dictionary(true, true)
case LSP.Exclude_Word(()) => update_dictionary(false, false)
case LSP.Exclude_Word_Permanently(()) => update_dictionary(false, true)
case LSP.Reset_Words(()) => reset_dictionary()
case LSP.Hover(id, node_pos) => hover(id, node_pos)
case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
case LSP.Caret_Update(caret) => update_caret(caret)
case LSP.State_Init(()) => State_Panel.init(server)
case LSP.State_Exit(id) => State_Panel.exit(id)
case LSP.State_Locate(id) => State_Panel.locate(id)
case LSP.State_Update(id) => State_Panel.update(id)
case LSP.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
case LSP.Preview_Request(file, column) => request_preview(file, column)
case LSP.Symbols_Request(()) => channel.write(LSP.Symbols())
case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
}
}
catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
}
@tailrec def loop(): Unit =
{
channel.read() match {
case Some(json) =>
json match {
case bulk: List[_] => bulk.foreach(handle)
case _ => handle(json)
}
loop()
case None => log("### TERMINATE")
}
}
loop()
}
/* abstract editor operations */
object editor extends Language_Server.Editor
{
/* session */
override def session: Session = server.session
override def flush(): Unit = resources.flush_input(session, channel)
override def invoke(): Unit = delay_input.invoke()
/* current situation */
override def current_node(context: Unit): Option[Document.Node.Name] =
resources.get_caret().map(_.model.node_name)
override def current_node_snapshot(context: Unit): Option[Document.Snapshot] =
resources.get_caret().map(_.model.snapshot())
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
{
resources.get_model(name) match {
case Some(model) => model.snapshot()
case None => session.snapshot(name)
}
}
def current_command(snapshot: Document.Snapshot): Option[Command] =
{
resources.get_caret() match {
case Some(caret) => snapshot.current_command(caret.node_name, caret.offset)
case None => None
}
}
override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] =
current_command(snapshot)
/* overlays */
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
resources.node_overlays(name)
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
resources.insert_overlay(command, fn, args)
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
resources.remove_overlay(command, fn, args)
/* hyperlinks */
override def hyperlink_command(
focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic,
offset: Symbol.Offset = 0): Option[Hyperlink] =
{
if (snapshot.is_outdated) None
else
snapshot.find_command_position(id, offset).map(node_pos =>
new Hyperlink {
def follow(unit: Unit): Unit = channel.write(LSP.Caret_Update(node_pos, focus))
})
}
/* dispatcher thread */
override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body)
override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body)
override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body)
override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body)
}
}
diff --git a/src/Tools/jEdit/src/main.scala b/src/Tools/jEdit/src/main.scala
--- a/src/Tools/jEdit/src/main.scala
+++ b/src/Tools/jEdit/src/main.scala
@@ -1,142 +1,142 @@
/* Title: src/Tools/jEdit/src/main.scala
Author: Makarius
Main Isabelle application entry point.
*/
package isabelle.jedit
import isabelle._
import org.gjt.sp.jedit.{MiscUtilities, jEdit}
object Main
{
/* main entry point */
def main(args: Array[String]): Unit =
{
if (args.nonEmpty && args(0) == "-init") {
Isabelle_System.init()
}
else {
val start =
{
try {
Isabelle_System.init()
Isabelle_Fonts.init()
GUI.init_lafs()
/* ROOTS template */
{
val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
if (!roots.is_file) File.write(roots, """# Additional session root directories
#
# * each line contains one directory entry in Isabelle path notation, e.g.
#
# $ISABELLE_HOME/../AFP/thys
#
# for a copy of AFP put side-by-side to the Isabelle distribution
#
# * Isabelle/jEdit provides formal markup for C-hover-click and completion
#
# * lines starting with "#" are stripped
#
# * changes require restart of the Isabelle application
#
#:mode=text:encoding=UTF-8:
#$ISABELLE_HOME/../AFP/thys
""")
}
/* settings directory */
val settings_dir = Path.explode("$JEDIT_SETTINGS")
val properties = settings_dir + Path.explode("properties")
if (properties.is_file) {
val props1 = split_lines(File.read(properties))
val props2 = props1.filterNot(_.startsWith("plugin-blacklist.isabelle_jedit"))
if (props1 != props2) File.write(properties, cat_lines(props2))
}
Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager"))
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
"""""")
File.write(settings_dir + Path.explode("perspective.xml"),
XML.header +
"""
""")
}
Scala_Project.plugin_contexts().foreach(_.build())
/* args */
val jedit_settings =
"-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
val jedit_server =
System.getProperty("isabelle.jedit_server") match {
case null | "" => "-noserver"
case name => "-server=" + name
}
val jedit_options =
Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
val more_args =
{
args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
case Nil | List("--") =>
args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
case List(":") => args.slice(0, args.length - 1)
case _ => args
}
}
/* environment */
for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
MiscUtilities.putenv(name, File.platform_path(Isabelle_System.getenv(name)))
}
MiscUtilities.putenv("ISABELLE_ROOT", null)
/* properties */
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME")))
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
System.setProperty("scala.color", "false")
/* main startup */
() => jEdit.main(Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
}
catch {
case exn: Throwable =>
GUI.init_laf()
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
- sys.exit(2)
+ sys.exit(Process_Result.RC.failure)
}
}
start()
}
}
}
diff --git a/src/Tools/jEdit/src/session_build.scala b/src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala
+++ b/src/Tools/jEdit/src/session_build.scala
@@ -1,183 +1,184 @@
/* Title: Tools/jEdit/src/session_build.scala
Author: Makarius
Session build management.
*/
package isabelle.jedit
import isabelle._
import java.awt.event.{WindowEvent, WindowAdapter}
import javax.swing.{WindowConstants, JDialog}
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
BorderPanel, TextArea, Component, Label}
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.View
object Session_Build
{
def check_dialog(view: View): Unit =
{
val options = PIDE.options.value
Isabelle_Thread.fork() {
try {
if (JEdit_Sessions.session_no_build ||
JEdit_Sessions.session_build(options, no_build = true) == 0)
JEdit_Sessions.session_start(options)
else GUI_Thread.later { new Dialog(view) }
}
catch {
case exn: Throwable =>
GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
}
}
}
private class Dialog(view: View) extends JDialog(view)
{
val options: Options = PIDE.options.value
/* text */
private val text = new TextArea {
editable = false
columns = 60
rows = 24
}
text.font = GUI.copy_font((new Label).font)
private val scroll_text = new ScrollPane(text)
/* progress */
private val progress = new Progress {
override def echo(txt: String): Unit =
GUI_Thread.later {
text.append(txt + "\n")
val vertical = scroll_text.peer.getVerticalScrollBar
vertical.setValue(vertical.getMaximum)
}
override def theory(theory: Progress.Theory): Unit = echo(theory.message)
}
/* layout panel with dynamic actions */
private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
private val layout_panel = new BorderPanel
layout_panel.layout(scroll_text) = BorderPanel.Position.Center
layout_panel.layout(action_panel) = BorderPanel.Position.South
setContentPane(layout_panel.peer)
private def set_actions(cs: Component*): Unit =
{
action_panel.contents.clear()
action_panel.contents ++= cs
layout_panel.revalidate()
layout_panel.repaint()
}
/* return code and exit */
private var _return_code: Option[Int] = None
private def return_code(rc: Int): Unit =
GUI_Thread.later {
_return_code = Some(rc)
delay_exit.invoke()
}
private val delay_exit =
Delay.first(Time.seconds(1.0), gui = true)
{
if (can_auto_close) conclude()
else {
val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } }
set_actions(button)
button.peer.getRootPane.setDefaultButton(button.peer)
}
}
private def conclude(): Unit =
{
setVisible(false)
dispose()
}
/* close */
setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
addWindowListener(new WindowAdapter {
override def windowClosing(e: WindowEvent): Unit =
{
if (_return_code.isDefined) conclude()
else stopping()
}
})
private def stopping(): Unit =
{
progress.stop()
set_actions(new Label("Stopping ..."))
}
private val stop_button = new Button("Stop") {
reactions += { case ButtonClicked(_) => stopping() }
}
private var do_auto_close = true
private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
private val auto_close = new CheckBox("Auto close") {
reactions += {
case ButtonClicked(_) => do_auto_close = this.selected
if (can_auto_close) conclude()
}
}
auto_close.selected = do_auto_close
auto_close.tooltip = "Automatically close dialog when finished"
set_actions(stop_button, auto_close)
/* main */
setTitle("Isabelle build (" +
Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
"jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
pack()
setLocationRelativeTo(view)
setVisible(true)
Isabelle_Thread.fork(name = "session_build") {
progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
val (out, rc) =
try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
catch {
case exn: Throwable =>
(Output.error_message_text(Exn.message(exn)) + "\n", Exn.failure_rc(exn))
}
- progress.echo(out + (if (rc == 0) "OK" else Process_Result.print_return_code(rc)) + "\n")
+ val ok = rc == Process_Result.RC.ok
+ progress.echo(out + (if (ok) "OK" else Process_Result.RC.print_long(rc)) + "\n")
- if (rc == 0) JEdit_Sessions.session_start(options)
+ if (ok) JEdit_Sessions.session_start(options)
else progress.echo("Session build failed -- prover process remains inactive!")
return_code(rc)
}
}
}