# HG changeset patch # User wenzelm # Date 1476477929 -7200 # Node ID 89514fa139c96c9dfef56f4dd3f9564aefe23138 # Parent 4d1d2de432fa666a35af86931e2abbf2cf9062b4# Parent 123e6dcd3852487b74adfe894a44d264d9cb42af merged diff -r 4d1d2de432fa -r 89514fa139c9 Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Thu Oct 13 15:43:15 2016 +0200 +++ b/Admin/Release/CHECKLIST Fri Oct 14 22:45:29 2016 +0200 @@ -78,7 +78,7 @@ - fully-automated packaging (e.g. on macbroy2): - hg up -r DISTNAME && Admin/Release/build -M macbroy30 -O -l -r DISTNAME /home/isabelle/dist + hg up -r DISTNAME && Admin/build_release -M macbroy30 -O -l -R DISTNAME /home/isabelle/dist Final release stage diff -r 4d1d2de432fa -r 89514fa139c9 Admin/Release/build --- a/Admin/Release/build Thu Oct 13 15:43:15 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# build full Isabelle distribution from repository - -THIS="$(cd "$(dirname "$0")"; pwd)" -PRG="$(basename "$0")" - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]" - echo - echo " Options are:" - echo " -M USER@HOST remote Mac OS X for dmg build" - echo " -O official release (not release-candidate)" - echo " -j INT maximum number of parallel jobs (default 1)" - echo " -l build library" - echo " -r RELEASE proper release with name" - echo - echo " Make Isabelle distribution DIR, using the local repository clone." - echo - echo " VERSION identifies the snapshot, using usual Mercurial terminology;" - echo " the default is RELEASE if given, otherwise \"tip\"." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -function check_number() -{ - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" -} - - -## process command line - -# options - -REMOTE_MAC="" -OFFICIAL_RELEASE="" -JOBS="" -LIBRARY="" -RELEASE="" - -while getopts "M:Oj:lr:" OPT -do - case "$OPT" in - M) - REMOTE_MAC="$OPTARG" - ;; - O) - OFFICIAL_RELEASE="-O" - ;; - j) - check_number "$OPTARG" - JOBS="-j $OPTARG" - ;; - l) - LIBRARY="true" - ;; - r) - RELEASE="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -BASE_DIR="" -[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; } -[ -z "$BASE_DIR" ] && usage - -VERSION="" -[ "$#" -gt 0 ] && { VERSION="$1"; shift; } -[ -z "$VERSION" ] && VERSION="$RELEASE" -[ -z "$VERSION" ] && VERSION="tip" - -[ "$#" -gt 0 ] && usage - - -## Isabelle settings - -ISABELLE_TOOL="$THIS/../../bin/isabelle" -ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)" - - -## main - -# make dist - -if [ -z "$RELEASE" ]; then - DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")" - "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -else - DISTNAME="$RELEASE" - "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -r "$RELEASE" -fi -[ "$?" = 0 ] || exit "$?" - -DISTBASE="$BASE_DIR/dist-${DISTNAME}" - - -# make bundles - -for PLATFORM_FAMILY in linux windows windows64 macos -do - -echo -echo "*** $PLATFORM_FAMILY ***" - -if [ -n "$REMOTE_MAC" ]; then - "$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY" "$REMOTE_MAC" -else - "$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY" -fi -[ "$?" = 0 ] || exit "$?" - -done - - -# minimal index - -cat > "$DISTBASE/index.html" < - - -${DISTNAME} - - - -

${DISTNAME}

