[isabelle-dev] NEWS: SSH and Mercurial support in Isabelle/Scala

Makarius makarius at sketis.net
Mon Oct 17 20:11:49 CEST 2016


*** System ***

* Isabelle/Scala: the SSH module supports ssh and sftp connections, for
remote command-execution and file-system access. This resembles
operations from module File and Isabelle_System to some extent. Note
that Path specifications need to be resolved remotely via
ssh.remote_path instead of File.standard_path: the implicit process
environment is different, Isabelle settings are not available remotely.

* Isabelle/Scala: the Mercurial module supports repositories via the
regular hg command-line interface. The repositroy clone and working
directory may reside on a local or remote file-system (via ssh
connection).


This refers to Isabelle/7ad033e28dbd.

The SSH support for the JVM platform is provided by
http://www.jcraft.com/jsch (which is also used by jEdit in its FTP and
SshConsole plugins). The jsch website looks outdated on first sight, but
that seems to be still the canonical Java library for SSH clients. It is
rather small and nice, precisely to the point of its task to connect to
SSH servers.

Having SSH in Isabelle/Scala opens a whole new world of cloud- and
cluster computing in the foreseeable future. E.g. there could be a
remote Isabelle/PIDE server offering some kind of "display protocol" on
localhost, which is tunneled over SSH: a local Isabelle/PIDE client can
connect to that in a secure fashion.

Right now, there is only plain command-execution and sftp file-system
access. It is used for various administrative tools, e.g. to produce a
.dmg on a well-defined remote Mac, when building a release on a
different machine (Linux or other Mac).


The Mercurial support is plain and simple, using hg command-line
execution. The lack for a proper JVM-library for Mercurial actually
turned out as an advantage, because the local vs. remote version (via
ssh) is now trivial. When that approach of command-line execution
reaches its limits, it should be easy to switch to the built-in
Mercurial "command server"
(https://www.mercurial-scm.org/wiki/CommandServer).


	Makarius


More information about the isabelle-dev mailing list