Add a GitHub Action to run lake build and stack build

Runs automatically for pull requests to `main` or pushes to `main`.
Uses Nix to obtain the packages declared in `shell.nix` (`elan` and `stack`).
Caches Lean toolchain and Lean packages, retrieving Mathlib via `lake exe cache get` if not already in the GitHub Actions cache.

.github/workflows/main.yml

@@ -0,0 +1,38 @@
+name: Build
+
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/[email protected]
+      - name: The Determinate Nix Installer
+        uses: DeterminateSystems/nix-installer-action@v14
+      - name: Magic Nix Cache
+        uses: DeterminateSystems/magic-nix-cache-action@v8
+      - name: Cache Lean toolchain
+        uses: actions/[email protected]
+        with:
+          path: ~/.elan/toolchains
+          key: ${{ runner.os }}-lean-toolchain-${{ hashFiles('lean-toolchain') }}
+      - name: Cache Lean packages
+        id: cache-lean-packages
+        uses: actions/[email protected]
+        with:
+          path: .lake/packages
+          key: ${{ runner.os }}-lean-packages-${{ hashFiles('lake-manifest.json') }}
+      - if: ${{ steps.cache-lean-packages.outputs.cache-hit != 'true' }}
+        name: Get Mathlib cache
+        run: nix-shell --run "lake exe cache get"
+      - name: Build vc tool
+        run: nix-shell --run "cd vc; stack --nix build"
+      - name: Build Lean files
+        run: nix-shell --run "lake build"