github workflows (push)

.github/workflows/push.yml

@@ -0,0 +1,58 @@
+on:
+  push:
+    branches:
+      - master
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  style_lint:
+    name: Lint style
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check for long lines
+        if: always()
+        run: |
+          ! (find GroupoidModel -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+
+      - name: Don't 'import Mathlib', use precise imports
+        if: always()
+        run: |
+          ! (find GroupoidModel -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
+
+  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 none
+
+      - name: Get cache
+        run: ~/.elan/bin/lake exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake build GroupoidModel
+
+      # - name: Cache mathlib docs
+      #   uses: actions/cache@v3
+      #   with:
+      #     path: |
+      #       .lake/build/doc/Init
+      #       .lake/build/doc/Lake
+      #       .lake/build/doc/Lean
+      #       .lake/build/doc/Std
+      #       .lake/build/doc/Mathlib
+      #       .lake/build/doc/declarations
+      #       !.lake/build/doc/declarations/declaration-data-GroupoidModel*
+      #     key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+      #     restore-keys: |
+      #       MathlibDoc-

.github/workflows/push_pr.yml

@@ -0,0 +1,21 @@
+on:
+  pull_request:
+
+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 exe cache get
+
+      - name: Build project
+        run: ~/.elan/bin/lake build GroupoidModel