Introduction

Isabelle Service Manager (ISM) is a supervisor and transparent load balancer intended to orchestrate the isabelle server.

It was created to augment the ProofBuddy backend by providing a transparent isabelle server load balancer to scale beyond a single Isabelle server instance. ISM also aims to ensure Isabelle server instances are isolated from the rest of the server environment with minimal overhead.

The main goals are:

  • Availability: Ensure the backend can always create new sessions. This will eventually include clustered operation of ISM.
  • Resilience: Ensure server failures and corrupt states are detected and handled
  • Security: Ensure servers are isolated from each other and the host.

Additionally, ISM aims to achieve a low latency overhead and resource usage.

Branches

ISM doesn't yet follow a release cycle. The current development model is trunk based development, with the main branch being our trunk.

There is a stable branch, which is a ref to the last well known working rev from main. This is the branch deployed in production. This branch may only get hot fixes in emergencies but will otherwise always be updated by being rebased on main.

Documentation

The ISM documentation is split into two parts:

  • internals: Documentation for developers and operators
  • users: Documentation for developers connecting via clients

Both parts have different target audiences and expect a different set of preexisting knowledge.

The users' documentation assumes familiarity with:

The internals' documentation assumes familiarity with: