Category Archives: Isabelle

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

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.

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