Saved in:
Bibliographic Details
Main Author: Huch, Fabian
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2412.13083
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866912159956467712
author Huch, Fabian
author_facet Huch, Fabian
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2412_13083
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
Huch, Fabian
Logic in Computer Science
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.
title Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
topic Logic in Computer Science
url https://arxiv.org/abs/2412.13083