Build the theories in CI

.github/workflows/ci.yml

@@ -0,0 +1,35 @@
+name: Build
+on:
+  push:
+    paths-ignore:
+      - '**.md'
+
+jobs:
+  build:
+    name: build
+    runs-on: ubuntu-18.04
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v2
+
+      - name: Setup buildx
+        uses: crazy-max/ghaction-docker-buildx@v3
+
+      - name: Cache docker layers
+        uses: actions/cache@v1
+        with:
+          path: /tmp/docker-cache
+          key: docker-cache-${{ hashFiles('Dockerfile') }}-1
+          restore-keys: |
+            docker-cache-
+
+      - name: Build Nominal Isabelle
+        run: |
+            docker buildx build \
+                --cache-from "type=local,src=/tmp/docker-cache" \
+                --cache-to "type=local,dest=/tmp/docker-cache,mode=max" \
+                --output "type=docker" \
+                --tag isabelle_nominal:latest .
+
+      - name: Run theories
+        run: docker run isabelle_nominal build -d . Lambda

Dockerfile

@@ -0,0 +1,15 @@
+FROM makarius/isabelle:Isabelle2020
+
+RUN for t in Nominal2 FinFun; do \
+        curl https://www.isa-afp.org/release/afp-$t-current.tar.gz -o $t.tar.gz ; \
+        cd Isabelle/src/ ; \
+        tar -xzf ../../$t.tar.gz ; \
+        cd .. ; \
+        echo "src/$t" >> ROOTS ; \
+        cd .. ; \
+        rm $t.tar.gz ; \
+    done
+
+RUN ./Isabelle/bin/isabelle build -o system_heaps -b Nominal2
+
+COPY ROOT Defs.thy Soundness.thy ./

ROOT

@@ -0,0 +1,4 @@
+session Lambda = HOL + sessions "HOL-Eisbach" Nominal2
+theories
+    Defs
+    Soundness