chore: enable build-specific documentation roots #7455
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR enables the use of the build-time configuration of the Lean reference manual URL and updates the release checklist to account for the reference manual. This is a follow-up to leanprover#7240, after the required `stage0` update.
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
kim-em
reviewed
Mar 13, 2025
| @@ -165,6 +168,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. | |||
| - 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`). | |||
| - change the `LEAN_MANUAL_ROOT` line to `set(LEAN_MANUAL_ROOT "https://.../4.7.0/")`, with the correct version, after confirming the deployment location for the reference manual for this release. (this should be a change; on `master` and nightly releases it is always `""`). | |||
There was a problem hiding this comment.
Can we just replace the ... with the URL from release_checklist.py?
kim-em
reviewed
Mar 13, 2025
| @@ -135,7 +135,8 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t | |||
| f"set(LEAN_VERSION_MAJOR {version_major})", | |||
| f"set(LEAN_VERSION_MINOR {version_minor})", | |||
| f"set(LEAN_VERSION_PATCH 0)", | |||
| f"set(LEAN_VERSION_IS_RELEASE 1)" | |||
| f"set(LEAN_VERSION_IS_RELEASE 1)", | |||
| f"set(LEAN_MANUAL_ROOT \"https://lean-lang.org/doc/reference/{version_major}.{version_minor}.0/\")" | |||
There was a problem hiding this comment.
I guess I don't really understand why we need an extra line here. Shouldn't this just be determined from the existing variables?
kim-em
reviewed
Mar 13, 2025
| @@ -20,6 +20,7 @@ if (LEAN_SPECIAL_VERSION_DESC) | |||
| elseif (NOT LEAN_VERSION_IS_RELEASE) | |||
| string(APPEND LEAN_VERSION_STRING "-pre") | |||
| endif() | |||
| set(LEAN_MANUAL_ROOT "") # Set this to the correct location for releases and release candidates. Include the trailing slash. | |||
There was a problem hiding this comment.
Similarly here, I think the comment should tell the human what the URL should be, if they need to set it by hand!
kim-em
reviewed
Mar 13, 2025
| @@ -124,6 +126,7 @@ We'll use `v4.6.0` as the intended release version as a running example. | |||
| - Create and push the tag | |||
| - Merge the tag into `stable` | |||
| - Run `script/release_checklist.py v4.6.0` again to check that everything is in order. | |||
| - Deploy the reference manual for the release to the specified URL, replacing the version that was deployed for the RC. | |||
There was a problem hiding this comment.
I don't know how to do this step! What am I actually meant to do here?
kim-em
reviewed
Mar 13, 2025
Comment on lines
+209
to
+210
| - Deploy the reference manual for the release candidate to the URL specified above. It will be replaced by | ||
| the final release's manual as part of the release process. |
There was a problem hiding this comment.
Similarly here. What do I need to do?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR enables the use of the build-time configuration of the Lean reference manual URL and updates the release checklist to account for the reference manual.
This is a follow-up to #7240, after the required
stage0update.The release process described here uses the same location for the reference manual for RCs and stable releases. This is for two reasons: