8000 cslib/scripts at split-runner · leanprover/cslib · GitHub
[go: up one dir, main page]
Skip to content

Latest commit

 

History

History
 
 

scripts

README.md

Scripts for working on cslib

This directory contains miscellaneous scripts that are useful for working on or with cslib. When adding a new script, please make sure to document it here, so other readers have a chance to learn about it as well!

Current scripts and their purpose

Documentation generation

  • gendocs.sh Generates the documentation for cslib using lake.

Managing nightly-testing and bump branches

  • create-adaptation-pr.sh is a variant of the script from Batteries and implements some of the steps in the workflow for managing nightly and bump branches.

    Specifically, it will:

    • merge main into bump/v4.x.y
    • create a new branch from bump/v4.x.y, called bump/nightly-YYYY-MM-DD
    • merge nightly-testing into the new branch
    • open a PR to merge the new branch back into bump/v4.x.y
    • announce the PR on zulip
    • finally, merge the new branch back into nightly-testing, if conflict resolution was required.

    If there are merge conflicts, it pauses and asks for help from the human driver.

    Usage:

    ./scripts/create-adaptation-pr.sh <BUMPVERSION> <NIGHTLYDATE>

    or with named parameters:

    ./scripts/create-adaptation-pr.sh --bumpversion=<BUMPVERSION> --nightlydate=<NIGHTLYDATE> --nightlysha=<SHA> [--auto=<yes|no>]

    Parameters:

    • BUMPVERSION: The upcoming release that we are targeting, e.g., 'v4.10.0'
    • NIGHTLYDATE: The date of the nightly toolchain currently used on 'nightly-testing'
    • NIGHTLYSHA: The SHA of the nightly toolchain that we want to adapt to
    • AUTO: Optional flag to specify automatic mode, default is 'no'

    Requirements:

    • gh (GitHub CLI) must be installed and authenticated
    • Optional: zulip-send CLI for automatic Zulip notifications

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 scripts/weekly_lint_report.sh <output_file> <sha> <repo> <run_id>
0