From 8850db19b009c942d7332d7de9a444bb08e29cd3 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 24 Sep 2025 16:49:55 +0200 Subject: [PATCH 1/6] fixiepoo --- .github/workflows/ci.yaml | 43 -------------------- .github/workflows/typecheck.yaml | 68 ++++++++++++++++++++++++++++++++ 2 files changed, 68 insertions(+), 43 deletions(-) create mode 100644 .github/workflows/typecheck.yaml diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c67fc81fcf4..1d8aeb0e398 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -27,49 +27,6 @@ concurrency: cancel-in-progress: true jobs: - typecheck: - if: - ${{ github.event_name == 'workflow_dispatch' || (github.event_name == - 'pull_request' && github.event.pull_request.draft == false) }} - runs-on: ${{ matrix.os }} - strategy: - matrix: - os: [ubuntu-latest] - agda: ['2.7.0'] - steps: - - name: Checkout our repository - uses: actions/checkout@v4 - with: - path: master - - name: Setup Agda - uses: wenkokke/setup-agda@v2.5.0 - with: - agda-version: ${{ matrix.agda }} - - - uses: actions/cache/restore@v4 - 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 }}- - ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}- - - - name: Typecheck library - run: | - cd master - agda --version - make check - - - name: Save Agda build cache - uses: actions/cache/save@v4 - with: - path: master/_build - key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}' - # We're only running the linkcheck renderer, so we don't need to install # any other packages; that gives a warning during building, but doesn't # fail the build. diff --git a/.github/workflows/typecheck.yaml b/.github/workflows/typecheck.yaml new file mode 100644 index 00000000000..f73ff2f1974 --- /dev/null +++ b/.github/workflows/typecheck.yaml @@ -0,0 +1,68 @@ +name: Agda typechecking +on: + # To run this workflow manually + workflow_dispatch: + inputs: + ref: + description: the repository ref to build + required: true + default: master + + pull_request: + branches: + - master + types: + - opened + - reopened + - synchronize + - ready_for_review + +# Cancel previous runs of the same branch +concurrency: + group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}' + cancel-in-progress: true + +jobs: + typecheck: + if: + ${{ github.event_name == 'workflow_dispatch' || (github.event_name == + 'push' && github.ref_name == 'master') || (github.event_name == + 'pull_request' && github.event.pull_request.draft == false) }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest] + agda: ['2.7.0'] + steps: + - name: Checkout our repository + uses: actions/checkout@v4 + with: + path: master + - name: Setup Agda + uses: wenkokke/setup-agda@v2.5.0 + with: + agda-version: ${{ matrix.agda }} + + - uses: actions/cache/restore@v4 + 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 }}- + ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}- + + - name: Typecheck library + run: | + cd master + agda --version + make check + + - name: Save Agda build cache + uses: actions/cache/save@v4 + with: + path: master/_build + key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}' From 005ee13722004501ae6977eb16a470626347d42c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 24 Sep 2025 16:54:46 +0200 Subject: [PATCH 2/6] any `push` event will do --- .github/workflows/typecheck.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/typecheck.yaml b/.github/workflows/typecheck.yaml index f73ff2f1974..b65aeec84c9 100644 --- a/.github/workflows/typecheck.yaml +++ b/.github/workflows/typecheck.yaml @@ -26,8 +26,8 @@ jobs: typecheck: if: ${{ github.event_name == 'workflow_dispatch' || (github.event_name == - 'push' && github.ref_name == 'master') || (github.event_name == - 'pull_request' && github.event.pull_request.draft == false) }} + 'push') || (github.event_name == 'pull_request' && + github.event.pull_request.draft == false) }} runs-on: ${{ matrix.os }} strategy: matrix: From f19657365d12ba2d509e9b18c5bf0e64724673dd Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 24 Sep 2025 17:01:53 +0200 Subject: [PATCH 3/6] remove a parenthesis --- .github/workflows/typecheck.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/typecheck.yaml b/.github/workflows/typecheck.yaml index b65aeec84c9..8877509be3c 100644 --- a/.github/workflows/typecheck.yaml +++ b/.github/workflows/typecheck.yaml @@ -25,8 +25,8 @@ concurrency: jobs: typecheck: if: - ${{ github.event_name == 'workflow_dispatch' || (github.event_name == - 'push') || (github.event_name == 'pull_request' && + ${{ github.event_name == 'workflow_dispatch' || github.event_name == + 'push' || (github.event_name == 'pull_request' && github.event.pull_request.draft == false) }} runs-on: ${{ matrix.os }} strategy: From 0570428360fb80724d990ebb32d574c06db65968 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 24 Sep 2025 17:12:28 +0200 Subject: [PATCH 4/6] rename profiling workflow to "Clean build and profiling of library" --- .github/workflows/{profiling.yaml => clean-build.yaml} | 4 ++-- .github/workflows/typecheck.yaml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) rename .github/workflows/{profiling.yaml => clean-build.yaml} (97%) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/clean-build.yaml similarity index 97% rename from .github/workflows/profiling.yaml rename to .github/workflows/clean-build.yaml index 95db9d7d2d0..37f6d7beb77 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/clean-build.yaml @@ -1,4 +1,4 @@ -name: Profile Library Typechecking +name: Clean build and profiling of library on: push: @@ -10,7 +10,7 @@ concurrency: cancel-in-progress: false jobs: - typecheck-performance: + typecheck-clean: runs-on: ${{ matrix.os }} strategy: matrix: diff --git a/.github/workflows/typecheck.yaml b/.github/workflows/typecheck.yaml index 8877509be3c..9fbce902ad7 100644 --- a/.github/workflows/typecheck.yaml +++ b/.github/workflows/typecheck.yaml @@ -1,4 +1,4 @@ -name: Agda typechecking +name: Typecheck with Agda on: # To run this workflow manually workflow_dispatch: From 3bf06bb69a75611a47d75608ca4ad415b78f80d8 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 25 Sep 2025 15:12:14 +0200 Subject: [PATCH 5/6] disable pre-commit and link-check on pushes to master --- .github/workflows/ci.yaml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 1d8aeb0e398..8dca843bc63 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -8,10 +8,6 @@ on: required: true default: master - push: - branches: - - master - pull_request: branches: - master From 2c016c9479fc925b7f450d6b51cd4123c9e6e5f0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 25 Sep 2025 15:13:42 +0200 Subject: [PATCH 6/6] move `typecheck` back --- .github/workflows/ci.yaml | 44 +++++++++++++++++++++ .github/workflows/typecheck.yaml | 68 -------------------------------- 2 files changed, 44 insertions(+), 68 deletions(-) delete mode 100644 .github/workflows/typecheck.yaml diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 8dca843bc63..5d18bdc5b9f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -23,6 +23,50 @@ concurrency: cancel-in-progress: true jobs: + typecheck: + if: + ${{ github.event_name == 'workflow_dispatch' || github.event_name == + 'push' || (github.event_name == 'pull_request' && + github.event.pull_request.draft == false) }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest] + agda: ['2.7.0'] + steps: + - name: Checkout our repository + uses: actions/checkout@v4 + with: + path: master + - name: Setup Agda + uses: wenkokke/setup-agda@v2.5.0 + with: + agda-version: ${{ matrix.agda }} + + - uses: actions/cache/restore@v4 + 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 }}- + ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}- + + - name: Typecheck library + run: | + cd master + agda --version + make check + + - name: Save Agda build cache + uses: actions/cache/save@v4 + with: + path: master/_build + key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}' + # We're only running the linkcheck renderer, so we don't need to install # any other packages; that gives a warning during building, but doesn't # fail the build. diff --git a/.github/workflows/typecheck.yaml b/.github/workflows/typecheck.yaml deleted file mode 100644 index 9fbce902ad7..00000000000 --- a/.github/workflows/typecheck.yaml +++ /dev/null @@ -1,68 +0,0 @@ -name: Typecheck with Agda -on: - # To run this workflow manually - workflow_dispatch: - inputs: - ref: - description: the repository ref to build - required: true - default: master - - pull_request: - branches: - - master - types: - - opened - - reopened - - synchronize - - ready_for_review - -# Cancel previous runs of the same branch -concurrency: - group: '${{ github.workflow }}-${{ github.head_ref || github.run_id }}' - cancel-in-progress: true - -jobs: - typecheck: - if: - ${{ github.event_name == 'workflow_dispatch' || github.event_name == - 'push' || (github.event_name == 'pull_request' && - github.event.pull_request.draft == false) }} - runs-on: ${{ matrix.os }} - strategy: - matrix: - os: [ubuntu-latest] - agda: ['2.7.0'] - steps: - - name: Checkout our repository - uses: actions/checkout@v4 - with: - path: master - - name: Setup Agda - uses: wenkokke/setup-agda@v2.5.0 - with: - agda-version: ${{ matrix.agda }} - - - uses: actions/cache/restore@v4 - 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 }}- - ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}- - - - name: Typecheck library - run: | - cd master - agda --version - make check - - - name: Save Agda build cache - uses: actions/cache/save@v4 - with: - path: master/_build - key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'