Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: enable build-specific documentation roots #7455

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+11 −6
Open

chore: enable build-specific documentation roots #7455

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion doc/dev/release_checklist.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,9 @@ We'll use `v4.6.0` as the intended release version as a running example.
- In `src/CMakeLists.txt`, verify you see
- `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
- `set(LEAN_VERSION_IS_RELEASE 1)`
- (both of these should already be in place from the release candidates)
- `set(LEAN_MANUAL_ROOT "https://lean-lang.org/doc/reference/4.6.0/")`
- (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.
Expand Down Expand Up @@ -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.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know how to do this step! What am I actually meant to do here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That was a bit of a TODO... I'll get it fleshed out, then return here. The plan is to have it be something like "push a tag that looks like this to such-and-such repo", but the deployment script isn't yet written.

- 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.
Expand Down Expand Up @@ -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 `""`).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we just replace the ... with the URL from release_checklist.py?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, will do!

- Commit your changes to `src/CMakeLists.txt`, and push.
- `git tag v4.7.0-rc1`
- `git push origin v4.7.0-rc1`
Expand Down Expand Up @@ -202,6 +206,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
- 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.
- 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.
Comment on lines +209 to +210
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly here. What do I need to do?

- (Note: we're currently uncertain if we really want to do this step. Check with Kim Morrison if you're unsure.)
For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
`nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
Expand Down
3 changes: 2 additions & 1 deletion script/release_checklist.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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/\")"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess I don't really understand why we need an extra line here. Shouldn't this just be determined from the existing variables?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That will work too. I'll update it. My thought process was that it lets us be flexible if we want, but we can always change this later if we decide on a different URL scheme.

]

for line in expected_lines:
Expand Down
1 change: 1 addition & 0 deletions src/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly here, I think the comment should tell the human what the URL should be, if they need to set it by hand!


set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform")
if (NOT LEAN_PLATFORM_TARGET)
Expand Down
5 changes: 1 addition & 4 deletions src/Lean/DocString/Links.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,8 @@ set_option linter.missingDocs true

namespace Lean

/- After a stage0 update:
@[extern "lean_get_manual_root"]
@[extern "lean_manual_get_root"]
private opaque getManualRoot : Unit → String
-/
private def getManualRoot : Unit → String := fun () => ""

private def fallbackManualRoot := "https://lean-lang.org/doc/reference/latest/"

Expand Down
Loading