From 0c415232cd921b4134c1913c95211f111d3644b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 11 Mar 2023 17:48:27 +0100 Subject: [PATCH] feat: new CI setup --- .github/workflows/build.yml | 29 +++--------- .github/workflows/mathlib4docs.yml | 29 ++++++++++++ DocGen4/Output/Index.lean | 3 +- deploy_docs.sh | 76 +++++++++++++++--------------- lake-manifest.json | 2 +- test_docs.sh | 17 +++++++ 6 files changed, 93 insertions(+), 63 deletions(-) create mode 100644 .github/workflows/mathlib4docs.yml create mode 100755 test_docs.sh diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 60baefa..8bdf61b 100644 --- a/.github/workflows/build.yml +++ b/.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" diff --git a/.github/workflows/mathlib4docs.yml b/.github/workflows/mathlib4docs.yml new file mode 100644 index 0000000..5e75fb6 --- /dev/null +++ b/.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 }} diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index 270daf7..0bc21d5 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -16,7 +16,8 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|

Welcome to the documentation page

-

This was built for commit {s!"{← getProjectCommit} "} using Lean 4 at commit {Lean.githash}

+ -- Temporary comment until the lake issue is resolved +

This was built /-for commit {s!"{← getProjectCommit} "}-/ using Lean 4 at commit {Lean.githash}

end Output diff --git a/deploy_docs.sh b/deploy_docs.sh index 61f1a99..9d910e9 100755 --- a/deploy_docs.sh +++ b/deploy_docs.sh @@ -1,49 +1,47 @@ -# 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 + +cd .. +rm -rf 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 +cd mathlib4_docs/docs +git remote set-url origin "git@github.com:leanprover-community/mathlib4_docs.git" +git config user.email "leanprover.community@gmail.com" +git config user.name "leanprover-community-bot" +git add -A . +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 -if [ "$3" = "true" ]; then - cd .. - rm -rf mathlib4_docs/docs/ - cp -r "$1/build/doc" mathlib4_docs/docs - mkdir ~/.ssh - echo "$MATHLIB4_DOCS_KEY" > ~/.ssh/id_ed25519 - chmod 600 ~/.ssh/id_ed25519 - cd mathlib4_docs/docs - git remote set-url origin "git@github.com:leanprover-community/mathlib4_docs.git" - git config user.email "leanprover.community@gmail.com" - git config user.name "leanprover-community-bot" - git add -A . - 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 diff --git a/lake-manifest.json b/lake-manifest.json index 024374b..9c8bded 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -28,6 +28,6 @@ {"git": {"url": "https://github.com/fgdorais/UnicodeData", "subDir?": null, - "rev": "ece7fa88d13ae92b670e46035119bab89e5225df", + "rev": "fb9efcfc2b832c2aff45a220779f35b79f62da11", "name": "UnicodeData", "inputRev?": "main"}}]} diff --git a/test_docs.sh b/test_docs.sh new file mode 100755 index 0000000..c805de3 --- /dev/null +++ b/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