feat: added new definition of code distance via Set.infsep
#5
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Compile blueprint | |
| on: | |
| push: | |
| branches: | |
| - main # Trigger on pushes to the default branch | |
| workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface | |
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | |
| permissions: | |
| contents: read # Read access to repository contents | |
| pages: write # Write access to GitHub Pages | |
| id-token: write # Write access to ID tokens | |
| jobs: | |
| build_project: | |
| runs-on: ubuntu-latest | |
| name: Build project | |
| steps: | |
| - name: Checkout project | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 # Fetch all history for all branches and tags | |
| - name: Install elan | |
| run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| - name: Get Mathlib cache | |
| run: ~/.elan/bin/lake exe cache get || true | |
| - name: Build project | |
| run: ~/.elan/bin/lake build ZKLib | |
| - name: Cache mathlib API docs | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build/doc/Init | |
| .lake/build/doc/Lake | |
| .lake/build/doc/Lean | |
| .lake/build/doc/Std | |
| .lake/build/doc/Mathlib | |
| .lake/build/doc/declarations | |
| .lake/build/doc/find | |
| .lake/build/doc/*.* | |
| !.lake/build/doc/declarations/declaration-data-ZKLib* | |
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | |
| restore-keys: MathlibDoc- | |
| - name: Build project API documentation | |
| run: ~/.elan/bin/lake -R -Kenv=dev build ZKLib:docs | |
| - name: Check for `home_page` folder # this is meant to detect a Jekyll-based website | |
| id: check_home_page | |
| run: | | |
| if [ -d home_page ]; then | |
| echo "The 'home_page' folder exists in the repository." | |
| echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV | |
| else | |
| echo "The 'home_page' folder does not exist in the repository." | |
| echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV | |
| fi | |
| - name: Build blueprint and copy to `home_page/blueprint` | |
| uses: xu-cheng/texlive-action@v2 | |
| with: | |
| docker_image: ghcr.io/xu-cheng/texlive-full:20231201 | |
| run: | | |
| # Install necessary dependencies and build the blueprint | |
| 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 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 | |
| leanblueprint pdf | |
| mkdir -p home_page | |
| cp blueprint/print/print.pdf home_page/blueprint.pdf | |
| leanblueprint web | |
| cp -r blueprint/web home_page/blueprint | |
| - name: Check declarations mentioned in the blueprint exist in Lean code | |
| run: | | |
| ~/.elan/bin/lake exe checkdecls blueprint/lean_decls | |
| - name: Copy API documentation to `home_page/docs` | |
| run: cp -r .lake/build/doc home_page/docs | |
| - name: Remove unnecessary lake files from documentation in `home_page/docs` | |
| run: | | |
| find home_page/docs -name "*.trace" -delete | |
| find home_page/docs -name "*.hash" -delete | |
| - name: Bundle dependencies | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: home_page | |
| ruby-version: "3.0" # Specify Ruby version | |
| bundler-cache: true # Enable caching for bundler | |
| - name: Build website using Jekyll | |
| if: env.HOME_PAGE_EXISTS == 'true' | |
| working-directory: home_page | |
| run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site | |
| - name: "Upload website (API documentation, blueprint and any home page)" | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }} | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 | |
| - name: Make sure the API documentation cache works | |
| run: mv home_page/docs .lake/build/doc | |