Merge pull request #107 from alissa-tung/master

ci: pub docs

.github/workflows/docs.yaml

@@ -0,0 +1,29 @@
+name: Build
+
+permissions:
+  contents: write
+
+on:
+  push:
+    branches:
+      - "master"
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Project
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 2
+      - name: Install Lean
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s - -y --default-toolchain `cat ./lean-toolchain`
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      - run: |
+          export CI_BUILD=1
+          lake update && lake exe cache get && lake build && lake -Kenv=CI_BUILD build EuclideanGeometry:docs
+      - name: Deploy
+        uses: JamesIves/github-pages-deploy-action@v4.4.3
+        with:
+          branch: gh-pages
+          folder: build/docs

lakefile.lean

@@ -5,10 +5,14 @@ package «EG» {
   -- add any package configuration options here
 }
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
 @[default_target]
 lean_lib «EuclideanGeometry» {
   -- add any library configuration options here
 }
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+meta if get_config? env = some "CI_BUILD" then
+  require «doc-gen4» from git
+    "https://github.com/leanprover/doc-gen4.git"