Add Show class
#6225
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 | |
| - experimental | |
| - 'v*-release' | |
| pull_request: | |
| branches: | |
| - master | |
| - experimental | |
| merge_group: | |
| ######################################################################## | |
| ## CONFIGURATION | |
| ## | |
| ## See SETTINGS for the most important configuration variable: AGDA_COMMIT. | |
| ## It has to be defined as a build step because it is potentially branch | |
| ## dependent. | |
| ## | |
| ## As for the rest: | |
| ## | |
| ## Basically do not touch GHC_VERSION and CABAL_VERSION as long as | |
| ## they aren't a problem in the build. If you have time to waste, it | |
| ## could be worth investigating whether newer versions of ghc produce | |
| ## more efficient Agda executable and could cut down the build time. | |
| ## Just be aware that actions are flaky and small variations are to be | |
| ## expected. | |
| ## | |
| ## The CABAL_INSTALL variable only passes `-O1` optimisations to ghc | |
| ## because github actions cannot currently handle a build using `-O2`. | |
| ## To be experimented with again in the future to see if things have | |
| ## gotten better. | |
| ## | |
| ## We mostly use `v1-install` rather than `install` as Agda as a community | |
| ## hasn't figured out how to manage dependencies with the new local | |
| ## style builds (see agda/agda#4627 for details). Once this is resolved | |
| ## we should upgrade to `install`. | |
| ## | |
| ## 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: | |
| GHC_VERSION: 9.12.2 | |
| CABAL_VERSION: 3.16.0.0 | |
| CABAL_V1_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' | |
| CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' | |
| AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc | |
| ######################################################################## | |
| ## SETTINGS | |
| ## | |
| ## AGDA_COMMIT picks the version of Agda to use to build the library. | |
| ## It can either be a hash of a specific commit (to target a bugfix for | |
| ## instance) or a tag e.g. tags/v2.6.1.3 (to target a released version). | |
| ## | |
| ## AGDA_HTML_DIR picks the html/ subdir in which to publish the docs. | |
| ## The content of the html/ directory will be deployed so we put the | |
| ## master version at the root and the experimental in a subdirectory. | |
| ######################################################################## | |
| jobs: | |
| ######################################################################## | |
| ## INITIALISATION | |
| ######################################################################## | |
| init: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| AGDA_COMMIT: ${{ steps.init_vars.outputs.AGDA_COMMIT }} | |
| AGDA_HTML_DIR: ${{ steps.init_vars.outputs.AGDA_HTML_DIR }} | |
| AGDA_DEPLOY: ${{ steps.init_vars.outputs.AGDA_DEPLOY }} | |
| BIN_PATH: ${{ steps.path.outputs.BIN_PATH }} | |
| GHC_PATH: ${{ steps.install-ghc-cabal.outputs.ghc-path }} | |
| steps: | |
| - name: Initialise variables | |
| id: init_vars | |
| run: | | |
| if [[ '${{ github.ref }}' == 'refs/heads/experimental' \ | |
| || '${{ github.base_ref }}' == 'experimental' ]]; then | |
| # Pick Agda version for experimental | |
| echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_OUTPUT}"; | |
| echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_OUTPUT}" | |
| else | |
| # Pick Agda version for master | |
| echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_OUTPUT}"; | |
| echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_OUTPUT}" | |
| fi | |
| if [[ '${{ github.ref }}' == 'refs/heads/master' \ | |
| || '${{ github.ref }}' == 'refs/heads/experimental' ]]; then | |
| echo "AGDA_DEPLOY=true" >> "${GITHUB_OUTPUT}" | |
| fi | |
| ######################################################################## | |
| ## CACHING | |
| ######################################################################## | |
| # This caching step allows us to save a lot of building time by only | |
| # downloading ghc and cabal and rebuilding Agda if absolutely necessary | |
| # i.e. if we change either the version of Agda, ghc, or cabal that we want | |
| # to use for the build. | |
| - name: Cache ~/.cabal directories | |
| uses: actions/cache@v4 | |
| id: cache-cabal | |
| with: | |
| path: | | |
| ~/.cabal/packages | |
| ~/.cabal/store | |
| ~/.cabal/bin | |
| ~/.cabal/share | |
| key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ steps.init_vars.outputs.AGDA_COMMIT }}-cache | |
| ######################################################################## | |
| ## INSTALLATION STEPS | |
| ######################################################################## | |
| - name: Install ghc & cabal | |
| id: install-ghc-cabal | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| ghc-version: ${{ env.GHC_VERSION }} | |
| cabal-version: ${{ env.CABAL_VERSION }} | |
| cabal-update: true | |
| - name: Put cabal programs in PATH | |
| run: | | |
| echo ~/.cabal/bin >> "${GITHUB_PATH}" | |
| echo ${{ steps.install-ghc-cabal.outputs.ghc-path }} >> "${GITHUB_PATH}" | |
| - name: Output PATH | |
| id: path | |
| run: echo "BIN_PATH=$PATH" >> "${GITHUB_OUTPUT}" | |
| - name: Install alex & happy | |
| if: steps.cache-cabal.outputs.cache-hit != 'true' | |
| run: | | |
| ${{ env.CABAL_INSTALL }} alex | |
| ${{ env.CABAL_INSTALL }} happy | |
| # happy>=2.0 cannot be v1-installed: https://github.com/haskell/happy/issues/315 | |
| # Since we only need the executable, it is fine to use v2-install here. | |
| - name: Download and install Agda from github | |
| if: steps.cache-cabal.outputs.cache-hit != 'true' | |
| run: | | |
| git clone https://github.com/agda/agda | |
| cd agda | |
| git checkout ${{ steps.init_vars.outputs.AGDA_COMMIT }} | |
| mkdir -p doc | |
| touch doc/user-manual.pdf | |
| ${{ env.CABAL_V1_INSTALL }} | |
| cd .. | |
| - name: Upload Cabal directory | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: ubuntu-cabal-dir | |
| path: ~/.cabal/ | |
| - name: Upload GHC directory | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| name: ubuntu-ghc-dir | |
| path: ${{ steps.install-ghc-cabal.outputs.ghc-path }} | |
| ######################################################################## | |
| ## TESTING | |
| ######################################################################## | |
| test-stdlib: | |
| needs: init | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v5 | |
| - name: Download Cabal directory | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-cabal-dir | |
| path: ~/.cabal/ | |
| - name: Download GHC directory | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-ghc-dir | |
| path: ${{ needs.init.outputs.GHC_PATH }} | |
| - name: Set permissions | |
| run: | | |
| sudo chmod -R 777 ~/.cabal/bin/ | |
| sudo chmod -R 777 ${{ needs.init.outputs.GHC_PATH }} | |
| - name: Set PATH | |
| run: echo "${{ needs.init.outputs.BIN_PATH }}" >> ${GITHUB_PATH} | |
| - name: Test stdlib | |
| run: | | |
| # Including deprecated modules purely for testing | |
| cabal run GenerateEverything -- --include-deprecated | |
| ${{ env.AGDA }} -WnoUserWarning --safe EverythingSafe.agda | |
| ${{ env.AGDA }} -WnoUserWarning Everything.agda | |
| ######################################################################## | |
| ## GOLDEN TESTING | |
| ######################################################################## | |
| test-stdlib-golden: | |
| needs: init | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v5 | |
| - name: Download Cabal directory | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-cabal-dir | |
| path: ~/.cabal/ | |
| - name: Download GHC directory | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-ghc-dir | |
| path: ${{ needs.init.outputs.GHC_PATH }} | |
| - name: Set permissions | |
| run: | | |
| sudo chmod -R 777 ~/.cabal/bin/ | |
| sudo chmod -R 777 ${{ needs.init.outputs.GHC_PATH }} | |
| - name: Cabal update | |
| run: cabal update | |
| - name: Set PATH | |
| run: echo "${{ needs.init.outputs.BIN_PATH }}" >> ${GITHUB_PATH} | |
| # always restore the cache, cabal will then figure the rest out | |
| - name: Restore cache | |
| uses: actions/cache/restore@v5 | |
| id: restore-golden | |
| with: | |
| path: ./tests/_config/dist-newstyle/ | |
| key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-golden-cache-${{ github.sha }} | |
| restore-keys: | | |
| ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-golden-cache | |
| # compute a hash to be compared against after running golden tests | |
| # if dist-newstyle changes, it means that the cache needs to be updated, so we use as hash to make that comparison | |
| - name: Compute cache hash | |
| id: cache-hash | |
| run: | | |
| { printf "CACHE_HASH=" && echo ${{ hashFiles('tests/_config/dist-newstyle/build/**/*') }} ; } >> ${GITHUB_OUTPUT} | |
| - name: Golden testing | |
| run: | | |
| make testsuite INTERACTIVE='' AGDA_EXEC='agda' GHC_EXEC='ghc' | |
| - name: Compute new cache hash | |
| id: new-cache-hash | |
| run: | | |
| { printf "NEW_CACHE_HASH=" && echo ${{ hashFiles('tests/_config/dist-newstyle/build/**/*') }} ; } >> ${GITHUB_OUTPUT} | |
| - name: Report hashes | |
| run: | | |
| if ${{ steps.cache-hash.outputs.CACHE_HASH == steps.new-cache-hash.outputs.NEW_CACHE_HASH }}; then | |
| echo "Hashes are equal" | |
| else | |
| echo "Hashes are not equal" | |
| fi | |
| printf "Old hash: " | |
| echo ${{ steps.cache-hash.outputs.CACHE_HASH }} | |
| printf "New hash: " | |
| echo ${{ steps.new-cache-hash.outputs.NEW_CACHE_HASH }} | |
| # cache the files built during golden testing, but only on master and if dist-newstyle has changed to prevent the cache overfilling too quickly | |
| - name: Save cache | |
| if: github.ref_name == 'master' && steps.cache-hash.outputs.CACHE_HASH != steps.new-cache-hash.outputs.NEW_CACHE_HASH | |
| uses: actions/cache/save@v5 | |
| id: cache-golden | |
| with: | |
| path: ./tests/_config/dist-newstyle/ | |
| key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-golden-cache-${{ github.sha }} | |
| ######################################################################## | |
| ## DOC DEPLOYMENT | |
| ######################################################################## | |
| html-generate: | |
| needs: init | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v5 | |
| - name: Download Cabal directory | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-cabal-dir | |
| path: ~/.cabal/ | |
| - name: Download GHC directory | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-ghc-dir | |
| path: ${{ needs.init.outputs.GHC_PATH }} | |
| - name: Set permissions | |
| run: | | |
| sudo chmod -R 777 ~/.cabal/bin/ | |
| sudo chmod -R 777 ${{ needs.init.outputs.GHC_PATH }} | |
| - name: Set PATH | |
| run: echo "${{ needs.init.outputs.BIN_PATH }}" >> ${GITHUB_PATH} | |
| - name: Prepare HTML index | |
| run: | | |
| # Regenerating the Everything files without the deprecated modules | |
| cabal run GenerateEverything | |
| cp .github/tooling/* . | |
| ./index.sh | |
| ${{ env.AGDA }} --safe EverythingSafe.agda | |
| ${{ env.AGDA }} Everything.agda | |
| ${{ env.AGDA }} index.agda | |
| # We start by retrieving the currently deployed docs | |
| # We remove the content that is in the directory we are going to populate | |
| # so that stale files corresponding to deleted modules do not accumulate. | |
| # We then generate the docs in the AGDA_HTML_DIR subdirectory | |
| - name: Generate HTML | |
| run: | | |
| git clone --depth 1 --single-branch --branch gh-pages https://github.com/agda/agda-stdlib html | |
| rm -f '${{ needs.init.outputs.AGDA_HTML_DIR }}'/*.html | |
| rm -f '${{ needs.init.outputs.AGDA_HTML_DIR }}'/*.css | |
| ${{ env.AGDA }} --html --html-dir ${{ needs.init.outputs.AGDA_HTML_DIR }} index.agda | |
| cp .github/tooling/* . | |
| ./landing.sh | |
| - name: Upload HTML | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ubuntu-html | |
| include-hidden-files: true | |
| path: ./html/ | |
| html-deploy: | |
| needs: [init, html-generate, test-stdlib-golden, test-stdlib] | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v5 | |
| - name: Download HTML | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ubuntu-html | |
| path: ./html/ | |
| - name: Deploy HTML | |
| uses: JamesIves/github-pages-deploy-action@v4 | |
| if: success() && needs.init.outputs.AGDA_DEPLOY | |
| with: | |
| branch: gh-pages | |
| folder: html | |
| git-config-name: Github Actions | |
| ######################################################################## | |
| ## CLEANUP | |
| ######################################################################## | |
| cleanup: | |
| needs: [html-deploy] | |
| runs-on: ubuntu-latest | |
| if: always() | |
| steps: | |
| - name: Delete artifacts | |
| uses: geekyeggo/delete-artifact@v6 | |
| with: | |
| failOnError: false | |
| name: | | |
| ubuntu-cabal-dir | |
| ubuntu-ghc-dir | |
| ubuntu-html |