Isabelle/Phabricator server setup

Recent Isabelle repository versions 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.)

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.