# HG changeset patch # User wenzelm # Date 1584825141 -3600 # Node ID f2c1154e9c8dfa143f0e17a6e18e299b02a02593 # Parent e9f53182c4aa2c0cbdd815ef5c707a636d4d02f6# Parent 24b68a932f26f71188dbc6b524f6118b923ad92a merged; diff -r e9f53182c4aa -r f2c1154e9c8d CONTRIBUTORS --- a/CONTRIBUTORS Sat Mar 21 21:41:13 2020 +0100 +++ b/CONTRIBUTORS Sat Mar 21 22:12:21 2020 +0100 @@ -3,6 +3,10 @@ listed as an author in one of the source files of this Isabelle distribution. +Contributions to this Isabelle version +-------------------------------------- + + Contributions to Isabelle2020 ----------------------------- diff -r e9f53182c4aa -r f2c1154e9c8d NEWS --- a/NEWS Sat Mar 21 21:41:13 2020 +0100 +++ b/NEWS Sat Mar 21 22:12:21 2020 +0100 @@ -4,6 +4,11 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) +New in this Isabelle version +---------------------------- + + + New in Isabelle2020 (April 2020) -------------------------------- diff -r e9f53182c4aa -r f2c1154e9c8d src/HOL/Tools/BNF/bnf_lift.ML --- a/src/HOL/Tools/BNF/bnf_lift.ML Sat Mar 21 21:41:13 2020 +0100 +++ b/src/HOL/Tools/BNF/bnf_lift.ML Sat Mar 21 22:12:21 2020 +0100 @@ -2012,14 +2012,10 @@ else bad_input [thm]) | NONE => (case Lifting_Info.lookup_quotients lthy absT_name of SOME {quot_thm = qthm, ...} => - let - val qthm = Thm.transfer' lthy qthm; - in - case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of - thm :: _ => (thm, Typedef) - | _ => (qthm RS @{thm Quotient_Quotient3}, - Quotient (find_equiv_thm_via_Quotient qthm)) - end + (case [qthm] RL @{thms Quotient_eq_onp_typedef Quotient_eq_onp_type_copy} of + thm :: _ => (thm, Typedef) + | _ => (qthm RS @{thm Quotient_Quotient3}, + Quotient (find_equiv_thm_via_Quotient qthm))) | NONE => (Typedef.get_info lthy absT_name |> hd |> snd |> #type_definition, Typedef)) | SOME thms => bad_input thms); val wits = (Option.map o map) (prepare_term lthy) raw_wits; diff -r e9f53182c4aa -r f2c1154e9c8d src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sat Mar 21 21:41:13 2020 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Mar 21 22:12:21 2020 +0100 @@ -147,9 +147,9 @@ sealed case class Remote_Build( description: String, host: String, + actual_host: String = "", user: String = "", port: Int = 0, - ssh_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, @@ -166,7 +166,7 @@ active: Boolean = true) { def ssh_session(context: SSH.Context): SSH.Session = - context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port, + context.open_session(host = host, user = user, port = port, actual_host = actual_host, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = proxy_host.nonEmpty) @@ -216,7 +216,6 @@ List( Remote_Build("AFP bulky", "lrzcloud1", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", - ssh_host = "10.155.208.96", options = "-m64 -M6 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, @@ -291,18 +290,18 @@ detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd")), List( - Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a", + Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start + " > date '2017-03-03'")), List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")), - List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", + List(Remote_Build("Mac OS X 10.13 High Sierra", "lapbroy68", options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true", self_update = true, args = "-a -d '~~/src/Benchmarks'")), - List(Remote_Build("macOS 10.14 Mojave", "lapnipkow3", + List(Remote_Build("Mac OS X 10.14 Mojave", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true", self_update = true, args = "-a -d '~~/src/Benchmarks'")), - List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", + List(Remote_Build("Mac OS X 10.15 Catalina", "laramac01", user = "makarius", proxy_host = "laraserver", proxy_user = "makarius", - self_update = true, options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true", + self_update = true, options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, @@ -339,9 +338,8 @@ val remote_builds2: List[List[Remote_Build]] = List( List( - Remote_Build("AFP2", "lrzcloud2", self_update = true, + Remote_Build("AFP2", "lrzcloud2", actual_host = "10.195.2.10", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", - ssh_host = "10.195.2.10", options = "-m32 -M1x8 -t AFP" + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton" + @@ -350,9 +348,8 @@ args = "-a -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), - Remote_Build("AFP bulky2", "lrzcloud2", self_update = true, + Remote_Build("AFP bulky2", "lrzcloud2", actual_host = "10.195.2.10", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", - ssh_host = "10.195.2.10", options = "-m64 -M8 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, diff -r e9f53182c4aa -r f2c1154e9c8d src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sat Mar 21 21:41:13 2020 +0100 +++ b/src/Pure/General/mercurial.scala Sat Mar 21 22:12:21 2020 +0100 @@ -82,7 +82,7 @@ val root: Path = ssh.expand_path(root_path) def root_url: String = ssh.hg_url + root.implode - override def toString: String = ssh.prefix + root.implode + override def toString: String = ssh.hg_url + root.implode def command(name: String, args: String = "", options: String = "", repository: Boolean = true): Process_Result = diff -r e9f53182c4aa -r f2c1154e9c8d src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Sat Mar 21 21:41:13 2020 +0100 +++ b/src/Pure/General/ssh.scala Sat Mar 21 22:12:21 2020 +0100 @@ -83,10 +83,12 @@ new Context(options, jsch) } - def open_session(options: Options, host: String, user: String = "", port: Int = 0, + def open_session(options: Options, + host: String, user: String = "", port: Int = 0, actual_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = - init_context(options).open_session(host = host, user = user, port = port, + init_context(options).open_session( + host = host, user = user, port = port, actual_host = actual_host, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = permissive) @@ -120,16 +122,18 @@ proper_string(nominal_user) getOrElse user) } - def open_session(host: String, user: String = "", port: Int = 0, + def open_session( + host: String, user: String = "", port: Int = 0, actual_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = { - if (proxy_host == "") connect_session(host = host, user = user, port = port) + val connect_host = proper_string(actual_host) getOrElse host + if (proxy_host == "") connect_session(host = connect_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)) } + try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) } catch { case exn: Throwable => proxy.close; throw exn } try { @@ -317,9 +321,6 @@ override def hg_url: String = "ssh://" + user_prefix(nominal_user) + nominal_host + "/" - override def prefix: String = - user_prefix(session.getUserName) + host + port_suffix(session.getPort) + ":" - override def toString: String = user_prefix(session.getUserName) + host + port_suffix(session.getPort) + (if (session.isConnected) "" else " (disconnected)") @@ -480,7 +481,6 @@ trait System { def hg_url: String = "" - def prefix: String = "" def expand_path(path: Path): Path = path.expand def bash_path(path: Path): String = File.bash_path(path) diff -r e9f53182c4aa -r f2c1154e9c8d src/Tools/VSCode/extension/README.md --- a/src/Tools/VSCode/extension/README.md Sat Mar 21 21:41:13 2020 +0100 +++ b/src/Tools/VSCode/extension/README.md Sat Mar 21 22:12:21 2020 +0100 @@ -1,15 +1,14 @@ # Isabelle Prover IDE support This extension connects VSCode to the Isabelle Prover IDE infrastructure: it -requires Isabelle2020. +requires a repository version of Isabelle. The implementation is centered around the VSCode Language Server protocol, but with many add-ons that are specific to VSCode and Isabelle/PIDE. See also: - * - * + * * @@ -59,8 +58,8 @@ ### Isabelle/VSCode Installation - * Download Isabelle2020 from - or any of its mirror sites. + * Download a recent Isabelle development snapshot from + * Unpack and run the main Isabelle/jEdit application as usual, to ensure that the logic image is built properly and Isabelle works as expected. @@ -69,7 +68,7 @@ * Open the VSCode *Extensions* view and install the following: - + *Isabelle2020* (needs to fit to the underlying Isabelle release). + + *Isabelle* (needs to fit to the underlying Isabelle release). + *Prettify Symbols Mode* (important for display of Isabelle symbols). @@ -90,17 +89,17 @@ + Linux: ``` - "isabelle.home": "/home/makarius/Isabelle2020" + "isabelle.home": "/home/makarius/Isabelle" ``` + Mac OS X: ``` - "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2020" + "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle" ``` + Windows: ``` - "isabelle.home": "C:\\Users\\makarius\\Isabelle2020" + "isabelle.home": "C:\\Users\\makarius\\Isabelle" ``` * Restart the VSCode application to ensure that all extensions are properly diff -r e9f53182c4aa -r f2c1154e9c8d src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Sat Mar 21 21:41:13 2020 +0100 +++ b/src/Tools/VSCode/extension/package.json Sat Mar 21 22:12:21 2020 +0100 @@ -1,6 +1,6 @@ { - "name": "Isabelle2020", - "displayName": "Isabelle2020", + "name": "Isabelle", + "displayName": "Isabelle", "description": "Isabelle Prover IDE", "keywords": [ "theorem prover",