ANNOUNCE
changeset 73010 a569465f8b57
parent 71491 0a20dd339a05
child 73112 efc58b56a6c7
equal deleted inserted replaced
73009:56eae6d161db 73010:a569465f8b57
     1 Subject: Announcing Isabelle2020
     1 Subject: Announcing Isabelle2021
     2 To: isabelle-users@cl.cam.ac.uk
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     3 
     4 Isabelle2020 is now available.
     4 Isabelle2021 is now available.
     5 
     5 
     6 This version introduces many changes over Isabelle2019: see the NEWS
     6 This version introduces many changes over Isabelle2020: see the NEWS
     7 file for further details. Here are some notable points:
     7 file for further details. Here are various details:
     8 
     8 
     9 * PIDE: much faster startup of Isabelle/jEdit thanks to more scalable
     9 * Improved HTML presentation in Isabelle/Scala, using PIDE markup.
    10 session directory structure.
       
    11 
    10 
    12 * PIDE: updated Isabelle/VSCode to follow recent moves of VSCode.
    11 * Improved PDF document preparation in Isabelle/Scala, using LuaLaTeX.
    13 
    12 
    14 * Pure: improved treatment of theorem dependencies and proof terms,
    13 * Isabelle/jEdit: improved monitoring of Java and ML process.
    15 accessible via command 'thm_deps'.
       
    16 
    14 
    17 * Pure: proper treatment of oracles within internal proof objects,
    15 * Isabelle/jEdit: various IDE feedback improvements.
    18 accessible via command 'thm_oracles'.
       
    19 
    16 
    20 * HOL: various library improvements.
    17 * Pure: improved handling of named contexts and local syntax bundles.
    21 
    18 
    22 * HOL: better organization of HOL-Analysis vs. HOL-Complex_Analysis.
    19 * HOL: substantially reworked support for Word library.
    23 
    20 
    24 * ML: more scalable export artifacts via XML blobs.
    21 * HOL: various syntax and library improvements.
    25 
    22 
    26 * Scala: support for external IDEs based on Gradle (e.g. IntelliJ IDEA).
    23 * HOL: various Sledgehammer and SMT improvements, with updated external tools.
    27 
    24 
    28 * Scala: support for Ubuntu server applications (Linux-Apache-MySQL-PHP).
    25 * HOL: support for Nitpick/Kodkod in Isabelle/Scala.
    29 
    26 
    30 * System: Isabelle/Phabricator as self-hosted project management platform.
    27 * ML: routine support for Isabelle/Scala functions in Isabelle/ML.
    31 
    28 
    32 * System: update to current Poly/ML 5.8.1 with improved robustness,
    29 * System: support for Isabelle/Scala services defined in user-space.
    33 especially on Windows.
       
    34 
    30 
    35 * System: improved support for macOS, notably 10.15 Catalina.
    31 * Experimental support for ARM64 platform on Linux and macOS (Apple Silicon).
    36 
    32 
    37 
    33 
    38 You may get Isabelle2020 from the following mirror sites:
    34 You may get Isabelle2021 from the following mirror sites:
    39 
    35 
    40   Cambridge (UK)       https://www.cl.cam.ac.uk/research/hvg/Isabelle
    36   Cambridge (UK)       https://www.cl.cam.ac.uk/research/hvg/Isabelle
    41   Munich (Germany)     https://isabelle.in.tum.de
    37   Munich (Germany)     https://isabelle.in.tum.de
    42   Sydney (Australia)   https://mirror.cse.unsw.edu.au/pub/isabelle
    38   Sydney (Australia)   https://mirror.cse.unsw.edu.au/pub/isabelle
    43   Potsdam, NY (USA)    https://mirror.clarkson.edu/isabelle
    39   Potsdam, NY (USA)    https://mirror.clarkson.edu/isabelle