# HG changeset patch # User wenzelm # Date 1520014475 -3600 # Node ID 7b84ecd54d7070d93e0718ae88d67e69ca7a675d # Parent 6306bd5829576d2b862181d4b175191d1f647211# Parent cb0f0f5f88764c035332506d73aa5603e8be1553 merged diff -r 6306bd582957 -r 7b84ecd54d70 Admin/cronjob/plain_identify --- 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 () diff -r 6306bd582957 -r 7b84ecd54d70 Admin/cronjob/self_update --- 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" diff -r 6306bd582957 -r 7b84ecd54d70 README_REPOSITORY --- 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 diff -r 6306bd582957 -r 7b84ecd54d70 etc/options --- 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" diff -r 6306bd582957 -r 7b84ecd54d70 src/Doc/Implementation/ML.thy --- 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>\See - \<^url>\http://isabelle.in.tum.de/repos/isabelle\ for the full Mercurial history. + \<^url>\https://isabelle.in.tum.de/repos/isabelle\ for the full Mercurial history. There are symbolic tags to refer to official Isabelle releases, as opposed to arbitrary \<^emph>\tip\ versions that merely reflect snapshots that are never really up-to-date.\ diff -r 6306bd582957 -r 7b84ecd54d70 src/Pure/Admin/build_history.scala --- 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, diff -r 6306bd582957 -r 7b84ecd54d70 src/Pure/Admin/build_log.scala --- 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))) } } diff -r 6306bd582957 -r 7b84ecd54d70 src/Pure/Admin/isabelle_cronjob.scala --- 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 diff -r 6306bd582957 -r 7b84ecd54d70 src/Pure/General/ssh.scala --- 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] = { diff -r 6306bd582957 -r 7b84ecd54d70 src/Tools/VSCode/extension/README.md --- 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: - * + * * diff -r 6306bd582957 -r 7b84ecd54d70 src/Tools/VSCode/extension/package.json --- 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"