diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index ac57954..1ea85e9 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -33,8 +33,8 @@ jobs: - name: Install elan run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none - - name: Update docgen4 - run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4 + # - name: Update doc-gen4 + # run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4» - name: Get cache run: ~/.elan/bin/lake -Kenv=dev exe cache get || true @@ -54,32 +54,23 @@ jobs: .lake/build/doc/declarations !.lake/build/doc/declarations/declaration-data-BonnAnalysis* key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} - restore-keys: | - MathlibDoc- + #restore-keys: MathlibDoc- - name: Build project documentation run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs - - name: Cache blueprint environment - uses: actions/cache@v3 - with: - path: | - ~/texlive-env - key: texlive-env-${{ hashFiles('blueprint/*') }} - restore-keys: | - texlive-env- - - name: Build blueprint and copy to `docs/blueprint` uses: xu-cheng/texlive-action@v2 with: docker_image: ghcr.io/xu-cheng/texlive-full:20231201 run: | + export PIP_BREAK_SYSTEM_PACKAGES=1 apk update apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev git config --global --add safe.directory $GITHUB_WORKSPACE git config --global --add safe.directory `pwd` - python3 -m venv ~/texlive-env || true - source ~/texlive-env/bin/activate + python3 -m venv env + source env/bin/activate pip install --upgrade pip requests wheel pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" pip install leanblueprint @@ -88,16 +79,12 @@ jobs: leanblueprint web cp -r blueprint/web docs/blueprint - # - name: Check declarations - # run: | - # ~/.elan/bin/lake exe checkdecls blueprint/lean_decls - - name: Remove lake files from documentation run: | find .lake/build/doc -name "*.trace" -delete find .lake/build/doc -name "*.hash" -delete - - name: Move documentation to `docs/docs` + - name: Copy documentation to `docs/docs` run: | sudo chown -R runner docs cp -r .lake/build/doc docs/docs @@ -113,11 +100,19 @@ jobs: working-directory: docs run: JEKYLL_ENV=production bundle exec jekyll build - - name: Upload docs & blueprint artifact + # - name: Upload docs & blueprint artifact to `docs/` + # uses: actions/upload-pages-artifact@v1 + # with: + # path: docs/ + + - name: Upload docs & blueprint artifact to `docs/_site` uses: actions/upload-pages-artifact@v1 with: path: docs/_site - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v1 \ No newline at end of file + uses: actions/deploy-pages@v1 + + - name: Make sure the cache works + run: mv docs/docs .lake/build/doc \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index 2580094..ff60eda 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446", + "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b387c548d1dc9cea5c5fcb71e5b3370cca1a04cc", + "rev": "363b8176ac29271af4b000b649f836c846f528fc", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5cf3352cd6090e58c5ee878c786af8b87e8bdd65", + "rev": "7aa0886dc3f8dd486e00c19589d28c5bc0d7d860", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main",