A GitHub Actions action for checking Isabelle theories. It mostly wraps makarius's Docker image makarius/isabelle:Isabelle2023_X11_Latex in a way that is digestible by GitHub Actions.
The action will run a session and build its PDF and HTML presentation. For this, it takes two inputs:
session
for the name of the session (from yourROOT
file).output
for the name of a directory where the HTML output (containing a hypertext version of your whole Isabelle library) will be put.
[...]
steps:
[...]
- name: Isabelle-action
uses: benkeks/[email protected]
with:
session: MySession
output: my-dir
If you are depending on more than HOL (e.g. HOL-Library), this will have to be built at every invocation. So, this might well burn 10 minutes of action running time.
The standard use case of this (apart from information about failing builds) is deploying a nice HTML version of your theory to GitHub pages or the like. An example of this can be seen at https://luisamontanari.github.io/ContrasimGame/AFP/Coupledsim_Contrasim/.