Fiberwise orthogonal maps and closure properties of the right class (… #532
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: Build and deploy library website | |
| on: | |
| # To run this workflow manually | |
| workflow_dispatch: | |
| inputs: | |
| ref: | |
| description: the repository ref to build | |
| required: true | |
| default: master | |
| push: | |
| branches: | |
| - master | |
| # Cancel previous runs of the same branch | |
| concurrency: | |
| group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}' | |
| cancel-in-progress: true | |
| jobs: | |
| website: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| agda: ['2.6.4'] | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| # Grant GITHUB_TOKEN the permissions required to make a Pages deployment | |
| permissions: | |
| pages: write # to deploy to Pages | |
| id-token: write # to verify the deployment originates from an appropriate source | |
| steps: | |
| - name: Checkout our repository | |
| uses: actions/checkout@v3 | |
| with: | |
| path: master | |
| # We need the entire history for contributor information | |
| fetch-depth: 0 | |
| - name: Setup Agda | |
| uses: wenkokke/setup-agda@v2.1.0 | |
| with: | |
| agda-version: ${{ matrix.agda }} | |
| - uses: actions/cache/restore@v3 | |
| id: cache-agda-formalization | |
| name: Restore Agda formalization cache | |
| with: | |
| path: master/_build | |
| key: | |
| ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}-${{ | |
| hashFiles('master/src/**') }} | |
| restore-keys: | | |
| ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}- | |
| # Keep versions in sync with the Makefile | |
| - name: MDBook setup | |
| uses: peaceiris/actions-mdbook@v1 | |
| with: | |
| mdbook-version: '0.4.34' | |
| - name: Install mdbook-pagetoc | |
| uses: baptiste0928/cargo-install@v2 | |
| with: | |
| crate: mdbook-pagetoc | |
| version: '0.1.7' | |
| - name: Install mdbook-katex | |
| uses: baptiste0928/cargo-install@v2 | |
| with: | |
| crate: mdbook-katex | |
| version: '0.5.7' | |
| - name: Install mdbook-linkcheck | |
| uses: baptiste0928/cargo-install@v2 | |
| with: | |
| crate: mdbook-linkcheck | |
| version: '0.7.7' | |
| - name: Install mdbook-catppuccin | |
| uses: baptiste0928/cargo-install@v2 | |
| with: | |
| crate: mdbook-catppuccin | |
| version: '1.2.0' | |
| - uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.8' | |
| check-latest: true | |
| cache: 'pip' | |
| - run: python3 -m pip install -r master/scripts/requirements.txt | |
| - name: Generate book | |
| env: | |
| MDBOOK_PREPROCESSOR__GIT_METADATA__ENABLE: 'true' | |
| run: | | |
| cd master | |
| make website | |
| - name: Setup Pages | |
| uses: actions/configure-pages@v3 | |
| if: >- | |
| github.ref == 'refs/heads/master' || github.event_name == | |
| 'workflow_dispatch' | |
| - name: Upload artifact | |
| uses: actions/upload-pages-artifact@v1 | |
| if: >- | |
| github.ref == 'refs/heads/master' || github.event_name == | |
| 'workflow_dispatch' | |
| with: | |
| path: master/book/html | |
| - name: Deploy to GitHub Pages | |
| uses: actions/deploy-pages@v1 | |
| id: deployment | |
| if: >- | |
| github.ref == 'refs/heads/master' || github.event_name == | |
| 'workflow_dispatch' |