Development of a distributed build platform for Isabelle

Chair for Logic and Verification

Bachelor Thesis

Changes to existing software can often lead to unpredicted behaviour or faults. In particular in theorem proving, changes to the inner machinery can have a large impact. In Isabelle, we address this problem with a large system test where the whole archive of formal proofs is built. It is thus desirable to check such a large body of formalizations quickly.

As a truly parallel interactive theorem prover, Isabelle can take advantage of a large degree of parallelism [1]. A single build can be distributed on multiple worker threads, which – up to a certain threshold on the number of parallel threads (typically 8 to 16) – increases performance greatly. Moreover, multiple independent sessions can be built in parallel on a single machine.

In the past, this meant that large server CPUs with hundreds of cores were a suitable choice for a build system to achieve short build times; however, nowadays performance gravitates towards high-speed consumer hardware, which allows only limited parallelism.

As a result, utilizing multiple individual consumer CPUs would yield much shorter build times than a single high-performance system, while being much more economical at the same time.

The scope of this thesis is designing and implementing a platform that enables this, so that builds can be distributed on a (potentially heterogeneous) cluster of worker machines. The main problems to solve are state management, scheduling, and handling of node outages.

Programming language: Scala, Shell

Prerequisites: Familiarity with Scala or similar language; English; Good linux experience


Fabian Huch, email {huch} AT []


Prof. Tobias Nipkow, email {nipkow} AT []


[1]: Wenzel, Makarius. “Parallel proof checking in Isabelle/Isar.” PLMMS (2009): 13-29