From e9047eadd5f48daf421b9014d5a98623ccc75bdf Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sun, 12 Apr 2026 08:57:32 -0400 Subject: [PATCH] feat: use full weeklyLintSet and mathlib-ci --- .github/workflows/weekly-lints.yml | 29 ++++++++-- lake-manifest.json | 6 +- scripts/README.md | 10 ---- scripts/weekly_lint_report.sh | 90 ------------------------------ 4 files changed, 27 insertions(+), 108 deletions(-) delete mode 100755 scripts/weekly_lint_report.sh diff --git a/.github/workflows/weekly-lints.yml b/.github/workflows/weekly-lints.yml index 57a22ff048..42462e34ef 100644 --- a/.github/workflows/weekly-lints.yml +++ b/.github/workflows/weekly-lints.yml @@ -5,20 +5,35 @@ on: - cron: '0 5 * * 1' # Run at 05:00 UTC every Monday workflow_dispatch: # Allow manual triggering +env: + CSLIB: cslib + jobs: weekly-lints: name: Weekly Linting runs-on: ubuntu-latest if: github.repository == 'leanprover/cslib' steps: + - name: Checkout Mathlib actions + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 1 + repository: leanprover-community/mathlib4 + sparse-checkout: .github/actions + path: workflow-actions + + - name: Get mathlib-ci + uses: ./workflow-actions/.github/actions/get-mathlib-ci + - uses: actions/checkout@v4 with: - ref: main + path: ${{ env.CSLIB }} - name: Enable weekly linters + working-directory: ${{ github.workspace }}/${{ env.CSLIB }} run: | # Add the mergeWithGrind linter back for this run - sed -i '/^\[leanOptions\]/a weak.linter.tacticAnalysis.mergeWithGrind = true' lakefile.toml + sed -i '/^\[leanOptions\]/a weak.linter.weeklyLintSet = true' lakefile.toml # Show what changed git diff lakefile.toml @@ -29,17 +44,21 @@ jobs: auto-config: false use-github-cache: true use-mathlib-cache: true + lake-package-directory: ${{ env.CSLIB }} - name: Build with weekly linters id: build + working-directory: ${{ github.workspace }}/${{ env.CSLIB }} continue-on-error: true run: | lean_outfile=$(mktemp) (lake build || true) 2>&1 | tee "${lean_outfile}" - # Generate report for Zulip - bash scripts/weekly_lint_report.sh "${lean_outfile}" \ - "${{ github.sha }}" "${{ github.repository }}" "${{ github.run_id }}" > "${GITHUB_OUTPUT}" + # Process output for posting to Zulip + SHA=${{ github.sha }} \ + REPO=${{ github.repository }} \ + RUN_ID=${{ github.run_id }} \ + "${CI_SCRIPTS_DIR}/reporting/zulip_build_report.sh" "${lean_outfile}" > "${GITHUB_OUTPUT}" - name: Post output to Zulip uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 diff --git a/lake-manifest.json b/lake-manifest.json index 6699e262e3..d9898a180a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ae0c6140a8312511dbb5bc265a0146dd418eca8d", + "rev": "3d8100bbc657181d1f48868decaba9159580aa40", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3", + "rev": "a3b459a8312125758e51c354b93d54ba620efda6", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7", + "rev": "4411c5f89c797401c609b3a946c8874569e69731", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/scripts/README.md b/scripts/README.md index df8e55c302..19d71dfa67 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -45,13 +45,3 @@ to learn about it as well! **Init Imports** - `CheckInitImports.lean` (run by `lake exe checkInitImports`) checks that all files transitively import `Cslib.Init`. - -**Linting** -- `weekly_lint_report.sh` - Generates a summary of the weekly lint run for posting to Zulip. Called by the `weekly-lints.yml` workflow. - The output format matches Mathlib's weekly linting reports, with tables showing grouped message counts. - - **Usage:** - ```bash - bash scripts/weekly_lint_report.sh - ``` diff --git a/scripts/weekly_lint_report.sh b/scripts/weekly_lint_report.sh deleted file mode 100755 index ca8bf31ce7..0000000000 --- a/scripts/weekly_lint_report.sh +++ /dev/null @@ -1,90 +0,0 @@ -#!/bin/bash -# Weekly lint report generator for CSLib. -# -# Parses Lean build output and generates a Zulip-formatted report with tables -# showing grouped message counts. Output format matches Mathlib's weekly linting reports. -# -# Usage: weekly_lint_report.sh - -set -euo pipefail - -lean_outfile=$1 -sha=$2 -repo=$3 -run_id=$4 - -short_sha=${sha:0:7} - -# Filter out build progress and trace lines -filtered_out=$(grep -v '^✔' "${lean_outfile}" | grep -v '^trace: ' | grep -v 'checking out revision' || true) -echo "$(echo "${filtered_out}" | grep -c '' || echo 0) lines of output" >&2 - -# Extract and count messages by type -error_lines=$(echo "${filtered_out}" | grep '^error: ' || true) -warning_lines=$(echo "${filtered_out}" | grep '^warning: ' || true) -info_lines=$(echo "${filtered_out}" | grep '^info: ' || true) - -# Strip prefix and file:line:col to get just descriptions -error_descriptions=$(echo "${error_lines}" | sed 's/^error: [^:]*:[0-9]*:[0-9]*: //' | sed 's/^error: //' || true) -warning_descriptions=$(echo "${warning_lines}" | sed 's/^warning: [^:]*:[0-9]*:[0-9]*: //' | sed 's/^warning: //' || true) -info_descriptions=$(echo "${info_lines}" | sed 's/^info: [^:]*:[0-9]*:[0-9]*: //' | sed 's/^info: //' || true) - -# Count non-empty lines -count_lines() { - local input="$1" - if [ -z "${input}" ]; then - echo 0 - else - echo "${input}" | grep -c '' || echo 0 - fi -} - -# Format descriptions as markdown table rows, grouped and sorted by count -format_table_rows() { - sort | uniq -c | sort -bgr | sed 's/^ *\([0-9][0-9]*\) \(.*\)$/| \1 | \2 |/' -} - -# Combine all descriptions -all_descriptions=$(printf '%s\n%s\n%s' "${error_descriptions}" "${warning_descriptions}" "${info_descriptions}" | grep -v '^$' || true) - -error_count=$(count_lines "${error_lines}") -warning_count=$(count_lines "${warning_lines}") -info_count=$(count_lines "${info_lines}") - -echo "${error_count} errors" >&2 -echo "${warning_count} warnings" >&2 -echo "${info_count} info messages" >&2 - -# Output in GitHub Actions multiline format -delimiter=$(uuidgen 2>/dev/null || cat /proc/sys/kernel/random/uuid 2>/dev/null || echo "EOF_${RANDOM}") -echo "zulip-message<<${delimiter}" - -echo "CSLib weekly lint run [completed](https://github.com/${repo}/actions/runs/${run_id}) ([${short_sha}](https://github.com/${repo}/commit/${sha}))." - -if [ "${error_count}" -eq 0 ] && [ "${warning_count}" -eq 0 ] && [ "${info_count}" -eq 0 ]; then - echo "Build completed without lint messages." -else - # Summary counts - if [ "${error_count}" -gt 0 ]; then - echo " Errors: ${error_count}" - fi - if [ "${warning_count}" -gt 0 ]; then - echo " Warnings: ${warning_count}" - fi - if [ "${info_count}" -gt 0 ]; then - echo " Info messages: ${info_count}" - fi - echo - - # Detail table - if [ -n "${all_descriptions}" ]; then - echo "\`\`\`spoiler Lint message counts" - echo "| | Message |" - echo "| ---: | --- |" - echo "${all_descriptions}" | format_table_rows - echo "\`\`\`" - echo - fi -fi - -echo "${delimiter}"