diff --git a/download_past.html b/download_past.html
--- a/download_past.html
+++ b/download_past.html
@@ -1,133 +1,137 @@
What is Isabelle?
Isabelle is a generic proof assistant. It allows mathematical
formulas to be expressed in a formal language and provides tools
for proving those formulas in a logical calculus. Isabelle was
originally developed at
the University
of Cambridge and Technische
Universität München, but now includes numerous
contributions from institutions and individuals worldwide. See
the Isabelle overview for a brief
introduction.
-
Now available: (September 2023)
+
Now available: (September 2024)
Hardware requirements:
- Small experiments: 4 GB memory, 2 CPU cores
- Medium applications: 8 GB memory, 4 CPU cores
- Large projects: 16 GB memory, 8 CPU cores
- Extra-large projects: 64 GB memory, 16 CPU cores
Some notable changes:
- More robust and scalable support for distributed build clusters.
- Official support for ARM64 on Linux (notably Docker on Apple Silicon).
- HOL: various improvements of theory libraries, notably in HOL-Analysis.
- HOL: updates and improvements of Sledgehammer.
- ML: antiquotations for try-catch-finally.
- ML: physical interrupts are now distinguished from runtime system failures.
- System: support for global registry in TOML format.
- System: support the Go development environment (all platforms).
- System: bundled MLton now includes both Linux and macOS (Intel).
See also the
cumulative NEWS.
Distribution & Support
Isabelle is distributed for free under a conglomerate of
open-source licenses, but the main code-base is subject to
BSD-style regulations. The application bundles include source and
binary packages and documentation, see the
detailed installation
instructions. A vast collection of Isabelle examples and
applications is available from
the Archive of Formal
Proofs.
Support is available by the
official documentation and
mailing lists:
Zulip Chat is a
real-time discussion platform to exchange ideas, ask questions,
and collaborate on Isabelle projects, with
minimalistic public
archive.
Stack
Overflow and Stack
Exchange are a question-and-answer platform, with complex
review process but limited discussion facilities.