# HG changeset patch # User wenzelm # Date 1342881715 -7200 # Node ID 1a634f9614fb1e189e3292c9884ee35423f95e22 # Parent bb1d4ec90f3088e33602523e1fef1efe344df2be some actual build function on ML side; further imitation of "usedir" shell script; diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Jul 21 12:57:31 2012 +0200 +++ b/src/Pure/General/file.scala Sat Jul 21 16:41:55 2012 +0200 @@ -83,10 +83,16 @@ /* misc */ - def with_tmp_file[A](prefix: String)(body: JFile => A): A = + def tmp_file(prefix: String): JFile = { val file = JFile.createTempFile(prefix, null) file.deleteOnExit + file + } + + def with_tmp_file[A](prefix: String)(body: JFile => A): A = + { + val file = tmp_file(prefix) try { body(file) } finally { file.delete } } diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Jul 21 12:57:31 2012 +0200 +++ b/src/Pure/IsaMakefile Sat Jul 21 16:41:55 2012 +0200 @@ -189,6 +189,7 @@ Syntax/syntax_trans.ML \ Syntax/term_position.ML \ System/invoke_scala.ML \ + System/build.ML \ System/isabelle_process.ML \ System/isabelle_system.ML \ System/isar.ML \ diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jul 21 12:57:31 2012 +0200 +++ b/src/Pure/ROOT.ML Sat Jul 21 16:41:55 2012 +0200 @@ -268,6 +268,7 @@ (* Isabelle/Isar system *) use "System/session.ML"; +use "System/build.ML"; use "System/system_channel.ML"; use "System/isabelle_process.ML"; use "System/invoke_scala.ML"; diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/System/build.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/build.ML Sat Jul 21 16:41:55 2012 +0200 @@ -0,0 +1,29 @@ +(* Title: Pure/System/build.ML + Author: Makarius + +Build Isabelle sessions. +*) + +signature BUILD = +sig + val build: string -> unit +end; + +structure Build: BUILD = +struct + +fun build args_file = + let + val (build_images, (parent, (name, theories))) = + File.read (Path.explode args_file) |> YXML.parse_body |> + let open XML.Decode in pair bool (pair string (pair string (list string))) end; + + val _ = Session.init false parent name; (* FIXME reset!? *) + val _ = Thy_Info.use_thys theories; + val _ = Session.finish (); + + val _ = if build_images then () else quit (); + in () end + handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); + +end; diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/System/build.scala --- a/src/Pure/System/build.scala Sat Jul 21 12:57:31 2012 +0200 +++ b/src/Pure/System/build.scala Sat Jul 21 16:41:55 2012 +0200 @@ -40,9 +40,10 @@ sealed case class Info( dir: Path, + parent: Option[String], description: String, options: Options, - theories: List[(Options, String)], + theories: List[(Options, List[String])], files: List[String]) object Queue @@ -56,7 +57,7 @@ { def defined(name: String): Boolean = keys.isDefinedAt(name) - def + (key: Key, info: Info, parent: Option[String]): Queue = + def + (key: Key, info: Info): Queue = { val keys1 = if (defined(key.name)) error("Duplicate session: " + quote(key.name)) @@ -64,7 +65,7 @@ val graph1 = try { - graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_))) + graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_))) } catch { case exn: Graph.Cycles[_] => @@ -184,10 +185,11 @@ } val key = Session.Key(full_name, entry.order) - val info = Session.Info(dir + path, entry.description, entry.options, - entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files) + val info = + Session.Info(dir + path, entry.parent, + entry.description, entry.options, entry.theories, entry.files) - queue1 + (key, info, entry.parent) + queue1 + (key, info) } catch { case ERROR(msg) => @@ -244,14 +246,57 @@ private def echo(msg: String) { java.lang.System.out.println(msg) } private def echo_n(msg: String) { java.lang.System.out.print(msg) } - private def build_job(build_images: Boolean, // FIXME - key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job = + class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String) { + private val args_file = File.tmp_file("args") + private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath)) + File.write(args_file, args) + + private val (thread, result) = Simple_Thread.future("build_job") { + Isabelle_System.bash_env(cwd, env1, script) + } + + def terminate: Unit = thread.interrupt + def is_finished: Boolean = result.is_finished + def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc } + } + + private def build_job(build_images: Boolean, name: String, info: Session.Info): Build_Job = + { + val parent = info.parent.getOrElse("") + val cwd = info.dir.file + val env = Map("INPUT" -> parent, "TARGET" -> name) val script = - if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name - else """echo "Bad session" >&2; exit 2""" - new Isabelle_System.Bash_Job(cwd, null, script) + if (is_pure(name)) "./build " + (if (build_images) "-b " else "") + name + else { + """ + . "$ISABELLE_HOME/lib/scripts/timestart.bash" + """ + + (if (build_images) + """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """ + else + """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) + + """ + RC="$?" + + . "$ISABELLE_HOME/lib/scripts/timestop.bash" + + if [ "$RC" -eq 0 ]; then + echo "Finished $TARGET ($TIMES_REPORT)" >&2 + fi + + exit "$RC" + """ + } + val args_xml = + { + import XML.Encode._ + def symbol_string: T[String] = (s => string(Symbol.encode(s))) + pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))( + build_images, (parent, (name, info.theories.map(_._2).flatten))) + } + new Build_Job(cwd, env, script, YXML.string_of_body(args_xml)) } def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean, @@ -292,10 +337,10 @@ { if (list_only) { echo(key.name + " in " + info.dir); 0 } else { - if (build_images) echo("Building " + key.name + "...") - else echo("Running " + key.name + "...") + if (build_images) echo("Building " + key.name + " ...") + else echo("Running " + key.name + " ...") - val (out, err, rc) = build_job(build_images, key, info).join + val (out, err, rc) = build_job(build_images, key.name, info).join echo_n(err) val log = log_dir + Path.basic(key.name) diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Jul 21 12:57:31 2012 +0200 +++ b/src/Pure/System/isabelle_system.scala Sat Jul 21 16:41:55 2012 +0200 @@ -260,17 +260,6 @@ def bash(script: String): (String, String, Int) = bash_env(null, null, script) - class Bash_Job(cwd: JFile, env: Map[String, String], script: String) - { - private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) } - - def terminate: Unit = thread.interrupt - def is_finished: Boolean = result.is_finished - def join: (String, String, Int) = result.join - - override def toString: String = if (is_finished) join._3.toString else "" - } - /* system tools */ diff -r bb1d4ec90f30 -r 1a634f9614fb src/Pure/System/session.ML --- a/src/Pure/System/session.ML Sat Jul 21 12:57:31 2012 +0200 +++ b/src/Pure/System/session.ML Sat Jul 21 16:41:55 2012 +0200 @@ -9,6 +9,7 @@ val id: unit -> string list val name: unit -> string val welcome: unit -> string + val init: bool -> string -> string -> unit val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> bool -> string list -> string -> string -> bool * string -> string -> int -> bool -> bool -> int -> int -> int -> int -> unit