# HG changeset patch # User wenzelm # Date 1689021271 -7200 # Node ID e23703e5b4d1ac9a30964441756e4eb4122972d4 # Parent 9e0c035d026d71dd2a3964ff3768166cd3895007# Parent 2a3577d0a27aa517c83f01e192883091d9cb4f63 merged diff -r 9e0c035d026d -r e23703e5b4d1 ANNOUNCE --- a/ANNOUNCE Mon Jul 10 18:48:22 2023 +0100 +++ b/ANNOUNCE Mon Jul 10 22:34:31 2023 +0200 @@ -1,37 +1,31 @@ -Subject: Announcing Isabelle2022 +Subject: Announcing Isabelle2023 To: isabelle-users@cl.cam.ac.uk -Isabelle2022 is now available. +Isabelle2023 is now available. -This version introduces notable changes over Isabelle2021-1: see the +This version introduces notable changes over Isabelle2022: see the NEWS file for further details. Here are various details: -* HTML presentation is more robust and covers more files and links. +* ML heap usage and stored heap size has been significantly reduced. -* Display of instantiation for schematic goals. +* Interactive document preparation via Isabelle/jEdit panel. -* PIDE: improved Isabelle/VSCode based on bundled VSCodium engine. +* Demo documents for well-known LaTeX classes. * HOL: various improvements of theory libraries. * HOL: updates and improvements of Sledgehammer. -* HOL: improved simproc support for record types. +* ML: improved implementations of functor Table() and corresponding Set(). -* ML: scalable type Bytes.T with support for XZ compression. - -* System: bundled Node.js/Chromium/Electron platform (via VSCodium). +* Scala and ML: support for Zstd compression. -* System: Isabelle/Scala is based on Scala 3 (dotty compiler). - -* System: tools to sync hg repositories, notably Isabelle + AFP. +* System: more robust "isabelle sync" tool via bundled "rsync" executables. -* System: improved "isabelle log" tool with regex filtering. - -* System: more robust SSH support in Isabelle/Scala. +* Support for the Dotnet platform (.NET) and Fsharp (F#). -You may get Isabelle2022 from the following mirror sites: +You may get Isabelle2023 from the following mirror sites: Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle Munich (Germany) https://isabelle.in.tum.de diff -r 9e0c035d026d -r e23703e5b4d1 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Jul 10 18:48:22 2023 +0100 +++ b/Admin/components/components.sha1 Mon Jul 10 22:34:31 2023 +0200 @@ -107,6 +107,7 @@ 9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz 212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz 6d4dbb6f2bde5804298d9008e3edceb0b9ee20ae flatlaf-2.4.tar.gz +31d6abd58a4c2f7522f14283dfe04e2801a6e828 flatlaf-2.6.tar.gz b1c40ce6c087da7e70e221ddd3fcadfa569acb2f foiltex-2.1.4b.tar.gz f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz 71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz @@ -289,6 +290,7 @@ 759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz 1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz 5557b396f5a9aa22388d3e2171f9bc58e4bd6cd7 lipics-3.1.2.tar.gz +881741f6e7192fd03835b542b1db820daf0ae79c lipics-3.1.3.tar.gz 71b6a272d10c53bb54cba23102e15334ec39bfce llncs-2.22.tar.gz 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz @@ -467,6 +469,7 @@ 8a2ca4d02cfedbfe4dad4490f1ed3ddba33a009a sqlite-jdbc-3.36.0.3.tar.gz d2c707638b08ad56469b92dc2941d403efbb3394 sqlite-jdbc-3.39.4.1.tar.gz 12cb90b265bc2308858c63f00d5ecbfb80603dbd sqlite-jdbc-3.41.0.0.tar.gz +3535a04b8612cb1d98f0f7e41a0668e41667ec8b sqlite-jdbc-3.42.0.0.tar.gz 8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz 2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz diff -r 9e0c035d026d -r e23703e5b4d1 Admin/components/main --- a/Admin/components/main Mon Jul 10 18:48:22 2023 +0100 +++ b/Admin/components/main Mon Jul 10 22:34:31 2023 +0200 @@ -7,7 +7,7 @@ e-2.6-1 easychair-3.5 eptcs-1.7.0 -flatlaf-2.4 +flatlaf-2.6 foiltex-2.1.4b idea-icons-20210508 isabelle_fonts-20211004 @@ -18,7 +18,7 @@ jortho-1.0-2 jsoup-1.15.4 kodkodi-1.5.7 -lipics-3.1.2 +lipics-3.1.3 llncs-2.22 minisat-2.2.1-1 mlton-20210117-1 @@ -32,7 +32,7 @@ scala-3.3.0 smbc-0.4.1 spass-3.8ds-2 -sqlite-jdbc-3.41.0.0 +sqlite-jdbc-3.42.0.0 stack-2.7.3 vampire-4.6 verit-2021.06.2-rmx diff -r 9e0c035d026d -r e23703e5b4d1 COPYRIGHT --- a/COPYRIGHT Mon Jul 10 18:48:22 2023 +0100 +++ b/COPYRIGHT Mon Jul 10 22:34:31 2023 +0200 @@ -1,6 +1,6 @@ ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER. -Copyright (c) 1986-2022, +Copyright (c) 1986-2023, University of Cambridge, Technische Universitaet Muenchen, and contributors. diff -r 9e0c035d026d -r e23703e5b4d1 NEWS --- a/NEWS Mon Jul 10 18:48:22 2023 +0100 +++ b/NEWS Mon Jul 10 22:34:31 2023 +0200 @@ -26,7 +26,8 @@ class.order.of_class.intro ~> order.intro_of_class * The Eisbach 'method' command now takes an optional description for -display with print_methods, similar to the 'method_setup' command. +display with 'print_methods', similar to the 'method_setup' command. + *** Document preparation *** @@ -80,7 +81,7 @@ - Add proof method "order". * 'primcorec': Made the internal tactic more robust in the face of - nested corecursion. +nested corecursion. * Theory "HOL.Map": - Map.empty has been demoted to an input abbreviation. diff -r 9e0c035d026d -r e23703e5b4d1 src/Pure/Admin/component_lipics.scala --- a/src/Pure/Admin/component_lipics.scala Mon Jul 10 18:48:22 2023 +0100 +++ b/src/Pure/Admin/component_lipics.scala Mon Jul 10 22:34:31 2023 +0200 @@ -23,7 +23,7 @@ /* build lipics component */ - val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz" + val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.3.tar.gz" def build_lipics( download_url: String = default_url, diff -r 9e0c035d026d -r e23703e5b4d1 src/Pure/Admin/component_sqlite.scala --- a/src/Pure/Admin/component_sqlite.scala Mon Jul 10 18:48:22 2023 +0100 +++ b/src/Pure/Admin/component_sqlite.scala Mon Jul 10 22:34:31 2023 +0200 @@ -11,7 +11,7 @@ /* build sqlite */ val default_download_url = - "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.41.0.0/sqlite-jdbc-3.41.0.0.jar" + "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.42.0.0/sqlite-jdbc-3.42.0.0.jar" def build_sqlite( download_url: String = default_download_url, diff -r 9e0c035d026d -r e23703e5b4d1 src/Pure/Tools/dotnet_setup.scala --- a/src/Pure/Tools/dotnet_setup.scala Mon Jul 10 18:48:22 2023 +0100 +++ b/src/Pure/Tools/dotnet_setup.scala Mon Jul 10 22:34:31 2023 +0200 @@ -52,7 +52,7 @@ def default_target_dir: Path = Components.default_components_base def default_install_url: String = "https://dot.net/v1/dotnet-install" - def default_version: String = "6.0.402" + def default_version: String = "6.0.411" def dotnet_setup( platform_spec: String = default_platform,