# HG changeset patch
# User wenzelm
# Date 1476188979 -7200
# Node ID b2486964b823319630b6dcd6640867b5a9e9ae02
# Parent 74fde524799e46d6eeb0df6eac002ea41d6bb74c# Parent 69d5509768a9082c14025aac6cd6c703f9d6c8c2
merged
diff -r 74fde524799e -r b2486964b823 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST Mon Oct 10 15:45:41 2016 +0100
+++ b/Admin/Release/CHECKLIST Tue Oct 11 14:29:39 2016 +0200
@@ -76,9 +76,9 @@
- Linux: avoid some versions of Debian / Ubuntu (bitmap fonts for prog-prove);
-- fully-automated packaging:
+- fully-automated packaging (e.g. on macbroy2):
- hg up -r DISTNAME && Admin/Release/build -O -l -r DISTNAME /home/isabelle/dist
+ hg up -r DISTNAME && Admin/Release/build -M macbroy30 -O -l -r DISTNAME /home/isabelle/dist
Final release stage
diff -r 74fde524799e -r b2486964b823 Admin/Release/build
--- a/Admin/Release/build Mon Oct 10 15:45:41 2016 +0100
+++ b/Admin/Release/build Tue Oct 11 14:29:39 2016 +0200
@@ -18,6 +18,7 @@
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"
@@ -47,14 +48,18 @@
# options
+REMOTE_MAC=""
OFFICIAL_RELEASE=""
JOBS=""
LIBRARY=""
RELEASE=""
-while getopts "Oj:lr:" OPT
+while getopts "M:Oj:lr:" OPT
do
case "$OPT" in
+ M)
+ REMOTE_MAC="$OPTARG"
+ ;;
O)
OFFICIAL_RELEASE="-O"
;;
@@ -121,7 +126,11 @@
echo
echo "*** $PLATFORM_FAMILY ***"
-"$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$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
@@ -155,4 +164,3 @@
if [ -n "$LIBRARY" ]; then
"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
fi
-
diff -r 74fde524799e -r b2486964b823 Admin/components/components.sha1
--- a/Admin/components/components.sha1 Mon Oct 10 15:45:41 2016 +0100
+++ b/Admin/components/components.sha1 Tue Oct 11 14:29:39 2016 +0200
@@ -153,6 +153,7 @@
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
+2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz
601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz
14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz
diff -r 74fde524799e -r b2486964b823 Admin/components/main
--- a/Admin/components/main Mon Oct 10 15:45:41 2016 +0100
+++ b/Admin/components/main Tue Oct 11 14:29:39 2016 +0200
@@ -12,6 +12,7 @@
kodkodi-1.5.2
polyml-5.6-1
scala-2.11.8
+ssh-java-20161009
spass-3.8ds
sqlite-jdbc-3.8.11.2
xz-java-1.5
diff -r 74fde524799e -r b2486964b823 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle Mon Oct 10 15:45:41 2016 +0100
+++ b/Admin/lib/Tools/makedist_bundle Tue Oct 11 14:29:39 2016 +0200
@@ -9,11 +9,13 @@
function usage()
{
echo
- echo "Usage: isabelle $PRG ARCHIVE PLATFORM_FAMILY"
+ echo "Usage: isabelle $PRG ARCHIVE PLATFORM_FAMILY [REMOTE_MAC]"
echo
echo " Re-package Isabelle source distribution with add-on components and"
echo " post-hoc patches for platform family linux, windows, windows64, macos."
echo
+ echo " The optional remote Mac OS X system is used for dmg build."
+ echo
echo " Add-on components are that of the running Isabelle version!"
echo
exit 1
@@ -28,10 +30,11 @@
## arguments
-[ "$#" -ne 2 ] && usage
+[ "$#" -ne 2 -a "$#" -ne 3 ] && usage
ARCHIVE="$1"; shift
PLATFORM_FAMILY="$1"; shift
+REMOTE_MAC="$1"; shift
if [ "$PLATFORM_FAMILY" = windows64 ]; then
PLATFORM_FAM="windows"
@@ -84,8 +87,6 @@
# bundled components
-init_component "$JEDIT_HOME"
-
if [ ! -e "$ARCHIVE_DIR/contrib" ]; then
if [ ! -e "$ARCHIVE_DIR/../contrib" ]; then
mkdir -p "$ARCHIVE_DIR/contrib"
@@ -201,6 +202,8 @@
for PLATFORM in 32 64
do
(
+ init_component "$JEDIT_HOME"
+
echo "# Java runtime options for ${PLATFORM}bit platform"
declare -a JAVA_ARGS
if [ "$PLATFORM" = 32 ]; then
@@ -268,6 +271,8 @@
"$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
(
+ init_component "$JEDIT_HOME"
+
declare -a JAVA_ARGS=()
if [ "$PLATFORM_FAMILY" = windows ]; then
echo -e "# Java runtime options for 32bit platform\r"
@@ -355,97 +360,99 @@
# platform-specific setup (outside archive)
-if [ "$ISABELLE_PLATFORM_FAMILY" = linux -a "$PLATFORM_FAMILY" != macos -o "$ISABELLE_PLATFORM_FAMILY" = macos ]
-then
- case "$PLATFORM_FAM" in
- linux)
- echo "application for $PLATFORM_FAMILY"
- ln -s "${ISABELLE_NAME}_linux.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}_app.tar.gz"
- ;;
- macos)
+case "$PLATFORM_FAM" in
+ linux)
+ echo "application for $PLATFORM_FAMILY"
+ ln -s "${ISABELLE_NAME}_linux.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}_app.tar.gz"
+ ;;
+ macos)
+ echo "application for $PLATFORM_FAMILY"
+ (
+ cd "$TMP"
+
+ APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
+ APP="dmg/${ISABELLE_NAME}.app"
+
+ mkdir -p "dmg/.background"
+ cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/"
+ cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store"
+ ln -s /Applications "dmg/."
+
+ for NAME in Java MacOS PlugIns Resources
+ do
+ mkdir -p "$APP/Contents/$NAME"
+ done
+
+ (
+ init_component "$JEDIT_HOME"
+
+ cat "$APP_TEMPLATE/Info.plist-part1"
+
+ declare -a OPTIONS=()
+ eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS64)"
+ for OPT in "${OPTIONS[@]}"
+ do
+ echo "$OPT"
+ done
+ echo "-Disabelle.jedit_server={ISABELLE_NAME}"
+ echo "-Dapple.awt.application.name={ISABELLE_NAME}"
+
+ cat "$APP_TEMPLATE/Info.plist-part2"
+ ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
+
+ for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+ do
+ ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java"
+ done
+
+ cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
+
+ ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \
+ "$APP/Contents/PlugIns/bundled.jdk"
+
+ cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \
+ chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
+
+ mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
+ ln -sf "../../Info.plist" "$APP/Contents/Resources/$ISABELLE_NAME/${ISABELLE_NAME}.plist"
+ ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
+
+ rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+ tar -C dmg -czf "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" .
+
+ if [ -n "$REMOTE_MAC" ]
+ then
+ echo "$REMOTE_MAC: dmg for $PLATFORM_FAMILY"
+ isabelle remote_dmg -V Isabelle "$REMOTE_MAC" \
+ "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+ fi
+ )
+ ;;
+ windows)
+ (
+ if [ "$PLATFORM_FAMILY" = windows ]; then
+ PLATFORM_SUFFIX="-win32"
+ else
+ PLATFORM_SUFFIX="-win64"
+ fi
+
+ cd "$TMP"
+ rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.7z"
+ 7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME" || exit 2
+
echo "application for $PLATFORM_FAMILY"
(
- cd "$TMP"
-
- APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
- APP="dmg/${ISABELLE_NAME}.app"
-
- mkdir -p "dmg/.background"
- cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/"
- cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store"
- ln -s /Applications "dmg/."
-
- for NAME in Java MacOS PlugIns Resources
- do
- mkdir -p "$APP/Contents/$NAME"
- done
-
- (
- cat "$APP_TEMPLATE/Info.plist-part1"
-
- declare -a OPTIONS=()
- eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS64)"
- for OPT in "${OPTIONS[@]}"
- do
- echo "$OPT"
- done
- echo "-Disabelle.jedit_server={ISABELLE_NAME}"
- echo "-Dapple.awt.application.name={ISABELLE_NAME}"
-
- cat "$APP_TEMPLATE/Info.plist-part2"
- ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
-
- for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
- do
- ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java"
- done
-
- cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
-
- ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \
- "$APP/Contents/PlugIns/bundled.jdk"
-
- cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \
- chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
-
- mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
- ln -sf "../../Info.plist" "$APP/Contents/Resources/$ISABELLE_NAME/${ISABELLE_NAME}.plist"
- ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
-
- rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
-
- cd dmg
- hdiutil create -srcfolder . -volname Isabelle "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
- )
- ;;
- windows)
- (
- if [ "$PLATFORM_FAMILY" = windows ]; then
- PLATFORM_SUFFIX="-win32"
- else
- PLATFORM_SUFFIX="-win64"
- fi
-
- cd "$TMP"
- rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.7z"
- 7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME" || exit 2
-
- echo "application for $PLATFORM_FAMILY"
- (
- cat "windows_app/7zsd_All.sfx"
- cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \
- perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;"
- cat "$TMP/${ISABELLE_NAME}.7z"
- ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}${PLATFORM_SUFFIX}.exe"
- chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}${PLATFORM_SUFFIX}.exe"
- )
- ;;
- *)
- ;;
- esac
-else
- echo "### Cannot build application for $PLATFORM_FAMILY on $ISABELLE_PLATFORM_FAMILY"
-fi
+ cat "windows_app/7zsd_All.sfx"
+ cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \
+ perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;"
+ cat "$TMP/${ISABELLE_NAME}.7z"
+ ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}${PLATFORM_SUFFIX}.exe"
+ chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}${PLATFORM_SUFFIX}.exe"
+ )
+ ;;
+ *)
+ ;;
+esac
# clean up
diff -r 74fde524799e -r b2486964b823 etc/options
--- a/etc/options Mon Oct 10 15:45:41 2016 +0100
+++ b/etc/options Tue Oct 11 14:29:39 2016 +0200
@@ -185,3 +185,21 @@
public option completion_limit : int = 40
-- "limit for completion within the formal context"
+
+
+section "Secure Shell"
+
+option ssh_config_dir : string = "~/.ssh"
+ -- "SSH configuration directory"
+
+option ssh_config_file : string = "~/.ssh/config"
+ -- "main SSH configuration file"
+
+option ssh_identity_files : string = "~/.ssh/id_dsa:~/.ssh/id_ecdsa:~/.ssh/id_rsa"
+ -- "possible SSH identity files (separated by colons)"
+
+option ssh_compression : bool = true
+ -- "enable SSH compression"
+
+option ssh_connect_timeout : real = 60
+ -- "SSH connection timeout (seconds)"
diff -r 74fde524799e -r b2486964b823 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/General/mercurial.scala Tue Oct 11 14:29:39 2016 +0200
@@ -47,7 +47,7 @@
command("manifest " + options + opt_rev(rev)).check.out_lines
def log(rev: String = "", template: String = "", options: String = ""): String =
- Library.trim_line(command("log " + options + opt_rev(rev) + opt_template(template)).check.out)
+ command("log " + options + opt_rev(rev) + opt_template(template)).check.out
def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
command("pull " + options + opt_rev(rev) + optional(remote)).check
diff -r 74fde524799e -r b2486964b823 src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/General/sqlite.scala Tue Oct 11 14:29:39 2016 +0200
@@ -27,7 +27,7 @@
{
override def toString: String = path.toString
- def close { connection.close }
+ def close() { connection.close }
def rebuild { using(statement("VACUUM"))(_.execute()) }
diff -r 74fde524799e -r b2486964b823 src/Pure/General/ssh.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/ssh.scala Tue Oct 11 14:29:39 2016 +0200
@@ -0,0 +1,338 @@
+/* Title: Pure/General/ssh.scala
+ Author: Makarius
+
+SSH client based on JSch (see also http://www.jcraft.com/jsch/examples).
+*/
+
+package isabelle
+
+
+import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
+
+import scala.collection.{mutable, JavaConversions}
+
+import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session,
+ OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
+
+
+object SSH
+{
+ /* user@host syntax */
+
+ object User_Host
+ {
+ val Pattern = "^([^@]+)@(.+)$".r
+
+ def parse(s: String): (String, String) =
+ s match {
+ case Pattern(user, host) => (user, host)
+ case _ => ("", s)
+ }
+
+ def unapplySeq(s: String): Option[List[String]] =
+ {
+ val (user, host) = parse(s)
+ Some(List(user, host))
+ }
+ }
+
+ val default_port = 22
+
+
+ /* init */
+
+ def init(options: Options): SSH =
+ {
+ val config_dir = Path.explode(options.string("ssh_config_dir"))
+ if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
+
+ val jsch = new JSch
+
+ val config_file = Path.explode(options.string("ssh_config_file"))
+ if (config_file.is_file)
+ jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
+
+ val known_hosts = config_dir + Path.explode("known_hosts")
+ if (!known_hosts.is_file) known_hosts.file.createNewFile
+ jsch.setKnownHosts(File.platform_path(known_hosts))
+
+ val identity_files =
+ Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
+ for (identity_file <- identity_files if identity_file.is_file)
+ jsch.addIdentity(File.platform_path(identity_file))
+
+ new SSH(options, jsch)
+ }
+
+ def connect_timeout(options: Options): Int =
+ options.seconds("ssh_connect_timeout").ms.toInt
+
+
+ /* logging */
+
+ def logging(verbose: Boolean = true, debug: Boolean = false)
+ {
+ JSch.setLogger(if (verbose) new Logger(debug) else null)
+ }
+
+ private class Logger(debug: Boolean) extends JSch_Logger
+ {
+ def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
+
+ def log(level: Int, msg: String)
+ {
+ level match {
+ case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
+ case JSch_Logger.WARN => Output.warning(msg)
+ case _ => Output.writeln(msg)
+ }
+ }
+ }
+
+
+ /* user info */
+
+ object No_User_Info extends UserInfo
+ {
+ def getPassphrase: String = null
+ def getPassword: String = null
+ def promptPassword(msg: String): Boolean = false
+ def promptPassphrase(msg: String): Boolean = false
+ def promptYesNo(msg: String): Boolean = false
+ def showMessage(msg: String): Unit = Output.writeln(msg)
+ }
+
+
+ /* channel */
+
+ class Channel[C <: JSch_Channel] private[SSH](
+ val session: Session, val kind: String, val options: Options, val channel: C)
+ {
+ override def toString: String = kind + " " + session.toString
+
+ def close() { channel.disconnect }
+ }
+
+
+ /* exec channel */
+
+ private val exec_wait_delay = Time.seconds(0.3)
+
+ class Exec private[SSH](
+ session: Session, kind: String, options: Options, channel: ChannelExec)
+ extends Channel[ChannelExec](session, kind, options, channel)
+ {
+ def kill(signal: String) { channel.sendSignal(signal) }
+
+ val exit_status: Future[Int] =
+ Future.thread("ssh_wait") {
+ while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)
+ channel.getExitStatus
+ }
+
+ val stdin: OutputStream = channel.getOutputStream
+ val stdout: InputStream = channel.getInputStream
+ val stderr: InputStream = channel.getErrStream
+
+ // after preparing streams
+ channel.connect(connect_timeout(options))
+
+ def result(
+ progress_stdout: String => Unit = (_: String) => (),
+ progress_stderr: String => Unit = (_: String) => (),
+ strict: Boolean = true): Process_Result =
+ {
+ stdin.close
+
+ def read_lines(stream: InputStream, progress: String => Unit): List[String] =
+ {
+ val result = new mutable.ListBuffer[String]
+ val line_buffer = new ByteArrayOutputStream(100)
+ def line_flush()
+ {
+ val line = line_buffer.toString(UTF8.charset_name)
+ progress(line)
+ result += line
+ line_buffer.reset
+ }
+
+ var c = 0
+ var finished = false
+ while (!finished) {
+ while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
+ if (c == 10) line_flush()
+ else if (channel.isClosed) {
+ if (line_buffer.size > 0) line_flush()
+ finished = true
+ }
+ else Thread.sleep(exec_wait_delay.ms)
+ }
+
+ result.toList
+ }
+
+ val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
+ val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
+
+ def terminate()
+ {
+ close
+ out_lines.join
+ err_lines.join
+ exit_status.join
+ }
+
+ val rc =
+ try { exit_status.join }
+ catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+
+ close
+ if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+
+ Process_Result(rc, out_lines.join, err_lines.join)
+ }
+ }
+
+
+ /* 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, options: Options, channel: ChannelSftp)
+ extends Channel[ChannelSftp](session, kind, options, channel)
+ {
+ channel.connect(connect_timeout(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 session_options: Options, val session: JSch_Session)
+ {
+ override def toString: String =
+ (if (session.getUserName == null) "" else session.getUserName + "@") +
+ (if (session.getHost == null) "" else session.getHost) +
+ (if (session.getPort == default_port) "" else ":" + session.getPort) +
+ (if (session.isConnected) "" else " (disconnected)")
+
+ def close() { session.disconnect }
+
+ def execute(command: String,
+ options: Options = session_options,
+ progress_stdout: String => Unit = (_: String) => (),
+ progress_stderr: String => Unit = (_: String) => (),
+ strict: Boolean = true): Process_Result =
+ exec(command, options).result(progress_stdout, progress_stderr, strict)
+
+ def exec(command: String, options: Options = session_options): Exec =
+ {
+ val kind = "exec"
+ val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
+ channel.setCommand(command)
+ new Exec(this, kind, options, channel)
+ }
+
+ def sftp(options: Options = session_options): Sftp =
+ {
+ val kind = "sftp"
+ val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
+ new Sftp(this, kind, options, channel)
+ }
+
+
+ /* tmp dirs */
+
+ def rm_tree(remote_dir: String): Unit =
+ execute("rm -r -f " + File.bash_string(remote_dir)).check
+
+ def tmp_dir(): String =
+ execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
+
+ def with_tmp_dir[A](body: String => A): A =
+ {
+ val remote_dir = tmp_dir()
+ try { body(remote_dir) } finally { rm_tree(remote_dir) }
+ }
+ }
+}
+
+class SSH private(val options: Options, val jsch: JSch)
+{
+ def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session =
+ {
+ val session = jsch.getSession(if (user == "") null else user, host, port)
+
+ session.setUserInfo(SSH.No_User_Info)
+ session.setConfig("MaxAuthTries", "3")
+
+ if (options.bool("ssh_compression")) {
+ session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
+ session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
+ session.setConfig("compression_level", "9")
+ }
+
+ session.connect(SSH.connect_timeout(options))
+ new SSH.Session(options, session)
+ }
+}
diff -r 74fde524799e -r b2486964b823 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Oct 11 14:29:39 2016 +0200
@@ -309,6 +309,8 @@
result(progress_stdout, progress_stderr, progress_limit, strict)
}
+ def hostname(): String = bash("hostname").check.out
+
def open(arg: String): Unit =
bash("exec \"$ISABELLE_OPEN\" " + File.bash_string(arg) + " >/dev/null 2>/dev/null &")
diff -r 74fde524799e -r b2486964b823 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/System/isabelle_tool.scala Tue Oct 11 14:29:39 2016 +0200
@@ -106,6 +106,7 @@
Doc.isabelle_tool,
ML_Process.isabelle_tool,
Options.isabelle_tool,
+ Remote_DMG.isabelle_tool,
Update_Cartouches.isabelle_tool,
Update_Header.isabelle_tool,
Update_Then.isabelle_tool,
diff -r 74fde524799e -r b2486964b823 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/System/process_result.scala Tue Oct 11 14:29:39 2016 +0200
@@ -29,15 +29,15 @@
def print: Process_Result =
{
- Output.warning(Library.trim_line(err))
- Output.writeln(Library.trim_line(out))
+ Output.warning(err)
+ Output.writeln(out)
copy(out_lines = Nil, err_lines = Nil)
}
def print_stdout: Process_Result =
{
- Output.warning(Library.trim_line(err), stdout = true)
- Output.writeln(Library.trim_line(out), stdout = true)
+ Output.warning(err, stdout = true)
+ Output.writeln(out, stdout = true)
copy(out_lines = Nil, err_lines = Nil)
}
diff -r 74fde524799e -r b2486964b823 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/Tools/build.scala Tue Oct 11 14:29:39 2016 +0200
@@ -752,15 +752,15 @@
val progress = new Console_Progress(verbose = verbose)
+ val start_date = Date.now()
+
if (verbose) {
progress.echo(
- Library.trim_line(
- Isabelle_System.bash(
- """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
+ "Started at " + Build_Log.Log_File.Date_Format(start_date) +
+ " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
progress.echo(Build_Log.Settings.show() + "\n")
}
- val start_time = Time.now()
val results =
progress.interrupt_handler {
build(options, progress,
@@ -781,12 +781,11 @@
session_groups = session_groups,
sessions = sessions)
}
- val elapsed_time = Time.now() - start_time
+ val end_date = Date.now()
+ val elapsed_time = end_date.time - start_date.time
if (verbose) {
- progress.echo("\n" +
- Library.trim_line(
- Isabelle_System.bash("""echo -n "Finished at "; date""").out))
+ progress.echo("\nFinished at " + Build_Log.Log_File.Date_Format(end_date))
}
val total_timing =
diff -r 74fde524799e -r b2486964b823 src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/Tools/build_history.scala Tue Oct 11 14:29:39 2016 +0200
@@ -217,7 +217,7 @@
/* main */
val build_history_date = Date.now()
- val build_host = Library.trim_line(Isabelle_System.bash("hostname").check.out)
+ val build_host = Isabelle_System.hostname()
var first_build = true
for (threads <- threads_list) yield
diff -r 74fde524799e -r b2486964b823 src/Pure/Tools/remote_dmg.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/remote_dmg.scala Tue Oct 11 14:29:39 2016 +0200
@@ -0,0 +1,64 @@
+/* Title: Pure/Tools/remote_dmg.scala
+ Author: Makarius
+
+Build dmg on remote Mac OS X system.
+*/
+
+package isabelle
+
+
+object Remote_DMG
+{
+ def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
+ {
+ session.with_tmp_dir(remote_dir =>
+ using(session.sftp())(sftp =>
+ {
+ val cd = "cd " + File.bash_string(remote_dir) + "; "
+
+ sftp.write_file(remote_dir + "/dmg.tar.gz", tar_gz_file)
+ session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
+ session.execute(
+ cd + "hdiutil create -srcfolder root" +
+ (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
+ " dmg.dmg").check
+ sftp.read_file(remote_dir + "/dmg.dmg", dmg_file)
+ }))
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool = Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
+ {
+ Command_Line.tool0 {
+ var port = SSH.default_port
+ var volume_name = ""
+
+ val getopts = Getopts("""
+Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
+
+ Options are:
+ -p PORT alternative SSH port (default: """ + SSH.default_port + """)
+ -V NAME specify volume name
+
+ Turn the contents of a tar.gz file into a dmg file -- produced on a remote
+ Mac OS X system.
+""",
+ "p:" -> (arg => port = Value.Int.parse(arg)),
+ "V:" -> (arg => volume_name = arg))
+
+ 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) =>
+ (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
+ case _ => getopts.usage()
+ }
+
+ val ssh = SSH.init(Options.init)
+ using(ssh.open_session(user = user, host = host, port = port))(
+ remote_dmg(_, tar_gz_file, dmg_file, volume_name))
+ }
+ })
+}
diff -r 74fde524799e -r b2486964b823 src/Pure/build-jars
--- a/src/Pure/build-jars Mon Oct 10 15:45:41 2016 +0100
+++ b/src/Pure/build-jars Tue Oct 11 14:29:39 2016 +0200
@@ -48,6 +48,7 @@
General/sha1.scala
General/sql.scala
General/sqlite.scala
+ General/ssh.scala
General/symbol.scala
General/time.scala
General/timing.scala
@@ -123,6 +124,7 @@
Tools/ml_statistics.scala
Tools/news.scala
Tools/print_operation.scala
+ Tools/remote_dmg.scala
Tools/simplifier_trace.scala
Tools/task_statistics.scala
Tools/update_cartouches.scala