diff options
| -rw-r--r-- | .github/isabelle-action/Dockerfile | 26 | ||||
| -rw-r--r-- | .github/isabelle-action/action.yml | 13 | ||||
| -rw-r--r-- | .github/isabelle-action/entrypoint.sh | 5 | ||||
| -rw-r--r-- | .github/workflows/build.yml | 13 | ||||
| -rw-r--r-- | README.md | 2 |
5 files changed, 58 insertions, 1 deletions
diff --git a/.github/isabelle-action/Dockerfile b/.github/isabelle-action/Dockerfile new file mode 100644 index 0000000..34a4adf --- /dev/null +++ b/.github/isabelle-action/Dockerfile @@ -0,0 +1,26 @@ +## Isabelle2020 Dockerfile for GitHub Actions + +FROM ubuntu +SHELL ["/bin/bash", "-c"] + +# Install packages +ENV DEBIAN_FRONTEND=noninteractive +RUN apt-get -y update &&\ + apt-get install -y curl less libfontconfig1 libgomp1 libwww-perl rlwrap unzip &&\ + apt-get clean + +# Set up Isabelle +ADD https://isabelle.in.tum.de/dist/Isabelle2020_linux.tar.gz Isabelle.tar.gz +RUN tar xzf Isabelle.tar.gz &&\ + mv Isabelle2020 Isabelle &&\ + perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$HOME/.isabelle",g;' Isabelle/etc/settings &&\ + perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=Pure,g;' Isabelle/etc/settings &&\ + Isabelle/bin/isabelle build -o system_heaps -b Pure &&\ + rm Isabelle.tar.gz + +# Set up entrypoint +COPY entrypoint.sh /entrypoint.sh +RUN chmod +x /entrypoint.sh + +ENTRYPOINT ["/entrypoint.sh"] + diff --git a/.github/isabelle-action/action.yml b/.github/isabelle-action/action.yml new file mode 100644 index 0000000..c9a1b4a --- /dev/null +++ b/.github/isabelle-action/action.yml @@ -0,0 +1,13 @@ +name: "Isabelle action" +description: "Run Isabelle" +author: "josh@joshchen.io" + +inputs: + TOOL_ARGS: + description: "Isabelle tool to invoke and arguments to pass" + required: true + +runs: + using: "docker" + image: "Dockerfile" + diff --git a/.github/isabelle-action/entrypoint.sh b/.github/isabelle-action/entrypoint.sh new file mode 100644 index 0000000..954226a --- /dev/null +++ b/.github/isabelle-action/entrypoint.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +chmod +x /Isabelle/bin/isabelle +sh -c "/Isabelle/bin/isabelle $INPUT_TOOL_ARGS" + diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..56b8c61 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,13 @@ +name: build +on: push + +jobs: + build: + name: build ROOT + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v1 + - uses: ./.github/isabelle-action + with: + TOOL_ARGS: "build -D $GITHUB_WORKSPACE" + @@ -1,4 +1,4 @@ -# Isabelle/HoTT +# Isabelle/HoTT [](https://github.com/jaycech3n/Isabelle-HoTT/actions?query=workflow%3Abuild) Isabelle/HoTT is an experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in the [Isabelle](https://isabelle.in.tum.de/) interactive theorem prover. It largely follows the development of the theory in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/), but aims to be general enough to eventually support cubical and other kinds of homotopy type theories. |