- - - -EOF - - -# HTML library - -if [ -n "$LIBRARY" ]; then - "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz" -fi diff -r 4d1d2de432fa -r 89514fa139c9 Admin/build_history --- a/Admin/build_history Thu Oct 13 15:43:15 2016 +0200 +++ b/Admin/build_history Fri Oct 14 22:45:29 2016 +0200 @@ -2,9 +2,7 @@ # # DESCRIPTION: build history versions from another repository clone - THIS="$(cd "$(dirname "$0")"; pwd)" "$THIS/build" jars || exit $? - exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@" diff -r 4d1d2de432fa -r 89514fa139c9 Admin/build_release --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/build_release Fri Oct 14 22:45:29 2016 +0200 @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# +# DESCRIPTION: build full Isabelle distribution from repository + +THIS="$(cd "$(dirname "$0")"; pwd)" + +"$THIS/build" jars || exit $? +exec "$THIS/../bin/isabelle_java" isabelle.Build_Release "$@" diff -r 4d1d2de432fa -r 89514fa139c9 Admin/cronjob/cronjob.options --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/cronjob/cronjob.options Fri Oct 14 22:45:29 2016 +0200 @@ -0,0 +1,7 @@ +(* :mode=isabelle-options: *) + +option isabelle_repos : string = "http://isabelle.in.tum.de/repos/isabelle" + +option isabelle_release_repos : string = "http://bitbucket.org/isabelle_project/isabelle-release" + +option afp_repos : string = "https://bitbucket.org/isa-afp/afp-devel" diff -r 4d1d2de432fa -r 89514fa139c9 Admin/cronjob/main --- a/Admin/cronjob/main Thu Oct 13 15:43:15 2016 +0200 +++ b/Admin/cronjob/main Fri Oct 14 22:45:29 2016 +0200 @@ -8,4 +8,5 @@ "$THIS/../build" jars_fresh || exit $? -exec "$THIS/../../bin/isabelle_java" "-Duser.timezone=Europe/Berlin" isabelle.Isabelle_Cronjob "$@" +exec env ISABELLE_IDENTIFIER="cronjob" \ + "$THIS/../../bin/isabelle_java" "-Duser.timezone=Europe/Berlin" isabelle.Isabelle_Cronjob "$@" diff -r 4d1d2de432fa -r 89514fa139c9 Admin/lib/Tools/makedist --- a/Admin/lib/Tools/makedist Thu Oct 13 15:43:15 2016 +0200 +++ b/Admin/lib/Tools/makedist Fri Oct 14 22:45:29 2016 +0200 @@ -199,6 +199,9 @@ ./bin/isabelle java isabelle.NEWS +rmdir "$USER_HOME/.isabelle/${DISTNAME}-build" +rmdir "$USER_HOME/.isabelle/${DISTNAME}" + # create archive diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/Admin/build_history.scala Fri Oct 14 22:45:29 2016 +0200 @@ -20,137 +20,75 @@ val META_INFO_MARKER = "\fmeta_info = " - - /** other Isabelle environment **/ - - private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String) - { - other_isabelle => - - - /* static system */ + /* augment settings */ - def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = - Isabelle_System.bash( - "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, - env = null, cwd = isabelle_home.file, redirect = redirect, - progress_stdout = progress.echo_if(echo, _), - progress_stderr = progress.echo_if(echo, _)) + def augment_settings( + other_isabelle: Other_Isabelle, + threads: Int, + arch_64: Boolean = false, + heap: Int = default_heap, + max_heap: Option[Int] = None, + more_settings: List[String]): String = + { + val (ml_platform, ml_settings) = + { + val windows_32 = "x86-windows" + val windows_64 = "x86_64-windows" + val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out + val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out + val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out - def copy_dir(dir1: Path, dir2: Path): Unit = - bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check - - def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = - bash("bin/isabelle " + cmdline, redirect, echo) + val polyml_home = + try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir } + catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } - def resolve_components(echo: Boolean): Unit = - other_isabelle("components -a", redirect = true, echo = echo).check + def ml_home(platform: String): Path = polyml_home + Path.explode(platform) - val isabelle_home_user: Path = - Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out) + def err(platform: String): Nothing = + error("Platform " + platform + " unavailable on this machine") - val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") - val log_dir: Path = isabelle_home_user + Path.explode("log") - - - /* reset settings */ - - def reset_settings(components_base: String, nonfree: Boolean) - { - if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) - error("Cannot proceed with existing user settings file: " + etc_settings) + def check_dir(platform: String): Boolean = + platform != "" && ml_home(platform).is_dir - Isabelle_System.mkdirs(etc_settings.dir) - File.write(etc_settings, - "# generated by Isabelle " + Date.now() + "\n" + - "#-*- shell-script -*- :mode=shellscript:\n") + 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_32)) windows_32 + else platform_32 // x86-cygwin + } + else { + val (platform, platform_name) = + if (arch_64) (platform_64, "x86_64-" + platform_family) + else (platform_32, "x86-" + platform_family) + if (check_dir(platform)) platform else err(platform_name) + } - val component_settings = - { - val components_base_path = - if (components_base == "") isabelle_home_user.dir + Path.explode("contrib") - else Path.explode(components_base).expand + val ml_options = + "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + + " --gcthreads " + threads + + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") - val catalogs = - if (nonfree) List("main", "optional", "nonfree") else List("main", "optional") - - catalogs.map(catalog => - "init_components " + File.bash_path(components_base_path) + - " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"") - } - File.append(etc_settings, "\n" + terminate_lines(component_settings)) + (ml_platform, + List( + "ML_HOME=" + File.bash_path(ml_home(ml_platform)), + "ML_PLATFORM=" + quote(ml_platform), + "ML_OPTIONS=" + quote(ml_options))) } - - /* augment settings */ - - def augment_settings( - threads: Int, - arch_64: Boolean = false, - heap: Int = default_heap, - max_heap: Option[Int] = None, - more_settings: List[String]): String = - { - val (ml_platform, ml_settings) = - { - val windows_32 = "x86-windows" - val windows_64 = "x86_64-windows" - val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out - val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out - val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out - - val polyml_home = - try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).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 thread_settings = + List( + "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", + "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") - 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_32)) windows_32 - else platform_32 // x86-cygwin - } - else { - val (platform, platform_name) = - if (arch_64) (platform_64, "x86_64-" + platform_family) - else (platform_32, "x86-" + platform_family) - if (check_dir(platform)) platform else err(platform_name) - } - - val ml_options = - "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + - " --gcthreads " + threads + - (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") + val settings = + List(ml_settings, thread_settings) ::: + (if (more_settings.isEmpty) Nil else List(more_settings)) - (ml_platform, - List( - "ML_HOME=" + File.bash_path(ml_home(ml_platform)), - "ML_PLATFORM=" + quote(ml_platform), - "ML_OPTIONS=" + quote(ml_options))) - } + File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) - 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(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) - - ml_platform - } + ml_platform } @@ -163,8 +101,8 @@ private val default_isabelle_identifier = "build_history" def build_history( - progress: Progress, hg: Mercurial.Repository, + progress: Progress = Ignore_Progress, rev: String = default_rev, isabelle_identifier: String = default_isabelle_identifier, components_base: String = "", @@ -177,11 +115,11 @@ max_heap: Option[Int] = None, more_settings: List[String] = Nil, verbose: Boolean = false, - build_args: List[String] = Nil): List[Process_Result] = + build_args: List[String] = Nil): List[(Process_Result, Path)] = { /* sanity checks */ - if (File.eq(Path.explode("~~").file, hg.root.file)) + if (File.eq(Path.explode("~~"), hg.root)) error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand) for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads) @@ -216,10 +154,10 @@ { /* init settings */ - other_isabelle.reset_settings(components_base, nonfree) + other_isabelle.init_settings(components_base, nonfree) other_isabelle.resolve_components(verbose) val ml_platform = - other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings) + augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out) val isabelle_output_log = isabelle_output + Path.explode("log") @@ -232,17 +170,17 @@ "bin/isabelle jedit -b" + (if (fresh) " -f" else ""), redirect = true, echo = verbose).check - Isabelle_System.rm_tree(isabelle_base_log.file) + Isabelle_System.rm_tree(isabelle_base_log) } - Isabelle_System.rm_tree(isabelle_output.file) + Isabelle_System.rm_tree(isabelle_output) Isabelle_System.mkdirs(isabelle_output) /* build */ if (multicore_base && !first_build && isabelle_base_log.is_dir) - other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log) + Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log) val build_start = Date.now() val res = @@ -253,8 +191,10 @@ /* output log */ val log_path = - other_isabelle.log_dir + - Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz") + other_isabelle.isabelle_home_user + + Build_Log.log_subdir(build_history_date) + + Build_Log.log_filename( + BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz") val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() @@ -292,17 +232,15 @@ ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) ::: heap_sizes)) - Output.writeln(log_path.implode, stdout = true) - /* next build */ if (multicore_base && first_build && isabelle_output_log.is_dir) - other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log) + Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) first_build = false - res + (res, log_path) } } @@ -373,14 +311,17 @@ val hg = Mercurial.repository(Path.explode(root)) val progress = new Console_Progress(stderr = true) val results = - build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier, + build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier, components_base = components_base, fresh = fresh, nonfree = nonfree, multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, more_settings = more_settings, verbose = verbose, build_args = build_args) - val rc = (0 /: results) { case (rc, res) => rc max res.rc } + for ((_, log_path) <- results) + Output.writeln(log_path.implode, stdout = true) + + val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc } if (rc != 0) sys.exit(rc) } } diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/Admin/build_log.scala Fri Oct 14 22:45:29 2016 +0200 @@ -27,9 +27,11 @@ DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep), new java.lang.Long((date.time - date.midnight.time).ms / 1000)) - def log_path(engine: String, date: Date, more: String*): Path = - Path.explode(date.rep.getYear.toString) + - Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log")) + def log_subdir(date: Date): Path = + Path.explode("log") + Path.explode(date.rep.getYear.toString) + + def log_filename(engine: String, date: Date, more: String*): Path = + Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log")) /* log file collections */ @@ -183,6 +185,9 @@ def find[A](f: String => Option[A]): Option[A] = lines.iterator.map(f).find(_.isDefined).map(_.get) + def find_line(marker: String): Option[String] = + find(Library.try_unprefix(marker, _)) + def find_match(regex: Regex): Option[String] = lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1). map(res => res.get.head) @@ -208,13 +213,17 @@ xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) def filter_props(marker: String): List[Properties.T] = - for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s) - - def find_line(marker: String): Option[String] = - find(Library.try_unprefix(marker, _)) + for { + line <- lines + s <- Library.try_unprefix(marker, line) + if YXML.detect(s) + } yield parse_props(s) def find_props(marker: String): Option[Properties.T] = - find_line(marker).map(parse_props(_)) + find_line(marker) match { + case Some(text) if YXML.detect(text) => Some(parse_props(text)) + case _ => None + } /* parse various formats */ diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/Admin/build_release.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_release.scala Fri Oct 14 22:45:29 2016 +0200 @@ -0,0 +1,205 @@ +/* Title: Pure/Admin/build_release.scala + Author: Makarius + +Build full Isabelle distribution from repository. +*/ + +package isabelle + + +object Build_Release +{ + sealed case class Release_Info( + date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path) + + private val default_platform_families = List("linux", "windows", "windows64", "macos") + + def build_release(base_dir: Path, + progress: Progress = Ignore_Progress, + rev: String = "", + official_release: Boolean = false, + release_name: String = "", + platform_families: List[String] = default_platform_families, + website: Option[Path] = None, + build_library: Boolean = false, + parallel_jobs: Int = 1, + remote_mac: String = ""): Release_Info = + { + /* release info */ + + val release_info = + { + val date = Date.now() + val name = if (release_name != "") release_name else "Isabelle_" + Date.Format.date(date) + val dist_dir = base_dir + Path.explode("dist-" + name) + val dist_archive = dist_dir + Path.explode(name + ".tar.gz") + val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz") + Release_Info(date, name, dist_dir, dist_archive, dist_library_archive) + } + + val main_platform_bundles = + List("linux" -> (release_info.name + "_app.tar.gz"), + "windows" -> (release_info.name + "-win32.exe"), + "windows64" -> (release_info.name + "-win64.exe"), + "macos" -> (release_info.name + ".dmg")) + + val fallback_platform_bundles = + List("macos" -> (release_info.name + "_dmg.tar.gz")) + + val platform_bundles = + for (platform_family <- platform_families) yield { + main_platform_bundles.toMap.get(platform_family) match { + case None => error("Unknown platform family " + quote(platform_family)) + case Some(bundle) => (platform_family, bundle) + } + } + + + /* make distribution */ + + val jobs_option = " -j" + parallel_jobs.toString + + if (release_info.dist_archive.is_file) + progress.echo("### Release archive already exists: " + release_info.dist_archive.implode) + else { + progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...") + progress.bash( + "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option + + (if (official_release) " -O" else "") + + (if (release_name != "") " -r " + File.bash_string(release_name) else "") + + (if (rev != "") " " + File.bash_string(rev) else ""), + echo = true).check + } + + + /* make application bundles */ + + for ((platform_family, platform_bundle) <- platform_bundles) { + val bundle_archive = + release_info.dist_dir + + Path.explode( + (if (remote_mac.isEmpty) fallback_platform_bundles.toMap.get(platform_family) else None) + getOrElse platform_bundle) + if (bundle_archive.is_file) + progress.echo("### Application bundle already exists: " + bundle_archive.implode) + else { + progress.echo("\nApplication bundle for " + platform_family + ": " + bundle_archive.implode) + progress.bash( + "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) + + " " + File.bash_string(platform_family) + + (if (remote_mac == "") "" else " " + File.bash_string(remote_mac)), + echo = true).check + } + } + + + /* minimal website */ + + website.foreach(dir => + { + val website_platform_bundles = + Library.distinct( + for { + (a, b) <- main_platform_bundles ::: fallback_platform_bundles + p = release_info.dist_dir + Path.explode(b) + if p.is_file + } yield (a, b), (x: (String, String), y: (String, String)) => x._1 == y._1) + + Isabelle_System.mkdirs(dir) + + File.write(dir + Path.explode("index.html"), +""" + + +""" + HTML.output(release_info.name) + """ + + + +

