diff --git a/community.html b/community.html
deleted file mode 100644
--- a/community.html
+++ /dev/null
@@ -1,24 +0,0 @@
-
-
-
-
-
-
-
Redirect
-
Please visit the Isabelle project page at https://isabelle.in.tum.de/community.
-
-
-
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: (April 2020)
+
Now available: (February 2021)
+
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:
- - PIDE: much faster startup of Isabelle/jEdit thanks to more
- scalable session directory structure.
-
- - PIDE: updated Isabelle/VSCode
- to follow recent moves of VSCode.
-
- - Pure: improved treatment of theorem dependencies and proof terms,
- accessible via command thm_deps.
-
- - Pure: proper treatment of oracles within internal proof
- objects, accessible via command thm_oracles.
-
- - HOL: various library improvements.
-
- - HOL: better organization of HOL-Analysis vs. HOL-Complex_Analysis.
-
- - ML: more scalable export artifacts via XML blobs.
+ - Improved HTML presentation in Isabelle/Scala, using PIDE markup.
- - Scala: support for external IDEs based on Gradle (e.g. IntelliJ IDEA).
-
- - Scala: support for Ubuntu
- server applications (Linux-Apache-MySQL-PHP).
+ - Improved PDF document preparation in Isabelle/Scala, using LuaLaTeX.
- - System: Isabelle/Phabricator
- as self-hosted project management platform.
+ - Isabelle/jEdit: improved monitoring of Java and ML process.
- - System: update to current Poly/ML 5.8.1 with improved
- robustness, especially
- on Windows.
+ - Isabelle/jEdit: various IDE feedback improvements.
- - System: improved support for macOS, notably 10.15
- Catalina.
+ - Pure: improved handling of named contexts and local syntax bundles.
+
+ - HOL: substantially reworked support for Word library.
+
+ - HOL: various syntax and library improvements.
+
+ - HOL: various Sledgehammer and SMT improvements, with updated external tools.
+
+ - HOL: support for Nitpick/Kodkod in Isabelle/Scala.
+
+ - ML: routine support for Isabelle/Scala functions in Isabelle/ML.
+
+ - System: support for Isabelle/Scala services defined in user-space.
+
+ - Experimental support for ARM64 platform on Linux and macOS (Apple Silicon).
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
- ample documentation,
- the Isabelle
- community
- Wiki, Stack
- Overflow, and in particular the following mailing lists:
-
+
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 is a question-and-answer platform, with
+ complex review process and limited discussion facilities.
+
+