--- a/Admin/cronjob/plain_identify Fri Mar 02 15:14:59 2018 +0100
+++ b/Admin/cronjob/plain_identify Fri Mar 02 19:14:35 2018 +0100
@@ -10,7 +10,7 @@
LANG=C
REPOS_DIR="$HOME/cronjob/plain_identify_repos"
-ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle"
+ISABELLE_REPOS_SOURCE="https://isabelle.in.tum.de/repos/isabelle"
AFP_REPOS_SOURCE="https://bitbucket.org/isa-afp/afp-devel"
function setup_repos ()
--- a/Admin/cronjob/self_update Fri Mar 02 15:14:59 2018 +0100
+++ b/Admin/cronjob/self_update Fri Mar 02 19:14:35 2018 +0100
@@ -10,5 +10,5 @@
cd "$HOME/cronjob"
mkdir -p run log
-hg -R isabelle pull "http://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed"
+hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed"
hg -R isabelle update -C -q || echo "self_update update failed"
--- a/README_REPOSITORY Fri Mar 02 15:14:59 2018 +0100
+++ b/README_REPOSITORY Fri Mar 02 19:14:35 2018 +0100
@@ -12,7 +12,7 @@
2. Clone repository (bash shell commands):
- hg clone http://isabelle.in.tum.de/repos/isabelle
+ hg clone https://isabelle.in.tum.de/repos/isabelle
cd isabelle
@@ -86,7 +86,7 @@
The main Isabelle repository can be cloned like this:
- hg clone http://isabelle.in.tum.de/repos/isabelle
+ hg clone https://isabelle.in.tum.de/repos/isabelle
This will create a local directory "isabelle", unless an alternative
name is specified. The full repository meta-data and history of
@@ -128,7 +128,7 @@
Shared pull/push access
-----------------------
-The entry point http://isabelle.in.tum.de/repos/isabelle is world
+The entry point https://isabelle.in.tum.de/repos/isabelle is world
readable, both via plain web browsing and the hg client as described
above. Anybody can produce a clone, change it locally, and then use
regular mechanisms of Mercurial to report changes upstream, say via
@@ -273,7 +273,7 @@
Isabelle changesets can be more spontaneous, growing from the
bottom-up.
- The web style of http://isabelle.in.tum.de/repos/isabelle/
+ The web style of https://isabelle.in.tum.de/repos/isabelle
accommodates the Isabelle changelog format. Note that multiple
lines will sometimes display as a single paragraph in HTML, so
some terminating punctuation is required. Do not squeeze multiple
--- a/etc/options Fri Mar 02 15:14:59 2018 +0100
+++ b/etc/options Fri Mar 02 19:14:35 2018 +0100
@@ -256,3 +256,4 @@
option build_log_ssh_user : string = ""
option build_log_ssh_port : int = 0
option build_log_history : int = 30 -- "length of relevant history (in days)"
+option build_log_transaction_size : int = 1 -- "number of log files for each db update"
--- a/src/Doc/Implementation/ML.thy Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Mar 02 19:14:35 2018 +0100
@@ -23,7 +23,7 @@
explanations should help to understand how proper Isabelle/ML is to be read
and written, and to get access to the wealth of experience that is expressed
in the source text and its history of changes.\<^footnote>\<open>See
- \<^url>\<open>http://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history.
+ \<^url>\<open>https://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history.
There are symbolic tags to refer to official Isabelle releases, as opposed
to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never
really up-to-date.\<close>
--- a/src/Pure/Admin/build_history.scala Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Pure/Admin/build_history.scala Fri Mar 02 19:14:35 2018 +0100
@@ -504,7 +504,7 @@
ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
- isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
+ isabelle_repos_source: String = "https://isabelle.in.tum.de/repos/isabelle",
afp_repos_source: String = AFP.repos_source,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
--- a/src/Pure/Admin/build_log.scala Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Pure/Admin/build_log.scala Fri Mar 02 19:14:35 2018 +0100
@@ -1101,7 +1101,10 @@
}
})
- for (file_group <- files.filter(file => status.exists(_.required(file))).grouped(100)) {
+ for (file_group <-
+ files.filter(file => status.exists(_.required(file))).
+ grouped(options.int("build_log_transaction_size") max 1))
+ {
val log_files = Par_List.map[JFile, Log_File](Log_File.apply _, file_group)
db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) }
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Mar 02 19:14:35 2018 +0100
@@ -114,6 +114,10 @@
host: String,
user: String = "",
port: Int = 0,
+ ssh_host: String = "",
+ proxy_host: String = "",
+ proxy_user: String = "",
+ proxy_port: Int = 0,
shared_home: Boolean = true,
historic: Boolean = false,
history: Int = 0,
@@ -282,7 +286,9 @@
val task_name = "build_history-" + r.host
Logger_Task(task_name, logger =>
{
- using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
+ using(logger.ssh_context.open_session(
+ host = proper_string(r.ssh_host) getOrElse r.host, user = r.user, port = r.port,
+ proxy_host = r.proxy_host, proxy_user = r.proxy_user, proxy_port = r.proxy_port))(
ssh =>
{
val self_update = !r.shared_home
--- a/src/Pure/General/ssh.scala Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Pure/General/ssh.scala Fri Mar 02 19:14:35 2018 +0100
@@ -37,6 +37,7 @@
}
val default_port = 22
+ def make_port(port: Int): Int = if (port > 0) port else default_port
def connect_timeout(options: Options): Int =
options.seconds("ssh_connect_timeout").ms.toInt
@@ -73,32 +74,52 @@
new Context(options, jsch)
}
- def open_session(options: Options, host: String, user: String = "", port: Int = 0): Session =
- init_context(options).open_session(host = host, user = user, port = port)
+ def open_session(options: Options, host: String, user: String = "", port: Int = 0,
+ proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0): Session =
+ init_context(options).open_session(host = host, user = user, port = port,
+ proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port)
class Context private[SSH](val options: Options, val jsch: JSch)
{
def update_options(new_options: Options): Context = new Context(new_options, jsch)
- def open_session(host: String, user: String = "", port: Int = 0): Session =
+ def connect_session(host: String, user: String = "", port: Int = 0,
+ host_key_alias: String = "", on_close: () => Unit = () => ()): Session =
{
- val session =
- jsch.getSession(proper_string(user) getOrElse null, host,
- if (port > 0) port else default_port)
+ val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port))
session.setUserInfo(No_User_Info)
session.setServerAliveInterval(alive_interval(options))
session.setServerAliveCountMax(alive_count_max(options))
session.setConfig("MaxAuthTries", "3")
+ if (host_key_alias != "") session.setHostKeyAlias(host_key_alias)
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(connect_timeout(options))
+ new Session(options, session, on_close)
+ }
- session.connect(connect_timeout(options))
- new Session(options, session)
+ def open_session(host: String, user: String = "", port: Int = 0,
+ proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0): Session =
+ {
+ if (proxy_host == "") connect_session(host = host, user = user, port = port)
+ else {
+ val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user)
+
+ val fw =
+ try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) }
+ catch { case exn: Throwable => proxy.close; throw exn }
+
+ try {
+ connect_session(host = fw.local_host, port = fw.local_port, host_key_alias = host,
+ user = user, on_close = () => { fw.close; proxy.close })
+ }
+ catch { case exn: Throwable => fw.close; proxy.close; throw exn }
+ }
}
}
@@ -262,9 +283,13 @@
/* session */
- class Session private[SSH](val options: Options, val session: JSch_Session) extends System
+ class Session private[SSH](
+ val options: Options,
+ val session: JSch_Session,
+ on_close: () => Unit) extends System
{
- def update_options(new_options: Options): Session = new Session(new_options, session)
+ def update_options(new_options: Options): Session =
+ new Session(new_options, session, on_close)
def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
def host: String = if (session.getHost == null) "" else session.getHost
@@ -292,7 +317,7 @@
val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
sftp.connect(connect_timeout(options))
- def close() { sftp.disconnect; session.disconnect }
+ def close() { sftp.disconnect; session.disconnect; on_close() }
val settings: Map[String, String] =
{
--- a/src/Tools/VSCode/extension/README.md Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Tools/VSCode/extension/README.md Fri Mar 02 19:14:35 2018 +0100
@@ -8,7 +8,7 @@
See also:
- * <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
+ * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
* <https://github.com/Microsoft/language-server-protocol>
--- a/src/Tools/VSCode/extension/package.json Fri Mar 02 15:14:59 2018 +0100
+++ b/src/Tools/VSCode/extension/package.json Fri Mar 02 19:14:35 2018 +0100
@@ -14,7 +14,7 @@
"publisher": "makarius",
"license": "MIT",
"repository": {
- "url": "http://isabelle.in.tum.de/repos/isabelle"
+ "url": "https://isabelle.in.tum.de/repos/isabelle"
},
"engines": {
"vscode": "^1.8.0"