--- 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
--- 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" <<EOF
-<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
-<html>
-<head>
-<title>${DISTNAME}</title>
-</head>
-
-<body>
-<h1>${DISTNAME}</h1>
-<ul>
-<li><a href="${DISTNAME}_app.tar.gz">Linux</a></li>
-<li><a href="${DISTNAME}-win32.exe">Windows</a></li>
-<li><a href="${DISTNAME}-win64.exe">Windows (64bit)</a></li>
-<li><a href="${DISTNAME}.dmg">Mac OS X</a></li>
-</ul>
-</body>
-
-</html>
-EOF
-
-
-# HTML library
-
-if [ -n "$LIBRARY" ]; then
- "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
-fi
--- 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 "$@"
--- /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 "$@"
--- /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"
--- 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 "$@"
--- 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
--- 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)
}
}
--- 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 */
--- /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"),
+"""<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
+<html>
+<head>
+<title>""" + HTML.output(release_info.name) + """</title>
+</head>
+
+<body>
+<h1>""" + HTML.output(release_info.name) + """</h1>
+<ul>
+""" +
+ cat_lines(website_platform_bundles.map({ case (a, b) =>
+ "<li><a href=" + quote(HTML.output(b)) + ">" + HTML.output(Word.capitalize(a)) + "</a></li>" })) +
+"""
+</ul>
+</body>
+
+</html>
+""")
+ 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)
+ }
+ }
+}
--- 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")
}
}
--- /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))
+ }
+}
--- 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()
}
--- 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)
}
--- 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 = "")
{
--- 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 */
--- 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
--- 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
--- 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
--- 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
--- 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)