""" + HTML.output(release_info.name) + """

" + HTML.output(Word.capitalize(a)) + "

+ + + +""") + for ((_, b) <- website_platform_bundles) + File.copy(release_info.dist_dir + Path.explode(b), dir) + }) + + + /* HTML library */ + + if (build_library) { + if (release_info.dist_library_archive.is_file) + progress.echo("### Library archive already exists: " + + release_info.dist_library_archive.implode) + else { + progress.bash("\"$ISABELLE_HOME/Admin/Release/build_library\"" + jobs_option + " " + + File.bash_path(release_info.dist_dir + + Path.explode(release_info.name + "_" + + Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") + ".tar.gz"))).check + } + } + + + release_info + } + + + + /** command line entry point **/ + + def main(args: Array[String]) + { + Command_Line.tool0 { + var remote_mac = "" + var official_release = false + var release_name = "" + var website: Option[Path] = None + var parallel_jobs = 1 + var build_library = false + var platform_families = default_platform_families + var rev = "" + + val getopts = Getopts(""" +Usage: Admin/build_release [OPTIONS] BASE_DIR + + Options are: + -M USER@HOST remote Mac OS X for dmg build + -O official release (not release-candidate) + -R RELEASE proper release with name + -W WEBSITE produce minimal website in given directory + -j INT maximum number of parallel jobs (default 1) + -l build library + -p NAMES platform families (comma separated list, default: """ + + default_platform_families.mkString(",") + """) + -r REV Mercurial changeset id (default: RELEASE or tip) + + Build Isabelle release in base directory, using the local repository clone. +""", + "M:" -> (arg => remote_mac = arg), + "O" -> (_ => official_release = true), + "R:" -> (arg => release_name = arg), + "W:" -> (arg => website = Some(Path.explode(arg))), + "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), + "l" -> (_ => build_library), + "p:" -> (arg => platform_families = Library.space_explode(',', arg)), + "r:" -> (arg => rev = arg)) + + val more_args = getopts(args) + val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } + + val progress = new Console_Progress() + + build_release(Path.explode(base_dir), progress = progress, rev = rev, + official_release = official_release, release_name = release_name, website = website, + platform_families = + if (platform_families.isEmpty) default_platform_families else platform_families, + build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) + } + } +} diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Oct 14 22:45:29 2016 +0200 @@ -13,19 +13,81 @@ object Isabelle_Cronjob { - /** file-system state: owned by main cronjob **/ + /* file-system state: owned by main cronjob */ val main_dir = Path.explode("~/cronjob") - val run_dir = main_dir + Path.explode("run") - val log_dir = main_dir + Path.explode("log") + val main_state_file = main_dir + Path.explode("run/main.state") + val main_log = main_dir + Path.explode("log/main.log") // owned by log service + + val isabelle_repos = main_dir + Path.explode("isabelle-build_history") + val afp_repos = main_dir + Path.explode("AFP-build_history") + + val release_snapshot = main_dir + Path.explode("release_snapshot") + + + + /** particular tasks **/ + + /* identify Isabelle + AFP repository snapshots */ - val main_state_file = run_dir + Path.explode("main.state") - val main_log = log_dir + Path.explode("main.log") // owned by log service + private val isabelle_identify = + Logger_Task("isabelle_identify", logger => + { + val isabelle_id = Mercurial.repository(isabelle_repos).pull_id() + val afp_id = Mercurial.repository(afp_repos).pull_id() + + File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), + terminate_lines( + List("isabelle_identify: " + Build_Log.print_date(logger.start_date), + "", + "Isabelle version: " + isabelle_id, + "AFP version: " + afp_id))) + }) - /* task logging */ + /* integrity test of build_history vs. build_history_base */ + + private val build_history_base = + Logger_Task("build_history_base", logger => + { + for { + (result, log_path) <- + Build_History.build_history(Mercurial.repository(isabelle_repos), + rev = "build_history_base", fresh = true, build_args = List("FOL")) + } { + result.check + File.copy(log_path, logger.log_dir + log_path.base) + } + }) + + + /* build release from repository snapshot */ - sealed case class Logger_Task(name: String, body: Logger => Unit) + private val build_release = + Logger_Task("build_release", logger => + Isabelle_System.with_tmp_dir("isadist")(tmp_dir => + { + val base_dir = File.path(tmp_dir) + + val new_snapshot = release_snapshot.ext("new") + val old_snapshot = release_snapshot.ext("old") + + Isabelle_System.rm_tree(new_snapshot) + Isabelle_System.rm_tree(old_snapshot) + + Build_Release.build_release(base_dir, parallel_jobs = 4, + remote_mac = "macbroy30", website = Some(new_snapshot)) + + if (release_snapshot.is_dir) File.mv(release_snapshot, old_snapshot) + File.mv(new_snapshot, release_snapshot) + Isabelle_System.rm_tree(old_snapshot) + })) + + + + /** task logging **/ + + sealed case class Logger_Task(name: String = "", body: Logger => Unit) class Log_Service private[Isabelle_Cronjob](progress: Progress) { @@ -43,8 +105,9 @@ val hostname = Isabelle_System.hostname() def log(date: Date, task_name: String, msg: String): Unit = - thread.send( - "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) + if (task_name != "") + thread.send( + "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) def start_logger(start_date: Date, task_name: String): Logger = new Logger(this, start_date, task_name) @@ -76,10 +139,13 @@ val elapsed_time = end_date.time - start_date.time val msg = (if (err.isEmpty) "finished" else "ERROR " + err.get) + - (if (elapsed_time.seconds < 3.0) "" else ", elapsed time " + elapsed_time.message_hms) + (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") log(end_date, msg) } + val log_dir: Path = main_dir + Build_Log.log_subdir(start_date) + + Isabelle_System.mkdirs(log_dir) log(start_date, "started") } @@ -91,41 +157,11 @@ - /** particular tasks **/ - - /* identify repository snapshots */ - - val isabelle_repos = main_dir + Path.explode("isabelle-build_history") - val afp_repos = main_dir + Path.explode("AFP-build_history") - - val isabelle_identify = - Logger_Task("isabelle_identify", logger => - { - def pull_repos(root: Path): String = - { - val hg = Mercurial.repository(root) - hg.pull(options = "-q") - hg.identify("tip", options = "-i") - } - - val isabelle_id = pull_repos(isabelle_repos) - val afp_id = pull_repos(afp_repos) - - val log_path = log_dir + Build_Log.log_path("isabelle_identify", logger.start_date) - Isabelle_System.mkdirs(log_path.dir) - File.write(log_path, - terminate_lines( - List("isabelle_identify: " + Build_Log.print_date(logger.start_date), - "", - "Isabelle version: " + isabelle_id, - "AFP version: " + afp_id))) - }) - - - /** cronjob **/ - def cronjob(progress: Progress) + def init_options(): Options = Options.load(Path.explode("~~/Admin/cronjob/cronjob.options")) + + def cronjob(progress: Progress, exclude_task: Set[String]) { /* soft lock */ @@ -139,33 +175,48 @@ error("Isabelle cronjob appears to be still running: " + running) } - val main_start_date = Date.now() + + /* log service */ + val log_service = new Log_Service(progress) - File.write(main_state_file, main_start_date + " " + log_service.hostname) + def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) } + + def run_now(task: Logger_Task) { run(Date.now(), task) } - /* parallel tasks */ + /* structured tasks */ - def parallel_tasks(tasks: List[Logger_Task]) - { - @tailrec def await(running: List[Task]) + def SEQ(tasks: Logger_Task*): Logger_Task = Logger_Task(body = _ => + for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") + run_now(task)) + + def PAR(tasks: Logger_Task*): Logger_Task = Logger_Task(body = _ => { - running.partition(_.is_finished) match { - case (Nil, Nil) => - case (Nil, _ :: _) => Thread.sleep(500); await(running) - case (_ :: _, remaining) => await(remaining) + @tailrec def join(running: List[Task]) + { + running.partition(_.is_finished) match { + case (Nil, Nil) => + case (Nil, _ :: _) => Thread.sleep(500); join(running) + case (_ :: _, remaining) => join(remaining) + } } - } - val start_date = Date.now() - await(tasks.map(task => log_service.fork_task(start_date, task))) - } + val start_date = Date.now() + val running = + for (task <- tasks.toList if !exclude_task(task.name)) + yield log_service.fork_task(start_date, task) + join(running) + }) /* main */ - log_service.run_task(main_start_date, - Logger_Task("isabelle_cronjob", _ => parallel_tasks(List(isabelle_identify)))) + val main_start_date = Date.now() + File.write(main_state_file, main_start_date + " " + log_service.hostname) + + run(main_start_date, + Logger_Task("isabelle_cronjob", _ => + run_now(SEQ(isabelle_identify, build_history_base, build_release)))) log_service.shutdown() @@ -181,6 +232,7 @@ Command_Line.tool0 { var force = false var verbose = false + var exclude_task = Set.empty[String] val getopts = Getopts(""" Usage: Admin/cronjob/main [OPTIONS] @@ -188,16 +240,18 @@ Options are: -f apply force to do anything -v verbose + -x NAME exclude tasks with this name """, "f" -> (_ => force = true), - "v" -> (_ => verbose = true)) + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_task += arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = if (verbose) new Console_Progress() else Ignore_Progress - if (force) cronjob(progress) + if (force) cronjob(progress, exclude_task) else error("Need to apply force to do anything") } } diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/Admin/other_isabelle.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/other_isabelle.scala Fri Oct 14 22:45:29 2016 +0200 @@ -0,0 +1,61 @@ +/* Title: Pure/Admin/other_isabelle.scala + Author: Makarius + +Manage other Isabelle distributions. +*/ + +package isabelle + + +private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String) +{ + other_isabelle => + + + /* static system */ + + def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = + progress.bash( + "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, + env = null, cwd = isabelle_home.file, redirect = redirect) + + def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = + bash("bin/isabelle " + cmdline, redirect, echo) + + def resolve_components(echo: Boolean): Unit = + other_isabelle("components -a", redirect = true, echo = echo).check + + val isabelle_home_user: Path = + Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out) + + val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") + + + /* init settings */ + + def init_settings(components_base: String, nonfree: Boolean) + { + if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) + error("Cannot proceed with existing user settings file: " + etc_settings) + + Isabelle_System.mkdirs(etc_settings.dir) + File.write(etc_settings, + "# generated by Isabelle " + Date.now() + "\n" + + "#-*- shell-script -*- :mode=shellscript:\n") + + val component_settings = + { + val components_base_path = + if (components_base == "") isabelle_home_user.dir + Path.explode("contrib") + else Path.explode(components_base).expand + + val catalogs = + if (nonfree) List("main", "optional", "nonfree") else List("main", "optional") + + catalogs.map(catalog => + "init_components " + File.bash_path(components_base_path) + + " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"") + } + File.append(etc_settings, "\n" + terminate_lines(component_settings)) + } +} diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/Admin/remote_dmg.scala --- a/src/Pure/Admin/remote_dmg.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/Admin/remote_dmg.scala Fri Oct 14 22:45:29 2016 +0200 @@ -52,7 +52,7 @@ val more_args = getopts(args) val (user, host, tar_gz_file, dmg_file) = more_args match { - case List(SSH.User_Host(user, host), tar_gz_file, dmg_file) => + case List(SSH.Target(user, host), tar_gz_file, dmg_file) => (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file)) case _ => getopts.usage() } diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/General/file.scala Fri Oct 14 22:45:29 2016 +0200 @@ -56,6 +56,8 @@ } catch { case _: MalformedURLException => standard_path(name) } + def path(file: JFile): Path = Path.explode(standard_path(file.getAbsolutePath)) + /* platform path (Windows or Posix) */ @@ -243,13 +245,13 @@ def write_backup(path: Path, text: CharSequence) { - path.file renameTo path.backup.file + mv(path, path.backup) write(path, text) } def write_backup2(path: Path, text: CharSequence) { - path.file renameTo path.backup2.file + mv(path, path.backup2) write(path, text) } @@ -263,12 +265,17 @@ def append(path: Path, text: CharSequence): Unit = append(path.file, text) - /* copy */ + /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } + def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) + + + /* copy */ + def copy(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst @@ -279,4 +286,12 @@ } def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) + + + /* move */ + + def mv(file1: JFile, file2: JFile): Unit = + Files.move(file1.toPath, file2.toPath, StandardCopyOption.REPLACE_EXISTING) + + def mv(path1: Path, path2: Path): Unit = mv(path1.file, path2.file) } diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/General/mercurial.scala Fri Oct 14 22:45:29 2016 +0200 @@ -77,6 +77,12 @@ def pull(remote: String = "", rev: String = "", options: String = ""): Unit = hg.command("pull", opt_rev(rev) + optional(remote), options).check + def pull_id(remote: String = ""): String = + { + hg.pull(remote = remote, options = "-q") + hg.identify("tip", options = "-i") + } + def update( rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") { diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/General/ssh.scala Fri Oct 14 22:45:29 2016 +0200 @@ -17,9 +17,9 @@ object SSH { - /* user@host syntax */ + /* target machine: user@host syntax */ - object User_Host + object Target { val Pattern = "^([^@]+)@(.+)$".r @@ -30,10 +30,10 @@ } def unapplySeq(s: String): Option[List[String]] = - { - val (user, host) = parse(s) - Some(List(user, host)) - } + parse(s) match { + case (_, "") => None + case (user, host) => Some(List(user, host)) + } } val default_port = 22 @@ -114,6 +114,77 @@ } + /* Sftp channel */ + + type Attrs = SftpATTRS + + sealed case class Dir_Entry(name: String, attrs: Attrs) + { + def is_file: Boolean = attrs.isReg + def is_dir: Boolean = attrs.isDir + } + + class Sftp private[SSH](session: Session, kind: String, channel: ChannelSftp) + extends Channel[ChannelSftp](session, kind, channel) + { + channel.connect(connect_timeout(session.options)) + + def home: String = channel.getHome() + + def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) } + def mv(remote_path1: String, remote_path2: String): Unit = + channel.rename(remote_path1, remote_path2) + def rm(remote_path: String) { channel.rm(remote_path) } + def mkdir(remote_path: String) { channel.mkdir(remote_path) } + def rmdir(remote_path: String) { channel.rmdir(remote_path) } + + def stat(remote_path: String): Dir_Entry = + Dir_Entry(remote_path, channel.stat(remote_path)) + + def read_dir(remote_path: String): List[Dir_Entry] = + { + val dir = channel.ls(remote_path) + (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, attrs)).toList + } + + def find_files(remote_path: String, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = + { + def find(dir: String): List[Dir_Entry] = + read_dir(dir).flatMap(entry => + { + val file = dir + "/" + entry.name + if (entry.is_dir) find(file) + else if (pred(entry)) List(entry.copy(name = file)) + else Nil + }) + find(remote_path) + } + + def open_input(remote_path: String): InputStream = channel.get(remote_path) + def open_output(remote_path: String): OutputStream = channel.put(remote_path) + + def read_file(remote_path: String, local_path: Path): Unit = + channel.get(remote_path, File.platform_path(local_path)) + def read_bytes(remote_path: String): Bytes = + using(open_input(remote_path))(Bytes.read_stream(_)) + def read(remote_path: String): String = + using(open_input(remote_path))(File.read_stream(_)) + + def write_file(remote_path: String, local_path: Path): Unit = + channel.put(File.platform_path(local_path), remote_path) + def write_bytes(remote_path: String, bytes: Bytes): Unit = + using(open_output(remote_path))(bytes.write_stream(_)) + def write(remote_path: String, text: String): Unit = + using(open_output(remote_path))(stream => Bytes(text).write_stream(stream)) + } + + /* exec channel */ private val exec_wait_delay = Time.seconds(0.3) @@ -193,77 +264,6 @@ } - /* Sftp channel */ - - type Attrs = SftpATTRS - - sealed case class Dir_Entry(name: String, attrs: Attrs) - { - def is_file: Boolean = attrs.isReg - def is_dir: Boolean = attrs.isDir - } - - class Sftp private[SSH](session: Session, kind: String, channel: ChannelSftp) - extends Channel[ChannelSftp](session, kind, channel) - { - channel.connect(connect_timeout(session.options)) - - def home: String = channel.getHome() - - def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) } - def mv(remote_path1: String, remote_path2: String): Unit = - channel.rename(remote_path1, remote_path2) - def rm(remote_path: String) { channel.rm(remote_path) } - def mkdir(remote_path: String) { channel.mkdir(remote_path) } - def rmdir(remote_path: String) { channel.rmdir(remote_path) } - - def stat(remote_path: String): Dir_Entry = - Dir_Entry(remote_path, channel.stat(remote_path)) - - def read_dir(remote_path: String): List[Dir_Entry] = - { - val dir = channel.ls(remote_path) - (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, attrs)).toList - } - - def find_files(remote_path: String, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = - { - def find(dir: String): List[Dir_Entry] = - read_dir(dir).flatMap(entry => - { - val file = dir + "/" + entry.name - if (entry.is_dir) find(file) - else if (pred(entry)) List(entry.copy(name = file)) - else Nil - }) - find(remote_path) - } - - def open_input(remote_path: String): InputStream = channel.get(remote_path) - def open_output(remote_path: String): OutputStream = channel.put(remote_path) - - def read_file(remote_path: String, local_path: Path): Unit = - channel.get(remote_path, File.platform_path(local_path)) - def read_bytes(remote_path: String): Bytes = - using(open_input(remote_path))(Bytes.read_stream(_)) - def read(remote_path: String): String = - using(open_input(remote_path))(File.read_stream(_)) - - def write_file(remote_path: String, local_path: Path): Unit = - channel.put(File.platform_path(local_path), remote_path) - def write_bytes(remote_path: String, bytes: Bytes): Unit = - using(open_output(remote_path))(bytes.write_stream(_)) - def write(remote_path: String, text: String): Unit = - using(open_output(remote_path))(stream => Bytes(text).write_stream(stream)) - } - - /* session */ class Session private[SSH](val options: Options, val session: JSch_Session) @@ -278,20 +278,6 @@ def close() { session.disconnect } - def execute(command: String, - progress_stdout: String => Unit = (_: String) => (), - progress_stderr: String => Unit = (_: String) => (), - strict: Boolean = true): Process_Result = - exec(command).result(progress_stdout, progress_stderr, strict) - - def exec(command: String): Exec = - { - val kind = "exec" - val channel = session.openChannel(kind).asInstanceOf[ChannelExec] - channel.setCommand(command) - new Exec(this, kind, channel) - } - def sftp(): Sftp = { val kind = "sftp" @@ -299,6 +285,20 @@ new Sftp(this, kind, channel) } + def exec(command: String): Exec = + { + val kind = "exec" + val channel = session.openChannel(kind).asInstanceOf[ChannelExec] + channel.setCommand("export USER_HOME=\"$HOME\"\n" + command) + new Exec(this, kind, channel) + } + + def execute(command: String, + progress_stdout: String => Unit = (_: String) => (), + progress_stderr: String => Unit = (_: String) => (), + strict: Boolean = true): Process_Result = + exec(command).result(progress_stdout, progress_stderr, strict) + /* tmp dirs */ diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri Oct 14 22:45:29 2016 +0200 @@ -173,7 +173,7 @@ } - /* mkdirs */ + /* directories */ def mkdirs(path: Path): Unit = if (!path.is_dir) { @@ -181,6 +181,9 @@ if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } + def copy_dir(dir1: Path, dir2: Path): Unit = + bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check + /* tmp files */ @@ -208,6 +211,8 @@ /* tmp dirs */ + def rm_tree(root: Path): Unit = rm_tree(root.file) + def rm_tree(root: JFile) { root.delete diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/System/options.scala Fri Oct 14 22:45:29 2016 +0200 @@ -124,6 +124,9 @@ } } + def load(file: Path): Options = + Parser.parse_file(options_syntax, Parser.option_entry, empty, file) + def init_defaults(): Options = { var options = empty @@ -197,7 +200,7 @@ val options: Map[String, Options.Opt] = Map.empty, val section: String = "") { - override def toString: String = options.iterator.mkString("Options (", ",", ")") + override def toString: String = options.iterator.mkString("Options(", ",", ")") private def print_opt(opt: Options.Opt): String = if (opt.public) "public " + opt.print else opt.print diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/System/progress.scala Fri Oct 14 22:45:29 2016 +0200 @@ -7,6 +7,9 @@ package isabelle +import java.io.{File => JFile} + + class Progress { def echo(msg: String) {} @@ -14,6 +17,17 @@ def theory(session: String, theory: String) {} def stopped: Boolean = false override def toString: String = if (stopped) "Progress(stopped)" else "Progress" + + def bash(script: String, + cwd: JFile = null, + env: Map[String, String] = Isabelle_System.settings(), + redirect: Boolean = false, + echo: Boolean = false): Process_Result = + { + Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, + progress_stdout = echo_if(echo, _), + progress_stderr = echo_if(echo, _)) + } } object Ignore_Progress extends Progress diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/build-jars --- a/src/Pure/build-jars Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/build-jars Fri Oct 14 22:45:29 2016 +0200 @@ -12,11 +12,13 @@ Admin/build_doc.scala Admin/build_history.scala Admin/build_log.scala + Admin/build_release.scala Admin/build_stats.scala Admin/check_sources.scala Admin/ci_api.scala Admin/ci_profile.scala Admin/isabelle_cronjob.scala + Admin/other_isabelle.scala Admin/remote_dmg.scala Concurrent/consumer_thread.scala Concurrent/counter.scala diff -r 4d1d2de432fa -r 89514fa139c9 src/Pure/library.scala --- a/src/Pure/library.scala Thu Oct 13 15:43:15 2016 +0200 +++ b/src/Pure/library.scala Fri Oct 14 22:45:29 2016 +0200 @@ -204,21 +204,21 @@ else if (xs.isEmpty) ys else ys.foldRight(xs)(Library.insert(_)(_)) - def distinct[A](xs: List[A]): List[A] = + def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] - xs.foreach(x => if (!result.contains(x)) result += x) + xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x) result.toList } - def duplicates[A](lst: List[A]): List[A] = + def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] @tailrec def dups(rest: List[A]): Unit = rest match { case Nil => case x :: xs => - if (!result.contains(x) && xs.contains(x)) result += x + if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x dups(xs) } dups(lst)