1 Subject: Announcing Isabelle2019 |
1 Subject: Announcing Isabelle2020 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2019 is now available. |
4 Isabelle2020 is now available. |
5 |
5 |
6 This version introduces many changes over Isabelle2018: see the NEWS |
6 This version introduces many changes over Isabelle2019: see the NEWS |
7 file for further details. Here are some notable points: |
7 file for further details. Here are some notable points: |
8 |
8 |
9 * Improved "Isabelle DejaVu" font collection, suitable for text and GUI. |
9 * PIDE: much faster startup of Isabelle/jEdit thanks to more scalable |
|
10 session directory structure. |
10 |
11 |
11 * Various Isabelle/jEdit improvements, with virtual file-system access to |
12 * PIDE: updated Isabelle/VSCode to follow recent moves of VSCode. |
12 sessions and exports. |
|
13 |
13 |
14 * Improved headless PIDE session (and server). |
14 * Pure: improved treatment of theorem dependencies and proof terms, |
|
15 accessible via command 'thm_deps'. |
15 |
16 |
16 * HOL: 'export_code' now generates logical files in the theory and session |
17 * Pure: proper treatment of oracles within internal proof objects, |
17 context, e.g. browsable as "isabelle-export:" in Isabelle/jEdit. |
18 accessible via command 'thm_oracles'. |
18 |
19 |
19 * HOL: various syntax and library improvements. |
20 * HOL: various library improvements. |
20 |
21 |
21 * HOL libraries: better organization and much more material in HOL-Algebra, |
22 * HOL: better organization of HOL-Analysis vs. HOL-Complex_Analysis. |
22 HOL-Analysis, HOL-Homology. |
|
23 |
23 |
24 * Isabelle/ML environments for separate SML applications. |
24 * ML: more scalable export artifacts via XML blobs. |
25 |
25 |
26 * Isabelle/Haskell library for implementation of Isabelle/PIDE backends. |
26 * Scala: support for external IDEs based on Gradle (e.g. IntelliJ IDEA). |
27 |
27 |
28 * Installation management for Haskell (Stack) and OCaml (OPAM). |
28 * Scala: support for Ubuntu server applications (Linux-Apache-MySQL-PHP). |
29 |
29 |
30 * Update to current Java 11 and Poly/ML 5.8 with better scalability. |
30 * System: Isabelle/Phabricator as self-hosted project management platform. |
|
31 |
|
32 * System: more robust support for Windows. |
|
33 |
|
34 * System: improved support for macOS, notably 10.15 Catalina. |
31 |
35 |
32 |
36 |
33 You may get Isabelle2019 from the following mirror sites: |
37 You may get Isabelle2020 from the following mirror sites: |
34 |
38 |
35 Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle |
39 Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle |
36 Munich (Germany) https://isabelle.in.tum.de |
40 Munich (Germany) https://isabelle.in.tum.de |
37 Sydney (Australia) https://mirror.cse.unsw.edu.au/pub/isabelle |
41 Sydney (Australia) https://mirror.cse.unsw.edu.au/pub/isabelle |
38 Potsdam, NY (USA) https://mirror.clarkson.edu/isabelle |
42 Potsdam, NY (USA) https://mirror.clarkson.edu/isabelle |