diff --git a/.claude/skills/release-highlights/SKILL.md b/.claude/skills/release-highlights/SKILL.md new file mode 100644 index 0000000000..f3bf1631c8 --- /dev/null +++ b/.claude/skills/release-highlights/SKILL.md @@ -0,0 +1,200 @@ +--- +name: release-highlights +description: Write the Highlights section for Lean 4 release notes. Use when asked to write, draft, or update release highlights for a Lean version. +allowed-tools: Bash, Read, Glob, Grep, Edit, Write, WebFetch, WebSearch +--- + +# Write Release Highlights for Lean + +You are writing the "Highlights" section for a Lean 4 release. This section goes at the top of the release notes (after the statistics paragraph) and summarizes the most important changes for users. + +## Input + +You will be given the release notes file for a Lean version (e.g. `v4.30.0`). This file is a `.lean` file in the `leanprover/reference-manual` repository under `Manual/Releases/`, containing embedded markdown. + +**Reference manual repo path:** Before starting, check whether you know the local path to the `leanprover/reference-manual` repository clone. If you don't know it, ask the user for the path. Do not guess or assume a path — the user may have it checked out anywhere. + +**Version:** Ask the user which version to write highlights for. Do not assume a version — the user must specify it explicitly (e.g. `v4.30.0`). + +The release notes file already contains: +- A statistics paragraph ("For this release, N changes landed...") +- Detailed per-category sections (Language, Library, Tactics, Lake, etc.) with one bullet per PR + +Your job is to write a `# Highlights` section to insert between the statistics paragraph and the detailed sections. + +## Process + +### Step 1: Gather context + +1. Read the full release notes file carefully. +2. **Fetch and read ALL PR descriptions** for every PR mentioned in the release notes for the *current* release — no exceptions, no sampling. Use `gh pr view NNNNN --repo leanprover/lean4 --json body` for each one. This includes cross-referenced PRs. Only read the current release's notes file — do NOT also read or fetch PRs from previous releases' notes files. Do not skip PRs that look minor from their one-line entry; the PR description is often the only way to discover that a change is significant. Batch these calls in parallel where possible. This is essential because: + - PR descriptions often contain examples, motivation, and context not present in the one-line release note entry. + - Long, human-written PR descriptions are a strong signal that the change is important and highlight-worthy. + - **Caveat**: If a PR description appears to be AI-generated (signed by Claude, or recognizable AI style with generic phrasing), do NOT treat length as a signal of importance. AI writes detailed descriptions even for minor fixes. + - **Watch for milestones hiding in terse entries.** Sometimes a single line like "The old compiler has been replaced by the new compiler" or "grind tactic is now available" represents a *huge* milestone that deserves top billing. Don't let a short release note entry cause you to overlook it. +3. Look at the previous release's highlights to understand the current trajectory of features (e.g., was `grind` highlighted last time? Is the module system still experimental?). + +### Step 2: Select highlights + +**What to highlight:** +- User-facing UX improvements (editor features, error messages, "try this" improvements, go-to-definition) — these should come first, as they affect the most users +- Major new language features (new commands, new syntax, new elaboration capabilities) +- Significant new tactic capabilities (grind, simp, bv_decide, etc.) +- Monadic verification / mvcgen features — these are a key research direction and should be highlighted when present +- Notable performance improvements +- Important breaking changes that users need to know about (migration guidance is valuable) +- New Lake features +- Major library redesigns or new APIs (String overhaul, iterator API, async primitives, new types) + +**What NOT to highlight:** +- Individual bug fixes (unless they fix a very prominent issue) +- Internal refactors +- Individual lemma additions +- Small performance tweaks +- Internal API changes +- Features that are still WIP/preparational for future releases (check with context if unsure) +- Changes where the PR description is the only signal of importance and it's AI-generated + +**Signals of highlight-worthiness (in rough priority order):** +1. Changes that affect how users write Lean code day-to-day (new syntax, new tactics, editor UX) +2. Long, human-written PR descriptions with examples — the author thought it was important +3. Multiple related PRs addressing the same feature — indicates sustained effort worth showcasing +4. Explicit "breaking change" labels — collect these in a dedicated subsection +5. Features with demo videos or playground links + +**Calibrating depth for different feature types:** +- **Flagship features** (e.g., a major tactic getting new capabilities like `grind`): Give these generous space. Use sub-headings (`###`) for each major new capability, include code examples from PR descriptions. The reader should understand what's new and be able to try it. When a feature like `grind` has multiple distinct new capabilities in one release, each deserves its own sub-section with examples. However, if a feature is being *introduced for the first time*, a brief announcement with a link to its documentation may be better than a deep dive — the reference manual is the right place for comprehensive docs, not the release notes. +- **Code examples are essential.** For any feature that can be demonstrated with code, include an example. Pull examples from PR descriptions — authors often include well-crafted demonstrations. A highlight without a code example is much less useful to the reader. +- **Themed groups of PRs** (e.g., "error messages improved", "performance gains"): A brief thematic summary + a list of PR links is sufficient. Do NOT elaborate on each PR individually — just convey the theme and let the reader follow the links if interested. +- **Related breaking changes should be unified into a single narrative.** When multiple PRs address the same underlying issue (e.g., transparency handling changes touching `isDefEq`, `@[implicit_reducible]`, `simp +instances`, and `inferInstanceAs`), present them as one coherent story with a migration guide, NOT as separate highlights. The reader needs to understand the whole picture, not piece it together from fragments. +- **Migration guides are high-value content.** When a breaking change is disruptive, include practical migration advice: `set_option` workarounds, lakefile.toml configuration examples, available porting scripts, and step-by-step guidance. Check PR descriptions thoroughly for migration instructions — they often contain lakefile.toml snippets, helper scripts, and diagnostic commands that are extremely valuable to include verbatim. This is often the most useful part of the highlights for affected users. +- **Experimental features** can be highlighted but should be clearly labeled with "Experimental:" in the heading (e.g., `## Experimental: Module System`). This signals to users that the feature is available for experimentation but not yet stable. Do NOT give experimental features the same prominence as stable features. +- **Policy/process changes** (e.g., backward compatibility options policy): Brief mention, 1-2 sentences. +- **Internal infrastructure** (e.g., symbol clash prevention, try? parallelism, compiler pass migrations): Usually not highlight-worthy unless the user impact is direct and significant (e.g., measurable startup time improvement). + +**What NOT to highlight (continued):** +- Internal milestones (e.g., removing old compiler backend) unless they have direct user impact +- Incremental improvements to a feature that was already highlighted in a previous release, unless there's a qualitative leap (e.g., don't re-highlight grind every release just because it got faster; DO highlight when grind gets a fundamentally new capability like interactive mode) +- Many small improvements to the same subsystem — summarize them in the intro paragraph instead of giving them their own section + +**How many highlights?** +- The number of highlights should reflect the release. Feature-rich releases (v4.18, v4.22, v4.25) may have 7-13 topics. Consolidation releases (v4.23, v4.24) may have just 2-5 topics. +- **Err on the side of fewer highlights.** A highlight section that's too long fails its purpose — it becomes just another copy of the detailed list. It is better to have 3 really well-written highlights than 10 mediocre ones. +- If the release is light on big features, say so in the intro paragraph (e.g., "brings significant performance improvements, better error messages, and a plethora of bug fixes and consolidations") and only highlight the 2-3 things that are genuinely new to users. +- If nearly everything seems highlight-worthy, you are probably not being selective enough. Step back and ask: "Would a Lean user who skims only this section get the right picture of this release?" +- **Breaking changes** should be collected into a dedicated `## Breaking Changes` subsection at the end of the highlights section. This is more useful to users than scattering breaking changes across feature descriptions. When a breaking change is directly related to a highlighted feature (e.g., String.Slice overhaul), mention it briefly in the feature highlight AND include it with migration details in the Breaking Changes section. + +### Step 3: Write the highlights + +**Structure:** + +```markdown +# Highlights + +[Optional 1-3 sentence overview of the release's themes] + +## [Descriptive Feature Name] + +[#NNNNN](https://github.com/leanprover/lean4/pull/NNNNN) [prose description +of the change, what it does, why it matters]. + +[Code example if available and illuminating] + +## [Flagship Feature with Sub-items] (e.g., "New Features in Grind") + +### [Sub-capability 1] + +[#NNNNN](...) [description with code example] + +### [Sub-capability 2] + +[#NNNNN](...) [description with code example] + +### Other New Features in [Feature] + +- [brief bullet list of smaller items with PR links] + +## [Themed Group] (e.g., "Error Messages", "Performance Gains") + +[1-2 sentence thematic summary] + +PRs: [#N1](...), [#N2](...), [#N3](...). + +## Library Highlights + +[Thematic summary of library changes, not an exhaustive list.] + +## Breaking Changes + +- [#NNNNN](...) [description + migration guidance] +- [#NNNNN](...) [description + migration guidance] +``` + +**Writing style:** +- Technical but accessible. Assume the reader uses Lean but may not follow development closely. +- Third person, declarative: "[#NNNNN] adds support for...", "[#NNNNN] implements..." +- Show excitement about genuine progress — these notes should "show off the hard work that went into the release" — but don't be breathless or use marketing language. +- Include code examples when they help illustrate a feature. Pull good examples from PR descriptions or linked issues. +- For breaking changes, always include migration guidance when available. +- Keep individual highlight entries concise (1-3 paragraphs typically). For major features, more detail is fine. + +**Formatting rules:** +- PR links are always full markdown links: `[#NNNNN](https://github.com/leanprover/lean4/pull/NNNNN)` +- Issue links similarly: `[#NNNN](https://github.com/leanprover/lean4/issues/NNNN)` +- Use `## ` for each major highlight topic heading +- Use `### ` for sub-topics within a highlight (e.g., multiple grind features under `## New Features in Grind`) +- Code blocks use triple backticks. Use `lean` language tag when appropriate for Verso-native files, plain triple backticks for markdown-block files. +- Breaking changes are marked with `*Breaking change:*` or `*Breaking Changes:*` in italic +- When consolidating multiple PRs into one highlight, list all PR links + +**Regarding the detailed sections below the highlights:** +- Do NOT reorder or restructure the detailed per-category sections +- If a PR was moved to highlights with extended description, optionally add a brief note in the detailed section: "see highlights for details" +- All PRs should remain in the detailed list even if highlighted above + +### Step 4: Library highlights + +Library changes deserve a `## Library Highlights` subsection only when there are genuinely notable library changes (new types, API redesigns, new frameworks). The approach: +- Do NOT try to list every library change — that would just duplicate the detailed list +- Summarize thematically: "expanded lemmas for Array/Vector/List", "better support for bitwise operations" +- Highlight genuinely new types, major API redesigns, or new frameworks (e.g., async primitives, iterator API) +- Call out breaking library changes explicitly +- If library changes are mostly incremental lemma additions and minor fixes, omit this subsection entirely or mention them in the intro paragraph + +### Step 5: Review + +Before finalizing, check: +- [ ] Is the highlights section between the statistics paragraph and the first detailed section? +- [ ] Are all PR links correctly formatted? +- [ ] Does each highlight actually add value over the one-line entry in the detailed list? +- [ ] Are breaking changes clearly called out with migration guidance? +- [ ] Is the length appropriate? (Not so long it's just a copy of the detailed list, not so short it misses important things) +- [ ] Does it sound exciting and professional without being over-the-top? +- [ ] Are WIP/preparational features excluded (or marked as experimental/preview)? + +### Step 6: Post-processing — Link to the reference manual + +After writing the highlights, do a post-processing pass to add cross-references to the Lean reference manual where relevant. This requires using **Verso-native format** (not markdown blocks). + +Use Verso cross-reference syntax: +- `{tactic}\`grind\`` — links to a tactic's documentation +- `{name}\`String.Slice\`` — links to a declaration's documentation +- `{option}\`backward.do.legacy\`` — links to an option's documentation +- `{ref "section-slug"}[display text]` — links to a named section +- `{keywordOf Lean.Parser.Command.grind_pattern}\`grind_pattern\`` — links to a keyword + +Examples of where to add these: +- When mentioning a tactic by name, use `{tactic}\`tacticName\`` +- When mentioning a type or definition, use `{name}\`Fully.Qualified.Name\`` +- When mentioning an option, use `{option}\`option.name\`` +- When referring to a documented section of the reference manual, use `{ref "slug"}[text]` + +To find valid section slugs, search the reference manual source for `tag :=` or section headings. Do not guess slugs — only use ones you can verify exist. + +This step does not affect highlight selection or phrasing — it just enriches the output with useful navigation links. + +## Format details + +Always use **Verso-native format**: markdown is written directly in the `#doc` block. Use `# Highlights` as the heading level, `## ` for topics, `### ` for sub-topics. + +Code blocks within Verso-native files use ` ```lean ` (with language tag) when the code should be checked by Lean, or plain ` ``` ` when it should not be checked (e.g., illustrative goal states, pseudo-code). diff --git a/.gitignore b/.gitignore index 4188c6fcbf..752fbe9f64 100644 --- a/.gitignore +++ b/.gitignore @@ -33,5 +33,4 @@ fwOut.txt wdErr.txt wdIn.txt wdOut.txt -downstream_releases/ .claude/worktrees/ diff --git a/doc/dev/release.md b/doc/dev/release.md new file mode 100644 index 0000000000..fb4e509fc7 --- /dev/null +++ b/doc/dev/release.md @@ -0,0 +1,82 @@ +# Releasing Lean + +The release process is driven by an interactive script at +`script/release/checklist.py`. When run without `-i/--interactive`, it's just an +automated checklist that reports the release's status. When run with +`-i/--interactive`, it also creates commits, tags, bump PRS, and updates the +release page itself. It will always wait for user consent before making any +modifications. + +``` +cd script/release +uv run checklist.py v4.X.Y -i +``` + +To perform a full release, you must be a member of the `lean-release-managers` +team in both `leanprover-community` and `leanprover`, as well as have write +access to the `fgdorais/lean4-unicode-basic` and `dupuisf/BibtexQuery` repos. + +The `checklist.py` script does not fully automate the process. In some cases, it +will ask the user for manual intervention. Other areas that require manual +action are described in the sections below. + +**You should double-check the script +outputs before choosing `Y` on prompts; manual intervention may be required +without the script noticing.** Details about each individual repository's +release process can be found in the comments in `script/release/repos.py`. + +The script never merges PRs; you'll always have to do that manually. Sometimes, +manual intervention is required to make the PR mergeable. This often includes +merging the repo's nightly or bump branch into the PR. Further information can +be found in the comments in `script/release/repos.py`. + +You should be able to ctrl+click any underlined parts of the script (assuming +your terminal emulator supports it) to open them in the browser. + +## Release notes + +The release notes live in the `leanprover/reference_manual` repository. In the +bump PR for a `v4.X.0-rc1` release, the release note page for `v4.X.0` is also +added to the reference manual. This not only adds a new file at +`Manual/Releases/v4_X_0.lean`, but also requires updates to imports in +`Manual/Releases.lean`. In later bump PRs, it is regenerated and updated using +the same script. + +Before merging the release notes, check and potentially fix the verso warnings +in the release notes file. + +At some point between the rc1 and the final release, a separate PR should be +opened to the reference manual containing release highlights. At the moment, +these highlights are generated using the `/release-highlights` claude skill and +then checked by at least one lean developer. + +## Reference manual deployments + +As described in the reference manual readme, the reference manual deploys +whenever one of its tags is pushed. You may need to force-push reference manual +tags after updating the release notes, e.g. after merging the release note +highlights PR. + +## Release announcements + +Once a version has been released, double check + +1. whether the release page on GitHub has a description, release artifacts, and + is tagged as pre-release if necessary, +2. whether the release notes have been deployed to the latest version of the + reference manual, and +3. whether the toolchain can be used in elan. + +If everything looks good, post an announcement of the release in the +corresponding channel in +. + +Announce stable releases on social media as well. + +## Graphviz graphs + +Both the `checklist.py` and the `repos.py` scripts have options to print a +graphviz dot graph of the different repos involved in the release process and +their dependencies. `checklist.py` includes the checklist status. Just chuck it +into a graphviz viewer of your choice, e.g. +. diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md deleted file mode 100644 index 487575285c..0000000000 --- a/doc/dev/release_checklist.md +++ /dev/null @@ -1,369 +0,0 @@ -# Releasing a stable version - -This checklist walks you through releasing a stable version. -See below for the checklist for release candidates. - -We'll use `v4.6.0` as the intended release version as a running example. - -- Run `script/release_checklist.py v4.6.0` to check the status of the release. - This script is idempotent, and should be safe to run at any stage of the release process. - Note that as of v4.19.0, this script takes some autonomous actions, which can be prevented via `--dry-run`. -- `git checkout releases/v4.6.0` - (This branch should already exist, from the release candidates.) -- `git pull` -- In `src/CMakeLists.txt`, verify you see - - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate) - - `set(LEAN_VERSION_IS_RELEASE 1)` - - (all of these should already be in place from the release candidates) -- `git tag v4.6.0` -- `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`) -- Now wait, while CI runs. - - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, - looking for the `v4.6.0` tag. - - This step can take up to two hours. - - If you are intending to cut the next release candidate on the same day, - you may want to start on the release candidate checklist now. -- Next we need to prepare the release notes. - - If the stable release is identical to the last release candidate (this should usually be the case), - you can reuse the release notes that are already in the Lean Language Reference. - - If you want to regenerate the release notes, - run `script/release_notes.py --since v4.5.0` on the `releases/v4.6.0` branch, - and see the section "Writing the release notes" below for more information. - - Release notes live in https://github.com/leanprover/reference-manual, in e.g. `Manual/Releases/v4.6.0.lean`. - It's best if you update these at the same time as you update the `lean-toolchain` for the `reference-manual` repository, see below. -- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears. - - Verify on Github that "Set as the latest release" is checked. -- Next, we will move a curated list of downstream repos to the latest stable release. - - 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. - - For each of the repositories listed in `script/release_repos.yml`, - - Run `script/release_steps.py v4.6.0 ` (e.g. replacing `` with `batteries`), which will walk you through the following steps: - - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.6.0`. - - Update the contents of `lean-toolchain` to `leanprover/lean4:v4.6.0`. - - In the `lakefile.toml` or `lakefile.lean`, if there are dependencies on specific version tags of dependencies, update them to the new tag. - If they depend on `main` or `master`, don't change this; you've just updated the dependency, so `lake update` will take care of modifying the manifest. - - Run `lake update` - - Commit the changes as `chore: bump toolchain to v4.6.0` and push. - - Create a PR with title "chore: bump toolchain to v4.6.0". - - Merge the PR once CI completes. - - Re-running `script/release_checklist.py` will then create the tag `v4.6.0` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file) - - `script/release_checklist.py` will then merge the tag `v4.6.0` into the `stable` branch and push it (unless `stable-branch: false` in the `release_repos.yml` file). - - Special notes on repositories with exceptional requirements: - - `doc-gen4` has additional dependencies which we do not update at each toolchain release, although occasionally these break and need to be updated manually. - - `verso`: - - The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously. - Usually you don't need to do anything. - If you think something is wrong here, please contact David Thrane Christiansen (@david-christiansen) - - Warnings during `lake update` and `lake build` are expected. - - `reference-manual`: the release notes generated by `script/release_notes.py` as described above must be included in - `Manual/Releases/v4.6.0.lean`, and `import` and `include` statements adding in `Manual/Releases.lean`. - - `ProofWidgets4` uses a non-standard sequential version tagging scheme, e.g. `v0.0.29`, which does not refer to the toolchain being used. - You will need to identify the next available version number from https://github.com/leanprover-community/ProofWidgets4/releases, - and push a new tag after merging the PR to `main`. - - `mathlib4`: - - The `lakefile.toml` should always refer to dependencies via their `main` or `master` branch, - not a toolchain tag - (with the exception of `ProofWidgets4`, which *must* use a sequential version tag). - - **Important:** After creating and pushing the ProofWidgets4 tag (see above), - the mathlib4 lakefile must be updated to reference the new tag (e.g. `v0.0.87`). - The `release_steps.py` script handles this automatically by looking up the latest - ProofWidgets4 tag compatible with the target toolchain. - - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably - - The "Verify Transient and Automated Commits" CI check on toolchain bump PRs can be ignored — - it often fails on automated commits (`x:` prefixed) from the nightly-testing history that can't be - reproduced in CI. This does not block merging. - - `repl`: - There are two copies of `lean-toolchain`/`lakefile.lean`: - in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories. - - `lean-fro.org`: - After updating the toolchains and running `lake update`, you must run `scripts/update.sh` to regenerate - the site content. This script updates generated files that depend on the Lean version. - The `release_steps.py` script handles this automatically. -- An awkward situation that sometimes occurs (e.g. with Verso) is that the `master`/`main` branch has already been moved - to a nightly toolchain that comes *after* the stable toolchain we are - targeting. In this case it is necessary to create a branch `releases/v4.6.0` from the last commit which was on - an earlier toolchain, move that branch to the stable toolchain, and create the toolchain tag from that branch. -- Run `script/release_checklist.py v4.6.0` one last time to check that everything is in order. -- Finally, make an announcement! - This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`. - Please see previous announcements for suggested language. - You will want a few bullet points for main topics from the release notes. - If there is a blog post, link to that from the zulip announcement. -- Make sure that whoever is handling social media knows the release is out. - -## Time estimates: -- Initial checks and push the tag: 10 minutes. -- Waiting for the release: 120 minutes. -- Preparing release notes: 10 minutes. -- Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 60 minutes. -- Waiting for Mathlib CI and bors: 120 minutes. -- Finalizing Mathlib tags and stable branch, and updating REPL: 20 minutes. -- Posting announcement and/or blog post: 30 minutes. - -# Creating a release candidate. - -This checklist walks you through creating the first release candidate for a version of Lean. - -For subsequent release candidates, the process is essentially the same, but we start out with the `releases/v4.7.0` branch already created. - -We'll use `v4.7.0-rc1` as the intended release version in this example. - -- Decide which nightly release you want to turn into a release candidate. - We will use `nightly-2024-02-29` in this example. -- It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion. -- Throughout this process you can use `script/release_checklist.py v4.7.0-rc1` to track progress. - This script will also try to do some steps autonomously. It is idempotent and safe to run at any point. - You can prevent it taking any actions using `--dry-run`. -- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly. - - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29` - in their `lean-toolchain`. - - The steps required to reach that state are beyond the scope of this checklist, but see below! -- Create the release branch from this nightly tag: - ``` - git remote add nightly https://github.com/leanprover/lean4-nightly.git - git fetch nightly tag nightly-2024-02-29 - git checkout nightly-2024-02-29 - git checkout -b releases/v4.7.0 - git push --set-upstream origin releases/v4.7.0 - ``` -- In `src/CMakeLists.txt`, - - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began. - - change the `LEAN_VERSION_IS_RELEASE` line to `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`). - - Commit your changes to `src/CMakeLists.txt`, and push. -- `git tag v4.7.0-rc1` -- `git push origin v4.7.0-rc1` -- Now wait, while CI runs. - - The CI setup parses the tag to discover the `-rc1` special description, and passes it to `cmake` using a `-D` option. The `-rc1` doesn't need to be placed in the configuration file. - - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag. - - This step can take up to two hours. -- Verify that the release appears at https://github.com/leanprover/lean4/releases/, marked as a prerelease (this should have been done automatically by the CI release job). -- Next we need to prepare the release notes. - - Run `script/release_notes.py --since v4.6.0` on the `releases/v4.7.0` branch, - which will report diagnostic messages on `stderr` - (including reporting commits that it couldn't associate with a PR, and hence will be omitted) - and then a chunk of markdown on `stdout`. - See the section "Writing the release notes" below for more information. - - Release notes live in https://github.com/leanprover/reference-manual, in e.g. `Manual/Releases/v4.7.0.lean`. - It's best if you update these at the same time as a you update the `lean-toolchain` for the `reference-manual` repository, see below. -- Next, we will move a curated list of downstream repos to the release candidate. - - This assumes that for each repository either: - * There is already a *reviewed* branch `bump/v4.7.0` containing the required adaptations. - The preparation of this branch is beyond the scope of this document. - * The repository does not need any changes to move to the new version. - * Note that sometimes there are *unreviewed* but necessary changes on the `nightly-testing` branch of the repository. - If so, you will need to merge these into the `bump_to_v4.7.0-rc1` branch manually. - * The `nightly-testing` branch may also contain temporary fix scripts (e.g. `fix_backward_defeq.py`, - `fix_deprecations.py`) that were used to adapt to breaking changes during the nightly cycle. - These should be reviewed and removed if no longer needed, as they can interfere with CI checks. - - For each of the repositories listed in `script/release_repos.yml`, - - Run `script/release_steps.py v4.7.0-rc1 ` (e.g. replacing `` with `batteries`), which will walk you through the following steps: - - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`. - - Merge `origin/bump/v4.7.0` if relevant (i.e. `bump-branch: true` appears in `release_repos.yml`). - - Otherwise, you *may* need to merge `origin/nightly-testing`. - - Note that for `verso` and `reference-manual` development happens on `nightly-testing`, so - we will merge that branch into `bump_to_v4.7.0-rc1`, but it is essential in the GitHub interface that we do a rebase merge, - in order to preserve the history. - - Update the contents of `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`. - - In the `lakefile.toml` or `lakefile.lean`, if there are dependencies on `nightly-testing`, `bump/v4.7.0`, or specific version tags, update them to the new tag. - If they depend on `main` or `master`, don't change this; you've just updated the dependency, so `lake update` will take care of modifying the manifest. - - Run `lake update` - - Run `lake build && if lake check-test; then lake test; fi` to check things are working. - - Commit the changes as `chore: bump toolchain to v4.7.0-rc1` and push. - - Create a PR with title "chore: bump toolchain to v4.7.0-rc1". - - Merge the PR once CI completes. (Recall: for `verso` and `reference-manual` you will need to do a rebase merge.) - - Re-running `script/release_checklist.py` will then create the tag `v4.7.0-rc1` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file) - - We do this for the same list of repositories as for stable releases, see above for notes about special cases. - As above, there are dependencies between these, and so the process above is iterative. - It greatly helps if you can merge the `bump/v4.7.0` PRs yourself! - - It is essential for Mathlib and Batteries CI that you then create the next `bump/v4.8.0` branch - for the next development cycle. - Set the `lean-toolchain` file on this branch to same `nightly` you used for this release. -- Run `script/release_checklist.py v4.7.0-rc1` one last time to check that everything is in order. -- Make an announcement! - This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`. - Please see previous announcements for suggested language. - You will want a few bullet points for main topics from the release notes. - Please also make sure that whoever is handling social media knows the release is out. -- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that: - - Uses branch name `dev_cycle_v4.8`. - - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)` - - Titled "chore: begin development cycle for v4.8.0" - -## Time estimates: -Slightly longer than the corresponding steps for a stable release. -Similar process, but more things go wrong. -In particular, updating the downstream repositories is significantly more work -(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain). - -# Preparing `bump/v4.7.0` branches - -While not part of the release process per se, -this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions. - -Please read https://leanprover-community.github.io/contribute/tags_and_branches.html - -* Each repo has an unreviewed `nightly-testing` branch that - receives commits automatically from `master`, and - has its toolchain updated automatically for every nightly. - (Note: the aesop branch is not automated, and is updated on an as needed basis.) - As a consequence this branch is often broken. - A bot posts in the (private!) "Mathlib reviewers" stream on Zulip about the status of these branches. -* We fix the breakages by committing directly to `nightly-testing`: there is no PR process. - * This can either be done by the person managing this process directly, - or by soliciting assistance from authors of files, or generally helpful people on Zulip! -* Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions. -* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we will create a PR to `bump/v4.7.0`. -* For Mathlib, there is a script in `scripts/create-adaptation-pr.sh` that automates this process. -* For Batteries and Aesop it is currently manual. -* For all of these repositories, the process is the same: - * Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary) - * Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch. - * In that branch, `git merge nightly-testing` to bring across changes from `nightly-testing`. - * Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch. - * Solicit review, merge the PR into `bump/v4.7.0`. -* It is always okay to merge in the following directions: - `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`. - Please remember to push any merges you make to intermediate steps! - -# Writing the release notes - -Release notes content is only written for the first release candidate (`-rc1`). For subsequent RCs and stable releases, -just update the title in the existing release notes file (see "Release notes title format" below). - -## Release notes title format - -The title in the `#doc (Manual)` line must follow these formats: - -- **For -rc1**: `"Lean 4.7.0-rc1 (2024-03-15)"` — Include the RC suffix and the release date -- **For -rc2, -rc3, etc.**: `"Lean 4.7.0-rc2 (2024-03-20)"` — Update the RC number and date -- **For stable release**: `"Lean 4.7.0 (2024-04-01)"` — Remove the RC suffix but keep the date - -The date should be the actual date when the tag was pushed (or when CI completed and created the release page). - -## Generating the release notes - -Release notes are automatically generated from the commit history, using `script/release_notes.py`. - -Run this as `script/release_notes.py --since v4.6.0`, where `v4.6.0` is the *previous* release version. -This script should be run on the `releases/v4.7.0` branch. -This will generate output for all commits since that tag. -Note that there is output on both stderr, which should be manually reviewed, -and on stdout, which should be manually copied into the `reference-manual` repository, in the file `Manual/Releases/v4.7.0.lean`. - -The output on stderr should mostly be about commits for which the script could not find an associated PR, -usually because a PR was rebase-merged because it contained an update to stage0. -Some judgement is required here: ignore commits which look minor, -but manually add items to the release notes for significant PRs that were rebase-merged. - -There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch. - -## Reviewing and fixing the generated markdown - -Before adding the release notes to the reference manual, carefully review the generated markdown for these common issues: - -1. **Unterminated code blocks**: PR descriptions sometimes have unclosed code fences. Look for code blocks - that don't have a closing ` ``` `. If found, fetch the original PR description with `gh pr view ` - and repair the code block with the complete content. - -2. **Truncated descriptions**: Some PR descriptions may end abruptly mid-sentence. Review these and complete - the descriptions based on the original PR. - -3. **Markdown syntax issues**: Check for other markdown problems that could cause parsing errors. - -## Creating the release notes file - -The release notes go in `Manual/Releases/v4_7_0.lean` in the reference-manual repository. - -The file structure must follow the Verso format: - -```lean -/- -Copyright (c) 2025 Lean FRO LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: --/ - -import VersoManual -import Manual.Meta -import Manual.Meta.Markdown - -open Manual -open Verso.Genre -open Verso.Genre.Manual -open Verso.Genre.Manual.InlineLean - -#doc (Manual) "Lean 4.7.0-rc1 (2024-03-15)" => -%%% -tag := "release-v4.7.0" -file := "v4.7.0" -%%% - - -``` - -**Important formatting rules for Verso:** -- Use `#` for section headers inside the document, not `##` (Verso uses header level 1 for subsections) -- Use plain ` ``` ` for code blocks, not ` ```lean ` (the latter will cause Lean to execute the code) -- Identifiers with underscores like `bv_decide` should be wrapped in backticks: `` `bv_decide` `` - (otherwise the underscore may be interpreted as markdown emphasis) - -## Updating Manual/Releases.lean - -After creating the release notes file, update `Manual/Releases.lean` to include it: - -1. Add the import near the top with other version imports: - ```lean - import Manual.Releases.«v4_7_0» - ``` - -2. Add the include statement after the other includes: - ```lean - {include 0 Manual.Releases.«v4_7_0»} - ``` - -## Building and verifying - -Build the release notes to check for errors: -```bash -lake build Manual.Releases.v4_7_0 -``` - -Common errors and fixes: -- "Wrong header nesting - got ## but expected at most #": Change `##` to `#` -- "Tactic 'X' failed" or similar: Code is being executed; change ` ```lean ` to ` ``` ` -- "'_'" errors: Underscore in identifier being parsed as emphasis; wrap in backticks - -## Creating the PR - -**Important: Timing with the reference-manual tag** - -The reference-manual repository deploys documentation when a version tag is pushed. If you merge -release notes AFTER the tag is created, the deployed documentation won't include them. - -You have two options: - -1. **Preferred**: Include the release notes in the same PR as the toolchain bump (or merge the - release notes PR before creating the tag). This ensures the tag includes the release notes. - -2. **If release notes are merged after the tag**: You must regenerate the tag to trigger a new deployment: - ```bash - cd /path/to/reference-manual - git fetch origin - git tag -d v4.7.0-rc1 # Delete local tag - git tag v4.7.0-rc1 origin/main # Create tag at current main (which has release notes) - git push origin :refs/tags/v4.7.0-rc1 # Delete remote tag - git push origin v4.7.0-rc1 # Push new tag (triggers Deploy workflow) - ``` - -If creating a separate PR for release notes: -```bash -git checkout -b v4.7.0-release-notes -git add Manual/Releases/v4_7_0.lean Manual/Releases.lean -git commit -m "doc: add v4.7.0 release notes" -git push -u origin v4.7.0-release-notes -gh pr create --title "doc: add v4.7.0 release notes" --body "This PR adds the release notes for Lean v4.7.0." -``` - -See `./releases_drafts/README.md` for more information about pre-written release note entries. -See `./releases_drafts/README.md` for more information. diff --git a/script/merge_remote.py b/script/merge_remote.py deleted file mode 100755 index b6cea10787..0000000000 --- a/script/merge_remote.py +++ /dev/null @@ -1,209 +0,0 @@ -#!/usr/bin/env python3 - -""" -Merge a tag into a branch on a GitHub repository. - -This script checks if a specified tag can be merged cleanly into a branch and performs -the merge if possible. If the merge cannot be done cleanly, it prints a helpful message. -Merge conflicts in the lean-toolchain file are automatically resolved by accepting the incoming changes. - -Usage: - python3 merge_remote.py - -Arguments: - org/repo: GitHub repository in the format 'organization/repository' - branch: The target branch to merge into - tag: The tag to merge from - -Example: - python3 merge_remote.py leanprover/mathlib4 stable v4.6.0 - -The script uses the GitHub CLI (`gh`), so make sure it's installed and authenticated. -""" - -import argparse -import subprocess -import sys -import tempfile -import os -import shutil - - -def run_command(command, check=True, capture_output=True): - """Run a shell command and return the result.""" - try: - result = subprocess.run( - command, - check=check, - shell=True, - text=True, - capture_output=capture_output - ) - return result - except subprocess.CalledProcessError as e: - if capture_output: - print(f"Command failed: {command}") - print(f"Error: {e.stderr}") - return e - - -def clone_repo(repo, temp_dir): - """Clone the repository to a temporary directory.""" - print(f"Cloning {repo}...") - # Remove shallow clone for better merge detection - clone_result = run_command(f"gh repo clone {repo} {temp_dir}", check=False) - if clone_result.returncode != 0: - print(f"Failed to clone repository {repo}.") - print(f"Error: {clone_result.stderr}") - return False - return True - - -def get_conflicted_files(): - """Get list of files with merge conflicts.""" - result = run_command("git diff --name-only --diff-filter=U", check=False) - if result.returncode == 0: - return result.stdout.strip().split('\n') if result.stdout.strip() else [] - return [] - - -def resolve_lean_toolchain_conflict(tag): - """Resolve lean-toolchain conflict by accepting incoming (tag) changes.""" - print("Resolving lean-toolchain conflict by accepting incoming changes...") - # Accept theirs (incoming) version for lean-toolchain - result = run_command(f"git checkout --theirs lean-toolchain", check=False) - if result.returncode != 0: - print("Failed to resolve lean-toolchain conflict") - return False - - # Add the resolved file - add_result = run_command("git add lean-toolchain", check=False) - if add_result.returncode != 0: - print("Failed to stage resolved lean-toolchain") - return False - - return True - - -def check_and_merge(repo, branch, tag, temp_dir): - """Check if tag can be merged into branch and perform the merge if possible.""" - # Change to the temporary directory - os.chdir(temp_dir) - - # First fetch the specific remote branch with its history - print(f"Fetching branch '{branch}'...") - fetch_branch = run_command(f"git fetch origin {branch}:refs/remotes/origin/{branch} --update-head-ok") - if fetch_branch.returncode != 0: - print(f"Error: Failed to fetch branch '{branch}'.") - return False - - # Then fetch the specific tag - print(f"Fetching tag '{tag}'...") - fetch_tag = run_command(f"git fetch origin tag {tag}") - if fetch_tag.returncode != 0: - print(f"Error: Failed to fetch tag '{tag}'.") - return False - - # Check if branch exists now that we've fetched it - branch_check = run_command(f"git branch -r | grep origin/{branch}") - if branch_check.returncode != 0: - print(f"Error: Branch '{branch}' does not exist in repository.") - return False - - # Check if tag exists - tag_check = run_command(f"git tag -l {tag}") - if tag_check.returncode != 0 or not tag_check.stdout.strip(): - print(f"Error: Tag '{tag}' does not exist in repository.") - return False - - # Checkout the branch - print(f"Checking out branch '{branch}'...") - checkout_result = run_command(f"git checkout -b {branch} origin/{branch}") - if checkout_result.returncode != 0: - return False - - # Try merging the tag directly - print(f"Merging {tag} into {branch}...") - merge_result = run_command(f"git merge {tag} --no-edit", check=False) - - if merge_result.returncode != 0: - # Check which files have conflicts - conflicted_files = get_conflicted_files() - - if conflicted_files == ['lean-toolchain']: - # Only lean-toolchain has conflicts, resolve it - print("Merge conflict detected only in lean-toolchain.") - if resolve_lean_toolchain_conflict(tag): - # Continue the merge with the resolved conflict - print("Continuing merge with resolved lean-toolchain...") - continue_result = run_command(f"git commit --no-edit", check=False) - if continue_result.returncode != 0: - print("Failed to complete merge after resolving lean-toolchain") - run_command("git merge --abort") - return False - else: - print("Failed to resolve lean-toolchain conflict") - run_command("git merge --abort") - return False - else: - # Other files have conflicts, or unable to determine - if conflicted_files: - print(f"Cannot merge {tag} cleanly into {branch}.") - print(f"Merge conflicts in: {', '.join(conflicted_files)}") - else: - print(f"Cannot merge {tag} cleanly into {branch}.") - print("Merge conflicts would occur.") - print("Aborting merge.") - run_command("git merge --abort") - return False - - print(f"Pushing changes to remote...") - push_result = run_command(f"git push origin {branch}") - if push_result.returncode != 0: - print(f"Failed to push changes to remote.") - return False - - print(f"Successfully merged {tag} into {branch} and pushed to remote.") - return True - - -def main(): - parser = argparse.ArgumentParser( - description="Merge a tag into a branch on a GitHub repository.", - formatter_class=argparse.RawDescriptionHelpFormatter, - epilog=""" -Examples: - %(prog)s leanprover/mathlib4 stable v4.6.0 Merge tag v4.6.0 into stable branch - -The script will: -1. Clone the repository -2. Check if the tag and branch exist -3. Check if the tag can be merged cleanly into the branch -4. Perform the merge and push to remote if possible - """ - ) - parser.add_argument("repo", help="GitHub repository in the format 'organization/repository'") - parser.add_argument("branch", help="The target branch to merge into") - parser.add_argument("tag", help="The tag to merge from") - - args = parser.parse_args() - - # Create a temporary directory for the repository - temp_dir = tempfile.mkdtemp() - try: - # Clone the repository - if not clone_repo(args.repo, temp_dir): - sys.exit(1) - - # Check if the tag can be merged and perform the merge - if not check_and_merge(args.repo, args.branch, args.tag, temp_dir): - sys.exit(1) - - finally: - # Clean up the temporary directory - print(f"Cleaning up temporary files...") - shutil.rmtree(temp_dir) - - -if __name__ == "__main__": - main() \ No newline at end of file diff --git a/script/push_repo_release_tag.py b/script/push_repo_release_tag.py deleted file mode 100755 index 3e62d59bb1..0000000000 --- a/script/push_repo_release_tag.py +++ /dev/null @@ -1,122 +0,0 @@ -#!/usr/bin/env python3 -import sys -import subprocess -import requests - -def check_gh_auth(): - """Check if GitHub CLI is properly authenticated.""" - try: - result = subprocess.run(["gh", "auth", "status"], capture_output=True, text=True) - if result.returncode != 0: - return False, result.stderr - return True, None - except FileNotFoundError: - return False, "GitHub CLI (gh) is not installed. Please install it first." - except Exception as e: - return False, f"Error checking authentication: {e}" - -def handle_gh_error(error_output): - """Handle GitHub CLI errors and provide helpful messages.""" - if "Not Found (HTTP 404)" in error_output: - return "Repository not found or access denied. Please check:\n" \ - "1. The repository name is correct\n" \ - "2. You have access to the repository\n" \ - "3. Your GitHub CLI authentication is valid" - elif "Bad credentials" in error_output or "invalid" in error_output.lower(): - return "Authentication failed. Please run 'gh auth login' to re-authenticate." - elif "rate limit" in error_output.lower(): - return "GitHub API rate limit exceeded. Please try again later." - else: - return f"GitHub API error: {error_output}" - -def main(): - if len(sys.argv) != 4: - print("Usage: ./push_repo_release_tag.py ") - sys.exit(1) - - repo, branch, version_tag = sys.argv[1], sys.argv[2], sys.argv[3] - - if branch not in {"master", "main"}: - print(f"Error: Branch '{branch}' is not 'master' or 'main'.") - sys.exit(1) - - # Check GitHub CLI authentication first - auth_ok, auth_error = check_gh_auth() - if not auth_ok: - print(f"Authentication error: {auth_error}") - print("\nTo fix this, run: gh auth login") - sys.exit(1) - - # Get the `lean-toolchain` file content - lean_toolchain_url = f"https://raw.githubusercontent.com/{repo}/{branch}/lean-toolchain" - try: - response = requests.get(lean_toolchain_url) - response.raise_for_status() - except requests.exceptions.RequestException as e: - print(f"Error fetching 'lean-toolchain' file: {e}") - sys.exit(1) - - lean_toolchain_content = response.text.strip() - expected_prefix = "leanprover/lean4:" - if not lean_toolchain_content.startswith(expected_prefix) or lean_toolchain_content != f"{expected_prefix}{version_tag}": - print(f"Error: 'lean-toolchain' content does not match '{expected_prefix}{version_tag}'.") - sys.exit(1) - - # Create and push the tag using `gh` - try: - # Check if the tag already exists - list_tags_cmd = ["gh", "api", f"repos/{repo}/git/matching-refs/tags/v4", "--jq", ".[].ref"] - list_tags_output = subprocess.run(list_tags_cmd, capture_output=True, text=True) - - if list_tags_output.returncode == 0: - existing_tags = list_tags_output.stdout.strip().splitlines() - if f"refs/tags/{version_tag}" in existing_tags: - print(f"Error: Tag '{version_tag}' already exists.") - print("Existing tags starting with 'v4':") - for tag in existing_tags: - print(tag.replace("refs/tags/", "")) - sys.exit(1) - elif list_tags_output.returncode != 0: - # Handle API errors when listing tags - error_msg = handle_gh_error(list_tags_output.stderr) - print(f"Error checking existing tags: {error_msg}") - sys.exit(1) - - # Get the SHA of the branch - get_sha_cmd = [ - "gh", "api", f"repos/{repo}/git/ref/heads/{branch}", "--jq", ".object.sha" - ] - sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True) - - if sha_result.returncode != 0: - error_msg = handle_gh_error(sha_result.stderr) - print(f"Error getting branch SHA: {error_msg}") - sys.exit(1) - - sha = sha_result.stdout.strip() - - # Create the tag - create_tag_cmd = [ - "gh", "api", f"repos/{repo}/git/refs", - "-X", "POST", - "-F", f"ref=refs/tags/{version_tag}", - "-F", f"sha={sha}" - ] - create_result = subprocess.run(create_tag_cmd, capture_output=True, text=True) - - if create_result.returncode != 0: - error_msg = handle_gh_error(create_result.stderr) - print(f"Error creating tag: {error_msg}") - sys.exit(1) - - print(f"Successfully created and pushed tag '{version_tag}' to {repo}.") - except subprocess.CalledProcessError as e: - error_msg = handle_gh_error(e.stderr.strip() if e.stderr else str(e)) - print(f"Error while creating/pushing tag: {error_msg}") - sys.exit(1) - except Exception as e: - print(f"Unexpected error: {e}") - sys.exit(1) - -if __name__ == "__main__": - main() diff --git a/script/release/.gitignore b/script/release/.gitignore new file mode 100644 index 0000000000..85f9bcfbbc --- /dev/null +++ b/script/release/.gitignore @@ -0,0 +1,2 @@ +/__pycache__/ +/uv.lock diff --git a/script/release/checklist.py b/script/release/checklist.py new file mode 100644 index 0000000000..2f24b5d165 --- /dev/null +++ b/script/release/checklist.py @@ -0,0 +1,739 @@ +from argparse import ArgumentParser +from dataclasses import dataclass +from pathlib import Path + +import repos +from github import Github, UnknownObjectException +from github.GitRef import GitRef +from rich import print +from rich.markup import escape as e + +import util +from util import Checklist, CMakeVersion, ReleaseRepo, Version + + +@dataclass +class Config: + version: Version + interactive: bool + skip_weak_deps: bool + skip_mathlib_checks: bool + github: Github + + +class RepoChecker: + def __init__(self, config: Config, rrepo: ReleaseRepo) -> None: + self.config = config + self.cl = Checklist() + + self.rrepo = rrepo + self.grepo = self.github.get_repo(self.rrepo.gh_full_name) + self.lrepo = self.rrepo.local + + @property + def github(self) -> Github: + return self.config.github + + @property + def version(self) -> Version: + return self.config.version + + def prompt(self, message: str) -> bool: + if not self.config.interactive: + return False + return util.prompt(message) == "y" + + def check_pr(self, base: str, head: str, title: str) -> bool: + pr = util.find_pr(self.grepo, head=head, base=base, title=title) + if not pr: + if not self.prompt("PR not found. Create?"): + self.cl.fatal("PR not found") + return False + + if pr.state == "open": + self.cl.blocked(f"PR open: {util.fmt_pr(pr)}") + + if pr.merged: + self.cl.success(f"PR merged: {util.fmt_pr(pr)}") + else: + self.cl.success(f"PR closed: {util.fmt_pr(pr)}") + + return True + + def create_pr( + self, base: str, head: str, title: str, nightly: ReleaseRepo | None = None + ) -> None: + if not self.prompt(f"Push branch [b]{e(head)}[/b]?"): + self.cl.fatal("Branch not pushed") + self.lrepo.push(head, remote="nightly" if nightly else "origin") + + # Mathlib bump PRs are opened from the nightly-testing repo, which + # pygithub doesn't support because both belong to the same organization: + # https://github.com/PyGithub/PyGithub/issues/2942 + # So we just give the user a link instead. + if nightly: + url = util.create_pr_url( + base=self.rrepo, + base_branch=base, + head=nightly, + head_branch=head, + title=title, + ) + self.cl.blocked(f"[u link={url}]Create PR manually[/]") + + if not self.prompt(f"Create PR for branch [b]{e(head)}[/b]?"): + self.cl.fatal("PR not created") + pr = util.create_pr(self.grepo, head=head, base=base, title=title) + self.cl.blocked(f"PR created: {util.fmt_pr(pr)}") + + +class DownstreamChecker(RepoChecker): + def check_dependencies_completed(self) -> None: + deps = list(self.rrepo.strong_deps) + if not self.config.skip_weak_deps: + deps += self.rrepo.weak_deps + for dep in deps: + if not dep.completed: + self.cl.wait( + f"Awaiting completion of dependency [b]{e(dep.gh_full_name)}[/b]" + ) + self.cl.ensure_success() + + def check_toolchain(self) -> bool: + expected = util.get_toolchain_for(self.version) + actual = util.get_toolchain(self.grepo, self.grepo.default_branch) + + if expected == actual: + self.cl.success(f"Toolchain is [b]{e(actual)}[/b]") + return True + else: + self.cl.fail(f"Toolchain is [b]{e(actual)}[/b]") + return False + + def _bump_toolchain(self, path: Path) -> None: + util.set_toolchain(path, self.version.tag) + + def _bump_toolchain_deps(self, path: Path) -> None: + if (path / "lakefile.toml").exists(): + util.edit( + path / "lakefile.toml", + r'rev = "v4\.[0-9]+(\.[0-9]+)?(-rc[0-9]+)?"', + f'rev = "{self.version}"', + ) + else: + util.edit( + path / "lakefile.lean", + r'git "v4\.[0-9]+(\.[0-9]+)?(-rc[0-9]+)?"', + f'git "{self.version}"', + ) + + util.run("lake", "update", cwd=path) + + def _bump_toolchain_mathlib4(self) -> None: + pw = self.github.get_repo(repos.PROOFWIDGETS4.gh_full_name) + tag = util.get_proofwidgets_release_for(pw, self.version) + if not tag: + raise SystemExit(1) + + # For both normal and rc1 PRs + util.edit( + self.lrepo.path / "lakefile.lean", + r'"proofwidgets" @ git ".*"', + f'"proofwidgets" @ git "{tag.name}"', + ) + + # For rc1 PRs + util.edit( + self.lrepo.path / "lakefile.lean", + r' @ git "nightly-testing"', + f' @ git "{self.version}"', + ) + + self._bump_toolchain_deps(self.lrepo.path) + + def _bump_toolchain_repl(self) -> None: + self._bump_toolchain_deps(self.lrepo.path) + + mathlib = self.lrepo.path / "test" / "Mathlib" + self._bump_toolchain(mathlib) + self._bump_toolchain_deps(mathlib) + + if self.prompt("Run tests?"): + try: + util.run("./test.sh", cwd=self.lrepo.path) + print("#####################") + print("## Tests succeeded ##") + print("#####################") + except SystemExit as e: + print("###################") + print("## Tests failed! ##") + print("###################") + raise e + + def _bump_toolchain_verso(self) -> None: + self._bump_toolchain_deps(self.lrepo.path) + util.run("./update-subverso.sh", cwd=self.lrepo.path) + + def _bump_toolchain_reference_manual(self) -> None: + self._bump_toolchain_deps(self.lrepo.path) + + if not self.prompt("Run release notes update script"): + self.cl.fatal("Release notes update script not run") + + here = Path(__file__).parent + util.run( + "uv", "run", "release_notes.py", self.version.tag, self.lrepo.path, cwd=here + ) + + self.prompt("Check release notes before commit") + + def _bump_toolchain_lean_fro_org(self) -> None: + self._bump_toolchain_deps(self.lrepo.path) + + hero = self.lrepo.path / "examples" / "hero" + self._bump_toolchain(hero) + self._bump_toolchain_deps(hero) + + util.run("scripts/update.sh", cwd=self.lrepo.path) + + def _bump_toolchain_bibtex_query(self) -> None: + lub = self.github.get_repo(repos.LEAN4_UNICODE_BASIC.gh_full_name) + tag = util.get_lean_unicode_basic_release_for(lub, self.version) + rev = str(tag) if tag else "main" + + util.edit( + self.lrepo.path / "lakefile.toml", + r'(name = "UnicodeBasic"[\s\S]*?rev =) ".+?"', + rf'\1 "{rev}"', + ) + + self._bump_toolchain_deps(self.lrepo.path) + + def _bump_toolchain_in_worktree(self) -> None: + self._bump_toolchain(self.lrepo.path) + + # Special cases + if self.rrepo.gh_full_name == repos.MATHLIB4.gh_full_name: + self._bump_toolchain_mathlib4() + elif self.rrepo.gh_full_name == repos.REPL.gh_full_name: + self._bump_toolchain_repl() + elif self.rrepo.gh_full_name == repos.VERSO.gh_full_name: + self._bump_toolchain_verso() + elif self.rrepo.gh_full_name == repos.REFERENCE_MANUAL.gh_full_name: + self._bump_toolchain_reference_manual() + elif self.rrepo.gh_full_name == repos.LEAN_FRO_ORG.gh_full_name: + self._bump_toolchain_lean_fro_org() + elif self.rrepo.gh_full_name == repos.BIBTEX_QUERY.gh_full_name: + self._bump_toolchain_bibtex_query() + elif self.rrepo.strong_deps: + self._bump_toolchain_deps(self.lrepo.path) + + def _bump_toolchain_unicode_basic(self) -> None: + base = self.grepo.default_branch + head = f"update-toolchain-{self.version}" + title = f"chore: update toolchain {self.version}" + if self.check_pr(base=base, head=head, title=title): + return + + workflow = self.grepo.get_workflow("update-toolchain.yml") + for run in workflow.get_runs(branch=base).get_page(0): + if not run.conclusion: + what = f"[b u link={run.html_url}]Bump workflow run {run.id}[/]" + self.cl.blocked(f"{what} is still running") + return + + if not self.prompt("No PR or running bump workflow run found. Trigger?"): + self.cl.fatal("No PR or running bump workflow run found") + + workflow.create_dispatch(ref=base) + self.cl.blocked("Triggered bump workflow run") + + def check_bump_pr(self) -> None: + if self.rrepo.gh_full_name == repos.LEAN4_UNICODE_BASIC.gh_full_name: + self._bump_toolchain_unicode_basic() + return + + # Normally: + # 1. Create bump branch from origin/main + # 2. Edit files 'n stuff and commit + # 3. Push branch to origin + # 4. Create PR to origin/main + + # Nightly: + # 1. Create bump branch from origin/main + # 2. Edit files 'n stuff and commit + # 3. Push branch to nightly + # 4. Create PR to origin/main + + # Normally, with RC1 and bump branch: + # 1. Switch to origin/bump/v* + # 2. Edit files 'n stuff and commit + # 3. Push branch to origin + # 4. Create PR to origin/main + + # Nightly, with RC1 and bump branch: + # 1. Switch to nightly/bump/v* + # 2. Edit files 'n stuff and commit + # 3. Push branch to nightly + # 4. Create PR to origin/main + + base = self.grepo.default_branch + head = f"bump-to-{self.version}" + nightly = None + + use_bump_branch = self.rrepo.bump_branch and self.version.rc == 1 + if use_bump_branch: + head = util.get_bump_branch(self.version) + nightly = self.rrepo.nightly + + title = util.get_toolchain_bump_message(self.version) + if self.check_pr(base=base, head=head, title=title): + return + + self.lrepo.prepare(nightly=nightly) + if use_bump_branch: + self.lrepo.switch(head, remote="nightly" if nightly else "origin") + else: + self.lrepo.create_branch(head) + + self._bump_toolchain_in_worktree() + self.lrepo.commit(title) + + self.create_pr(base=base, head=head, title=title, nightly=nightly) + + def check_next_bump_branch(self) -> None: + if not self.rrepo.bump_branch: + return + + grepo = self.grepo + if self.rrepo.nightly: + grepo = self.github.get_repo(self.rrepo.nightly.gh_full_name) + + branch_name = util.get_bump_branch(self.version.next_minor) + what = f"Bump branch [b]{e(branch_name)}[/b]" + try: + grepo.get_branch(branch_name) + self.cl.success(f"{what} exists") + return + except UnknownObjectException: + pass + + if not self.prompt(f"{what} not found. Create?"): + self.cl.fail(f"{what} not found") + return + + lean4_nightly = self.github.get_repo(repos.LEAN4_NIGHTLY.gh_full_name) + latest_nightly_tag = util.get_latest_nightly_tag(lean4_nightly) + + self.lrepo.prepare(nightly=self.rrepo.nightly) + self.lrepo.create_branch(branch_name) + util.set_toolchain(self.lrepo.path, latest_nightly_tag.name) + + message = f"chore: bump toolchain to {latest_nightly_tag.name}" + self.lrepo.commit(message) + + if not self.prompt(f"Push branch [b]{e(branch_name)}[/b]?"): + self.cl.fail(f"{what} not found") + return + remote = "nightly" if self.rrepo.nightly else "origin" + self.lrepo.push(branch_name, remote=remote) + self.cl.success(f"{what} created") + + def _check_lean_release_tag(self) -> GitRef | None: + tag_name = self.version.tag + what = f"Toolchain tag [b]{tag_name}[/b]" + + try: + tag = self.grepo.get_git_ref(f"tags/{tag_name}") + self.cl.success(f"{what} exists") + return tag + except UnknownObjectException: + pass + + if not self.prompt(f"{what} not found. Create?"): + self.cl.fail(f"{what} not found") + return + + self.lrepo.prepare() + bump_sha = util.find_merged_toolchain_bump_sha(self.lrepo, self.version) + self.lrepo.create_tag(tag_name, bump_sha) + + if not self.prompt(f"Push tag [b]{tag_name}[/b]?"): + self.cl.fatal(f"{what} does not exist") + self.lrepo.push(tag_name, upstream=False) + + tag = self.grepo.get_git_ref(f"tags/{tag_name}") + self.cl.success(f"{what} created") + return tag + + def _check_proofwidgets_release_tag(self) -> GitRef | None: + what = f"Proofwidgets release with toolchain {self.version}" + + tag = util.get_proofwidgets_release_for(self.grepo, self.version) + if tag: + self.cl.success(f"{what} found: [b]{e(tag.name)}[/b]") + return + + tag_name = util.get_next_proofwidgets_release(self.grepo) + if not self.prompt(f"{what} not found. Create [b]{e(tag_name)}[/b]?"): + self.cl.fail(f"{what} not found") + return + + self.lrepo.prepare() + bump_sha = util.find_merged_toolchain_bump_sha(self.lrepo, self.version) + self.lrepo.create_tag(tag_name, bump_sha) + + if not self.prompt(f"Push tag [b]{tag_name}[/b]?"): + self.cl.fatal(f"{what} does not exist") + self.lrepo.push(tag_name, upstream=False) + + tag = self.grepo.get_git_ref(f"tags/{tag_name}") + self.cl.success(f"{what} created") + return tag + + def check_release_tag(self) -> GitRef | None: + match self.rrepo.release_tag: + case "lean": + return self._check_lean_release_tag() + case "proofwidgets": + return self._check_proofwidgets_release_tag() + case None: + pass + + def check_stable_branch_points_to_release_tag(self, tag: GitRef) -> None: + if not self.rrepo.stable_branch: + return + if not self.version.is_stable: + return + + what = "Stable branch" + + branch = self.grepo.get_branch("stable") + if branch.commit.sha == tag.object.sha: + self.cl.success(f"{what} points to toolchain tag") + return + + if not self.prompt(f"{what} does not point to toolchain tag. Update?"): + self.cl.fail(f"{what} does not point to toolchain tag") + return + + self.lrepo.prepare() + self.lrepo.switch("stable") + self.lrepo.git("merge", "--ff-only", self.version.tag) + + if not self.prompt("Push branch [b]stable[/b] to origin?"): + self.cl.fail(f"{what} does not point to toolchain tag") + return + + self.lrepo.push("stable") + self.cl.success(f"{what} updated to point to toolchain tag") + + def check_mathlib4_version_tags(self) -> None: + if self.rrepo.gh_full_name != repos.MATHLIB4.gh_full_name: + return + if self.config.skip_mathlib_checks: + return + + # At this point, the PR has been merged + self.lrepo.prepare() + self.lrepo.switch(self.grepo.default_branch) + + script = "scripts/verify_version_tags.py" + try: + self.lrepo.run("python", script, self.version.tag) + self.cl.success(f"Version tags verified by [b]{e(script)}[/b]") + except Exception: + self.cl.fatal(f"Version tag verification by [b]{e(script)}[/b] failed") + + def check(self) -> None: + self.check_dependencies_completed() + + toolchain = self.check_toolchain() + if not toolchain: + self.check_bump_pr() + self.cl.ensure_success() + self.check_next_bump_branch() + + release_tag = self.check_release_tag() + if release_tag: + self.check_stable_branch_points_to_release_tag(release_tag) + + if toolchain: + self.check_mathlib4_version_tags() + + self.cl.ensure_success() + self.rrepo.completed = True + + +class LeanChecker(RepoChecker): + def __init__(self, config: Config) -> None: + super().__init__(config=config, rrepo=repos.LEAN4) + + def _check_label_exists( + self, name: str, color: str, description: str | None = None + ) -> None: + what = f"Label [b]{e(name)}[/b]" + + try: + self.grepo.get_label(name) + self.cl.success(f"{what} exists") + return + except UnknownObjectException: + pass + + if not self.prompt(f"{what} does not exist. Create?"): + self.cl.fail(f"{what} does not exist") + return + + if description is None: + self.grepo.create_label(name=name, color=color) + else: + self.grepo.create_label(name=name, color=color, description=description) + self.cl.success(f"{what} created") + + def check_backport_label_exists(self, version: Version) -> None: + self._check_label_exists( + name=util.get_backport_label(version), + color="1d76db", + ) + + def check_blocking_label_exists(self, version: Version) -> None: + self._check_label_exists( + name=util.get_blocking_label(version), + color="b60205", + description=f"Blocks the next {version.base} release candidate or release from being published.", + ) + + def check_release_branch_exists(self) -> None: + branch_name = util.get_releases_branch(self.version) + what = f"Release branch [b]{e(branch_name)}[/b]" + + try: + self.grepo.get_branch(branch_name) + self.cl.success(f"{what} exists") + return + except UnknownObjectException: + pass + + if not self.prompt(f"{what} does not exist. Create?"): + self.cl.fatal(f"{what} does not exist") + + self.lrepo.prepare() + self.lrepo.create_branch(branch_name) + + if not self.prompt(f"Push branch [b]{e(branch_name)}[/b]?"): + self.cl.fatal(f"{what} does not exist") + self.lrepo.push(branch_name) + + self.grepo.get_branch(branch_name) + self.cl.success(f"{what} created") + + def check_release_branch_cmake_version(self) -> None: + branch_name = util.get_releases_branch(self.version) + what = f"CMake version settings on [b]{e(branch_name)}[/b]" + target = CMakeVersion(self.version.stable, is_release=True) + + cur = util.get_cmake_version(self.grepo, branch_name) + if cur == target: + self.cl.success(f"{what} are correct") + return + + if not self.prompt(f"{what} are incorrect. Update?"): + self.cl.fail(f"{what} are incorrect") + return + + self.lrepo.prepare() + self.lrepo.switch(branch_name) + util.set_cmake_version(self.lrepo, target) + self.lrepo.commit("chore: prepare release") + + if not self.prompt(f"Push branch [b]{e(branch_name)}[/b]?"): + self.cl.fail(f"{what} are incorrect") + return + self.lrepo.push(branch_name) + self.cl.success(f"{what} updated") + + def check_master_branch_cmake_version(self) -> None: + branch_name = self.grepo.default_branch + what = f"CMake version settings on [b]{e(branch_name)}[/b]" + target = CMakeVersion(self.version.next_minor, is_release=False) + + cur = util.get_cmake_version(self.grepo, branch_name) + if cur == target: + self.cl.success(f"{what} are correct") + return + self.cl.fail(f"{what} are incorrect") + + head = f"dev-cycle-{self.version.next_minor}" + title = f"chore: prepare development cycle for {self.version.next_minor}" + if self.check_pr(base=branch_name, head=head, title=title): + return + + self.lrepo.prepare() + self.lrepo.create_branch(head, branch_name) + util.set_cmake_version(self.lrepo, target) + self.lrepo.commit(title) + + self.create_pr(base=branch_name, head=head, title=title) + + def _check_no_open_prs_labeled(self, label: str) -> None: + success = True + for issue in self.grepo.get_issues(state="open", labels=[label]): + kind = "PR" if issue.pull_request else "issue" + self.cl.fail(f"Found {kind} {util.fmt_pr(issue)} labeled [b]{e(label)}[/b]") + success = False + if success: + self.cl.success(f"Found no open PRs labeled [b]{e(label)}[/b]") + + def check_no_open_prs_labeled_backport(self) -> None: + self._check_no_open_prs_labeled(util.get_backport_label(self.version)) + + def check_no_open_prs_labeled_blocking(self) -> None: + self._check_no_open_prs_labeled(util.get_blocking_label(self.version)) + + def check_no_open_backport_prs(self) -> None: + base = util.get_releases_branch(self.version) + success = True + for pr in self.grepo.get_pulls(state="open", base=base): + if "backport" in pr.title.lower(): + self.cl.fail(f"Found backport PR #{pr.number} {util.fmt_pr(pr)}") + success = False + if success: + self.cl.success("Found no open backport PRs") + + def check_release_tag(self) -> GitRef: + tag_name = self.version.tag + what = f"Tag [b]{tag_name}[/b]" + + try: + ref = self.grepo.get_git_ref(f"tags/{tag_name}") + self.cl.success(f"{what} exists") + return ref + except UnknownObjectException: + pass + + if not self.prompt(f"{what} does not exist. Create?"): + self.cl.fatal(f"{what} does not exist") + + self.lrepo.prepare() + self.lrepo.create_tag(tag_name, util.get_releases_branch(self.version)) + + if not self.prompt(f"Push tag [b]{tag_name}[/b]?"): + self.cl.fatal(f"{what} does not exist") + self.lrepo.push(tag_name, upstream=False) + + tag = self.grepo.get_git_ref(f"tags/{tag_name}") + self.cl.success(f"{what} created") + return tag + + def check_release_ci(self, release_tag: GitRef) -> None: + tag_sha = release_tag.object.sha + runs = self.grepo.get_workflow_runs(event="push", head_sha=tag_sha).get_page(0) + if len(runs) == 0: + self.cl.fail("Release workflow run not found") + return + + run = runs[0] + what = f"[b u link={run.html_url}]Release workflow run {run.id}[/]" + + if not run.conclusion: + self.cl.blocked(f"{what} is still running") + if run.conclusion != "success": + self.cl.fatal(f"{what} failed") + self.cl.success(f"{what} finished") + + def check_release_page(self) -> None: + url = f"https://github.com/leanprover/lean4/releases/tag/{self.version}" + what = f"[b u link={url}]Release page for {self.version.tag}[/]" + try: + release = self.grepo.get_release(self.version.tag) + except UnknownObjectException: + self.cl.blocked(f"{what} not found") + + target = "This is" + if not self.version.is_stable: + target += f" release candidate {self.version.rc} for" + target += f" the {self.version.stable} release of Lean." + relnotes = f"https://lean-lang.org/doc/reference/latest/releases/{self.version.stable}/" + target += f" View the [release notes]({relnotes}) for more information." + + incorrect = [] + if release.name != str(self.version): + incorrect.append("name") + if release.body is None or release.body.strip() != target: + incorrect.append("message") + if not incorrect: + self.cl.success(f"{what} exists") + return + + if not self.prompt(f"{what} has incorrect {'/'.join(incorrect)}. Update?"): + self.cl.fail(f"{what} has incorrect {'/'.join(incorrect)}") + return + + release.update_release( + name=str(self.version), + message=target, + prerelease=not self.version.is_stable, + ) + self.cl.success(f"{what} updated") + + def check(self) -> None: + self.cl.section("Prepare release cycle") + self.check_backport_label_exists(self.version) + self.check_blocking_label_exists(self.version) + self.check_blocking_label_exists(self.version.next_minor) + self.check_release_branch_exists() + self.check_release_branch_cmake_version() + self.check_master_branch_cmake_version() + + self.cl.section("Release") + self.check_no_open_prs_labeled_backport() + self.check_no_open_prs_labeled_blocking() + self.check_no_open_backport_prs() + release_tag = self.check_release_tag() + self.check_release_ci(release_tag) + self.check_release_page() + + for drepo in repos.ALL: + self.cl.section(f"[u link={drepo.gh_url}]{e(drepo.gh_full_name)}[/u link]") + try: + DownstreamChecker(config=self.config, rrepo=drepo).check() + except SystemExit: + self.cl.failed = True + + self.cl.ensure_success() + + +class Args: + version: Version + interactive: bool + skip_weak_deps: bool + skip_mathlib_checks: bool + graph: bool + + +if __name__ == "__main__": + parser = ArgumentParser() + parser.add_argument("version", type=Version.parse) + parser.add_argument("-i", "--interactive", action="store_true") + parser.add_argument("-W", "--skip-weak-deps", action="store_true") + parser.add_argument("-M", "--skip-mathlib-checks", action="store_true") + parser.add_argument("-g", "--graph", action="store_true") + args = parser.parse_args(namespace=Args()) + + util.initialize_rich() + github = util.get_github_instance() + config = Config( + version=args.version, + interactive=args.interactive, + skip_weak_deps=args.skip_weak_deps, + skip_mathlib_checks=args.skip_mathlib_checks, + github=github, + ) + + try: + LeanChecker(config=config).check() + finally: + if args.graph: + print() + repos.print_graphviz_dot() diff --git a/script/release/pyproject.toml b/script/release/pyproject.toml new file mode 100644 index 0000000000..c84898ea26 --- /dev/null +++ b/script/release/pyproject.toml @@ -0,0 +1,10 @@ +[project] +name = "lean4-release-scripts" +version = "0.0.0" +requires-python = ">=3.13" +dependencies = [ + "click>=8.3.1", + "gitpython>=3.1.46", + "pygithub>=2.9.0", + "rich>=14.3.3", +] diff --git a/script/release/release_notes.py b/script/release/release_notes.py new file mode 100755 index 0000000000..ab098169ed --- /dev/null +++ b/script/release/release_notes.py @@ -0,0 +1,337 @@ +import datetime +import re +from argparse import ArgumentParser, Namespace +from dataclasses import dataclass +from pathlib import Path + +import repos +from git import Commit, Repo +from github.Repository import Repository +from rich import print +from rich.markup import escape as e +from rich.prompt import IntPrompt + +import util +from util import Version + +SECTIONS = [ + "Language", + "Library", + "Tactics", + "Compiler", + "Pretty Printing", + "Documentation", + "Server", + "Lake", + "Other", + "Uncategorised", +] + + +def link_commit(commit: Commit, title: str) -> str: + link = f"{repos.LEAN4.gh_url}/commit/{commit.hexsha}" + return f"[u link={link}]{e(title)}[/]" + + +def print_commit(commit: Commit, title: str) -> None: + print(f"{link_commit(commit, title)}") + + +def get_commits_for(repo: Repo, version: Version) -> list[Commit]: + print(f"Loading commits for range [cyan]{version.prev}[/]..[cyan]{version}[/]") + return list(repo.iter_commits(f"{version.prev}..{version}")) + + +def get_commit_message(commit: Commit) -> tuple[str, str]: + message = commit.message + if isinstance(message, bytes): + message = message.decode("utf-8") + + title, *body = message.splitlines() + return title.strip(), "\n".join(body).strip() + + +def parse_pr_number(title: str) -> int | None: + if match := re.search(r"\(\#(\d+)\)$", title): + return int(match.group(1)) + + +def parse_pr_title(title: str) -> tuple[str, str] | None: + parts = title.split(":", 1) + if len(parts) != 2: + return None + kind, content = parts + return kind, content + + +def parse_backport_pr_body(body: str) -> int | None: + match = re.search(r"Backport .* from #(\d+)", body) + if not match: + return + return int(match.group(1)) + + +def get_description_from_body(body: str) -> str: + paragraphs = [] + paragraph = [] + in_code_block = False + + def flush() -> None: + nonlocal paragraph + if paragraph: + paragraphs.append("\n".join(paragraph)) + paragraph = [] + + for line in body.splitlines(): + if line.startswith("```"): + in_code_block = not in_code_block + if not in_code_block and line.strip() == "": + flush() + continue + paragraph.append(line) + if not in_code_block and line.strip() == "```": + flush() + flush() + + if not paragraphs: + return "" + + description = paragraphs[0] + if paragraphs[0].endswith(":"): + description = "\n\n".join(paragraphs[:2]) + + if description.startswith("This PR "): + return description[len("This PR ") :] + + return "" # Body has incorrect format + + +def get_category(labels: set[str]) -> str | None: + cats = { + label[len("changelog-") :] for label in labels if label.startswith("changelog-") + } + if len(cats) > 1: + print(f"[red]Warning: Multiple changelog-* labels found: {cats}[/]") + if not cats: + return + + cat = cats.pop() + if cat == "doc": + return "Documentation" + if cat == "pp": + return "Pretty Printing" + return cat.capitalize() + + +@dataclass +class CommitInfo: + pr: int + kind: str + category: str | None + description: str + + +def load_commits(version: Version, repo: Repo, grepo: Repository) -> list[CommitInfo]: + skip_pr_number_prompt = False + + commits = [] + for commit in get_commits_for(repo, version): + title, _ = get_commit_message(commit) + print_commit(commit, title) + + if title == "chore: update stage0" or title.startswith("chore: CI: bump "): + print("[blue]Ignored[/]") + continue + + pr_number = parse_pr_number(title) + if pr_number is None and skip_pr_number_prompt: + print("[red]No PR number in title, skipping[/]") + continue + elif pr_number is None: + pr_number = IntPrompt.ask("[red]No PR number in title.[/] PR", default=-1) + if pr_number < 0: + print("[red]Invalid PR number, skipping[/]") + if pr_number == -2: + print("[red]Skipping PR number prompt for remaining commits[/]") + skip_pr_number_prompt = True + continue + + pr = grepo.get_pull(pr_number) + if backported := parse_backport_pr_body(pr.body or ""): + print(f"[yellow]PR is a backport of #{backported}[/]") + pr_number = backported + pr = grepo.get_pull(pr_number) + + parsed = parse_pr_title(pr.title) + if parsed is None: + print("[red]Title does not match expected format[/]") + continue + + # Intentionally overwriting commit title with PR title + kind, title = parsed + warn = kind in {"feat", "fix"} + + labels = {label.name for label in pr.get_labels()} + if "changelog-no" in labels: + print("[blue]Ignored, labeled [b]changelog-no[/b][/]") + continue + + description = get_description_from_body(pr.body or "") + if not description: + if warn: + print("[yellow]No description in body[/]") + description = title + + category = get_category(labels) + if not category: + if warn: + print("[yellow]No changelog-* label found[/]") + if category is not None and category not in SECTIONS: + print(f"[yellow]Unknown category {category!r}[/]") + category = "Uncategorised" + + info = CommitInfo( + pr=pr_number, + kind=kind, + category=category, + description=description, + ) + commits.append(info) + + return commits + + +@dataclass +class CommitCounts: + total: int + feat: int + fix: int + refactor: int + doc: int + perf: int + test: int + other: int + + +def count_by_kind(commits: list[CommitInfo]) -> CommitCounts: + feat = 0 + fix = 0 + refactor = 0 + doc = 0 + perf = 0 + test = 0 + other = 0 + for commit in commits: + if commit.kind == "feat": + feat += 1 + elif commit.kind == "fix": + fix += 1 + elif commit.kind == "refactor": + refactor += 1 + elif commit.kind == "doc": + doc += 1 + elif commit.kind == "perf": + perf += 1 + elif commit.kind == "test": + test += 1 + else: + other += 1 + return CommitCounts( + total=len(commits), + feat=feat, + fix=fix, + refactor=refactor, + doc=doc, + perf=perf, + test=test, + other=other, + ) + + +def pl(n: int, singular: str, plural: str | None = None) -> str: + plural = singular + "s" if plural is None else plural + return f"{n} {singular if n == 1 else plural}" + + +def main(version: Version, refman: Path): + util.initialize_rich() + github = util.get_github_instance() + + repo = Repo(Path(__file__).parent.parent.parent) + grepo = github.get_repo(repos.LEAN4.gh_full_name) + release = grepo.get_release(version.tag) + date = release.created_at.astimezone(datetime.timezone.utc) + title = util.get_release_notes_title_for(version, release) + + commits = load_commits(version, repo, grepo) + counts = count_by_kind(commits) + + lines = [] + lines.append("/-") + lines.append(f"Copyright (c) {date.year} Lean FRO LLC. All rights reserved.") + lines.append("Released under Apache 2.0 license as described in the file LICENSE.") + lines.append("Author: Joscha Mennicken") + lines.append("-/") + lines.append("") + lines.append("import VersoManual") + lines.append("import Manual.Meta") + lines.append("import Manual.Meta.Markdown") + lines.append("") + lines.append("open Manual") + lines.append("open Verso.Genre") + lines.append("open Verso.Genre.Manual") + lines.append("open Verso.Genre.Manual.InlineLean") + lines.append("") + lines.append(f'#doc (Manual) "{title}" =>') + lines.append("%%%") + lines.append(f'tag := "release-{version.stable}"') + lines.append(f'file := "{version.stable}"') + lines.append("%%%") + if not version.is_stable: + lines.append("") + lines.append(":::warn") + lines.append( + "These release notes describe a _release candidate_, not the final release." + ) + lines.append("They may be incomplete and are subject to change.") + lines.append(":::") + lines.append("") + lines.append(f"For this release, {pl(counts.total, 'change')} landed.") + lines.append(f"In addition to the {pl(counts.feat, 'feature addition')},") + lines.append(f"and {pl(counts.fix, 'fix', 'fixes')} listed below,") + lines.append(f"there were {pl(counts.refactor, 'refactoring change')},") + lines.append(f"{pl(counts.doc, 'documentation improvement')},") + lines.append(f"{pl(counts.perf, 'performance improvement')},") + lines.append(f"{pl(counts.test, 'improvement')} to the test suite,") + lines.append(f"and {pl(counts.other, 'other change')}.") + for section in SECTIONS: + for_section = [commit for commit in commits if commit.category == section] + if not for_section: + continue + lines.append("") + lines.append(f"# {section}") + lines.append("") + lines.append("````markdown") + for commit in for_section: + lines.append("") + lines.append(f"- [#{commit.pr}]({repos.LEAN4.gh_url}/pull/{commit.pr})") + for line in commit.description.splitlines(): + lines.append(f" {line}".rstrip()) + lines.append("") + lines.append("````") + + out = refman / util.get_release_notes_path_for(version) + out.write_text("\n".join(lines) + "\n") + + +class Args(Namespace): + version: Version + refman: Path + + +if __name__ == "__main__": + parser = ArgumentParser() + parser.add_argument("version", type=Version.parse) + parser.add_argument("refman", type=Path) + args = parser.parse_args(namespace=Args) + main(args.version, args.refman) diff --git a/script/release/repos.py b/script/release/repos.py new file mode 100644 index 0000000000..4ef4e50ba3 --- /dev/null +++ b/script/release/repos.py @@ -0,0 +1,456 @@ +from argparse import ArgumentParser + +from util import ReleaseRepo + +ALL: list[ReleaseRepo] = [] +BY_FULL_NAME: dict[str, ReleaseRepo] = {} + + +def _register(repo: ReleaseRepo) -> None: + ALL.append(repo) + BY_FULL_NAME[repo.gh_full_name] = repo + + +################## +## Repositories ## +################## + + +# Repositories managed by this release process should specify their dependencies +# through reservoir name/scope. The versions should be specified via tags, where +# available, or commit hashes otherwise. + + +# For release `v4.X.0-rc1`, a branch `releases/v4.X.0` is created off of +# `master`. This branch is reused for all subsequent release candidates and +# releases with the same major and minor version, e.g. `v4.X.0`, `v4.X.1`. +# +# `src/CMakeLists.txt` contains the variables LEAN_VERSION_MAJOR, +# LEAN_VERSION_MINOR, LEAN_VERSION_PATCH, and LEAN_VERSION_IS_RELEASE. On +# master, these should point to the next release once the release branch is cut, +# i.e. `v4.X+1.0`, and LEAN_VERSION_IS_RELEASE should be 0. On the release +# branch, these should point to the current release (and updated only when +# necessary for patch releases), and LEAN_VERSION_IS_RELEASE should be 1. +# +# Before creating a release, ensure that no blocking issues/PRs or open backport +# PRs exist. See also the labels `backport releases/v4.X.0` and +# `blocks-release-v4.X.0` on GitHub. There should also be a +# `blocks-release-v4.X+1.0` label corresponding to the CMakeLists version on +# `master`, which should be created after cutting a release branch. +# +# To create a release, push a tag `v4.X.Y` or `v4.X.Y-rcZ`. The tag triggers CI, +# which builds the release artifacts and creates a release on GitHub. +# +# After a release has been created, its description may need to be updated. For +# release candidates, it should read "This is the n-th release candidate for the +# v4.X.Y release of Lean." For releases, it should read "This is the v4.X.Y +# release of Lean. View the release notes for more information." where "release +# notes" is a link to the corresponding release notes section. If the release +# notes has not yet been updated, this second sentence can be omitted and added +# later. +# +# Finally, all the other repos listed below should be updated to use the newly +# released version of Lean. +LEAN4 = ReleaseRepo(github=("leanprover", "lean4")) +# Don't register this repo! + +LEAN4_NIGHTLY = ReleaseRepo(github=("leanprover", "lean4-nightly")) +# Don't register this repo! + + +# To create a new release, open a PR into `main`. In it, bump the toolchain. +# +# For `v4.X.0-rc1` releases, use the existing `bump/v4.X.0` branch. To get the +# latest nightly fixes, you may need to merge the latest +# `bump/nightly-YYYY-MM-DD` PRs, or merge `nightly-testing` directly. After +# merging the PR, create a new `bump/v4.X+1.0` branch off of `main`. +# +# For other releases, create a new branch off of `main` and use it for the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +# Then, update the `stable` branch to point to the same commit. +BATTERIES = ReleaseRepo( + github=("leanprover-community", "batteries"), + bump_branch=True, + release_tag="lean", + stable_branch="stable", +) +_register(BATTERIES) + + +# To create a new release, open a PR into `master`. In it, bump the toolchain +# and all dependencies. For `v4.X.0-rc1` releases, you may need to merge +# `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +# Then, update the `stable` branch to point to the same commit. +AESOP = ReleaseRepo( + github=("leanprover-community", "aesop"), + release_tag="lean", + stable_branch="stable", + strong_deps=[BATTERIES], +) +_register(AESOP) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. For `v4.X.0-rc1` releases, you may need to merge +# `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +LEAN4_CLI = ReleaseRepo( + github=("leanprover", "lean4-cli"), + release_tag="lean", +) +_register(LEAN4_CLI) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. For `v4.X.0-rc1` releases, you may need to merge +# `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +IMPORT_GRAPH = ReleaseRepo( + github=("leanprover-community", "import-graph"), + release_tag="lean", + strong_deps=[LEAN4_CLI], +) +_register(IMPORT_GRAPH) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain. For +# `v4.X.0-rc1` releases, you may need to merge `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +PLAUSIBLE = ReleaseRepo( + github=("leanprover-community", "plausible"), + release_tag="lean", +) +_register(PLAUSIBLE) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain. For +# `v4.X.0-rc1` releases, you may need to merge `nightly-testing` into the PR. +# +# Obtain the next ProofWidgets version number by incrementing the patch version +# of the latest release (which will have the form `v0.0.X`). Once the release PR +# is merged, tag the resulting commit with the new version number. +PROOFWIDGETS4 = ReleaseRepo( + github=("leanprover-community", "ProofWidgets4"), + release_tag="proofwidgets", +) +_register(PROOFWIDGETS4) + +# To create a new release, open a PR into `main`. In it, bump the toolchain. For +# `v4.X.0-rc1` releases, you may need to merge `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +# Then, update the `stable` branch to point to the same commit. +QUOTE4 = ReleaseRepo( + github=("leanprover-community", "quote4"), + release_tag="lean", + stable_branch="stable", +) +_register(QUOTE4) + + +# To create a new release, open a PR into `master`. In it, bump the toolchain +# and all dependencies. +# +# For `v4.X.0-rc1` releases, use the existing `bump/v4.X.0` branch from the +# nightly repo. To get the latest nightly fixes, you may need to merge the +# latest `bump/nightly-YYYY-MM-DD` PRs, or merge `nightly-testing` directly. +# After merging the PR, create a new `bump/v4.X+1.0` branch off of `master`. +# +# For other releases, create a new branch off of `master` and use it for the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +# Then, update the `stable` branch to point to the same commit. +MATHLIB4 = ReleaseRepo( + github=("leanprover-community", "mathlib4"), + nightly=ReleaseRepo(github=("leanprover-community", "mathlib4-nightly-testing")), + bump_branch=True, + release_tag="lean", + stable_branch="stable", + strong_deps=[BATTERIES, QUOTE4, AESOP, PROOFWIDGETS4, IMPORT_GRAPH, PLAUSIBLE], +) +_register(MATHLIB4) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. +# +# For `v4.X.0-rc1` releases, use the existing `bump/v4.X.0` branch. To get the +# latest nightly fixes, you may need to merge the latest +# `bump/nightly-YYYY-MM-DD` PRs, or merge `nightly-testing` directly. After +# merging the PR, create a new `bump/v4.X+1.0` branch off of `main`. +# +# For other releases, create a new branch off of `main` and use it for the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +# Then, update the `stable` branch to point to the same commit. +CSLIB = ReleaseRepo( + github=("leanprover", "cslib"), + bump_branch=True, + release_tag="lean", + stable_branch="stable", + strong_deps=[MATHLIB4], +) +_register(CSLIB) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. Also bump the toolchain and deps in `test/Mathlib`. Maybe +# run the tests locally before creating the PR? For `v4.X.0-rc1` releases, you +# may need to merge `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +# Then, update the `stable` branch to point to the same commit. +REPL = ReleaseRepo( + github=("leanprover-community", "repl"), + release_tag="lean", + stable_branch="stable", + strong_deps=[MATHLIB4], # For tests in CI +) +_register(REPL) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies, then run `update-subverso.sh`. For `v4.X.0-rc1` releases, +# you may need to merge `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +VERSO = ReleaseRepo( + github=("leanprover", "verso"), + release_tag="lean", + strong_deps=[PLAUSIBLE], + weak_deps=[MATHLIB4], # For benchmarks +) +_register(VERSO) + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. For `v4.X.0-rc1` releases, you may need to merge +# `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +VERSO_WEB_COMPONENTS = ReleaseRepo( + github=("leanprover", "verso-web-components"), + release_tag="lean", + strong_deps=[VERSO], +) +_register(VERSO_WEB_COMPONENTS) + + +# To bump the toolchain, open a PR into `main`. In it, bump the toolchain and +# all dependencies. +# +# For `v4.X.0-rc1` releases, generate a new set of release notes and ensure +# they're imported and linked. For other releases, regenerate the existing +# release notes. For `v4.X.0-rc1` releases, you may also need to merge +# `nightly-testing` into the PR. +# +# Once the toolchain bump PR is merged, tag the resulting commit with the lean +# version. If the tag already exists, it may need to be updated manually. +# +# Highlights should be added in a separate PR and merged only shortly before the +# final release. That way, they don't get in the way of the RC bumps and can be +# commented on by the other developers. +REFERENCE_MANUAL = ReleaseRepo( + github=("leanprover", "reference-manual"), + release_tag="lean", + strong_deps=[VERSO_WEB_COMPONENTS, VERSO], +) +_register(REFERENCE_MANUAL) + + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. Also bump the toolchain and dependencies in `examples/hero`. +# Finally, run `scripts/update.sh`. For `v4.X.0-rc1` releases, you may need to +# merge `nightly-testing` into the PR. +LEAN_FRO_ORG = ReleaseRepo( + github=("leanprover", "lean-fro.org"), + strong_deps=[VERSO, VERSO_WEB_COMPONENTS], +) +_register(LEAN_FRO_ORG) + + +# To create a new release, trigger the "Update Toolchain" CI workflow and wait +# for it to open a PR, then merge the PR if it looks good. For non-RC releases, +# wait for the maintainer to release a new version. +LEAN4_UNICODE_BASIC = ReleaseRepo( + github=("fgdorais", "lean4-unicode-basic"), +) +_register(LEAN4_UNICODE_BASIC) + + +# To create a new release, open a PR into `master`. In it, bump the toolchain +# and all dependencies. For `v4.X.0-rc1` releases, you may need to merge +# `nightly-testing` into the PR. +BIBTEX_QUERY = ReleaseRepo( + github=("dupuisf", "BibtexQuery"), + release_tag="lean", + strong_deps=[LEAN4_UNICODE_BASIC], +) +_register(BIBTEX_QUERY) + +# To create a new release, open a PR into `master`. In it, bump the toolchain +# and all dependencies. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +LEANSQLITE = ReleaseRepo( + github=("leanprover", "leansqlite"), + release_tag="lean", + strong_deps=[PLAUSIBLE], +) +_register(LEANSQLITE) + +# To create a new release, open a PR into `main`. In it, bump the toolchain and +# all dependencies. For `v4.X.0-rc1` releases, you may need to merge +# `nightly-testing` into the PR. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +DOC_GEN4 = ReleaseRepo( + github=("leanprover", "doc-gen4"), + release_tag="lean", + strong_deps=[BIBTEX_QUERY, LEAN4_UNICODE_BASIC, LEAN4_CLI, LEANSQLITE], + # Doc-gen4 shouldn't lag behind mathlib if possible because of downstream + # users, and doc-gen4 benchmarks failing for a short while is an acceptable + # price to pay for that. + # https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Tagging.20commits.20in.20mathlib4/near/585725955 + ignored_deps=[MATHLIB4], # For benchmarks +) +_register(DOC_GEN4) +BATTERIES.ignored_deps.append(DOC_GEN4) + + +# To create a new release, open a PR into `master`. In it, bump the toolchain +# and all dependencies. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +COMPARATOR = ReleaseRepo( + github=("leanprover", "comparator"), + release_tag="lean", +) +_register(COMPARATOR) + + +# To create a new release, open a PR into `master`. In it, bump the toolchain +# and all dependencies. +# +# Once the release PR is merged, tag the resulting commit with the lean version. +LEAN4EXPORT = ReleaseRepo( + github=("leanprover", "lean4export"), + release_tag="lean", +) +_register(LEAN4EXPORT) + + +################### +## Visualization ## +################### + + +def transitive_strong_deps(repo: ReleaseRepo) -> set[str]: + result = set() + for dep in repo.strong_deps: + result.add(dep.gh_full_name) + result |= transitive_strong_deps(dep) + return result + + +def indirect_strong_deps(repo: ReleaseRepo) -> set[str]: + result = set() + for dep in repo.strong_deps: + result |= transitive_strong_deps(dep) + return result + + +def graphviz_attrs(**kwargs: str) -> str: + if not kwargs: + return "" + style_str = " ".join(f"{k}=<{v}>" for k, v in kwargs.items()) + return f" [{style_str}]" + + +def print_graphviz_line( + repo: ReleaseRepo, + dep: ReleaseRepo, + comment: bool = False, + attrs: dict[str, str] | None = None, +) -> None: + comment_str = "// " if comment else "" + attrs_str = graphviz_attrs(**attrs or {}) + print(f' {comment_str}"{dep.gh_full_name}" -> "{repo.gh_full_name}"{attrs_str};') + + +def print_graphviz_dot( + prune: bool = True, no_weak: bool = False, no_ignored: bool = False +) -> None: + print("digraph G {") + print(" rankdir=LR;") + + for repo in sorted(ALL, key=lambda r: r.gh_full_name): + indirect = indirect_strong_deps(repo) + + # label = f"{repo.gh_owner}{repo.gh_name}" + label = f'{repo.gh_owner}
{repo.gh_name}' + attrs = {"label": label} + if repo.completed: + attrs["style"] = "filled" + attrs["color"] = "palegreen" + print(f' "{repo.gh_full_name}"{graphviz_attrs(**attrs)};') + + for dep in repo.strong_deps: + comment = prune and dep.gh_full_name in indirect + print_graphviz_line(repo, dep, comment=comment) + for dep in repo.weak_deps: + comment = no_weak or (prune and dep.gh_full_name in indirect) + print_graphviz_line(repo, dep, comment=comment, attrs={"style": "dashed"}) + for dep in repo.ignored_deps: + comment = no_ignored or (prune and dep.gh_full_name in indirect) + attrs = {"style": "dashed", "color": "red", "constraint": "false"} + print_graphviz_line(repo, dep, comment=comment, attrs=attrs) + + print("}") + + +def print_all_urls() -> None: + for repo in ALL: + print(f"- {repo.gh_url}") + + +def clone_all_repos() -> None: + for repo in ALL: + print(f"Cloning {repo.gh_full_name}...") + repo.local.prepare() + + +class Args: + graph: bool + prune: bool + no_weak: bool + no_ignored: bool + urls: bool + clone: bool + + +if __name__ == "__main__": + parser = ArgumentParser() + parser.add_argument("-g", "--graph", action="store_true") + parser.add_argument("-p", "--prune", action="store_true") + parser.add_argument("-W", "--no-weak", action="store_true") + parser.add_argument("-I", "--no-ignored", action="store_true") + parser.add_argument("-u", "--urls", action="store_true") + parser.add_argument("-c", "--clone", action="store_true") + args = parser.parse_args(namespace=Args()) + + if args.graph: + print_graphviz_dot( + prune=args.prune, no_weak=args.no_weak, no_ignored=args.no_ignored + ) + + if args.urls: + print_all_urls() + + if args.clone: + clone_all_repos() diff --git a/script/release/util.py b/script/release/util.py new file mode 100644 index 0000000000..8e67b65c2f --- /dev/null +++ b/script/release/util.py @@ -0,0 +1,554 @@ +import datetime +import re +import shlex +import subprocess +import urllib.parse +from dataclasses import dataclass, field +from os import PathLike +from pathlib import Path +from re import Match, Pattern +from typing import Callable, Literal, NoReturn, Self + +from github import Auth, Github +from github.GithubException import UnknownObjectException +from github.GitRelease import GitRelease +from github.Issue import Issue +from github.PullRequest import PullRequest +from github.Repository import Repository +from github.Tag import Tag +from rich import get_console, print, reconfigure +from rich.markup import escape as e + +type Arg = str | bytes | PathLike[str] | PathLike[bytes] + + +def run(*args: Arg, cwd: Path | None = None, silent: bool = False) -> None: + print(f"[bright_black]$ {e(' '.join(shlex.quote(str(arg)) for arg in args))}[/]") + subprocess.run(args, check=True, cwd=cwd, capture_output=silent) + + +def run_stdout(*args: Arg, cwd: Path | None = None) -> str: + print(f"[bright_black]$ {e(' '.join(shlex.quote(str(arg)) for arg in args))}[/]") + return subprocess.run( + args, + check=True, + stdout=subprocess.PIPE, + text=True, + cwd=cwd, + ).stdout + + +def prompt(message: str, options: str = "Yn") -> str: + default: str | None = None + for c in options: + if c.isupper(): + default = c.lower() + break + + options = options.lower() + options_display = "/".join(c.upper() if c == default else c for c in options) + + console = get_console() + while True: + response = ( + console.input(f"{message} [cyan]\\[{options_display}]:[/] ").strip().lower() + ) + if not response and default: + return default + elif response in options.lower(): + return response + else: + print(f"Please enter {options_display}.") + + +@dataclass +class Version: + major: int + minor: int + patch: int + rc: int | None = None + + @classmethod + def parse(cls, s: str) -> Self: + m = re.fullmatch(r"v(\d+)\.(\d+)\.(\d+)(-rc(\d+))?", s) + if m is None: + raise ValueError(f"Invalid version string: {s!r}") + return cls( + major=int(m.group(1)), + minor=int(m.group(2)), + patch=int(m.group(3)), + rc=int(m.group(5)) if m.group(4) else None, + ) + + @property + def raw(self) -> str: + main = f"{self.major}.{self.minor}.{self.patch}" + rc = "" if self.rc is None else f"-rc{self.rc}" + return main + rc + + @property + def tag(self) -> str: + return f"v{self.raw}" + + @property + def base(self) -> Self: + return Version(major=self.major, minor=self.minor, patch=0, rc=None) + + @property + def next_minor(self) -> Self: + return Version(major=self.major, minor=self.minor + 1, patch=0, rc=None) + + @property + def prev(self) -> Self: + if self.patch > 0: + return Version(major=self.major, minor=self.minor, patch=self.patch - 1) + return Version(major=self.major, minor=self.minor - 1, patch=0) + + @property + def stable(self) -> Self: + return Version(major=self.major, minor=self.minor, patch=self.patch, rc=None) + + @property + def is_stable(self) -> bool: + return self.rc is None + + def __str__(self) -> str: + return self.tag + + +@dataclass +class ReleaseRepo: + github: tuple[str, str] # (owner, name) + + # If present, nightly-related branches and tags are expected to be in this + # repo instead of the main repo. + nightly: Self | None = None + + # Use "bump/v4.X.0" branches for rc1 releases. Respect `nightly` if set. + bump_branch: bool = False + + # When set, the version bump commit should be tagged. When set to "lean", + # use the lean version tag as release tag. When set to "proofwidgets", use + # proofwidgets versioning logic. + release_tag: Literal["lean", "proofwidgets"] | None = None + + # When set, this branch should be updated to point to the version bump commit. + stable_branch: str | None = None + + # Strong deps are dependencies that *must* be updated before a new version + # of the repo can be released. Strong deps include all dependencies + # specified in the lakefile, as well as those used by CI involved in merging + # PRs or creating releases. + strong_deps: list[Self] = field(default_factory=list) + + # Weak deps are indirect dependencies that are not strictly required to + # create a new release, but make life easier if they're respected. For + # example, this includes dependencies in parts of the CI that are not + # related to releases, or dependencies used during benchmarking. + # + # These dependencies should be safe to ignore when time-critical. + weak_deps: list[Self] = field(default_factory=list) + + # Ignored deps are weak deps that are intentionally ignored, e.g. to prevent + # dependency cycles. + ignored_deps: list[Self] = field(default_factory=list) + + # Mutable + completed: bool = False + + @property + def gh_owner(self) -> str: + return self.github[0] + + @property + def gh_name(self) -> str: + return self.github[1] + + @property + def gh_full_name(self) -> str: + return "/".join(self.github) + + @property + def gh_url(self) -> str: + return f"https://github.com/{self.gh_full_name}" + + @property + def local(self) -> "LocalRepo": + path = Path(__file__).parent.parent.parent.parent / "release" / self.gh_name + return LocalRepo(rrepo=self, path=path) + + +@dataclass +class LocalRepo: + rrepo: ReleaseRepo + path: Path + + def run(self, *args: Arg, silent: bool = False) -> None: + run(*args, cwd=self.path, silent=silent) + + def run_stdout(self, *args: Arg) -> str: + return run_stdout(*args, cwd=self.path) + + def git(self, *args: Arg, silent: bool = False) -> None: + self.run("git", *args, silent=silent) + + def git_stdout(self, *args: Arg) -> str: + return self.run_stdout("git", *args) + + def _prepare_remotes(self, nightly: ReleaseRepo | None) -> None: + target = {"origin": self.rrepo} + if nightly: + target["nightly"] = nightly + + actual = {r.strip() for r in self.git_stdout("remote").splitlines()} + + for remote in actual - target.keys(): + self.git("remote", "remove", remote) + + for name, repo in target.items(): + url = f"git@github.com:{repo.gh_full_name}.git" + if name in actual: + self.git("remote", "set-url", name, url) + else: + self.git("remote", "add", name, url) + + def prepare(self, nightly: ReleaseRepo | None = None) -> None: + # Clone + if not self.path.exists(): + run("gh", "repo", "clone", self.rrepo.gh_full_name, self.path) + + self._prepare_remotes(nightly) + + # Check worktree is ready + self.git("diff", "--quiet") + self.git("clean", "-dffx", silent=True) + + # Fetch recent changes + self.git("fetch", "--all", "--prune", "--prune-tags", "--force", silent=True) + if nightly: # Some tags may have been pruned away + self.git("fetch", "--all", "--prune", silent=True) + + def switch(self, branch: str, remote: str = "origin") -> None: + self.git("switch", "-C", branch, f"{remote}/{branch}") + + def create_branch( + self, branch: str, remote: str = "origin", remote_branch: str | None = None + ) -> None: + if remote_branch is None: + self.git("switch", "-C", branch, remote) # Default branch + else: + self.git("switch", "-C", branch, f"{remote}/{remote_branch}") + + def create_tag(self, tag: str, target: str) -> None: + self.git("tag", "-f", tag, target) + + def commit(self, message: str) -> None: + self.git("add", ".") + try: + self.git("diff", "--cached", "--quiet") + except Exception: + self.git("commit", "-m", message) + + def push(self, branch: str, remote: str = "origin", upstream: bool = True) -> None: + if upstream: + self.git("push", "-u", remote, branch, silent=True) + else: + self.git("push", remote, branch, silent=True) + + +class Checklist: + def __init__(self) -> None: + self.failed = False + + def section(self, *message: str) -> None: + print() + print(f"[bold]{''.join(message)}[/]") + + def success(self, *message: str) -> None: + print(f"[b green]\\[Y][/] {''.join(message)}") + + def warn(self, *message: str) -> None: + print(f"[b yellow]\\[W][/] {''.join(message)}") + + def wait(self, *message: str) -> None: + print(f"[b yellow]\\[B][/] {''.join(message)}") + self.failed = True + + def blocked(self, *message: str) -> NoReturn: + print(f"[b yellow]\\[B][/] {''.join(message)}") + raise SystemExit(1) + + def fail(self, *message: str) -> None: + print(f"[b red]\\[N][/] {''.join(message)}") + self.failed = True + + def fatal(self, *message: str) -> NoReturn: + print(f"[b red]\\[N][/] {''.join(message)}") + raise SystemExit(1) + + def ensure_success(self) -> None: + if self.failed: + raise SystemExit(1) + + +def initialize_rich() -> None: + reconfigure(highlight=False) + + +def get_github_instance() -> Github: + try: + token = run_stdout("gh", "auth", "token").strip() + print("Using GitHub token from `gh auth token`") + return Github(auth=Auth.Token(token)) + except Exception: + Checklist().fatal("Failed to get GitHub token from `gh auth token`") + + +def get_releases_branch(version: Version) -> str: + return f"releases/{version.base}" + + +def get_bump_branch(version: Version) -> str: + return f"bump/{version.base}" + + +def get_backport_label(version: Version) -> str: + return f"backport {get_releases_branch(version)}" + + +def get_blocking_label(version: Version) -> str: + return f"blocks-release-{version.base}" + + +def get_latest_nightly_tag(grepo: Repository) -> Tag: + for tag in grepo.get_tags(): + return tag + raise SystemExit("No lean4 nightly tags found") + + +def get_file_contents(grepo: Repository, ref: str, path: str | Path) -> str: + if isinstance(path, Path): + assert not path.is_absolute() + path = str(path) + + try: + file = grepo.get_contents(path, ref=ref) + except UnknownObjectException: + raise SystemExit(f"Failed to read {path!r} from {ref!r} in {grepo.full_name!r}") + if isinstance(file, list): + raise SystemExit(f"Failed to read {path!r} from {ref!r} in {grepo.full_name!r}") + return file.decoded_content.decode("utf-8") + + +def edit( + path: Path, pattern: Pattern[str] | str, repl: Callable[[Match[str]], str] | str +) -> None: + text = path.read_text() + text = re.sub(pattern, repl, text) + path.write_text(text) + + +######### +## PRs ## +######### + + +def fmt_pr(pr: PullRequest | Issue) -> str: + return f"[link={pr.html_url}][green]#{pr.number}[/green] [b u]{e(pr.title)}[/b u][/link]" + + +def find_pr(grepo: Repository, head: str, base: str, title: str) -> PullRequest | None: + head = f"{grepo.owner.login}:{head}" + + for pr in grepo.get_pulls( + state="all", head=head, base=base, sort="created", direction="desc" + ).get_page(0): + return pr + + for pr in grepo.get_pulls( + state="all", base=base, sort="created", direction="desc" + ).get_page(0): + if title in pr.title: + return pr + + +def create_pr(grepo: Repository, head: str, base: str, title: str) -> PullRequest: + head = f"{grepo.owner.login}:{head}" + return grepo.create_pull(head=head, base=base, title=title) + + +# https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/using-query-parameters-to-create-a-pull-request +def create_pr_url( + base: ReleaseRepo, + base_branch: str, + head: ReleaseRepo, + head_branch: str, + title: str, + body: str = "", +) -> str: + url = f"{base.gh_url}/compare/{base_branch}...{head.gh_owner}:{head.gh_name}:{head_branch}" + params = {"title": title, "body": body} + return f"{url}?{urllib.parse.urlencode(params)}" + + +################### +## Cmake version ## +################### + + +@dataclass +class CMakeVersion: + version: Version + is_release: bool + + +def _parse_cmake_set(text: str, component: str) -> int: + match = re.search(rf"set\({component}\s+(\d+) ", text) + if not match: + raise ValueError(f"Failed to parse {component} from CMakeLists.txt") + return int(match.group(1)) + + +def _update_cmake_set(text: str, component: str, value: int) -> str: + return re.sub(rf"set\({component}\s+\d+ ", f"set({component} {value} ", text) + + +def get_cmake_version(grepo: Repository, ref: str) -> CMakeVersion: + text = get_file_contents(grepo, ref, "src/CMakeLists.txt") + major = _parse_cmake_set(text, "LEAN_VERSION_MAJOR") + minor = _parse_cmake_set(text, "LEAN_VERSION_MINOR") + patch = _parse_cmake_set(text, "LEAN_VERSION_PATCH") + is_release = _parse_cmake_set(text, "LEAN_VERSION_IS_RELEASE") + return CMakeVersion(Version(major, minor, patch), bool(is_release)) + + +def set_cmake_version(lrepo: LocalRepo, version: CMakeVersion) -> None: + cmakelists = lrepo.path / "src" / "CMakeLists.txt" + text = cmakelists.read_text() + text = _update_cmake_set(text, "LEAN_VERSION_MAJOR", version.version.major) + text = _update_cmake_set(text, "LEAN_VERSION_MINOR", version.version.minor) + text = _update_cmake_set(text, "LEAN_VERSION_PATCH", version.version.patch) + text = _update_cmake_set(text, "LEAN_VERSION_IS_RELEASE", int(version.is_release)) + cmakelists.write_text(text) + + +################### +## Release notes ## +################### + + +def get_release_notes_path_for(version: Version) -> str: + stem = str(version.stable).replace(".", "_") + return f"Manual/Releases/{stem}.lean" + + +def get_release_notes_title_for(version: Version, release: GitRelease) -> str: + date = release.created_at.astimezone(datetime.timezone.utc).strftime("%Y-%m-%d") + return f"Lean {version.raw} ({date})" + + +def get_release_notes_title(grepo: Repository, version: Version) -> str | None: + path = get_release_notes_path_for(version) + try: + text = get_file_contents(grepo, grepo.default_branch, path) + except SystemExit: + return None + + match = re.search(r'#doc \(Manual\) "(.+)" =>', text) + if match is None: + raise ValueError(f"Failed to parse release notes title from {grepo.full_name}") + return match.group(1) + + +def set_release_notes_title( + lrepo: LocalRepo, version: Version, release: GitRelease +) -> None: + file = lrepo.path / get_release_notes_path_for(version) + title = get_release_notes_title_for(version, release) + edit(file, r'#doc \(Manual\) ".+" =>', f'#doc (Manual) "{title}" =>') + + +############### +## Toolchain ## +############### + + +def get_toolchain_for(version: Version) -> str: + return f"leanprover/lean4:{version.tag}" + + +def get_toolchain(grepo: Repository, ref: str) -> str: + return get_file_contents(grepo, ref, "lean-toolchain").strip() + + +def set_toolchain(path: Path, tag: str) -> None: + toolchain_file = path / "lean-toolchain" + toolchain_file.write_text(f"leanprover/lean4:{tag}\n") + + +##################### +## Toolchain bumps ## +##################### + + +def get_toolchain_bump_message(version: Version) -> str: + return f"chore: bump toolchain to {version}" + + +# Assumes the PR has been merged into master in some way +# Assumes the commit message is predictable +def find_merged_toolchain_bump_sha(lrepo: LocalRepo, version: Version) -> str: + n = 100 + expected = get_toolchain_bump_message(version) + + for line in lrepo.git_stdout( + "log", + "origin", + "--pretty=format:%H %s", + f"--max-count={n}", + ).splitlines(): + sha, message = line.split(" ", 1) + if message == expected or message.startswith(expected + " "): + return sha + + raise SystemExit(f"Failed to find release commit in {n} latest commits") + + +########################### +## ProofWidgets releases ## +########################### + + +def get_proofwidgets_release_for(grepo: Repository, version: Version) -> Tag | None: + expected_toolchain = get_toolchain_for(version) + for tag in grepo.get_tags().get_page(0): + if not re.fullmatch(r"v0\.0\.\d+", tag.name): + continue + toolchain = get_file_contents(grepo, tag.commit.sha, "lean-toolchain") + if toolchain.strip() == expected_toolchain: + return tag + + +def get_next_proofwidgets_release(grepo: Repository) -> str: + for tag in grepo.get_tags(): + if match := re.fullmatch(r"v0\.0\.(\d+)", tag.name): + patch = int(match.group(1)) + return f"v0.0.{patch + 1}" + raise SystemExit("No releases found in tags") + + +################################## +## lean4-unicode-basic releases ## +################################## + + +def get_lean_unicode_basic_release_for( + grepo: Repository, version: Version +) -> Tag | None: + expected_toolchain = get_toolchain_for(version) + for tag in grepo.get_tags().get_page(0): + if not re.fullmatch(r"v\d+\.\d+\.\d+", tag.name): + continue + toolchain = get_file_contents(grepo, tag.commit.sha, "lean-toolchain") + if toolchain.strip() == expected_toolchain: + return tag diff --git a/script/release_checklist.py b/script/release_checklist.py deleted file mode 100755 index 185e3fbf03..0000000000 --- a/script/release_checklist.py +++ /dev/null @@ -1,1027 +0,0 @@ -#!/usr/bin/env python3 - -""" -Release Checklist for Lean4 and Downstream Repositories - -This script validates the status of a Lean4 release across all dependent repositories. -It checks whether repositories are ready for release and identifies missing steps. - -IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior! - -What this script does: -1. Validates preliminary Lean4 release infrastructure: - - Checks that the release branch (releases/vX.Y.0) exists - - Verifies CMake version settings are correct (both src/ and stage0/) - - Confirms the release tag exists - - Validates the release page exists on GitHub (created automatically by CI after tag push) - - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository) - - **IMPORTANT: If the release page doesn't exist, the script will skip checking - downstream repositories and the master branch configuration. The preliminary - infrastructure must be in place before the release process can proceed.** - - **NOTE: The GitHub release page is created AUTOMATICALLY by CI after the tag is pushed. - DO NOT create it manually. Wait for CI to complete after pushing the tag.** - -2. For each downstream repository (batteries, mathlib4, etc.): - - Checks if dependencies are ready (e.g., mathlib4 depends on batteries) - - Verifies the main branch is on the target toolchain (or newer) - - Checks if a PR exists to bump the toolchain (if not yet updated) - - Validates tags exist for the release version - - Ensures tags are merged into stable branches (for non-RC releases) - - Verifies bump branches exist and are configured correctly - - Special handling for ProofWidgets4 release tags - - For mathlib4: runs verify_version_tags.py to validate the release tag - (checks git/GitHub consistency, toolchain, elan, cache, and build) - -3. Optionally automates missing steps (when not in --dry-run mode): - - Creates missing release tags using push_repo_release_tag.py - - Merges tags into stable branches using merge_remote.py - -Usage: - ./release_checklist.py v4.24.0 # Check release status - ./release_checklist.py v4.24.0 --verbose # Show detailed debug info - ./release_checklist.py v4.24.0 --dry-run # Check only, don't execute fixes - -For automated release management with Claude Code: - /release v4.24.0 # Run full release process with Claude - -The script reads repository configurations from release_repos.yml and reports: -- ✅ for completed requirements -- ❌ for missing requirements (with instructions to fix) -- 🟡 for repositories waiting on dependencies -- ⮕ for automated actions being taken - -This script is idempotent and safe to rerun multiple times. -""" - -import argparse -import yaml -import requests -import base64 -import subprocess -import sys -import os -import re # Import re module -# Import run_command from merge_remote.py -from merge_remote import run_command - -def debug(verbose, message): - """Print debug message if verbose mode is enabled.""" - if verbose: - print(f" [DEBUG] {message}") - -def parse_repos_config(file_path): - with open(file_path, "r") as f: - return yaml.safe_load(f)["repositories"] - -def get_github_token(): - try: - import subprocess - result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True) - if result.returncode == 0: - return result.stdout.strip() - except FileNotFoundError: - print("Warning: 'gh' CLI not found. Some API calls may be rate-limited.") - return None - -def strip_rc_suffix(toolchain): - """Remove -rcX suffix from the toolchain.""" - return toolchain.split("-")[0] - -def branch_exists(repo_url, branch, github_token): - api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/branches/{branch}" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - response = requests.get(api_url, headers=headers) - return response.status_code == 200 - -def tag_exists(repo_url, tag_name, github_token): - # Use /git/matching-refs/tags/ to get all matching tags - api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/matching-refs/tags/{tag_name}" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - response = requests.get(api_url, headers=headers) - - if response.status_code != 200: - return False - - # Check if any of the returned refs exactly match our tag - matching_tags = response.json() - return any(tag["ref"] == f"refs/tags/{tag_name}" for tag in matching_tags) - -def commit_hash_for_tag(repo_url, tag_name, github_token): - # Use /git/matching-refs/tags/ to get all matching tags - api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/matching-refs/tags/{tag_name}" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - response = requests.get(api_url, headers=headers) - - if response.status_code != 200: - return False - - # Check if any of the returned refs exactly match our tag - matching_tags = response.json() - matching_commits = [tag["object"]["sha"] for tag in matching_tags if tag["ref"] == f"refs/tags/{tag_name}"] - if len(matching_commits) != 1: - return None - else: - return matching_commits[0] - -def release_page_exists(repo_url, tag_name, github_token): - api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/releases/tags/{tag_name}" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - response = requests.get(api_url, headers=headers) - return response.status_code == 200 - -def get_tag_workflow_status(repo_url, tag_name, github_token): - """Get the status of CI workflows running for a specific tag.""" - api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/") - headers = {'Authorization': f'token {github_token}'} if github_token else {} - - # Get workflow runs for the tag - # GitHub's workflow runs API uses the branch/tag name in the 'head_branch' field - api_url = f"{api_base}/actions/runs?event=push&head_branch={tag_name}" - response = requests.get(api_url, headers=headers) - - if response.status_code != 200: - return None - - data = response.json() - workflow_runs = data.get('workflow_runs', []) - - if not workflow_runs: - return None - - # Get the most recent workflow run for this tag - run = workflow_runs[0] - status = run.get('status') - conclusion = run.get('conclusion') - workflow_name = run.get('name', 'CI') - run_id = run.get('id') - - return { - 'status': status, - 'conclusion': conclusion, - 'workflow_name': workflow_name, - 'run_id': run_id - } - -def get_release_notes(tag_name): - """Fetch release notes page title from lean-lang.org.""" - # Strip -rcX suffix if present for the URL - base_tag = tag_name.split('-')[0] - reference_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/" - try: - response = requests.get(reference_url) - response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx) - - # Extract title using regex - match = re.search(r"(.*?)", response.text, re.IGNORECASE | re.DOTALL) - if match: - return match.group(1).strip() - else: - return None - - except requests.exceptions.RequestException: - return None - except Exception: - return None - -def check_release_notes_file_exists(toolchain, github_token): - """Check if the release notes file exists in the reference-manual repository. - - For -rc1 releases, this checks that the release notes have been created. - For subsequent RCs and stable releases, release notes should already exist. - - Returns tuple (exists: bool, is_rc1: bool) where is_rc1 indicates if this is - the first release candidate (when release notes need to be written). - """ - # Determine the release notes file path - # e.g., v4.28.0-rc1 -> Manual/Releases/v4_28_0.lean - base_version = strip_rc_suffix(toolchain.lstrip('v')) # "4.28.0" - file_name = f"v{base_version.replace('.', '_')}.lean" # "v4_28_0.lean" - file_path = f"Manual/Releases/{file_name}" - - is_rc1 = toolchain.endswith("-rc1") - - repo_url = "https://github.com/leanprover/reference-manual" - - # Check if the file exists on main branch - content = get_branch_content(repo_url, "main", file_path, github_token) - - return (content is not None, is_rc1) - -def get_branch_content(repo_url, branch, file_path, github_token): - api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - response = requests.get(api_url, headers=headers) - if response.status_code == 200: - content = response.json().get("content", "") - content = content.replace("\n", "") - try: - return base64.b64decode(content).decode('utf-8').strip() - except Exception: - return None - return None - -def parse_version(version_str): - # Remove 'v' prefix and extract version and release candidate suffix - if ':' in version_str: - version_str = version_str.split(':')[1] - version = version_str.lstrip('v') - parts = version.split('-') - base_version = tuple(map(int, parts[0].split('.'))) - rc_part = parts[1] if len(parts) > 1 and parts[1].startswith('rc') else None - rc_number = int(rc_part[2:]) if rc_part else float('inf') # Treat non-rc as higher than rc - return base_version + (rc_number,) - -def is_version_gte(version1, version2): - """Check if version1 >= version2, including proper handling of release candidates.""" - # Check if version1 is a nightly toolchain - if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"): - return False - return parse_version(version1) >= parse_version(version2) - -def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token, verbose=False): - # First get the commit SHA for the tag - api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/") - headers = {'Authorization': f'token {github_token}'} if github_token else {} - - # Get tag's commit SHA - tag_response = requests.get(f"{api_base}/git/refs/tags/{tag_name}", headers=headers) - if tag_response.status_code != 200: - debug(verbose, f"Could not fetch tag {tag_name}, status code: {tag_response.status_code}") - return False - - # Handle both single object and array responses - tag_data = tag_response.json() - if isinstance(tag_data, list): - # Find the exact matching tag in the list - matching_tags = [tag for tag in tag_data if tag['ref'] == f'refs/tags/{tag_name}'] - if not matching_tags: - debug(verbose, f"No matching tag found for {tag_name} in response list") - return False - tag_sha = matching_tags[0]['object']['sha'] - else: - tag_sha = tag_data['object']['sha'] - - # Check if the tag is an annotated tag and get the actual commit SHA - if tag_data.get('object', {}).get('type') == 'tag' or ( - isinstance(tag_data, list) and - matching_tags and - matching_tags[0].get('object', {}).get('type') == 'tag'): - - # Get the commit that this tag points to - tag_obj_response = requests.get(f"{api_base}/git/tags/{tag_sha}", headers=headers) - if tag_obj_response.status_code == 200: - tag_obj = tag_obj_response.json() - if 'object' in tag_obj and tag_obj['object']['type'] == 'commit': - commit_sha = tag_obj['object']['sha'] - debug(verbose, f"Tag is annotated. Resolved commit SHA: {commit_sha}") - tag_sha = commit_sha # Use the actual commit SHA - - # Get commits on stable branch containing this SHA - commits_response = requests.get( - f"{api_base}/commits?sha={stable_branch}&per_page=100", - headers=headers - ) - if commits_response.status_code != 200: - debug(verbose, f"Could not fetch commits for branch {stable_branch}, status code: {commits_response.status_code}") - return False - - # Check if any commit in stable's history matches our tag's SHA - stable_commits = [commit['sha'] for commit in commits_response.json()] - - is_merged = tag_sha in stable_commits - - debug(verbose, f"Tag SHA: {tag_sha}") - debug(verbose, f"First 5 stable commits: {stable_commits[:5]}") - debug(verbose, f"Total stable commits fetched: {len(stable_commits)}") - if not is_merged: - debug(verbose, f"Tag SHA not found in first {len(stable_commits)} commits of stable branch") - - return is_merged - -def is_release_candidate(version): - return "-rc" in version - -def check_cmake_version(repo_url, branch, version_major, version_minor, github_token): - """Verify the CMake version settings in src/CMakeLists.txt.""" - cmake_file_path = "src/CMakeLists.txt" - content = get_branch_content(repo_url, branch, cmake_file_path, github_token) - if content is None: - print(f" ❌ Could not retrieve {cmake_file_path} from {branch}") - return False - - expected_patterns = [ - (f"LEAN_VERSION_MAJOR", rf"^set\(LEAN_VERSION_MAJOR\s+{version_major}[\s)]", f"set(LEAN_VERSION_MAJOR {version_major} ...)"), - (f"LEAN_VERSION_MINOR", rf"^set\(LEAN_VERSION_MINOR\s+{version_minor}[\s)]", f"set(LEAN_VERSION_MINOR {version_minor} ...)"), - (f"LEAN_VERSION_PATCH", rf"^set\(LEAN_VERSION_PATCH\s+0[\s)]", f"set(LEAN_VERSION_PATCH 0 ...)"), - (f"LEAN_VERSION_IS_RELEASE", rf"^set\(LEAN_VERSION_IS_RELEASE\s+1[\s)]", f"set(LEAN_VERSION_IS_RELEASE 1 ...)"), - ] - - for name, pattern, display in expected_patterns: - if not any(re.match(pattern, l.strip()) for l in content.splitlines()): - print(f" ❌ Missing or incorrect line in {cmake_file_path}: {display}") - return False - - print(f" ✅ CMake version settings are correct in {cmake_file_path}") - return True - -def check_stage0_version(repo_url, branch, version_major, version_minor, github_token): - """Verify that stage0/src/CMakeLists.txt has the same version as src/CMakeLists.txt. - - The stage0 pre-built binaries stamp .olean headers with their baked-in version. - If stage0 has a different version (e.g. from a 'begin development cycle' bump), - the release tarball will contain .olean files with the wrong version. - """ - stage0_cmake = "stage0/src/CMakeLists.txt" - content = get_branch_content(repo_url, branch, stage0_cmake, github_token) - if content is None: - print(f" ❌ Could not retrieve {stage0_cmake} from {branch}") - return False - - errors = [] - for line in content.splitlines(): - stripped = line.strip() - if stripped.startswith("set(LEAN_VERSION_MAJOR "): - actual = stripped.split()[1].rstrip(")") - if actual != str(version_major): - errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}") - elif stripped.startswith("set(LEAN_VERSION_MINOR "): - actual = stripped.split()[1].rstrip(")") - if actual != str(version_minor): - errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}") - - if errors: - print(f" ❌ stage0 version mismatch in {stage0_cmake}:") - for error in errors: - print(f" {error}") - print(f" The stage0 compiler stamps .olean headers with its baked-in version.") - print(f" Run `make update-stage0` to rebuild stage0 with the correct version.") - return False - - print(f" ✅ stage0 version matches in {stage0_cmake}") - return True - -def extract_org_repo_from_url(repo_url): - """Extract the 'org/repo' part from a GitHub URL.""" - if repo_url.startswith("https://github.com/"): - return repo_url.replace("https://github.com/", "").rstrip("/") - return repo_url - -def get_next_version(version): - """Calculate the next version number, ignoring RC suffix.""" - # Strip v prefix and RC suffix if present - base_version = strip_rc_suffix(version.lstrip('v')) - major, minor, patch = map(int, base_version.split('.')) - # Next version is always .0 - return f"v{major}.{minor + 1}.0" - -def get_latest_nightly_tag(github_token): - """Get the most recent nightly tag from leanprover/lean4-nightly.""" - api_url = "https://api.github.com/repos/leanprover/lean4-nightly/tags" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - response = requests.get(api_url, headers=headers) - if response.status_code != 200: - return None - tags = response.json() - if not tags: - return None - # Return the most recent tag name - return tags[0]['name'] - -def update_lean_toolchain_in_branch(org_repo, branch, toolchain_content, github_token): - """Update the lean-toolchain file in a specific branch.""" - api_url = f"https://api.github.com/repos/{org_repo}/contents/lean-toolchain" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - - # First get the current file to get its SHA - response = requests.get(f"{api_url}?ref={branch}", headers=headers) - if response.status_code != 200: - return False - - current_file = response.json() - file_sha = current_file['sha'] - - # Update the file - update_data = { - "message": f"chore: update lean-toolchain to {toolchain_content}", - "content": base64.b64encode(toolchain_content.encode('utf-8')).decode('utf-8'), - "sha": file_sha, - "branch": branch - } - - response = requests.put(api_url, json=update_data, headers=headers) - return response.status_code in [200, 201] - -def check_bump_branch_toolchain(url, bump_branch, github_token): - """Check if the lean-toolchain file in bump branch starts with either 'leanprover/lean4:nightly-' or the next version.""" - content = get_branch_content(url, bump_branch, "lean-toolchain", github_token) - if content is None: - print(f" ❌ No lean-toolchain file found in {bump_branch} branch") - return False - - # Extract the next version from the bump branch name (bump/v4.X.0) - next_version = bump_branch.split('/')[1] - - if not (content.startswith("leanprover/lean4:nightly-") or - content.startswith(f"leanprover/lean4:{next_version}")): - print(f" ❌ Bump branch toolchain should use either nightly or {next_version}, but found: {content}") - return False - - print(f" ✅ Bump branch correctly uses toolchain: {content}") - return True - -def get_pr_ci_status(repo_url, pr_number, github_token): - """Get the CI status for a pull request.""" - api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/") - headers = {'Authorization': f'token {github_token}'} if github_token else {} - - # Get PR details to find the head SHA - pr_response = requests.get(f"{api_base}/pulls/{pr_number}", headers=headers) - if pr_response.status_code != 200: - return "unknown", "Could not fetch PR details" - - pr_data = pr_response.json() - head_sha = pr_data['head']['sha'] - - # Get check runs for the commit - check_runs_response = requests.get( - f"{api_base}/commits/{head_sha}/check-runs", - headers=headers - ) - - if check_runs_response.status_code != 200: - return "unknown", "Could not fetch check runs" - - check_runs_data = check_runs_response.json() - check_runs = check_runs_data.get('check_runs', []) - - if not check_runs: - # No check runs, check for status checks (legacy) - status_response = requests.get( - f"{api_base}/commits/{head_sha}/status", - headers=headers - ) - if status_response.status_code == 200: - status_data = status_response.json() - state = status_data.get('state', 'unknown') - if state == 'success': - return "success", "All status checks passed" - elif state == 'failure': - return "failure", "Some status checks failed" - elif state == 'pending': - return "pending", "Status checks in progress" - return "unknown", "No CI checks found" - - # Analyze check runs - conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed'] - in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']] - - failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required']) - if in_progress: - if failed > 0: - return "failure", f"{failed} check(s) failing, {len(in_progress)} still in progress" - return "pending", f"{len(in_progress)} check(s) in progress" - - if not conclusions: - return "pending", "Checks queued" - - if all(c == 'success' for c in conclusions): - return "success", f"All {len(conclusions)} checks passed" - - if failed > 0: - return "failure", f"{failed} check(s) failed" - - # Some checks are cancelled, skipped, or neutral - return "warning", f"Some checks did not complete normally" - -def pr_exists_with_title(repo_url, title, github_token): - api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + "/pulls" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - params = {'state': 'open'} - response = requests.get(api_url, headers=headers, params=params) - if response.status_code != 200: - return None - pull_requests = response.json() - for pr in pull_requests: - if pr['title'] == title: - return pr['number'], pr['html_url'] - return None - -def check_proofwidgets4_release(repo_url, target_toolchain, github_token): - """Check if ProofWidgets4 has a release tag that uses the target toolchain.""" - api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/") - headers = {'Authorization': f'token {github_token}'} if github_token else {} - - # Get all tags matching v0.0.* pattern - response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers) - if response.status_code != 200: - print(f" ❌ Could not fetch ProofWidgets4 tags") - return False - - tags = response.json() - if not tags: - print(f" ❌ No v0.0.* tags found for ProofWidgets4") - return False - - # Extract tag names and sort by version number (descending) - tag_names = [] - for tag in tags: - ref = tag['ref'] - if ref.startswith('refs/tags/v0.0.'): - tag_name = ref.replace('refs/tags/', '') - try: - # Extract the number after v0.0. - version_num = int(tag_name.split('.')[-1]) - tag_names.append((version_num, tag_name)) - except (ValueError, IndexError): - continue - - if not tag_names: - print(f" ❌ No valid v0.0.* tags found for ProofWidgets4") - return False - - # Sort by version number (descending) and take the most recent 10 - tag_names.sort(reverse=True) - recent_tags = tag_names[:10] - - # Check each recent tag to see if it uses the target toolchain - for version_num, tag_name in recent_tags: - toolchain_content = get_branch_content(repo_url, tag_name, "lean-toolchain", github_token) - if toolchain_content is None: - continue - - if is_version_gte(toolchain_content.strip(), target_toolchain): - print(f" ✅ Found release {tag_name} using compatible toolchain (>= {target_toolchain})") - return True - - # If we get here, no recent release uses the target toolchain - # Find the highest version number to suggest the next one - highest_version = max(version_num for version_num, _ in recent_tags) - next_version = highest_version + 1 - print(f" ❌ No recent ProofWidgets4 release uses toolchain >= {target_toolchain}") - print(f" You will need to create and push a tag v0.0.{next_version}") - return False - -def check_reference_manual_release_title(repo_url, toolchain, pr_branch, github_token): - """Check if the reference-manual release notes title matches the release type. - - For RC releases (e.g., v4.27.0-rc1), the title should contain the exact RC suffix. - For final releases (e.g., v4.27.0), the title should NOT contain any "-rc". - - Returns True if check passes or is not applicable, False if title needs updating. - """ - is_rc = is_release_candidate(toolchain) - - # For RC releases, get the base version and RC suffix - # e.g., "v4.27.0-rc1" -> version="4.27.0", rc_suffix="-rc1" - if is_rc: - parts = toolchain.lstrip('v').split('-', 1) - version = parts[0] - rc_suffix = '-' + parts[1] if len(parts) > 1 else '' - else: - version = toolchain.lstrip('v') - rc_suffix = '' - - # Construct the release notes file path (e.g., Manual/Releases/v4_27_0.lean for v4.27.0) - file_name = f"v{version.replace('.', '_')}.lean" # "v4_27_0.lean" - file_path = f"Manual/Releases/{file_name}" - - # Try to get the file from the PR branch first, then fall back to main branch - content = get_branch_content(repo_url, pr_branch, file_path, github_token) - if content is None: - # Try the default branch - content = get_branch_content(repo_url, "main", file_path, github_token) - - if content is None: - print(f" ⚠️ Could not check release notes file: {file_path}") - return True # Don't block on this - - # Look for the #doc line with the title - for line in content.splitlines(): - if line.strip().startswith('#doc') and 'Manual' in line: - has_rc_in_title = '-rc' in line.lower() - - if is_rc: - # For RC releases, title should contain the exact RC suffix (e.g., "-rc1") - # Use regex to match exact suffix followed by non-digit (to avoid -rc1 matching -rc10) - # Pattern matches the RC suffix followed by a non-digit or end-of-string context - # e.g., "-rc1" followed by space, quote, paren, or similar - exact_match = re.search(rf'{re.escape(rc_suffix)}(?![0-9])', line, re.IGNORECASE) - if exact_match: - print(f" ✅ Release notes title correctly shows {rc_suffix}") - return True - elif has_rc_in_title: - print(f" ❌ Release notes title shows wrong RC version (expected {rc_suffix})") - print(f" Update {file_path} to use '{rc_suffix}' in the title") - return False - else: - print(f" ❌ Release notes title missing RC suffix") - print(f" Update {file_path} to include '{rc_suffix}' in the title") - return False - else: - # For final releases, title should NOT contain -rc - if has_rc_in_title: - print(f" ❌ Release notes title still shows RC version") - print(f" Update {file_path} to remove '-rcN' from the title") - return False - else: - print(f" ✅ Release notes title is updated for final release") - return True - - # If we didn't find the #doc line, don't block - print(f" ⚠️ Could not find release notes title in {file_path}") - return True - -def run_mathlib_verify_version_tags(toolchain, verbose=False): - """Run mathlib4's verify_version_tags.py script to validate the release tag. - - This clones mathlib4 to a temp directory and runs the verification script. - Returns True if verification passes, False otherwise. - """ - import tempfile - - print(f" ... Running mathlib4 verify_version_tags.py {toolchain}") - - with tempfile.TemporaryDirectory() as tmpdir: - # Clone mathlib4 (shallow clone is sufficient for running the script) - clone_result = subprocess.run( - ['git', 'clone', '--depth', '1', 'https://github.com/leanprover-community/mathlib4.git', tmpdir], - capture_output=True, - text=True - ) - if clone_result.returncode != 0: - print(f" ❌ Failed to clone mathlib4: {clone_result.stderr.strip()[:200]}") - return False - - # Run the verification script - script_path = os.path.join(tmpdir, 'scripts', 'verify_version_tags.py') - if not os.path.exists(script_path): - print(f" ❌ verify_version_tags.py not found in mathlib4 (expected at scripts/verify_version_tags.py)") - return False - - # Run from the mathlib4 directory so git operations work - result = subprocess.run( - ['python3', script_path, toolchain], - cwd=tmpdir, - capture_output=True, - text=True, - timeout=900 # 15 minutes timeout for cache download etc. - ) - - # Print output with indentation - if result.stdout: - for line in result.stdout.strip().split('\n'): - print(f" {line}") - if result.stderr: - for line in result.stderr.strip().split('\n'): - print(f" {line}") - - if result.returncode != 0: - print(f" ❌ mathlib4 verify_version_tags.py failed") - return False - - print(f" ✅ mathlib4 verify_version_tags.py passed") - return True - -def main(): - parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories") - parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)") - parser.add_argument("--verbose", "-v", action="store_true", help="Enable verbose debugging output") - parser.add_argument("--dry-run", action="store_true", help="Dry run mode (no actions taken)") - args = parser.parse_args() - - github_token = get_github_token() - toolchain = args.toolchain - verbose = args.verbose - # dry_run = args.dry_run # Not used yet but available for future implementation - - stripped_toolchain = strip_rc_suffix(toolchain) - lean_repo_url = "https://github.com/leanprover/lean4" - - # Track repository status - repo_status = {} # Will store True for success, False for failure - - # Preliminary checks for lean4 itself - print("\nPerforming preliminary checks...") - lean4_success = True - - # Check for branch releases/v4.Y.0 - version_major, version_minor, _ = map(int, stripped_toolchain.lstrip('v').split('.')) - branch_name = f"releases/v{version_major}.{version_minor}.0" - if not branch_exists(lean_repo_url, branch_name, github_token): - print(f" ❌ Branch {branch_name} does not exist") - print(f" 🟡 After creating the branch, we'll need to check CMake version settings.") - lean4_success = False - else: - print(f" ✅ Branch {branch_name} exists") - # Check CMake version settings - if not check_cmake_version(lean_repo_url, branch_name, version_major, version_minor, github_token): - lean4_success = False - # Check that stage0 version matches (stage0 stamps .olean headers with its version) - if not check_stage0_version(lean_repo_url, branch_name, version_major, version_minor, github_token): - lean4_success = False - - # Check for tag and release page - if not tag_exists(lean_repo_url, toolchain, github_token): - print(f" ❌ Tag {toolchain} does not exist.") - lean4_success = False - else: - print(f" ✅ Tag {toolchain} exists") - commit_hash = commit_hash_for_tag(lean_repo_url, toolchain, github_token) - SHORT_HASH_LENGTH = 7 # Lake abbreviates the Lean commit to 7 characters. - if commit_hash is None: - print(f" ❌ Could not resolve tag {toolchain} to a commit.") - lean4_success = False - elif commit_hash[0] == '0' and commit_hash[:SHORT_HASH_LENGTH].isnumeric(): - print(f" ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.") - lean4_success = False - - release_page_ready = release_page_exists(lean_repo_url, toolchain, github_token) - if not release_page_ready: - print(f" ❌ Release page for {toolchain} does not exist (This will be created by CI.)") - - # Check CI workflow status - workflow_status = get_tag_workflow_status(lean_repo_url, toolchain, github_token) - if workflow_status: - status = workflow_status['status'] - conclusion = workflow_status['conclusion'] - workflow_name = workflow_status['workflow_name'] - run_id = workflow_status['run_id'] - workflow_url = f"{lean_repo_url}/actions/runs/{run_id}" - - if status == 'in_progress' or status == 'queued': - print(f" 🔄 {workflow_name} workflow is {status}: {workflow_url}") - elif status == 'completed': - if conclusion == 'success': - print(f" ✅ {workflow_name} workflow completed successfully: {workflow_url}") - elif conclusion == 'failure': - print(f" ❌ {workflow_name} workflow failed: {workflow_url}") - else: - print(f" ⚠️ {workflow_name} workflow completed with status: {conclusion}: {workflow_url}") - else: - print(f" ℹ️ {workflow_name} workflow status: {status}: {workflow_url}") - - lean4_success = False - else: - print(f" ✅ Release page for {toolchain} exists") - - # Check the actual release notes page title (informational only - does not block) - actual_title = get_release_notes(toolchain) - expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1" - base_tag = toolchain.split('-')[0] - release_notes_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/" - - if actual_title is None: - print(f" ⚠️ Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)") - elif not actual_title.startswith(expected_title_prefix): - print(f" ⚠️ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}") - else: - print(f" ✅ Release notes page title looks good ('{actual_title}').") - - # Check if release notes file exists in reference-manual repository - # For -rc1 releases, this is when release notes need to be written - # For subsequent RCs and stable releases, they should already exist - release_notes_exists, is_rc1 = check_release_notes_file_exists(toolchain, github_token) - base_version = strip_rc_suffix(toolchain.lstrip('v')) - release_notes_file = f"Manual/Releases/v{base_version.replace('.', '_')}.lean" - - if not release_notes_exists: - if is_rc1: - print(f" ❌ Release notes file not found: {release_notes_file}") - print(f" This is an -rc1 release, so release notes need to be written.") - print(f" Run `script/release_notes.py --since ` to generate them.") - print(f" See doc/dev/release_checklist.md section 'Writing the release notes' for details.") - lean4_success = False - else: - print(f" ❌ Release notes file not found: {release_notes_file}") - print(f" Release notes should have been created for -rc1. Check the reference-manual repository.") - lean4_success = False - else: - print(f" ✅ Release notes file exists: {release_notes_file}") - - repo_status["lean4"] = lean4_success - - # If the release page doesn't exist, skip repository checks and master branch checks - # The preliminary infrastructure must be in place first - if not release_page_exists(lean_repo_url, toolchain, github_token): - print("\n⚠️ Release process blocked: preliminary Lean4 infrastructure incomplete.") - print(" Complete the steps above, then rerun this script to proceed with downstream repositories.") - return - - # Load repositories and perform further checks - print("\nChecking repositories...") - - with open(os.path.join(os.path.dirname(__file__), "release_repos.yml")) as f: - repos = yaml.safe_load(f)["repositories"] - - for repo in repos: - name = repo["name"] - url = repo["url"] - org_repo = extract_org_repo_from_url(url) - branch = repo["branch"] - check_stable = repo["stable-branch"] - check_tag = repo.get("toolchain-tag", True) - check_bump = repo.get("bump-branch", False) - dependencies = repo.get("dependencies", []) - - print(f"\nRepository: {name}") - - # Check if any dependencies have failed - failed_deps = [dep for dep in dependencies if dep in repo_status and not repo_status[dep]] - if failed_deps: - print(f" 🟡 Dependencies not ready: {', '.join(failed_deps)}") - repo_status[name] = False - continue - - # Initialize success flag for this repo - success = True - - # Check if branch is on at least the target toolchain - lean_toolchain_content = get_branch_content(url, branch, "lean-toolchain", github_token) - if lean_toolchain_content is None: - print(f" ❌ No lean-toolchain file found in {branch} branch") - repo_status[name] = False - continue - - on_target_toolchain = is_version_gte(lean_toolchain_content.strip(), toolchain) - if not on_target_toolchain: - print(f" ❌ Not on target toolchain (needs ≥ {toolchain}, but {branch} is on {lean_toolchain_content.strip()})") - pr_title = f"chore: bump toolchain to {toolchain}" - pr_info = pr_exists_with_title(url, pr_title, github_token) - if pr_info: - pr_number, pr_url = pr_info - print(f" ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})") - - # Check CI status - ci_status, ci_message = get_pr_ci_status(url, pr_number, github_token) - if ci_status == "success": - print(f" ✅ CI: {ci_message}") - elif ci_status == "failure": - print(f" ❌ CI: {ci_message}") - elif ci_status == "pending": - print(f" 🔄 CI: {ci_message}") - elif ci_status == "warning": - print(f" ⚠️ CI: {ci_message}") - else: - print(f" ❓ CI: {ci_message}") - - # For reference-manual, check that the release notes title has been updated - if name == "reference-manual": - pr_branch = f"bump_to_{toolchain}" - check_reference_manual_release_title(url, toolchain, pr_branch, github_token) - else: - print(f" ❌ PR with title '{pr_title}' does not exist") - print(f" Run `script/release_steps.py {toolchain} {name}` to create it") - repo_status[name] = False - continue - print(f" ✅ On compatible toolchain (>= {toolchain})") - - # For reference-manual, check that the release notes title is correct BEFORE tagging. - # This catches the case where the toolchain bump PR was merged without updating - # the release notes title (e.g., still showing "-rc1" for a stable release). - if name == "reference-manual": - if not check_reference_manual_release_title(url, toolchain, branch, github_token): - repo_status[name] = False - continue - - # Special handling for ProofWidgets4 - if name == "ProofWidgets4": - if not check_proofwidgets4_release(url, toolchain, github_token): - repo_status[name] = False - continue - - if check_tag: - tag_exists_initially = tag_exists(url, toolchain, github_token) - if not tag_exists_initially: - if args.dry_run: - print(f" ❌ Tag {toolchain} does not exist. Run `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`.") - repo_status[name] = False - continue - else: - print(f" ⮕ Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...") - - # Run the script to create the tag - subprocess.run(["script/push_repo_release_tag.py", org_repo, branch, toolchain]) - - # Check again if the tag exists now - if not tag_exists(url, toolchain, github_token): - print(f" ❌ Manual intervention required.") - repo_status[name] = False - continue - - # This will print in all successful cases - whether tag existed initially or was created successfully - print(f" ✅ Tag {toolchain} exists") - - if check_stable and not is_release_candidate(toolchain): - if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose): - org_repo = extract_org_repo_from_url(url) - if args.dry_run: - print(f" ❌ Tag {toolchain} is not merged into stable") - print(f" Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it") - repo_status[name] = False - continue - else: - print(f" ⮕ Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...") - - # Run the script to merge the tag - subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain]) - - # Check again if the tag is merged now - if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose): - print(f" ❌ Manual intervention required.") - repo_status[name] = False - continue - - # This will print in all successful cases - whether tag was merged initially or was merged successfully - print(f" ✅ Tag {toolchain} is merged into stable") - - if check_bump: - next_version = get_next_version(toolchain) - bump_branch = f"bump/{next_version}" - - # For mathlib4, use the nightly-testing fork for bump branches - bump_org_repo = org_repo - bump_url = url - if name == "mathlib4": - bump_org_repo = "leanprover-community/mathlib4-nightly-testing" - bump_url = "https://github.com/leanprover-community/mathlib4-nightly-testing" - - branch_created = False - if not branch_exists(bump_url, bump_branch, github_token): - if args.dry_run: - latest_nightly = get_latest_nightly_tag(github_token) - nightly_note = f" (will set lean-toolchain to {latest_nightly})" if name in ["batteries", "mathlib4"] and latest_nightly else "" - print(f" ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it{nightly_note}.") - repo_status[name] = False - continue - print(f" ⮕ Bump branch {bump_branch} does not exist. Creating it...") - result = run_command(f"gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False) - if result.returncode != 0: - print(f" ❌ Failed to create bump branch {bump_branch}") - repo_status[name] = False - continue - branch_created = True - - print(f" ✅ Bump branch {bump_branch} exists") - - # Update the lean-toolchain to the latest nightly for newly created bump branches - if branch_created: - latest_nightly = get_latest_nightly_tag(github_token) - if latest_nightly: - nightly_toolchain = f"leanprover/lean4:{latest_nightly}" - print(f" ⮕ Updating lean-toolchain to {nightly_toolchain}...") - if update_lean_toolchain_in_branch(bump_org_repo, bump_branch, nightly_toolchain, github_token): - print(f" ✅ Updated lean-toolchain to {nightly_toolchain}") - else: - print(f" ❌ Failed to update lean-toolchain to {nightly_toolchain}") - repo_status[name] = False - continue - else: - print(f" ❌ Could not fetch latest nightly tag") - repo_status[name] = False - continue - if not check_bump_branch_toolchain(bump_url, bump_branch, github_token): - repo_status[name] = False - continue - - # For mathlib4, run verify_version_tags.py to validate the release tag - if name == "mathlib4": - if not run_mathlib_verify_version_tags(toolchain, verbose): - repo_status[name] = False - continue - - repo_status[name] = success - - # Final check for lean4 master branch - print("\nChecking lean4 master branch configuration...") - next_version = get_next_version(toolchain) - next_minor = int(next_version.split('.')[1]) - - cmake_content = get_branch_content(lean_repo_url, "master", "src/CMakeLists.txt", github_token) - if cmake_content is None: - print(" ❌ Could not retrieve CMakeLists.txt from master") - else: - cmake_lines = cmake_content.splitlines() - # Find the actual minor version in CMakeLists.txt - for line in cmake_lines: - if line.strip().startswith("set(LEAN_VERSION_MINOR "): - m = re.search(r'set\(LEAN_VERSION_MINOR\s+(\d+)', line) - actual_minor = int(m.group(1)) if m else 0 - version_minor_correct = actual_minor >= next_minor - break - else: - version_minor_correct = False - - is_release_correct = any( - re.match(r'set\(LEAN_VERSION_IS_RELEASE\s+0[\s)]', l.strip()) - for l in cmake_lines - ) - - if not (version_minor_correct and is_release_correct): - print(" ❌ lean4 needs a \"begin dev cycle\" PR") - else: - print(" ✅ lean4 master branch is configured for next development cycle") - -if __name__ == "__main__": - main() diff --git a/script/release_notes.py b/script/release_notes.py deleted file mode 100755 index 84d93d1cdd..0000000000 --- a/script/release_notes.py +++ /dev/null @@ -1,182 +0,0 @@ -#!/usr/bin/env python3 - -import sys -import re -import json -import requests -import subprocess -import argparse -from collections import defaultdict -from git import Repo - -def get_commits_since_tag(repo, tag): - try: - tag_commit = repo.commit(tag) - commits = list(repo.iter_commits(f"{tag_commit.hexsha}..HEAD")) - return [ - (commit.hexsha, commit.message.splitlines()[0], commit.message) - for commit in commits - ] - except Exception as e: - sys.stderr.write(f"Error retrieving commits: {e}\n") - sys.exit(1) - -def check_pr_number(first_line): - match = re.search(r"\(\#(\d+)\)$", first_line) - if match: - return int(match.group(1)) - return None - -def fetch_pr_labels(pr_number): - try: - # Use gh CLI to fetch PR details - result = subprocess.run([ - "gh", "api", f"repos/leanprover/lean4/pulls/{pr_number}" - ], capture_output=True, text=True, check=True) - pr_data = result.stdout - pr_json = json.loads(pr_data) - return [label["name"] for label in pr_json.get("labels", [])] - except subprocess.CalledProcessError as e: - sys.stderr.write(f"Failed to fetch PR #{pr_number} using gh: {e.stderr}\n") - return [] - -def format_section_title(label): - title = label.replace("changelog-", "").capitalize() - if title == "Doc": - return "Documentation" - elif title == "Pp": - return "Pretty Printing" - return title - -def sort_sections_order(): - return [ - "Language", - "Library", - "Tactics", - "Compiler", - "Pretty Printing", - "Documentation", - "Server", - "Lake", - "Other", - "Uncategorised" - ] - -def format_markdown_description(pr_number, description): - link = f"[#{pr_number}](https://github.com/leanprover/lean4/pull/{pr_number})" - return f"{link} {description}" - -def commit_types(): - # see doc/dev/commit_convention.md - return ['feat', 'fix', 'doc', 'style', 'refactor', 'test', 'chore', 'perf'] - -def count_commit_types(commits): - counts = { - 'total': len(commits), - } - for commit_type in commit_types(): - counts[commit_type] = 0 - - for _, first_line, _ in commits: - for commit_type in commit_types(): - if first_line.startswith(f'{commit_type}:'): - counts[commit_type] += 1 - break - - return counts - -def main(): - parser = argparse.ArgumentParser(description='Generate release notes from Git commits') - parser.add_argument('--since', required=True, help='Git tag to generate release notes since') - args = parser.parse_args() - - try: - repo = Repo(".") - except Exception as e: - sys.stderr.write(f"Error opening Git repository: {e}\n") - sys.exit(1) - - commits = get_commits_since_tag(repo, args.since) - - sys.stderr.write(f"Found {len(commits)} commits since tag {args.since}:\n") - for commit_hash, first_line, _ in commits: - sys.stderr.write(f"- {commit_hash}: {first_line}\n") - - changelog = defaultdict(list) - - for commit_hash, first_line, full_message in commits: - # Skip commits with the specific first lines - if first_line == "chore: update stage0" or first_line.startswith("chore: CI: bump "): - continue - - pr_number = check_pr_number(first_line) - - if not pr_number: - sys.stderr.write(f"No PR number found in commit:\n{commit_hash}\n{first_line}\n") - continue - - # Remove the first line from the full_message for further processing - body = full_message[len(first_line):].strip() - - paragraphs = body.split('\n\n') - description = paragraphs[0] if len(paragraphs) > 0 else "" - - # If there's a third paragraph and second ends with colon, include it - if len(paragraphs) > 1 and description.endswith(':'): - description = description + '\n\n' + paragraphs[1] - - labels = fetch_pr_labels(pr_number) - - # Skip entries with the "changelog-no" label - if "changelog-no" in labels: - continue - - report_errors = first_line.startswith("feat:") or first_line.startswith("fix:") - - if not description.startswith("This PR "): - if report_errors: - sys.stderr.write(f"No PR description found in commit:\n{commit_hash}\n{first_line}\n{body}\n\n") - fallback_description = re.sub(r":$", "", first_line.split(" ", 1)[1]).rsplit(" (#", 1)[0] - markdown_description = format_markdown_description(pr_number, fallback_description) - else: - continue - else: - markdown_description = format_markdown_description(pr_number, description.replace("This PR ", "")) - - changelog_labels = [label for label in labels if label.startswith("changelog-")] - if len(changelog_labels) > 1: - sys.stderr.write(f"Warning: Multiple changelog-* labels found for PR #{pr_number}: {changelog_labels}\n") - - if not changelog_labels: - if report_errors: - sys.stderr.write(f"Warning: No changelog-* label found for PR #{pr_number}\n") - else: - continue - - for label in changelog_labels: - changelog[label].append((pr_number, markdown_description)) - - # Add commit type counting - counts = count_commit_types(commits) - print(f"For this release, {counts['total']} changes landed. " - f"In addition to the {counts['feat']} feature additions and {counts['fix']} fixes listed below " - f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements, " - f"{counts['perf']} performance improvements, {counts['test']} improvements to the test suite " - f"and {counts['style'] + counts['chore']} other changes.\n") - - section_order = sort_sections_order() - sorted_changelog = sorted(changelog.items(), key=lambda item: section_order.index(format_section_title(item[0])) if format_section_title(item[0]) in section_order else len(section_order)) - - for label, entries in sorted_changelog: - section_title = format_section_title(label) if label != "Uncategorised" else "Uncategorised" - print(f"## {section_title}\n") - for _, entry in sorted(entries, key=lambda x: x[0]): - # Split entry into lines and indent all lines after the first - lines = entry.splitlines() - print(f"* {lines[0]}") - for line in lines[1:]: - print(f" {line}") - print() # Empty line after each entry - -if __name__ == "__main__": - main() diff --git a/script/release_repos.yml b/script/release_repos.yml deleted file mode 100644 index 44a21b3e76..0000000000 --- a/script/release_repos.yml +++ /dev/null @@ -1,156 +0,0 @@ -repositories: - - name: lean4-cli - url: https://github.com/leanprover/lean4-cli - toolchain-tag: true - stable-branch: false - branch: main - dependencies: [] - - - name: batteries - url: https://github.com/leanprover-community/batteries - toolchain-tag: true - stable-branch: true - branch: main - bump-branch: true - dependencies: [] - - - name: quote4 - url: https://github.com/leanprover-community/quote4 - toolchain-tag: true - stable-branch: true - branch: master - dependencies: [] - - - name: plausible - url: https://github.com/leanprover-community/plausible - toolchain-tag: true - stable-branch: false - branch: main - dependencies: [] - - - name: leansqlite - url: https://github.com/leanprover/leansqlite - toolchain-tag: true - stable-branch: false - branch: main - dependencies: - - plausible - - - name: verso - url: https://github.com/leanprover/verso - toolchain-tag: true - stable-branch: false - branch: main - dependencies: - - plausible - - - name: import-graph - url: https://github.com/leanprover-community/import-graph - toolchain-tag: true - stable-branch: false - branch: main - dependencies: - - lean4-cli - - - name: lean4-unicode-basic - url: https://github.com/fgdorais/lean4-unicode-basic - toolchain-tag: true - stable-branch: false - branch: main - dependencies: [] - - - name: BibtexQuery - url: https://github.com/dupuisf/BibtexQuery - toolchain-tag: true - stable-branch: false - branch: master - dependencies: [lean4-unicode-basic] - - - name: reference-manual - url: https://github.com/leanprover/reference-manual - toolchain-tag: true - stable-branch: false - branch: main - dependencies: [verso] - - - name: ProofWidgets4 - url: https://github.com/leanprover-community/ProofWidgets4 - toolchain-tag: false - stable-branch: false - branch: main - dependencies: [] - - - name: aesop - url: https://github.com/leanprover-community/aesop - toolchain-tag: true - stable-branch: true - branch: master - dependencies: - - batteries - - - name: mathlib4 - url: https://github.com/leanprover-community/mathlib4 - toolchain-tag: true - stable-branch: true - branch: master - bump-branch: true - dependencies: - - aesop - - ProofWidgets4 - - lean4checker - - batteries - - lean4-cli - - import-graph - - plausible - - - name: doc-gen4 - url: https://github.com/leanprover/doc-gen4 - toolchain-tag: true - stable-branch: false - branch: main - dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite] - - - name: cslib - url: https://github.com/leanprover/cslib - toolchain-tag: true - stable-branch: true - branch: main - bump-branch: true - dependencies: - - mathlib4 - - - name: repl - url: https://github.com/leanprover-community/repl - toolchain-tag: true - stable-branch: true - branch: master - dependencies: - - mathlib4 - - - name: verso-web-components - url: https://github.com/leanprover/verso-web-components - toolchain-tag: true - stable-branch: false - branch: main - dependencies: - - verso - - - name: lean-fro.org - url: https://github.com/leanprover/lean-fro.org - toolchain-tag: false - stable-branch: false - branch: master - dependencies: - - verso-web-components - - - name: comparator - url: https://github.com/leanprover/comparator - toolchain-tag: true - stable-branch: false - branch: master - - - name: lean4export - url: https://github.com/leanprover/lean4export - toolchain-tag: true - stable-branch: false - branch: master diff --git a/script/release_steps.py b/script/release_steps.py deleted file mode 100755 index 4e12b1fde3..0000000000 --- a/script/release_steps.py +++ /dev/null @@ -1,840 +0,0 @@ -#!/usr/bin/env python3 - -""" -Execute Release Steps for Lean4 Downstream Repositories - -This script automates the process of updating a downstream repository to a new Lean4 release. -It handles creating branches, updating toolchains, merging changes, building, testing, and -creating pull requests. - -IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior! - -What this script does: -1. Sets up the downstream_releases/ directory for cloning repositories - -2. Clones or updates the target repository - -3. Creates a branch named bump_to_{version} for the changes - -4. Updates the lean-toolchain file to the target version - -5. Handles repository-specific variations: - - Different dependency update mechanisms - - Special merging strategies for repositories with nightly-testing branches - - Safety checks for repositories using bump branches - - Custom build and test procedures - - lean-fro.org: runs scripts/update.sh to regenerate site content - - mathlib4: updates ProofWidgets4 pin (v0.0.X sequential tags, not v4.X.Y) - -6. Commits the changes with message "chore: bump toolchain to {version}" - -7. Builds the project (with a clean .lake cache) - -8. Runs tests if available - -9. Pushes the branch to GitHub - -10. Creates a pull request (or reports if one already exists) - -Usage: - ./release_steps.py v4.24.0 batteries # Update batteries to v4.24.0 - ./release_steps.py v4.24.0-rc1 mathlib4 # Update mathlib4 to v4.24.0-rc1 - -The script reads repository configurations from release_repos.yml. -Each repository has specific handling for merging, dependencies, and testing. - -This script is idempotent - it's safe to rerun if it fails partway through. -Existing branches, commits, and PRs will be reused rather than duplicated. - -Error handling: -- If build or tests fail, the script continues to create the PR anyway -- Manual conflicts must be resolved by the user -- Network issues during push/PR creation are reported with manual instructions -""" - -import argparse -import yaml -import os -import sys -import re -import subprocess -import shutil -import json -import requests -import base64 -from pathlib import Path - -# Color functions for terminal output -def blue(text): - """Blue text for 'I'm doing something' messages.""" - return f"\033[94m{text}\033[0m" - -def green(text): - """Green text for 'successful step' messages.""" - return f"\033[92m{text}\033[0m" - -def red(text): - """Red text for 'this looks bad' messages.""" - return f"\033[91m{text}\033[0m" - -def yellow(text): - """Yellow text for warnings.""" - return f"\033[93m{text}\033[0m" - -def run_command(cmd, cwd=None, check=True, stream_output=False): - """Run a shell command and return the result.""" - print(blue(f"Running: {cmd}")) - try: - if stream_output: - # Stream output in real-time for long-running commands - result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, text=True) - return result - else: - # Capture output for commands where we need to process the result - result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, - capture_output=True, text=True) - if result.stdout: - # Command output in plain white (default terminal color) - print(result.stdout) - return result - except subprocess.CalledProcessError as e: - print(red(f"Error running command: {cmd}")) - print(red(f"Exit code: {e.returncode}")) - if not stream_output: - print(f"Stdout: {e.stdout}") - print(f"Stderr: {e.stderr}") - raise - -def load_repos_config(file_path): - with open(file_path, "r") as f: - return yaml.safe_load(f)["repositories"] - -def find_repo(repo_name, config): - matching_repos = [r for r in config if r["name"] == repo_name] - if not matching_repos: - print(red(f"Error: No repository named '{repo_name}' found in configuration.")) - available_repos = [r["name"] for r in config] - print(yellow(f"Available repositories: {', '.join(available_repos)}")) - sys.exit(1) - return matching_repos[0] - -def get_github_token(): - try: - result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True) - if result.returncode == 0: - return result.stdout.strip() - except FileNotFoundError: - pass - return None - -def find_proofwidgets_tag(version): - """Find the latest ProofWidgets4 tag that uses the given toolchain version. - - ProofWidgets4 uses sequential version tags (v0.0.X) rather than toolchain-based tags. - This function finds the most recent tag whose lean-toolchain matches the target version - exactly, checking the 20 most recent tags. - """ - github_token = get_github_token() - api_base = "https://api.github.com/repos/leanprover-community/ProofWidgets4" - headers = {'Authorization': f'token {github_token}'} if github_token else {} - - response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers, timeout=30) - if response.status_code != 200: - return None - - tags = response.json() - tag_names = [] - for tag in tags: - ref = tag['ref'] - if ref.startswith('refs/tags/v0.0.'): - tag_name = ref.replace('refs/tags/', '') - try: - version_num = int(tag_name.split('.')[-1]) - tag_names.append((version_num, tag_name)) - except (ValueError, IndexError): - continue - - if not tag_names: - return None - - # Sort by version number (descending) and check recent tags - tag_names.sort(reverse=True) - target = f"leanprover/lean4:{version}" - for _, tag_name in tag_names[:20]: - # Fetch lean-toolchain for this tag - api_url = f"{api_base}/contents/lean-toolchain?ref={tag_name}" - resp = requests.get(api_url, headers=headers, timeout=30) - if resp.status_code != 200: - continue - content = base64.b64decode(resp.json().get("content", "").replace("\n", "")).decode('utf-8').strip() - if content == target: - return tag_name - - return None - -def setup_downstream_releases_dir(): - """Create the downstream_releases directory if it doesn't exist.""" - downstream_dir = Path("downstream_releases") - if not downstream_dir.exists(): - print(blue(f"Creating {downstream_dir} directory...")) - downstream_dir.mkdir() - print(green(f"Created {downstream_dir} directory")) - return downstream_dir - -def clone_or_update_repo(repo_url, repo_dir, downstream_dir): - """Clone the repository if it doesn't exist, or update it if it does.""" - repo_path = downstream_dir / repo_dir - - if repo_path.exists(): - print(blue(f"Repository {repo_dir} already exists, updating...")) - run_command("git fetch", cwd=repo_path) - print(green(f"Updated repository {repo_dir}")) - else: - print(blue(f"Cloning {repo_url} to {repo_path}...")) - run_command(f"git clone {repo_url}", cwd=downstream_dir) - print(green(f"Cloned repository {repo_dir}")) - - return repo_path - -def get_remotes_for_repo(repo_name): - """Get the appropriate remotes for bump and nightly-testing branches based on repository.""" - if repo_name == "mathlib4": - return "nightly-testing", "nightly-testing" - else: - return "origin", "origin" - -def check_and_abort_merge(repo_path): - """Check if repository is in the middle of a merge and abort it if so.""" - merge_head_file = repo_path / ".git" / "MERGE_HEAD" - - if merge_head_file.exists(): - print(yellow(f"Repository {repo_path.name} is in the middle of a merge. Aborting merge...")) - run_command("git merge --abort", cwd=repo_path) - print(green("Merge aborted successfully")) - return True - - # Also check git status for other merge-related states - try: - result = run_command("git status --porcelain=v1", cwd=repo_path, check=False) - if result.returncode == 0: - # Check for unmerged paths (indicated by 'UU', 'AA', etc. in git status) - for line in result.stdout.splitlines(): - if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']: - print(yellow(f"Repository {repo_path.name} has unmerged paths. Aborting merge...")) - run_command("git merge --abort", cwd=repo_path) - print(green("Merge aborted successfully")) - return True - except subprocess.CalledProcessError: - # If git status fails, we'll let the main process handle it - pass - - return False - -def execute_release_steps(repo, version, config): - repo_config = find_repo(repo, config) - repo_name = repo_config['name'] - repo_url = repo_config['url'] - # Extract the last component of the URL, removing the .git extension if present - repo_dir = repo_url.split('/')[-1].replace('.git', '') - 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) - - # Setup downstream releases directory - downstream_dir = setup_downstream_releases_dir() - - # Clone or update the repository - repo_path = clone_or_update_repo(repo_url, repo_dir, downstream_dir) - - # Special remote setup for mathlib4 - if repo_name == "mathlib4": - print(blue("Setting up special remotes for mathlib4...")) - try: - # Check if nightly-testing remote already exists - result = run_command("git remote get-url nightly-testing", cwd=repo_path, check=False) - if result.returncode != 0: - # Add the nightly-testing remote - run_command("git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git", cwd=repo_path) - print(green("Added nightly-testing remote")) - else: - print(green("nightly-testing remote already exists")) - - # Fetch from the nightly-testing remote - run_command("git fetch nightly-testing", cwd=repo_path) - print(green("Fetched from nightly-testing remote")) - except subprocess.CalledProcessError as e: - print(red(f"Error setting up mathlib4 remotes: {e}")) - print(yellow("Continuing with default remote setup...")) - - print(blue(f"\n=== Executing release steps for {repo_name} ===")) - - # Check if repository is in the middle of a merge and abort it if necessary - check_and_abort_merge(repo_path) - - # Execute the release steps - run_command(f"git checkout {default_branch} && git pull", cwd=repo_path) - - # Special rc1 safety check for batteries and mathlib4 (before creating any branches) - if repo_name in ["batteries", "mathlib4"] and version.endswith('-rc1'): - print(blue("This repo has nightly-testing infrastructure")) - print(blue(f"Checking if nightly-testing can be safely merged into bump/{version.split('-rc')[0]}...")) - - # Get the base version (e.g., v4.6.0 from v4.6.0-rc1) - base_version = version.split('-rc')[0] - bump_branch = f"bump/{base_version}" - - # Determine which remote to use for bump and nightly-testing branches - bump_remote, nightly_remote = get_remotes_for_repo(repo_name) - - try: - # Fetch latest changes from the appropriate remote - run_command(f"git fetch {bump_remote}", cwd=repo_path) - - # Check if the bump branch exists - result = run_command(f"git show-ref --verify --quiet refs/remotes/{bump_remote}/{bump_branch}", cwd=repo_path, check=False) - if result.returncode != 0: - print(red(f"Bump branch {bump_remote}/{bump_branch} does not exist. Cannot perform safety check.")) - print(yellow("Please ensure the bump branch exists before proceeding.")) - return - - # Create a temporary branch for testing the merge - temp_branch = f"temp-merge-test-{base_version}" - - # Clean up any existing temp branch from previous runs - result = run_command(f"git show-ref --verify --quiet refs/heads/{temp_branch}", cwd=repo_path, check=False) - if result.returncode == 0: - print(blue(f"Cleaning up existing temp branch {temp_branch}...")) - # Make sure we're not on the temp branch before deleting it - run_command(f"git checkout {default_branch}", cwd=repo_path) - run_command(f"git branch -D {temp_branch}", cwd=repo_path) - print(green(f"Deleted existing temp branch {temp_branch}")) - - run_command(f"git checkout -b {temp_branch} {bump_remote}/{bump_branch}", cwd=repo_path) - - # Try to merge nightly-testing - try: - run_command(f"git merge {nightly_remote}/nightly-testing", cwd=repo_path) - - # Check what files have changed compared to the bump branch - changed_files = run_command(f"git diff --name-only {bump_remote}/{bump_branch}..HEAD", cwd=repo_path) - - # Filter out allowed changes - allowed_patterns = ['lean-toolchain', 'lake-manifest.json'] - problematic_files = [] - - for file in changed_files.stdout.strip().split('\n'): - if file.strip(): # Skip empty lines - is_allowed = any(pattern in file for pattern in allowed_patterns) - if not is_allowed: - problematic_files.append(file) - - # Clean up temporary branch and return to default branch - run_command(f"git checkout {default_branch}", cwd=repo_path) - run_command(f"git branch -D {temp_branch}", cwd=repo_path) - - if problematic_files: - print(red("❌ Safety check failed!")) - print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:")) - for file in problematic_files: - print(red(f" - {file}")) - print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first.")) - print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes.")) - return - else: - print(green("✅ Safety check passed - only lean-toolchain and/or lake-manifest.json would change")) - - except subprocess.CalledProcessError: - # Merge failed due to conflicts - check which files are conflicted - print(blue("Merge failed, checking which files are affected...")) - - # Get all changed files using git status - status_result = run_command("git status --porcelain", cwd=repo_path) - changed_files = [] - - for line in status_result.stdout.splitlines(): - if line.strip(): # Skip empty lines - # Extract filename (skip the first 3 characters which are status codes) - changed_files.append(line[3:]) - - # Filter out allowed files - allowed_patterns = ['lean-toolchain', 'lake-manifest.json'] - problematic_files = [] - - for file in changed_files: - is_allowed = any(pattern in file for pattern in allowed_patterns) - if not is_allowed: - problematic_files.append(file) - - if problematic_files: - # There are changes in non-allowed files - fail the safety check - # First abort the merge to clean up the conflicted state - run_command("git merge --abort", cwd=repo_path) - run_command(f"git checkout {default_branch}", cwd=repo_path) - run_command(f"git branch -D {temp_branch}", cwd=repo_path) - print(red("❌ Safety check failed!")) - print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:")) - for file in problematic_files: - print(red(f" - {file}")) - print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first.")) - print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes.")) - return - else: - # Only allowed files are changed - resolve them and continue - print(green(f"✅ Only allowed files changed: {', '.join(changed_files)}")) - print(blue("Resolving conflicts by taking nightly-testing version...")) - - # For each changed allowed file, take the nightly-testing version - for file in changed_files: - run_command(f"git checkout --theirs {file}", cwd=repo_path) - - # Complete the merge - run_command("git add .", cwd=repo_path) - run_command("git commit --no-edit", cwd=repo_path) - - print(green("✅ Safety check passed - changes only in allowed files")) - - # Clean up temporary branch and return to default branch - run_command(f"git checkout {default_branch}", cwd=repo_path) - run_command(f"git branch -D {temp_branch}", cwd=repo_path) - - except subprocess.CalledProcessError as e: - # Ensure we're back on the default branch even if setup failed - try: - run_command(f"git checkout {default_branch}", cwd=repo_path) - except subprocess.CalledProcessError: - print(red(f"Cannot return to {default_branch} branch. Repository is in an inconsistent state.")) - print(red("Please manually check the repository state and fix any issues.")) - return - print(red(f"Error during safety check: {e}")) - print(yellow("Skipping safety check and proceeding with normal merge...")) - - # Check if the branch already exists - branch_name = f"bump_to_{version}" - try: - # Check if branch exists locally - result = run_command(f"git show-ref --verify --quiet refs/heads/{branch_name}", cwd=repo_path, check=False) - if result.returncode == 0: - print(blue(f"Branch {branch_name} already exists, checking it out...")) - run_command(f"git checkout {branch_name}", cwd=repo_path) - print(green(f"Checked out existing branch {branch_name}")) - else: - print(blue(f"Creating new branch {branch_name}...")) - run_command(f"git checkout -b {branch_name}", cwd=repo_path) - print(green(f"Created new branch {branch_name}")) - except subprocess.CalledProcessError: - print(blue(f"Creating new branch {branch_name}...")) - run_command(f"git checkout -b {branch_name}", cwd=repo_path) - print(green(f"Created new branch {branch_name}")) - - # Update lean-toolchain - print(blue("Updating lean-toolchain file...")) - toolchain_file = repo_path / "lean-toolchain" - with open(toolchain_file, "w") as f: - f.write(f"leanprover/lean4:{version}\n") - print(green(f"Updated lean-toolchain to leanprover/lean4:{version}")) - - # Special cases for specific repositories - if repo_name == "repl": - run_command("lake update", cwd=repo_path, stream_output=True) - mathlib_test_dir = repo_path / "test" / "Mathlib" - run_command(f'perl -pi -e \'s/rev = "v\\d+\\.\\d+\\.\\d+(-rc\\d+)?"/rev = "{version}"/g\' lakefile.toml', cwd=mathlib_test_dir) - - # Update lean-toolchain in test/Mathlib - print(blue("Updating test/Mathlib/lean-toolchain...")) - mathlib_toolchain = mathlib_test_dir / "lean-toolchain" - with open(mathlib_toolchain, "w") as f: - f.write(f"leanprover/lean4:{version}\n") - print(green(f"Updated test/Mathlib/lean-toolchain to leanprover/lean4:{version}")) - - run_command("lake update", cwd=mathlib_test_dir, stream_output=True) - try: - result = run_command("./test.sh", cwd=repo_path, stream_output=True, check=False) - if result.returncode == 0: - print(green("Tests completed successfully")) - else: - print(red("Tests failed, but continuing with PR creation...")) - print(red(f"Test exit code: {result.returncode}")) - except subprocess.CalledProcessError as e: - print(red("Tests failed, but continuing with PR creation...")) - print(red(f"Test error: {e}")) - elif repo_name == "lean-fro.org": - # Update lean-toolchain in examples/hero - print(blue("Updating examples/hero/lean-toolchain...")) - docs_toolchain = repo_path / "examples" / "hero" / "lean-toolchain" - with open(docs_toolchain, "w") as f: - f.write(f"leanprover/lean4:{version}\n") - print(green(f"Updated examples/hero/lean-toolchain to leanprover/lean4:{version}")) - - print(blue("Running `lake update`...")) - run_command("lake update", cwd=repo_path, stream_output=True) - print(blue("Running `lake update` in examples/hero...")) - run_command("lake update", cwd=repo_path / "examples" / "hero", stream_output=True) - - # Run scripts/update.sh to regenerate content - print(blue("Running `scripts/update.sh` to regenerate content...")) - run_command("scripts/update.sh", cwd=repo_path, stream_output=True) - print(green("Content regenerated successfully")) - elif repo_name == "cslib": - print(blue("Updating lakefile.toml...")) - run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path) - run_command("lake update", cwd=repo_path, stream_output=True) - elif repo_name == "verso": - # verso has nested Lake projects in test-projects/ that each have their own - # lake-manifest.json with a subverso pin and their own lean-toolchain. - # After updating the root manifest via `lake update`, sync the de-modulized - # subverso rev into all sub-manifests, and update their lean-toolchain files. - run_command("lake update", cwd=repo_path, stream_output=True) - print(blue("Syncing de-modulized subverso rev to test-project sub-manifests...")) - sync_script = ( - 'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); ' - 'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); ' - 'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); ' - 'find test-projects -name lake-manifest.json -print0 | while IFS= read -r -d \'\' f; do ' - 'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "$f" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "$f"; ' - 'done' - ) - run_command(sync_script, cwd=repo_path) - print(green("Synced de-modulized subverso rev to all test-project sub-manifests")) - # Update all lean-toolchain files in test-projects/ to match the root - print(blue("Updating lean-toolchain files in test-projects/...")) - find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path) - for tc_path in find_result.stdout.strip().splitlines(): - if tc_path: - tc_file = repo_path / tc_path - with open(tc_file, "w") as f: - f.write(f"leanprover/lean4:{version}\n") - print(green(f" Updated {tc_path}")) - elif dependencies: - run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path) - run_command("lake update", cwd=repo_path, stream_output=True) - - # For reference-manual, update the release notes title to match the target version. - # e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)" - # e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)" - if repo_name == "reference-manual": - base_version = version.lstrip('v').split('-')[0] # "4.28.0" - file_name = f"v{base_version.replace('.', '_')}.lean" - release_notes_file = repo_path / "Manual" / "Releases" / file_name - - if release_notes_file.exists(): - is_rc = "-rc" in version - if is_rc: - # For RC releases, update to the exact RC version - display_version = version.lstrip('v') # "4.28.0-rc2" - else: - # For stable releases, strip any RC suffix - display_version = base_version # "4.28.0" - - print(blue(f"Updating release notes title in {file_name}...")) - content = release_notes_file.read_text() - # Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)" - new_content = re.sub( - r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)', - rf'\g<1>{display_version}\3', - content - ) - if new_content != content: - release_notes_file.write_text(new_content) - print(green(f"Updated release notes title to Lean {display_version}")) - else: - print(green("Release notes title already correct")) - else: - print(yellow(f"Release notes file {file_name} not found, skipping title update")) - - # For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y) - if repo_name == "mathlib4": - print(blue("Checking ProofWidgets4 version pin...")) - pw_tag = find_proofwidgets_tag(version) - if pw_tag: - print(blue(f"Updating ProofWidgets4 pin to {pw_tag}...")) - for lakefile in repo_path.glob("lakefile.*"): - content = lakefile.read_text() - # Only update the ProofWidgets4 dependency line, not other v0.0.X pins - new_content = re.sub( - r'(require\s+"leanprover-community"\s*/\s*"proofwidgets"\s*@\s*git\s+"v)0\.0\.\d+(")', - rf'\g<1>{pw_tag.removeprefix("v")}\2', - content - ) - if new_content != content: - lakefile.write_text(new_content) - print(green(f"Updated ProofWidgets4 pin in {lakefile.name}")) - run_command("lake update proofwidgets", cwd=repo_path, stream_output=True) - print(green(f"Updated ProofWidgets4 to {pw_tag}")) - else: - print(yellow(f"Could not find a ProofWidgets4 tag for toolchain {version}")) - print(yellow("You may need to update the ProofWidgets4 pin manually")) - - # Commit changes (only if there are changes) - print(blue("Checking for changes to commit...")) - try: - # Check if there are any changes to commit (staged or unstaged) - result = run_command("git status --porcelain", cwd=repo_path, check=False) - if result.stdout.strip(): # There are changes - print(blue("Committing changes...")) - run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path) - print(green(f"Committed changes: chore: bump toolchain to {version}")) - else: - print(green("No changes to commit - toolchain already up to date")) - except subprocess.CalledProcessError: - print(yellow("Failed to check for changes, attempting commit anyway...")) - try: - run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path) - except subprocess.CalledProcessError as e: - if "nothing to commit" in e.stderr: - print(green("No changes to commit - toolchain already up to date")) - else: - raise - - # Handle special merging cases - if version.endswith('-rc1') and repo_name in ["batteries", "mathlib4"]: - print(blue("This repo uses `bump/v4.X.0` branches for reviewed content from nightly-testing.")) - - # Determine which remote to use for bump branches - bump_remote, nightly_remote = get_remotes_for_repo(repo_name) - - # Fetch latest changes to ensure we have the most up-to-date bump branch - print(blue(f"Fetching latest changes from {bump_remote}...")) - run_command(f"git fetch {bump_remote}", cwd=repo_path) - - try: - print(blue(f"Merging {bump_remote}/bump/{version.split('-rc')[0]}...")) - run_command(f"git merge {bump_remote}/bump/{version.split('-rc')[0]}", cwd=repo_path) - print(green("Merge completed successfully")) - except subprocess.CalledProcessError: - # Merge failed due to conflicts - check which files are conflicted - print(blue("Merge conflicts detected, checking which files are affected...")) - - # Get conflicted files using git status - status_result = run_command("git status --porcelain", cwd=repo_path) - conflicted_files = [] - - for line in status_result.stdout.splitlines(): - if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']: - # Extract filename (skip the first 3 characters which are status codes) - conflicted_files.append(line[3:]) - - # Filter out allowed files - allowed_patterns = ['lean-toolchain', 'lake-manifest.json'] - problematic_files = [] - - for file in conflicted_files: - is_allowed = any(pattern in file for pattern in allowed_patterns) - if not is_allowed: - problematic_files.append(file) - - if problematic_files: - # There are conflicts in non-allowed files - fail - print(red("❌ Merge failed!")) - print(red(f"Merging {bump_remote}/bump/{version.split('-rc')[0]} resulted in conflicts in:")) - for file in problematic_files: - print(red(f" - {file}")) - print(red("Please resolve these conflicts manually.")) - return - else: - # Only allowed files are conflicted - resolve them automatically - print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}")) - print(blue("Resolving conflicts automatically...")) - - # Overwrite lean-toolchain with our target version - if 'lean-toolchain' in conflicted_files: - print(blue(f"Overwriting lean-toolchain with target version {version}")) - toolchain_file = repo_path / "lean-toolchain" - with open(toolchain_file, "w") as f: - f.write(f"leanprover/lean4:{version}\n") - - # For other allowed files, take our version (since we want our changes) - for file in conflicted_files: - if file != 'lean-toolchain': - run_command(f"git checkout --ours {file}", cwd=repo_path) - - # Run lake update to rebuild lake-manifest.json - print(blue("Running lake update to rebuild lake-manifest.json...")) - run_command("lake update", cwd=repo_path, stream_output=True) - - # Complete the merge - run_command("git add .", cwd=repo_path) - run_command("git commit --no-edit", cwd=repo_path) - - print(green("✅ Merge completed successfully with automatic conflict resolution")) - - elif version.endswith('-rc1'): - # For all other repos with rc versions, merge nightly-testing - if repo_name in ["verso", "reference-manual"]: - print(yellow("This repo does development on nightly-testing: remember to rebase merge the PR.")) - - # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch - print(blue("Fetching latest changes from origin...")) - run_command("git fetch origin", cwd=repo_path) - - # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match) - nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False) - if nightly_check.returncode != 0: - print(yellow("No nightly-testing branch found on origin, skipping merge")) - else: - try: - print(blue("Merging origin/nightly-testing...")) - run_command("git merge origin/nightly-testing", cwd=repo_path) - print(green("Merge completed successfully")) - except subprocess.CalledProcessError: - # Merge failed due to conflicts - check which files are conflicted - print(blue("Merge conflicts detected, checking which files are affected...")) - - # Get conflicted files using git status - status_result = run_command("git status --porcelain", cwd=repo_path) - conflicted_files = [] - - for line in status_result.stdout.splitlines(): - if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']: - # Extract filename (skip the first 3 characters which are status codes) - conflicted_files.append(line[3:]) - - # Filter out allowed files - allowed_patterns = ['lean-toolchain', 'lake-manifest.json'] - problematic_files = [] - - for file in conflicted_files: - is_allowed = any(pattern in file for pattern in allowed_patterns) - if not is_allowed: - problematic_files.append(file) - - if problematic_files: - # There are conflicts in non-allowed files - fail - print(red("❌ Merge failed!")) - print(red(f"Merging nightly-testing resulted in conflicts in:")) - for file in problematic_files: - print(red(f" - {file}")) - print(red("Please resolve these conflicts manually.")) - return - else: - # Only allowed files are conflicted - resolve them automatically - print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}")) - print(blue("Resolving conflicts automatically...")) - - # For lean-toolchain and lake-manifest.json, keep our versions - for file in conflicted_files: - print(blue(f"Keeping our version of {file}")) - run_command(f"git checkout --ours {file}", cwd=repo_path) - - # Complete the merge - run_command("git add .", cwd=repo_path) - run_command("git commit --no-edit", cwd=repo_path) - - print(green("✅ Merge completed successfully with automatic conflict resolution")) - - # Build and test (skip for Mathlib) - if repo_name not in ["mathlib4"]: - print(blue("Building project...")) - - # Clean lake cache for a fresh build - print(blue("Cleaning lake cache...")) - run_command("lake clean", cwd=repo_path) - - # Check if downstream of Mathlib and get cache if so - mathlib_package_dir = repo_path / ".lake" / "packages" / "mathlib" - if mathlib_package_dir.exists(): - print(blue("Project is downstream of Mathlib, fetching cache...")) - try: - run_command("lake exe cache get", cwd=repo_path, stream_output=True) - print(green("Cache fetched successfully")) - except subprocess.CalledProcessError as e: - print(yellow("Failed to fetch cache, continuing anyway...")) - print(yellow(f"Cache fetch error: {e}")) - - try: - run_command("lake build", cwd=repo_path, stream_output=True) - print(green("Build completed successfully")) - except subprocess.CalledProcessError as e: - print(red("Build failed, but continuing with PR creation...")) - print(red(f"Build error: {e}")) - - # Check if lake check-test exists before running tests - print(blue("Running tests...")) - check_test_result = run_command("lake check-test", cwd=repo_path, check=False) - if check_test_result.returncode == 0: - try: - run_command("lake test", cwd=repo_path, stream_output=True) - print(green("Tests completed successfully")) - except subprocess.CalledProcessError as e: - print(red("Tests failed, but continuing with PR creation...")) - print(red(f"Test error: {e}")) - else: - print(yellow("lake check-test reports that there is no test suite")) - - # Push the branch to remote before creating PR - print(blue("Checking remote branch status...")) - try: - # Check if branch exists on remote - result = run_command(f"git ls-remote --heads origin {branch_name}", cwd=repo_path, check=False) - if not result.stdout.strip(): - print(blue(f"Pushing branch {branch_name} to remote...")) - run_command(f"git push -u origin {branch_name}", cwd=repo_path) - print(green(f"Successfully pushed branch {branch_name} to remote")) - else: - print(blue(f"Branch {branch_name} already exists on remote, pushing any new commits...")) - run_command(f"git push", cwd=repo_path) - print(green("Successfully pushed commits to remote")) - except subprocess.CalledProcessError: - print(red("Failed to push branch to remote. Please check your permissions and network connection.")) - print(yellow(f"You may need to run: git push -u origin {branch_name}")) - return - - # Create pull request (only if one doesn't already exist) - print(blue("Checking for existing pull request...")) - try: - # Check if PR already exists for this branch - result = run_command(f'gh pr list --head {branch_name} --json number', cwd=repo_path, check=False) - if result.returncode == 0 and result.stdout.strip() != "[]": - print(green(f"Pull request already exists for branch {branch_name}")) - # Get the PR URL - pr_result = run_command(f'gh pr view {branch_name} --json url', cwd=repo_path, check=False) - if pr_result.returncode == 0: - pr_data = json.loads(pr_result.stdout) - print(green(f"PR URL: {pr_data.get('url', 'N/A')}")) - else: - # Create new PR - print(blue("Creating new pull request...")) - run_command(f'gh pr create --title "chore: bump toolchain to {version}" --body ""', cwd=repo_path) - print(green("Pull request created successfully!")) - except subprocess.CalledProcessError: - print(red("Failed to check for existing PR or create new PR.")) - print(yellow("This could be due to:")) - print(yellow("1. GitHub CLI not authenticated")) - print(yellow("2. No push permissions to the repository")) - print(yellow("3. Network issues")) - print(f"Branch: {branch_name}") - print(f"Title: chore: bump toolchain to {version}") - print(yellow("Please create the PR manually if needed.")) - -def main(): - parser = argparse.ArgumentParser( - description="Execute release steps for Lean4 repositories.", - formatter_class=argparse.RawDescriptionHelpFormatter, - epilog=""" -Examples: - %(prog)s v4.6.0 mathlib4 Execute steps for updating Mathlib to v4.6.0 - %(prog)s v4.6.0 batteries Execute steps for updating Batteries to v4.6.0 - -The script will: -1. Create a downstream_releases/ directory -2. Clone or update the target repository -3. Update the lean-toolchain file -4. Create appropriate branches and commits -5. Build and test the project -6. Create pull requests - -(Note that the steps of creating toolchain version tags, and merging these into `stable` branches, -are handled by `script/release_checklist.py`.) -""" - ) - parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)") - parser.add_argument("repo", help="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) - - execute_release_steps(args.repo, args.version, config) - -if __name__ == "__main__": - main()