All posts by Makarius

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.

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.

(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.

Isabelle/Phabricator server setup

Recent Isabelle repository versions (or release candidates for Isabelle2020) include support for Phabricator; a current release snapshot is also available. The following introduction to Isabelle/Phabricator is from the system manual (chapter 6).

Phabricator is an open-source product to support the development process of complex software projects (open or closed ones). The official slogan is:

Discuss. Plan. Code. Review. Test.
Every application your project needs, all in one tool.

Ongoing changes and discussions about changes are maintained uniformly within a MySQL database. There are standard connections to major version control systems: Subversion, Mercurial, Git. So Phabricator offers a counter-model to trends of monoculture and centralized version control, especially due to Microsoft’s Github and Atlassian’s Bitbucket.

The small company behind Phabricator provides paid plans for support and hosting of servers, but it is easy to do independent self-hosting on a standard LAMP server (Linux, Apache, MySQL, PHP). This merely requires a virtual machine on the Net, which can be rented cheaply from local hosting providers — there is no need to follow big cloud corporations. So it is feasible to remain the master of your virtual home, following the slogan “own all your data”. In many respects, Phabricator is similar to the well-known Nextcloud product, concerning both the technology and sociology.

The following Phabricator instances may serve as examples:

Initial Phabricator configuration requires many details to be done right. Isabelle provides some command-line tools to help with the setup, and afterwards Isabelle support is optional: it is possible to run and maintain the server, without requiring the somewhat bulky Isabelle distribution again.

Assuming an existing Phabricator installation, the command-line tool isabelle hg_setup helps to create new repositories or to migrate old ones. In particular, this avoids the lengthy sequence of clicks in Phabricator to make a new private repository with hosting on the server. (Phabricator is a software project management platform, where initial repository setup happens rarely in practice.)

Update 20-Jan-2020: follow Isabelle/597059a44d6f.

Update 21-Mar-2020: link to release candidates of Isabelle2020.

Isabelle as “the world’s most complicated video game”

Martin Kleppmann from the University of Cambridge has given very nice introductory lectures about formal verification with Isabelle: the title is Correctness proofs of distributed systems with Isabelle, see these slides. Further information and video recordings are available from here:

The lecture motivates the use of Isabelle by the very fitting characterization by Dominic Mulligan: Isabelle is the world’s most complicated video game.

Later in the talk there is a hands-on demo of the Isabelle Prover IDE, using the standard Isabelle/jEdit front-end: this is not a classic “REPL”, but a semantic document editor with immediate feedback by the prover.

Update (19-Dec-2019): An extended version of both talks is now available.

Talk on Export of formal theory content

On 22-Nov-2019 I have delivered the following talk at TUM (Garching bei München):

Title:
Export of formal theory content in Isabelle/Scala
Abstract:
This is an overview of the state of affairs of systematic export of formal theory content. The general motivation is to provide semantically enriched views on the Isabelle/AFP library, without requiring a running Isabelle process. A typical application could be search over a database of digested theories, e.g. for an AFP web service.
Materials:
Slides with sources, which include practically relevant links and examples.

MMT as component for Isabelle2019

MMT is a language, system and library (in Scala) to represent a broad range of languages in the OMDoc format: this supports formal, informal, semi-formal content. The MMT repository includes
general APIs to operate on OMDoc theories, together with various tools and applications. There are several MMT sub-projects to connect to other systems. This includes Isabelle/MMT, which appeared as preliminary version already in Nov-2018.

The release of Isabelle2019 (June 2019) is an opportunity to distribute MMT version 17.0.0 (May 2019) as Isabelle application. An alternative is to incorporate the underlying Isabelle component manually into Isabelle2019 in $ISABELLE_HOME_USER/etc/settings like this: init_component ".../mmt-20190611" — where the three dots refer to the directory where the component tar.gz has been unpacked.

In either case, the mmt.jar of the MMT distribution is included in the Isabelle/Scala package name space. The component provides Isabelle command-line tools as follows:

  • isabelle mmt_build to (re)build the MMT project inside the Isabelle system environment (only required after change of the Scala sources)
  • isabelle mmt_import to import the content of a headless Isabelle/PIDE session into MMT (OMDoc and RDF/XML triples)
  • isabelle mmt_server to present imported content using the built-in HTTP server of MMT
  • isabelle mmt to run the interactive MMT shell inside the Isabelle system environment, e.g. for experimentation within the Isabelle + MMT package namespace, using the scala sub-shell.

The main functionality is provided by isabelle mmt_import: that is a medium-sized Scala module (57KB) within the MMT code-base (file src/mmt-isabelle/src/info/kwarc/mmt/isabelle/Importer.scala). It refers to general export facilities of Isabelle/Scala, which are part of the Isabelle2019 distribution (file src/Pure/Thy/export_theory.scala). The latter may be studied independently of MMT in the implementation of the isabelle dump tool (file src/Pure/Tools/dump.scala); see also the Isabelle System Manual, section 2.6.

The following papers provide further explanations on Isabelle/MMT: