Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds

TL;DR

The paper addresses the limitations of a Jenkins-based CI for Isabelle by introducing a native Isabelle/Scala build_manager that supports quasi-interactive, multi-host builds. It presents a multi-process architecture with a PostgreSQL-backed shared state, SSH-based remote execution, and a static HTML iframe-based web UI that eliminates client-side JavaScript. Key contributions include end-to-end build orchestration, task management, robust logging, and a simplified deployment that integrates with existing Isabelle tooling. The approach yields significant improvements in reliability and performance (including substantial speed-ups for cluster-based builds) and enables future work on live source updates, dynamic scaling, and richer build-state visualization, with practical benefits for reproducibility and data-management-aware research workflows.

Abstract

Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platform exemplifies this with its Isabelle/Scala systems programming environment, which has proven to be very successful. In contrast, much of the project infrastructure has relied on external tooling in the past, despite shortcomings. For continuous integration, the previous system employed a Jenkins server, which did not adequately support user-submitted Isabelle builds and faced issues with reliability and performance. In this work, we present our design and implementation of a new Isabelle build manager that replaces the old continuous integration system, fully implemented within Isabelle/Scala. We illustrate how our implementation utilizes different modules of the environment, which supported all aspects of the build manager well.

Figures (2)

• Figure 1: Isabelle execution contexts for a typical example deployment.
• Figure 2: Dashboard page of the build manager web application.