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.

翻译：交互式定理证明器是复杂的系统，需要精密的平台支撑——即系统编程环境——以实现有效管理。Isabelle 平台以其 Isabelle/Scala 系统编程环境为例，证明了该方法的极大成功。相比之下，尽管存在不足，项目基础设施的许多部分过去一直依赖外部工具。在持续集成方面，先前系统采用 Jenkins 服务器，其未能充分支持用户提交的 Isabelle 构建，并面临可靠性与性能问题。本工作中，我们提出了一种新的 Isabelle 构建管理器的设计与实现，它取代了旧的持续集成系统，并完全在 Isabelle/Scala 中实现。我们阐述了该实现如何利用环境中的不同模块，这些模块很好地支撑了构建管理器的所有方面。