Merge branch 'leanprover:main' into main

Author: zayn7lie

.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

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",

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 <output_file> <sha> <repo> <run_id>
-  ```