--- 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
-----------------------------
--- 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)
--------------------------------
--- 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;
--- 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,
--- 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 =
--- 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)
--- 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:
- * <https://isabelle.in.tum.de/website-Isabelle2020>
- * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2020/src/Tools/VSCode>
+ * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
* <https://github.com/Microsoft/language-server-protocol>
@@ -59,8 +58,8 @@
### Isabelle/VSCode Installation
- * Download Isabelle2020 from <https://isabelle.in.tum.de/website-Isabelle2020>
- or any of its mirror sites.
+ * Download a recent Isabelle development snapshot from
+ <https://isabelle.in.tum.de/devel/release_snapshot>
* 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
--- 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",