Isabelle/Pure was originally introduced by Paulson (1986/1989) as a Logical Framework to specify object-logics declaratively, based on Higher-order Natural Deduction. Isabelle/HOL emerged soon as main object-logic and Isabelle application, with many tools for specifications and proofs written in Isabelle/ML.
Isabelle/Isar was added by Wenzel (1999) as a structured language for Human-readable formal proof documents: it works with Isabelle/Pure and regular object-logics. The proof language has been reworked over the decades, with notable extensions in 2015/2016, including the Eisbach language for Isar Proof Methods. Already, from the beginning, Isar had been accompanied by the Isabelle Document language, to write mathematical texts with high-quality typesetting in LaTeX.
So today we may see Isabelle as an agglomeration of many languages for different purposes, all integrated into a single System Framework in Isabelle/Scala. That includes the Isabelle/PIDE Prover IDE with parallel and asynchronous processing of formal documents, and the Isabelle build system (with its distributed cluster manager). Thus we can carry the weight and gravity of large proof documents, as e.g. seen in the Archive of Formal Proofs (AFP).
The official Isabelle2025-1 release is scheduled for mid December 2025. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.
Isabelle2025-1-RC1 (05-Nov-2025): first official release candidate, approx. 6 weeks before final lift-off. Almost everything is ready for testing; some documentation and add-on components still require updates.. See also AFP/695d78dfa92a.
The next anticipated release after Isabelle2025 (March 2025) will be Isabelle2025-1 (December 2025). The hot phase of the release is presently scheduled for 03-Nov-2025..15-Dec-2025. The detailed plan is as follows:
06-Oct-2025: Isabelle2025-1-RC0 as informal preview
03-Nov-2025 Isabelle2025-1-RC1 as first formal release candidate
15-Dec-2025: final and unchangeable Isabelle2025-1 release
Important: Contributors need to have things ready for RC1 or RC2. There need to be several weeks left to consolidate everything, before the release becomes final and unchangable (until the subsequent release).
The Isabelle Workshop usually happens every second year: this time on 14-Sep-2024 in Tbilisi, Georgia, colocated with the ITP 2024 conference. The workshop website includes all papers (and some slides).
The Phorge project has succeeded Phabricator as a community fork, starting in June 2021 when the latter was “winding down” (see also https://sketis.net/2021/after-phabricator-we-phorge-it). In Dec-2023 Phorge has become sufficiently stable to consider moving the isabelle-dev service to it, using up-to-date versions of PHP and Ubuntu-Linux. Everything has been cleaned-up and reworked on our side, and we can continue this approach to self-hosting for more years to come.
At the Dagstuhl-Seminar 23401Automated mathematics: integrating proofs, algorithms and data (01..06-Oct-2023), I delivered a talk on Isabelle as System Platform for the Archive of Formal Proofs (AFP).
Abstract:
Isabelle is usually seen as an interactive proof assistant, mostly for Higher-Order Logic (HOL), but that is somehow accidental. In reality, Isabelle is a system platform for functional programming and formal proofs, with sufficient infrastructure to carry its own weight and gravity. The Archive of Formal Proofs (AFP) is the official collection of Isabelle applications that is maintained together with the base system. That poses ever growing demands on the Isabelle platform. This talk gives an overviewof Isabelle software technology, with specific focus on Programming and Scaling, e.g. distributed build clusters for AFP.
See also the slides, which contain further links to relevant materials.
Following our usual 2-years cycle, we have another Isabelle Workshop on Thu 11-Aug-2022. This will be a truly hybrid event: the organizers of the FLoC multiconference will provide local facilities at the Technion Haifa; this will include a digital projector and network connection. We will use that to provide our own virtual facilities on top, to accommodate remote participants via BigBlueButton hosted at TU Munich.
The remote organizers of the workshop, including myself, are very grateful to the few heroic colleagues who will be there in Haifa, despite these confused times of plague and war – and rather expensive conference registration.
Already in June 2021, the main author and maintainer has announced that the platform is “winding down”, i.e. no longer actively maintained – while a few updates have already appeared afterwards. From a technical standpoint, this somewhat undefined state can easily continue one more year without further worries: our self-hosted server is running well without particular problems.
Moreover, a group of Phabricator users has already started to work on the successor project, which is called “Phorge” and developed on the site we.phorge.it. So lets see how this looks like in 6–12 months, when it is time to reconsider that part of the Isabelle infrastructure.
Das Schlagwort “Digitalisierung” wird immer lauter verkündet, obwohl dahinter oft wenig substantieller Inhalt steht. Handelt es sich hierbei um ein Werkzeug für die Menschen oder ein Machtinstrument der großen IT-Konzerne?
Unter dem Namen Augsburg.One nähern sich Bürger in Augsburg diesem Themenkomplex im Sinne der klassischen Aufklärung, mit selbständigem Denken und Handeln. Sowohl die Technologie als auch die Soziologie der “Digitalisierung” soll im Sinne der “Nachhaltigkeit” verstanden und gestaltet werden. Es ist nicht erforderlich, die Daseinsvorsorge im virtuellen Raum über global operierende Konzerne abzuwickeln: Man kann dies auch lokal in die eigene Hand nehmen.
Aktuelle Beiträge aus diesem Prozess sammeln sich im Blog an.
Am 21. September 2020 um 19:30 findet im Hollsaal ab des Zeughaus Augsburg (Zeugplatz 4, 86150 Augsburg) ein Vortrag mit Dr. Christian Kreiß statt.
HINWEIS:
Voranmeldung erforderlich: AUSGEBUCHT
Thema:
Die Jahrhundertrezession – Wie geht es weiter?
Zusammenfassung:
Im Frühjahr 2020 gab es den weltweit größten Wirtschaftseinbruch der Neuzeit. Gleichzeitig sind die Schulden wegen massiver kreditfinanzierter staatlicher Konjunkturmaßnahmen auf einen neuen Rekordstand gestiegen. Abwürgen der Ökonomie durch staatliche Zwangs-Lockdowns und gleichzeitige massive Schuldenaufnahme führen ökonomisch in eine Sackgasse, in gravierende Schuldenprobleme mit chaotischem Wirtschaftsabsturz oder Inflation. So kann es nicht weitergehen. Was kommt nun? Wie können wir damit umgehen? Was sind die Hintergründe dieser Entwicklung?
Referent:
Prof. Dr. Christian Kreiß, Jahrgang 1962, studierte Volkswirtschaftslehre und promovierte in München über die Große Depression 1929 bis 1932. Nach neun Jahren Berufstätigkeit als Bankier in verschiedenen Geschäftsbanken, davon sieben Jahre als Investment Banker, unterrichtet er seit 2002 als Professor an der Hochschule Aalen Finanzierung und Wirtschaftspolitik. 2004 und 2006 hielt er an der University of Maine, USA, Master of Business Administration (MBA)- Vorlesungen über Investment Banking.
Autor von mehreren Büchern: unter anderem Profitwahn (2013), Geplanter Verschleiß (2014), Gekaufte Forschung (2015), Werbekritik (2016). Zahlreiche Veröffentlichungen. Ca. 30 bis 40 öffentliche Vorträge pro Jahr. Etwa 15 Fernseh- sowie zahlreiche Rundfunkinterviews. Drei Einladungen in den Deutschen Bundestag als Experte zu geplantem Verschleiß und Wissenschaftsethik. Homepage https://menschengerechtewirtschaft.de
Veranstalter:
Aktionskreis für Frieden, Freiheit und Menschengerechte Wirtschaft, E-Mail Frieden.Freiheit.Menschenger.Wirtschaft(at)protonmail.com
Aufgrund der Corona-Vorschriften sind die Plätze im Vortragsraum begrenzt. Eine Voranmeldung per E-Mail ist unter der Adresse: Anmeldung.Vortrag.Christian.Kreiss(at)protonmail.com möglich. Wegen der Corona-Auflagen für die Veranstaltung muss eine Anwesenheitsliste mit Kontaktdaten aller Teilnehmer/innen geführt werden, vergleichbar wie bei einem Restaurantbesuch. Diese Daten werden nach 2 Wochen vernichtet.