All posts by Makarius

Isabelle

Isabelle development self-hosted on Phorge

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.

Isabelle, Scala, Science

Isabelle as System Platform for the Archive of Formal Proofs (AFP)

At the Dagstuhl-Seminar 23401 Automated 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.

Isabelle, Science

Isabelle Workshop 2022 at FLoC

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.

Isabelle

After Phabricator: We Phorge It!

For almost 2 years already, the Isabelle project has been using Phabricator quite successfully, in order to stay away from the big black data holes like Bitbucket or Github, see also https://sketis.net/2019/isabelle-phabricator-server-setup

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.

Local

Augsburg.One – Nachhaltige Digitalisierung in Augsburg

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.

Global Financial System, Local

Dr. Christian Kreiß: Die Jahrhundertrezession – Wie geht es weiter?

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
  • Forum Fließendes Geld – Lokale Agenda 21 der Stadt Augsburg
Voranmeldung:
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.
Global Financial System, Isabelle

(Self)Hosting of Mercurial Repositories

The Mercurial community has relied a bit too long on Bitbucket (by Atlassian) to provide “free” hosting for it. The ultimate purpose of such big corporations is to maximize profits and return of investments, while the needs of customers are of little concern, and marketing fills this semantic gap. Who did not know this triviality in advance, and merely ignored it on the spot when creating repositories on Bitbucket?

So the discontinuation of Mercurial by Bitbucket will happen in two stages, on 01-Feb-2020 and 01-Jun-2020. Independently of such market-driven policies, Mercurial developers are quite alive and active to develop alternatives. In the past few months, two emerging projects for (self)hosting of Mercurial repositories have gained some attention:

  1. Sourcehut as a newcomer for Git and Mercurial hosting
  2. Heptapod as a version of Gitlab for Mercurial (eventually both for Git and Mercurial). See also the blog for ongoing activity.

Development of these projects is very active, but they are not yet ready for production use.

In contrast, Phabricator is a pretty stable and scalable hosting platform right now; it supports Git, Mercurial, Subversion. In fact, Phabricator is a sophisticated platform for software project management, and repository hosting is only a secondary function of it. See also the related post on Isabelle/Phabrictor tooling, with Isabelle development as a notable example.

Update 21-Mar-2020: link to Heptapod blog.