feat: new CI setup

.github/workflows/build.yml

@@ -1,8 +1,6 @@
-name: build and deploy docs
+name: std4 test build
 
 on:
-  schedule:
-    - cron: '0 */8 * * *' # every 8 hours
   push:
     branches:
       - "main"
@@ -10,7 +8,7 @@ on:
 
 jobs:
   build:
-    name: build and deploy docs
+    name: std4 test build
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
@@ -27,27 +25,14 @@ jobs:
         run: |
           lake build
 
-      - name: Checkout and compile mathlib4
+      - name: Checkout and compile std4
         run: |
           cd ../
-          git clone https://github.com/leanprover-community/mathlib4
-          cd mathlib4
-          lake exe cache get
+          git clone https://github.com/leanprover/std4
+          cd std4
           lake build
 
-      - name: generate docs (PRs only)
-        if: github.event_name == 'pull_request'
+      - name: generate docs
         run: |
           cd ../
-          ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "false" "LeanInk"
-        env:
-          DOC_GEN_REF: ${{ github.event.pull_request.head.sha }}
-
-      - name: generate and deploy docs (main only)
-        if: (github.event_name == 'push' || github.event_name == 'schedule') && github.repository == 'leanprover/doc-gen4' && github.ref_name == 'main'
-        run: |
-          cd ../
-          ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "true" "LeanInk"
-        env:
-          MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
-          DOC_GEN_REF: ${{ github.sha }}
+          ./doc-gen4/test_docs.sh "std4" "doc-gen4"

.github/workflows/mathlib4docs.yml

@@ -0,0 +1,29 @@
+name: build and deploy mathlib4 docs
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 */8 * * *' # every 8 hours
+jobs:
+  build:
+    name: build and deploy mathlib4 docs
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v3
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: generate and deploy docs
+        if: github.repository == 'leanprover/doc-gen4'
+        run: |
+          cd ../
+          ./doc-gen4/deploy_docs.sh
+        env:
+          MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
+          DOC_GEN_REF: ${{ github.sha }}

DocGen4/Output/Index.lean

@@ -16,7 +16,8 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
     <main>
       <a id="top"></a>
       <h1> Welcome to the documentation page </h1>
-      <p>This was built for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a> using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
+      -- Temporary comment until the lake issue is resolved
+      <p>This was built /-for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a>-/ using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
     </main>
 
 end Output

deploy_docs.sh

@@ -1,40 +1,38 @@
-# Arguments:
-# $1 : path to mathlib4 from working directory
-# $2 : path to doc-gen4 from working directory
-# $3 : whether to deploy
-
 set -e
 set -x
 
-cp -r $2/lake-packages/* $1/lake-packages
-cd $1
-mathlib_short_git_hash="$(git log -1 --pretty=format:%h)"
-
-cd ../$2
-DOC_GEN_URL="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY"
-
-cd ../
+git config --global user.email "leanprover.community@gmail.com"
+git config --global user.name "leanprover-community-bot"
 
 git clone "https://github.com/leanprover-community/mathlib4_docs.git" mathlib4_docs
 
-# skip if docs for this commit have already been generated
-if [ "$(cd mathlib4_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF" ]; then
+# Workaround for the lake issue
+elan default leanprover/lean4:nightly
+lake new workaround math
+cd workaround
+echo 'require «doc-gen4» from ".." / "doc-gen4" ' >> lakefile.lean
+
+# doc-gen4 expects to work on github repos with at least one commit
+git add .
+git commit -m "workaround"
+git remote add origin "https://github.com/leanprover/workaround"
+
+lake update
+
+cd lake-packages/mathlib
+mathlib_short_git_hash="$(git log -1 --pretty=format:%h)"
+cd ../../
+
+if [ "$(cd ../mathlib4_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF" ]; then
   exit 0
 fi
 
-# generate the docs
-cd $1
-sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\" with NameMap.empty|" lakefile.lean
-# This can destroy caching properties if std4 or aesop master are out of sync with mathlib4 but
-# we need it since lake does not provide the ability to update singular deps
-# right now. Once the feature is implemented we can stop doing that.
-lake -Kdoc=on update
-lake -Kdoc=on build Mathlib:docs Std:docs
+lake exe cache get
+lake build Mathlib:docs Std:docs
 
-if [ "$3" = "true" ]; then
 cd ..
 rm -rf mathlib4_docs/docs/
-  cp -r "$1/build/doc" mathlib4_docs/docs
+cp -r "workaround/build/doc" mathlib4_docs/docs
 mkdir ~/.ssh
 echo "$MATHLIB4_DOCS_KEY" > ~/.ssh/id_ed25519
 chmod 600 ~/.ssh/id_ed25519
@@ -46,4 +44,4 @@ if [ "$3" = "true" ]; then
 git checkout --orphan master2
 git commit -m "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF"
 git push -f origin HEAD:master
-fi
+

lake-manifest.json

@@ -28,6 +28,6 @@
   {"git":
    {"url": "https://github.com/fgdorais/UnicodeData",
     "subDir?": null,
-    "rev": "ece7fa88d13ae92b670e46035119bab89e5225df",
+    "rev": "fb9efcfc2b832c2aff45a220779f35b79f62da11",
     "name": "UnicodeData",
     "inputRev?": "main"}}]}

test_docs.sh

@@ -0,0 +1,17 @@
+# Arguments:
+# $1 : path to std4 from working directory
+# $2 : path to doc-gen4 from working directory
+
+set -e
+set -x
+
+# carry the already built doc-gen4 over
+mkdir -p "$1"/lake-packages
+cp -r "$2"/lake-packages/* "$1"/lake-packages
+
+# generate the docs
+cd "$1"
+sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\" with NameMap.empty|" lakefile.lean
+
+lake -Kdoc=on update
+lake -Kdoc=on build Std:docs