introduce total categories #4512
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
| on: [push, pull_request] | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: ${{ github.ref != 'refs/heads/main' }} | |
| name: Build | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| env: | |
| mailmap: ${{ secrets.MAILMAP }} | |
| steps: | |
| - name: Checkout ⬇️ | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 # we need the commit history for authors | |
| - name: Install Nix ❄️ | |
| uses: cachix/install-nix-action@v26 | |
| - name: Set up Cachix ♻️ | |
| uses: cachix/cachix-action@v14 | |
| with: | |
| name: 1lab | |
| authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} | |
| - name: Check that imports are sorted | |
| if: github.event_name == 'pull_request' | |
| run: | | |
| nix run -f . sort-imports | |
| if ! git diff --quiet; then | |
| echo 'Imports are not sorted. Please run `support/sort-imports.hs`.' | |
| exit 1 | |
| fi | |
| - name: Build the Shakefile 🧰 | |
| run: | | |
| hash=$(nix-build -A shakefile --no-out-link) | |
| hash=${hash#/nix/store/} hash=${hash%%-*} | |
| echo "shake_version=$hash" >> "$GITHUB_ENV" | |
| - name: Cache _build ♻️ | |
| uses: actions/cache@v4 | |
| with: | |
| path: _build | |
| key: shake-5-${{ env.shake_version }}-${{ github.run_id }} | |
| restore-keys: shake-5-${{ env.shake_version }}- | |
| - name: Typecheck 👩🏫 | |
| run: | | |
| nix-shell --arg interactive false --run "$build_command" | |
| # Run Agda as a separate stage so it doesn't have to be subject to | |
| # the absolutely spartan GC tuning parameters we run the build in | |
| # CI with | |
| env: | |
| NIX_BUILD_SHELL: bash | |
| build_command: | | |
| set -eu | |
| 1lab-shake _build/all-pages.agda | |
| agda _build/all-pages.agda +RTS -A128M -s -RTS | |
| - name: Build 🛠️ | |
| run: | | |
| echo "$mailmap" > .mailmap | |
| nix-shell --arg interactive false --run "$build_command" | |
| # Shake is a bit of a pig, what with our abuses of caches, and | |
| # the default 2× heap overhead GHC uses means that a clean build | |
| # (with existing interface files) ends up using about ~10 GiB of | |
| # memory. This is probably not entirely unrelated to our CI jobs | |
| # being randomly cancelled. | |
| # | |
| # We can beat it back down into shape by telling GHC to use a | |
| # much lower heap overhead (1.25×) and a smaller allocation area | |
| # size. On my machine using -A128M gives | |
| # | |
| # 3,202,995,288 bytes maximum residency | |
| # 10202 MiB total memory in use | |
| # Productivity 85.4% of total user, 92.8% of total elapsed | |
| # | |
| # but the flags below give | |
| # | |
| # 3,686,172,648 bytes maximum residency (64 sample(s)) | |
| # 5778 MiB total memory in use | |
| # Productivity 68.8% of total user, 64.2% of total elapsed | |
| env: | |
| NIX_BUILD_SHELL: bash | |
| build_command: | | |
| set -eu | |
| 1lab-shake -j all +RTS -F1.25 -A8M | |
| eval "$installPhase" | |
| - name: Upload site ⬆️ | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: _build/site | |
| retention-days: 1 | |
| deploy: | |
| needs: build | |
| if: ${{ github.ref_name == 'main' }} | |
| permissions: | |
| pages: write | |
| id-token: write | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Deploy 🚀 | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |