Build, Test, and Benchmark #186
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
| ###################################################### | |
| ## ## | |
| ## !!!! Autogenerated YAML file, do not edit !!!! ## | |
| ## ## | |
| ## Edit source in /src/github/workflows/ instead! ## | |
| ## ## | |
| ###################################################### | |
| env: | |
| AGDA_TESTS_OPTIONS: -j${PARALLEL_TESTS} --hide-successes | |
| GHC_VER: 9.14.1 | |
| PARALLEL_TESTS: 2 | |
| STACK: stack --system-ghc | |
| TASTY_ANSI_TRICKS: 'false' | |
| jobs: | |
| build: | |
| if: | | |
| !contains(github.event.head_commit.message, '[skip ci]') | |
| && !contains(github.event.head_commit.message, '[ci skip]') | |
| && !contains(github.event.head_commit.message, '[github skip]') | |
| && !contains(github.event.head_commit.message, '[skip github]') | |
| || github.event_name == 'schedule' | |
| || github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - name: Info about the context | |
| run: | | |
| echo "github.base_ref = ${{ github.base_ref }}" | |
| echo "github.head_ref = ${{ github.head_ref }}" | |
| echo "github.event_name = ${{ github.event_name }}" | |
| echo "github.ref = ${{ github.ref }}" | |
| echo "github.ref_name = ${{ github.ref_name }}" | |
| echo "github.ref_type = ${{ github.ref_type }}" | |
| - if: github.ref != 'refs/heads/master' | |
| uses: styfle/cancel-workflow-action@0.13.1 | |
| with: | |
| access_token: ${{ github.token }} | |
| - uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - id: setup-haskell | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| cabal-update: false | |
| enable-stack: true | |
| ghc-version: ${{ env.GHC_VER }} | |
| stack-version: latest | |
| - name: Copy stack-${{ env.GHC_VER}}.yaml to stack.yaml | |
| run: cp stack-${{ env.GHC_VER }}.yaml stack.yaml | |
| - name: Update package index | |
| run: | | |
| ${STACK} update | |
| - name: List dependencies and versions | |
| run: | | |
| ${STACK} ls dependencies | tee deps.txt | |
| - name: Determine the ICU version | |
| run: | | |
| ICU_VER=$(pkg-config --modversion icu-i18n) | |
| echo "ICU_VER=${ICU_VER}" | |
| echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}" | |
| - id: cache | |
| name: Restore cache from approximate key | |
| uses: actions/cache/restore@v5 | |
| with: | |
| key: test.yml-1-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{ | |
| steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{ | |
| hashFiles('Agda.cabal','stack.yaml','deps.txt') }} | |
| path: ${{ steps.setup-haskell.outputs.stack-root }} | |
| restore-keys: test.yml-1-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{ | |
| steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}- | |
| - name: Install dependencies for Agda and its test suites | |
| run: make install-deps | |
| - name: Build Agda | |
| run: make install-bin | |
| - name: Pack artifacts | |
| run: | | |
| tar --use-compress-program zstd --absolute-names -cvf stack.tzst ${{ steps.setup-haskell.outputs.stack-root }} | |
| tar --use-compress-program zstd -cvf stack-work.tzst .stack-work stack.yaml stack.yaml.lock deps.txt | |
| - name: Upload artifacts | |
| uses: actions/upload-artifact@v7 | |
| with: | |
| if-no-files-found: error | |
| name: agda-${{ runner.os }}-${{ github.sha }} | |
| path: | | |
| stack.tzst | |
| stack-work.tzst | |
| retention-days: 1 | |
| - if: steps.cache.outputs.cache-hit != 'true' | |
| name: Save cache | |
| uses: actions/cache/save@v5 | |
| with: | |
| key: test.yml-1-ghc-${{ steps.setup-haskell.outputs.ghc-version }}-stack-${{ | |
| steps.setup-haskell.outputs.stack-version }}-icu-${{ env.ICU_VER }}-plan-${{ | |
| hashFiles('Agda.cabal','stack.yaml','deps.txt') }} | |
| path: ${{ steps.setup-haskell.outputs.stack-root }} | |
| cubical: | |
| needs: build | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - id: setup-haskell | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| cabal-update: false | |
| enable-stack: true | |
| ghc-version: ${{ env.GHC_VER }} | |
| stack-version: latest | |
| - uses: actions/download-artifact@v8 | |
| with: | |
| name: agda-${{ runner.os }}-${{ github.sha }} | |
| - name: Unpack artifacts | |
| run: | | |
| tar --use-compress-program zstd --absolute-names -xvf stack.tzst | |
| tar --use-compress-program zstd -xvf stack-work.tzst | |
| - name: Setup Agda | |
| run: make setup-agda | |
| - name: Cubical library test | |
| run: make cubical-test | |
| - name: Successful tests using the cubical library | |
| run: make cubical-succeed | |
| interaction-latex-html: | |
| needs: build | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - id: setup-haskell | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| cabal-update: false | |
| enable-stack: true | |
| ghc-version: ${{ env.GHC_VER }} | |
| stack-version: latest | |
| - uses: actions/download-artifact@v8 | |
| with: | |
| name: agda-${{ runner.os }}-${{ github.sha }} | |
| - name: Unpack artifacts | |
| run: | | |
| tar --use-compress-program zstd --absolute-names -xvf stack.tzst | |
| tar --use-compress-program zstd -xvf stack-work.tzst | |
| - name: Determine the ICU version | |
| run: | | |
| ICU_VER=$(pkg-config --modversion icu-i18n) | |
| echo "ICU_VER=${ICU_VER}" | |
| echo "ICU_VER=${ICU_VER}" >> "${GITHUB_ENV}" | |
| - name: Setup Agda | |
| run: make setup-agda | |
| - name: Install Tex Live and Emacs | |
| run: | | |
| sudo apt-get update | |
| # shellcheck disable=SC2086 | |
| sudo apt-get install ${APT_GET_OPTS} texlive-binaries emacs-nox | |
| - name: Test agda --build-library (successful) | |
| run: make build-succeed-test | |
| - if: always() | |
| name: Test agda --build-library (failing) | |
| run: make build-fail-test | |
| - if: always() | |
| name: Suite of tests for the LaTeX and HTML backends | |
| run: make DONT_RUN_LATEX=Y latex-html-test | |
| - if: always() | |
| name: Testing the Emacs mode | |
| run: make testing-emacs-mode | |
| - if: always() | |
| name: User manual (test) | |
| run: make user-manual-test | |
| - if: always() | |
| name: User manual covers all options | |
| run: make user-manual-covers-options | |
| - if: always() | |
| name: User manual covers all warnings | |
| run: make user-manual-covers-warnings | |
| - if: always() | |
| name: Test suite covers all warnings | |
| run: make test-suite-covers-warnings | |
| - if: always() | |
| name: Test suite covers all errors | |
| run: make test-suite-covers-errors | |
| - if: always() | |
| name: Suite of interaction tests | |
| run: make interaction | |
| stdlib-test: | |
| needs: build | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - id: setup-haskell | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| cabal-update: false | |
| enable-stack: true | |
| ghc-version: ${{ env.GHC_VER }} | |
| stack-version: latest | |
| - uses: actions/download-artifact@v8 | |
| with: | |
| name: agda-${{ runner.os }}-${{ github.sha }} | |
| - name: Unpack artifacts | |
| run: | | |
| tar --use-compress-program zstd --absolute-names -xvf stack.tzst | |
| tar --use-compress-program zstd -xvf stack-work.tzst | |
| - name: Setup Agda | |
| run: make setup-agda | |
| - name: Parallel standard library build | |
| run: | | |
| # ASR (2021-01-17). `cabal update` is required due to #5138. | |
| # We should also use `stack` in this test. | |
| cabal update | |
| make AGDA_OPTS="-j" std-lib-test | |
| - if: always() | |
| name: Benchmark | |
| run: | | |
| make benchmark-without-logs | |
| make benchmark-summary | |
| - name: Standard library compiler tests | |
| run: make std-lib-compiler-test | |
| - name: Successful tests using the standard library | |
| run: make std-lib-succeed | |
| - name: Interaction tests using the standard library | |
| run: make std-lib-interaction | |
| test: | |
| needs: build | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - id: setup-haskell | |
| uses: haskell-actions/setup@v2 | |
| with: | |
| cabal-update: false | |
| enable-stack: true | |
| ghc-version: ${{ env.GHC_VER }} | |
| stack-version: latest | |
| - uses: actions/download-artifact@v8 | |
| with: | |
| name: agda-${{ runner.os }}-${{ github.sha }} | |
| - name: Unpack artifacts | |
| run: | | |
| tar --use-compress-program zstd --absolute-names -xvf stack.tzst | |
| tar --use-compress-program zstd -xvf stack-work.tzst | |
| - name: Setup Agda | |
| run: make setup-agda | |
| - name: Suite of tests for bugs | |
| run: make bugs | |
| - if: always() | |
| name: 'Suite of successful tests: mini-library Common' | |
| run: make common | |
| - if: always() | |
| name: Suite of successful tests | |
| run: make succeed | |
| - if: always() | |
| name: Suite of failing tests | |
| run: make fail | |
| - if: always() | |
| name: Suite of examples | |
| run: make examples | |
| - if: always() | |
| name: Suite of interactive tests | |
| run: make interactive | |
| - if: always() | |
| name: Successful tests using Agda as a Haskell library | |
| run: make api-test | |
| - if: always() | |
| name: Internal test suite | |
| run: make internal-tests | |
| - if: always() | |
| name: Compiler tests | |
| run: make compiler-test | |
| name: Build, Test, and Benchmark | |
| 'on': | |
| pull_request: | |
| paths: | |
| - '**' | |
| - '!.github/**' | |
| - .github/workflows/test.yml | |
| - '!src/github/**' | |
| - src/github/workflows/test.yml | |
| - '!doc/**' | |
| - doc/user-manual/**/*.lagda.rst | |
| - '!src/agda-bisect/**' | |
| - '!src/fix-whitespace/**' | |
| - '!src/hs-tags/**' | |
| - '!src/release-tools/**' | |
| - '!.travis' | |
| - '!macros/**' | |
| - '!notes/**' | |
| - '!.mailmap' | |
| - '!.gitignore' | |
| - '!.hlint.yaml' | |
| - '!.readthedocs.yaml' | |
| - '!.travis.yml' | |
| - '!CHANGELOG.md' | |
| - '!HACKING.md' | |
| - '!LICENSE' | |
| - '!README.md' | |
| - '!fix-whitespace.yaml' | |
| - '!hie*.yaml' | |
| - '!stack-*.yaml' | |
| - '!touchup.sh' | |
| - '!CITATION.cff' | |
| push: | |
| branches: | |
| - master | |
| - ci-* | |
| - release* | |
| paths: | |
| - '**' | |
| - '!.github/**' | |
| - .github/workflows/test.yml | |
| - '!src/github/**' | |
| - src/github/workflows/test.yml | |
| - '!doc/**' | |
| - doc/user-manual/**/*.lagda.rst | |
| - '!src/agda-bisect/**' | |
| - '!src/fix-whitespace/**' | |
| - '!src/hs-tags/**' | |
| - '!src/release-tools/**' | |
| - '!.travis' | |
| - '!macros/**' | |
| - '!notes/**' | |
| - '!.mailmap' | |
| - '!.gitignore' | |
| - '!.hlint.yaml' | |
| - '!.readthedocs.yaml' | |
| - '!.travis.yml' | |
| - '!CHANGELOG.md' | |
| - '!HACKING.md' | |
| - '!LICENSE' | |
| - '!README.md' | |
| - '!fix-whitespace.yaml' | |
| - '!hie*.yaml' | |
| - '!stack-*.yaml' | |
| - '!touchup.sh' | |
| - '!CITATION.cff' | |
| schedule: | |
| - cron: 0 0 * * 0 | |
| workflow_dispatch: null |