Merge pull request #3 from oliver-butterley/main

CI to build lean

.github/workflows/build.yml

@@ -0,0 +1,31 @@
+name: Lean build
+
+on:
+  pull_request:
+    branches:
+      - main
+  push:
+    branches:
+      - main
+  workflow_dispatch:
+
+concurrency:
+  group: lean-build
+  cancel-in-progress: true
+
+jobs:
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
+      - name: Get cache
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build Birkhoff
+

README.md

@@ -1,4 +1,6 @@
-## Birkhoff's ergodic theorem in LEAN4
+# Birkhoff's ergodic theorem in LEAN4
+
+![Lean build](https://github.com/mseri/birkhoff/actions/workflows/build.yml/badge.svg)
 
 This repository contains the output of our project
 at the [Machine-Checked Mathematics Workshop](https://www.lorentzcenter.nl/machine-checked-mathematics.html)