docs: improve release_steps.py usage documentation and help messages

A step towards automating the release process.
Somewhat following the idea of
https://blog.danslimmon.com/2019/07/15/do-nothing-scripting-the-key-to-gradual-automation/

doc/dev/release_checklist.md

@@ -41,6 +41,10 @@ We'll use `v4.6.0` as the intended release version as a running example.
   - In order to have the access rights to push to these repositories and merge PRs,
     you will need to be a member of the `lean-release-managers` team at both `leanprover-community` and `leanprover`.
     Contact Kim Morrison (@kim-em) to arrange access.
+  - There is an experimental script that will guide you through the steps for each of the repositories below.
+    The script should be invoked as
+    `script/release_steps.py vx.y.x <repo>` where `<repo>` is a case-insensitive substring of the repo name.
+    For example: `script/release_steps.py v4.6.0 batt` will guide you through the steps for the Batteries repository.
   - For each of the repositories listed below:
     - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
       - The usual branch name would be `bump_to_v4.6.0`.

script/release_steps.py

@@ -0,0 +1,140 @@
+#!/usr/bin/env python3
+
+"""
+Generate release steps script for Lean4 repositories.
+
+This script helps automate the release process for Lean4 and its dependent repositories
+by generating step-by-step instructions for updating toolchains, creating tags,
+and managing branches.
+
+Usage:
+    python3 release_steps.py <version> <repo>
+
+Arguments:
+    version: The version to set in the lean-toolchain file (e.g., v4.6.0)
+    repo: A substring of the repository name as specified in release_repos.yml
+
+Example:
+    python3 release_steps.py v4.6.0 mathlib
+    python3 release_steps.py v4.6.0 batt
+
+The script reads repository configurations from release_repos.yml in the same directory.
+Each repository may have specific requirements for:
+- Branch management
+- Toolchain updates
+- Dependency updates
+- Tagging conventions
+- Stable branch handling
+"""
+
+import argparse
+import yaml
+import os
+import sys
+import re
+
+def load_repos_config(file_path):
+    with open(file_path, "r") as f:
+        return yaml.safe_load(f)["repositories"]
+
+def find_repo(repo_substring, config):
+    pattern = re.compile(re.escape(repo_substring), re.IGNORECASE)
+    matching_repos = [r for r in config if pattern.search(r["name"])]
+    if not matching_repos:
+        print(f"Error: No repository matching '{repo_substring}' found in configuration.")
+        sys.exit(1)
+    if len(matching_repos) > 1:
+        print(f"Error: Multiple repositories matching '{repo_substring}' found in configuration: {', '.join(r['name'] for r in matching_repos)}")
+        sys.exit(1)
+    return matching_repos[0]
+
+def generate_script(repo, version, config):
+    repo_config = find_repo(repo, config)
+    repo_name = repo_config['name']
+    default_branch = repo_config.get("branch", "main")
+    dependencies = repo_config.get("dependencies", [])
+    requires_tagging = repo_config.get("toolchain-tag", True)
+    has_stable_branch = repo_config.get("stable-branch", True)
+
+    script_lines = [
+        f"cd {repo_name}",
+        "git fetch",
+        f"git checkout {default_branch}",
+        f"git checkout -b bump_to_{version}",
+        f"echo leanprover/lean4:{version} > lean-toolchain",
+    ]
+
+    # Special cases for specific repositories
+    if repo_name == "REPL":
+        script_lines.extend([
+            "cd test/Mathlib",
+            f"echo leanprover/lean4:{version} > lean-toolchain",
+            'echo "Please update the dependencies in lakefile.{lean,toml}"',
+            "lake update",
+            "cd ../.."
+        ])
+    elif dependencies:
+        script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"')
+
+    script_lines.append("lake update")
+    script_lines.append("")
+
+    if not re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
+        script_lines.extend([
+            "echo 'This repo has nightly-testing infrastructure'",
+            f"git merge bump/{version}",
+            "echo 'Please resolve any conflicts.'",
+            ""
+        ])
+
+    script_lines.extend([
+        f'git commit -am "chore: bump toolchain to {version}"',
+        "gh pr create",
+        "echo 'Please review the PR and merge it.'",
+        ""
+    ])
+
+    # Special cases for specific repositories
+    if repo_name == "ProofWidgets4":
+        script_lines.append(f"echo 'Note: Follow the version convention of the repository for tagging.'")
+    elif requires_tagging:
+        script_lines.append(f"git tag -a {version} -m 'Release {version}'")
+        script_lines.append("git push origin --tags")
+
+    if has_stable_branch:
+        script_lines.extend([
+            "git checkout stable",
+            f"git merge {version}",
+            "git push origin stable"
+        ])
+
+    return "\n".join(script_lines)
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Generate release steps script for Lean4 repositories.",
+        formatter_class=argparse.RawDescriptionHelpFormatter,
+        epilog="""
+Examples:
+  %(prog)s v4.6.0 mathlib    Generate steps for updating Mathlib to v4.6.0
+  %(prog)s v4.6.0 batt       Generate steps for updating Batteries to v4.6.0
+  
+The script will generate shell commands to:
+1. Update the lean-toolchain file
+2. Create appropriate branches and commits
+3. Create pull requests
+4. Create version tags
+5. Update stable branches where applicable"""
+    )
+    parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)")
+    parser.add_argument("repo", help="A substring of the repository name as specified in release_repos.yml")
+    args = parser.parse_args()
+
+    config_path = os.path.join(os.path.dirname(__file__), "release_repos.yml")
+    config = load_repos_config(config_path)
+
+    script = generate_script(args.repo, args.version, config)
+    print(script)
+
+if __name__ == "__main__":
+    main()