diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 7680d0c10a2e..e8a5d0aa5b56 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -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. @@ -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. - 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. @@ -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 `""`). - Commit your changes to `src/CMakeLists.txt`, and push. - `git tag v4.7.0-rc1` - `git push origin v4.7.0-rc1` @@ -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. - (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 diff --git a/script/release_checklist.py b/script/release_checklist.py index f6b6ab9ff9da..b6479303af48 100755 --- a/script/release_checklist.py +++ b/script/release_checklist.py @@ -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/\")" ] for line in expected_lines: diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 31e5cb5b537a..4d3d44068a39 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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. set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform") if (NOT LEAN_PLATFORM_TARGET) diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean index 53b50150160e..e30026cf7beb 100644 --- a/src/Lean/DocString/Links.lean +++ b/src/Lean/DocString/Links.lean @@ -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/"