# HG changeset patch # User wenzelm # Date 1342811043 -7200 # Node ID 527e2bad7cca004d5f153e002953f1b33f17b739 # Parent d0fa3efec93b51be4d6aa093cb233bcaf4cad5a9 further imitation of "usedir" shell script; Pure/build observes build_images option, unlike traditional version; tuned signature; diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/General/path.scala --- a/src/Pure/General/path.scala Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/General/path.scala Fri Jul 20 21:04:03 2012 +0200 @@ -8,6 +8,8 @@ package isabelle +import java.io.File + import scala.util.matching.Regex @@ -162,4 +164,9 @@ new Path(Path.norm_elems(elems.map(eval).flatten)) } + + + /* platform file */ + + def file: File = Isabelle_System.platform_file(this) } diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/System/build.scala --- a/src/Pure/System/build.scala Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/System/build.scala Fri Jul 20 21:04:03 2012 +0200 @@ -198,7 +198,7 @@ private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue = { - val root = Isabelle_System.platform_file(dir + ROOT) + val root = (dir + ROOT).file if (root.isFile) sessions_root(dir, root, queue) else if (strict) error("Bad session root file: " + quote(root.toString)) else queue @@ -212,7 +212,7 @@ (queue /: dirs)((queue1, dir1) => try { val dir2 = dir + Path.explode(dir1) - if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, queue1) + if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1) else error("Bad session directory: " + dir2.toString) } catch { @@ -228,7 +228,7 @@ for (dir <- Isabelle_System.components()) { queue = sessions_dir(false, dir, queue) - val catalog = Isabelle_System.platform_file(dir + SESSIONS) + val catalog = (dir + SESSIONS).file if (catalog.isFile) queue = sessions_catalog(dir, catalog, queue) } @@ -242,12 +242,15 @@ /** build **/ + 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 = { - val cwd = Isabelle_System.platform_file(info.dir) + val cwd = info.dir.file val script = - if (is_pure(key.name)) "./build " + key.name + 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) } @@ -256,7 +259,6 @@ more_dirs: List[Path], options: List[String], sessions: List[String]): Int = { val full_queue = find_sessions(more_dirs) - val build_options = (Options.init() /: options)(_.define_simple(_)) sessions.filter(name => !full_queue.defined(name)) match { @@ -268,15 +270,54 @@ if (all_sessions) full_queue else full_queue.required(sessions) - for ((key, info) <- required_queue.topological_order) { - if (list_only) println(key.name + " in " + info.dir) - else { - val (out, err, rc) = build_job(build_images, key, info).join - java.lang.System.err.print(err) - } + // prepare browser info dir + if (build_options.bool("browser_info") && + !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile) + { + Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs() + Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file, + Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file) + Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file, + Standard_System.read_file( + Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) + + Standard_System.read_file( + Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) + + Standard_System.read_file( + Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file)) } - 0 + // prepare log dir + val log_dir = Path.explode("$ISABELLE_OUTPUT/log") + log_dir.file.mkdirs() + + // run jobs + val rcs = + for ((key, info) <- required_queue.topological_order) yield + { + if (list_only) { echo(key.name + " in " + info.dir); 0 } + else { + if (build_images) echo("Building " + key.name + "...") + else echo("Running " + key.name + "...") + + val (out, err, rc) = build_job(build_images, key, info).join + echo_n(err) + + val log = log_dir + Path.basic(key.name) + if (rc == 0) { + Standard_System.write_file(log.ext("gz").file, out, true) + } + else { + Standard_System.write_file(log.file, out) + echo(key.name + " FAILED") + echo("(see also " + log.file + ")") + val lines = split_lines(out) + val tail = lines.drop(lines.length - 20 max 0) + echo("\n" + cat_lines(tail)) + } + rc + } + } + (0 /: rcs)(_ max _) } diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri Jul 20 21:04:03 2012 +0200 @@ -146,10 +146,9 @@ if (path.is_absolute || path.is_current) try_file(platform_file(path)) else { - val pure_file = platform_file(Path.explode("~~/src/Pure") + path) + val pure_file = (Path.explode("~~/src/Pure") + path).file if (pure_file.isFile) Some(pure_file) - else if (getenv("ML_SOURCES") != "") - try_file(platform_file(Path.explode("$ML_SOURCES") + path)) + else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file) else None } } @@ -278,7 +277,7 @@ def isabelle_tool(name: String, args: String*): (String, Int) = { Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir => - val file = platform_file(dir + Path.basic(name)) + val file = (dir + Path.basic(name)).file try { file.isFile && file.canRead && file.canExecute && !name.endsWith("~") && !name.endsWith(".orig") @@ -309,7 +308,7 @@ val ml_ident = getenv_strict("ML_IDENTIFIER") val logics = new mutable.ListBuffer[String] for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) { - val files = platform_file(dir + Path.explode(ml_ident)).listFiles() + val files = (dir + Path.explode(ml_ident)).file.listFiles() if (files != null) { for (file <- files if file.isFile) logics += file.getName } @@ -327,6 +326,6 @@ { val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() for (font <- Path.split(getenv_strict("ISABELLE_FONTS"))) - ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font))) + ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file)) } } diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/System/options.scala --- a/src/Pure/System/options.scala Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/System/options.scala Fri Jul 20 21:04:03 2012 +0200 @@ -66,7 +66,7 @@ var options = empty for { dir <- Isabelle_System.components() - file = Isabelle_System.platform_file(dir + OPTIONS) + file = (dir + OPTIONS).file if file.isFile entry <- Parser.parse_entries(file) } { diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/System/standard_system.scala --- a/src/Pure/System/standard_system.scala Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/System/standard_system.scala Fri Jul 20 21:04:03 2012 +0200 @@ -15,6 +15,7 @@ BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader, File, FileFilter, IOException} import java.nio.charset.Charset +import java.util.zip.GZIPOutputStream import scala.io.Codec import scala.util.matching.Regex @@ -115,10 +116,11 @@ def read_file(file: File): String = slurp(new FileInputStream(file)) - def write_file(file: File, text: CharSequence) + def write_file(file: File, text: CharSequence, zip: Boolean = false) { - val writer = - new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset)) + val stream1 = new FileOutputStream(file) + val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1 + val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset)) try { writer.append(text) } finally { writer.close } } diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/System/system_channel.scala --- a/src/Pure/System/system_channel.scala Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/System/system_channel.scala Fri Jul 20 21:04:03 2012 +0200 @@ -47,8 +47,7 @@ } private def rm_fifo(fifo: String): Boolean = - Isabelle_System.platform_file( - Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete + Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete private def fifo_input_stream(fifo: String): InputStream = { diff -r d0fa3efec93b -r 527e2bad7cca src/Pure/build --- a/src/Pure/build Fri Jul 20 18:50:33 2012 +0200 +++ b/src/Pure/build Fri Jul 20 21:04:03 2012 +0200 @@ -12,7 +12,10 @@ function usage() { echo - echo "Usage: $PRG TARGET" + echo "Usage: $PRG [OPTIONS] TARGET" + echo + echo " Options are:" + echo " -b build target images" echo echo " Build Isabelle/ML TARGET: RAW or Pure" echo @@ -30,6 +33,27 @@ ## process command line +# options + +BUILD_IMAGES=false + +while getopts "b" OPT +do + case "$OPT" in + b) + BUILD_IMAGES="true" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + TARGET="Pure" [ "$#" -ge 1 ] && { TARGET="$1"; shift; } [ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\"" @@ -54,29 +78,37 @@ . "$ISABELLE_HOME/lib/scripts/timestart.bash" -echo "Building $TARGET ..." >&2 +if [ "$TARGET" = RAW ]; then + if [ "$BUILD_IMAGES" = false ]; then + "$ISABELLE_PROCESS" \ + -e "use\"$COMPAT\" handle _ => exit 1;" \ + -q RAW_ML_SYSTEM + else + "$ISABELLE_PROCESS" \ + -e "use\"$COMPAT\" handle _ => exit 1;" \ + -e "structure Isar = struct fun main () = () end;" \ + -e "ml_prompts \"ML> \" \"ML# \";" \ + -q -w RAW_ML_SYSTEM RAW + fi +else + if [ "$BUILD_IMAGES" = false ]; then + "$ISABELLE_PROCESS" \ + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ + -q RAW_ML_SYSTEM + else + "$ISABELLE_PROCESS" \ + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ + -e "ml_prompts \"ML> \" \"ML# \";" \ + -f -q -w RAW_ML_SYSTEM Pure + fi +fi -if [ "$TARGET" = RAW ]; then - "$ISABELLE_PROCESS" \ - -e "use\"$COMPAT\" handle _ => exit 1;" \ - -e "structure Isar = struct fun main () = () end;" \ - -e "ml_prompts \"ML> \" \"ML# \";" \ - -q -w RAW_ML_SYSTEM RAW - RC="$?" -else - "$ISABELLE_PROCESS" \ - -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ - -e "ml_prompts \"ML> \" \"ML# \";" \ - -f -q -w RAW_ML_SYSTEM Pure - RC="$?" -fi +RC="$?" . "$ISABELLE_HOME/lib/scripts/timestop.bash" if [ "$RC" -eq 0 ]; then echo "Finished $TARGET ($TIMES_REPORT)" >&2 -else - echo "$TARGET FAILED" >&2 fi exit "$RC"