From 7760855bdf661875936874cda1a4ebe34cc4427d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 21 Jan 2026 09:25:03 +0100 Subject: [PATCH 1/2] new CI attempt --- .github/workflows/blueprint.yml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index ec7c169f..8031180b 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -16,9 +16,12 @@ concurrency: # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages permissions: - contents: read # Read access to repository contents - pages: write # Write access to GitHub Pages - id-token: write # Write access to ID tokens + contents: read # Read access to repository contents + pages: write # Write access to GitHub Pages + id-token: write # Write access to ID tokens + issues: write # Write access to issues + pull-requests: write # Write access to pull requests + actions: write # Write access to GitHub Actions jobs: build_project: @@ -44,8 +47,9 @@ jobs: - name: Build and lint project uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0 with: - use-github-cache: false - build-args: :blueprint + build: true + lint: true + mk_all-check: true - name: Compile blueprint and documentation uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26 From 3277035923cdd25b7628f342a229a620d775c174 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Wed, 21 Jan 2026 09:36:13 +0100 Subject: [PATCH 2/2] remove linting step --- .github/workflows/blueprint.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 8031180b..20bc433d 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -48,7 +48,7 @@ jobs: uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0 with: build: true - lint: true + lint: false mk_all-check: true - name: Compile blueprint and documentation