diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a9a40617..0e840e35 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -12,7 +12,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout repo - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: install elan run: | @@ -21,12 +21,10 @@ jobs: ~/.elan/bin/lean --version echo "$HOME/.elan/bin" >> $GITHUB_PATH - - name: Checkout and compile batteries + - name: Checkout batteries run: | cd ../ git clone https://github.com/leanprover-community/batteries - cd batteries - lake build - name: generate docs run: | diff --git a/test_docs.sh b/test_docs.sh index bc3a73d7..430547a7 100755 --- a/test_docs.sh +++ b/test_docs.sh @@ -7,7 +7,7 @@ set -x # generate the docs cd "$1" -sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\"|" lakefile.lean +echo 'require «doc-gen4» from ".." / "doc-gen4"' >> lakefile.lean -lake -R -Kdoc=on update -lake -R -Kdoc=on build Batteries:docs +lake update doc-gen4 +lake build Batteries:docs