Guruswami-Sudan blueprint. #11
This file contains hidden or 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 ANY branch now | |
| workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface | |
| # pull_request: | |
| # branches: [main] | |
| # 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 | |
| issues: write # Write access to issues | |
| pull-requests: write # Write access to pull requests | |
| jobs: | |
| cancel: | |
| name: "Cancel Previous Runs (CI)" | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: styfle/cancel-workflow-action@0.12.1 | |
| with: | |
| all_but_latest: true | |
| access_token: ${{ github.token }} | |
| check_imported: | |
| name: Check Library File Imports | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: update ArkLib.lean | |
| run: | | |
| git ls-files 'ArkLib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > ArkLib.lean | |
| - name: check that all files are imported | |
| run: git diff --exit-code | |
| 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 ArkLib | |
| - 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: Cache build artifacts and API docs | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build | |
| key: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }} | |
| # Optionally add restore-keys if needed, e.g.: | |
| # restore-keys: LakeBuild-${{ runner.os }}-${{ hashFiles('lean-toolchain') }} | |
| - name: Build project API documentation | |
| # Only build blueprint on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| run: | | |
| ~/.elan/bin/lake -R -Kenv=dev build ArkLib:docs | |
| - name: Check for `home_page` folder # this is meant to detect a Jekyll-based website | |
| # Only build blueprint on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| 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: Copy API documentation to `home_page/docs` | |
| # Only copy docs on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| run: cp -r .lake/build/doc home_page/docs | |
| - name: Remove unnecessary lake files from documentation in `home_page/docs` | |
| # Only remove files on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| run: | | |
| find home_page/docs -name "*.trace" -delete | |
| find home_page/docs -name "*.hash" -delete | |
| - name: Bundle dependencies | |
| # Only bundle on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| uses: ruby/setup-ruby@v1 | |
| with: | |
| working-directory: home_page | |
| ruby-version: "3.4.3" # Specify Ruby version | |
| bundler-cache: true # Enable caching for bundler | |
| - name: Build website using Jekyll | |
| # Only build website on push to main or manual trigger, if home_page exists | |
| if: ((github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch') && 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: Copy API documentation to `home_page/docs` | |
| # Only run this step related to docs on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| run: cp -r .lake/build/doc home_page/docs | |
| - name: "Upload website (API documentation, blueprint and any home page)" | |
| # Only upload artifact on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }} | |
| - name: Deploy to GitHub Pages | |
| # Only deploy on push to main or manual trigger | |
| if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' | |
| id: deployment | |
| uses: actions/deploy-pages@v4 | |
| # lint: | |
| # name: Lint Files | |
| # runs-on: ubuntu-latest | |
| # steps: | |
| # - name: install Python | |
| # if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} | |
| # uses: actions/setup-python@v5 | |
| # with: | |
| # python-version: 3.8 | |
| # - uses: actions/checkout@v4 | |
| # - name: lint | |
| # run: | | |
| # ./scripts/lint-style.sh |