Use glueTrianglesʳ in definition of _∘_ for slice categories #604
Workflow file for this run
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: Ubuntu build | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - master | |
| ######################################################################## | |
| ## CONFIGURATION | |
| ## | |
| ## Key variables: | |
| ## | |
| ## AGDA_VERSION picks the version of Agda to use to build the library. | |
| ## | |
| ## STDLIB_VERSION picks the version of the stdlib to pull. The current | |
| ## design requires that the number corresponds to a released version | |
| ## but we could change that to a commit-based approach if you need to. | |
| ## | |
| ## The rest: | |
| ## | |
| ## The AGDA variable specifies the command to use to build the library. | |
| ## It currently passes the flag `-Werror` to ensure maximal compliance | |
| ## with e.g. not relying on deprecated definitions. | |
| ## The rest are some arbitrary runtime arguments that shape the way Agda | |
| ## allocates and garbage collects memory. It should make things faster. | |
| ## Limits can be bumped if the builds start erroring with out of memory | |
| ## errors. | |
| ## | |
| ######################################################################## | |
| env: | |
| AGDA_VERSION: "2.8.0" | |
| STDLIB_VERSION: "2.3" | |
| AGDA: agda --auto-inline -Werror +RTS -M6G -H3.5G -A128M -RTS -i . -i src/ | |
| jobs: | |
| test-categories: | |
| runs-on: ubuntu-latest | |
| steps: | |
| # By default github actions do not pull the repo | |
| - name: Checkout agda-categories | |
| uses: actions/checkout@v5 | |
| ######################################################################## | |
| ## SETTINGS | |
| ######################################################################## | |
| - name: Initialise variables | |
| run: | | |
| # Only deploy if the build follows from pushing to master | |
| if [[ '${{ github.ref }}' == 'refs/heads/master' ]]; then | |
| echo "AGDA_DEPLOY=true" >> "${GITHUB_ENV}" | |
| fi | |
| ######################################################################## | |
| ## INSTALLATION STEPS | |
| ######################################################################## | |
| - name: Install Agda | |
| uses: agda/agda-setup-action@v1 | |
| id: setup | |
| with: | |
| agda-version: ${{ env.AGDA_VERSION }} | |
| agda-stdlib-version: ${{ env.STDLIB_VERSION }} | |
| ######################################################################## | |
| ## CACHING: RESTORE | |
| ######################################################################## | |
| # This caching step allows us to save a lot of building time by | |
| # saving the previous build. | |
| - name: Restore cache | |
| uses: actions/cache/restore@v4 | |
| id: cache | |
| with: | |
| path: | | |
| ${{ steps.setup.outputs.agda-dir }} | |
| _build | |
| key: ${{ runner.os }}-agda-${{ env.AGDA_VERSION }}-commit-${{ github.sha }} | |
| ######################################################################## | |
| ## TESTING | |
| ######################################################################## | |
| # Generate a fresh Everything.agda & index.agda and start building! | |
| - name: Test agda-categories | |
| run: | | |
| cp travis/* . | |
| ./everything.sh | |
| ${{ env.AGDA }} Everything.agda | |
| ${{ env.AGDA }} index.agda | |
| # Note that if you want to deploy html for different versions like the | |
| # standard library does, you will need to be a bit more subtle in this | |
| # step. | |
| - name: Generate HTML | |
| run: | | |
| ${{ env.AGDA }} --html --html-dir html index.agda | |
| ######################################################################## | |
| ## DEPLOYMENT | |
| ######################################################################## | |
| - name: Deploy HTML | |
| uses: JamesIves/github-pages-deploy-action@v4 | |
| if: success() && env.AGDA_DEPLOY | |
| with: | |
| branch: gh-pages | |
| folder: html | |
| ######################################################################## | |
| ## CACHING: SAVE | |
| ######################################################################## | |
| # This caching step allows us to save a lot of building time by | |
| # saving the previous build. | |
| - name: Save cache | |
| uses: actions/cache/save@v4 | |
| if: always() | |
| with: | |
| path: | | |
| ${{ steps.setup.outputs.agda-dir }} | |
| _build | |
| key: ${{ steps.cache.outputs.cache-primary-key }} |