From 5c927878382e7d4edf9ec5e336a32b5d41eb8d57 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Tue, 16 Sep 2025 15:05:51 -0700 Subject: [PATCH 1/2] chore: add manual backport instructions to readme --- README.md | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/README.md b/README.md index c5b24f652..1eb74bb36 100644 --- a/README.md +++ b/README.md @@ -67,6 +67,36 @@ python3 ./server.py 8880 & Then open in your browser. +## Backporting Manual Changes + +In the event that a backported update is necessary, manual deployment of the newly built HTML is handled via Git tags, which are version-numbered tags based on major Lean versions matching the RegEx pattern `^v4\.\d+\.\d+$`. Pushing a new tag triggers the necessary deployment, but to do so requires first deleting any existing tag of the same name. The following describes the steps and commands you may use to manage this process. + +Make any desired changes to the codebase. Once you have tested changes locally, create a new branch based on the version of the reference manual you are modifying. By convention, this branch should match the tag (i.e. version number), but without the leading `v`. Push this branch to the remote. + +For example, for modifications to the reference manual associated with Lean version 4.22, the branch should be named `4.22.0`: + +``` +git checkout -b 4.22.0 //create new branch +git push origin 4.22.0 //push new branch to remote +``` + +Any existing tag matching the desired version number must be deleted on both the remote and locally, then regeneratged locally and pushed to the remote to trigger deployment. + +For example, for modifications to the reference manual associated with Lean version 4.22, the tag to be regenerated is `v4.22.0` and the commands to delete it are: + +``` +git push origin :v4.22.0 //delete remote tag +git tag --delete v4.22.0 //delete local tag +``` + +Recreating the `v4.22.0` tag locally and pushing to origin will now trigger the new deployment: + +``` +git tag v4.22.0 //create new tag locally +git push origin v4.22.0 //push tag to remote +``` + + ## Contributing Please see [CONTRIBUTING.md](CONTRIBUTING.md) for more information. From 33581dc913f78cb49bb01becbb44619b37fe52ad Mon Sep 17 00:00:00 2001 From: Ashley Blacquiere Date: Wed, 17 Sep 2025 16:23:59 -0700 Subject: [PATCH 2/2] Apply suggestions from code review Co-authored-by: David Thrane Christiansen --- README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 1eb74bb36..cfb67af1d 100644 --- a/README.md +++ b/README.md @@ -69,15 +69,15 @@ Then open in your browser. ## Backporting Manual Changes -In the event that a backported update is necessary, manual deployment of the newly built HTML is handled via Git tags, which are version-numbered tags based on major Lean versions matching the RegEx pattern `^v4\.\d+\.\d+$`. Pushing a new tag triggers the necessary deployment, but to do so requires first deleting any existing tag of the same name. The following describes the steps and commands you may use to manage this process. +The manual for a Lean version is automatically deployed when a Git tag that matches the version is pushed. For Lean version `4.X.Y`, the manual is deployed from the contents of Git tag `v4.X.Y` (note the leading `v`). For version `4.X.Y-rcN`, the tag is `v4.X.Y-rcN`. In the event that a backported update is necessary, the tag should be changed. Pushing a new tag triggers the necessary deployment, but to do so requires first deleting any existing tag of the same name, because Git doesn't support modification of existing tags. The following describes the steps and commands you may use to manage this process. Make any desired changes to the codebase. Once you have tested changes locally, create a new branch based on the version of the reference manual you are modifying. By convention, this branch should match the tag (i.e. version number), but without the leading `v`. Push this branch to the remote. -For example, for modifications to the reference manual associated with Lean version 4.22, the branch should be named `4.22.0`: +For example, for modifications to the reference manual associated with Lean version 4.22, the branch should be named `4.22.0`. These examples assume that the main reference manual repository is named `origin` in your local checkout: ``` -git checkout -b 4.22.0 //create new branch -git push origin 4.22.0 //push new branch to remote +git checkout -b 4.22.0 # create new branch +git push origin 4.22.0 # push new branch to remote ``` Any existing tag matching the desired version number must be deleted on both the remote and locally, then regeneratged locally and pushed to the remote to trigger deployment. @@ -85,15 +85,15 @@ Any existing tag matching the desired version number must be deleted on both the For example, for modifications to the reference manual associated with Lean version 4.22, the tag to be regenerated is `v4.22.0` and the commands to delete it are: ``` -git push origin :v4.22.0 //delete remote tag -git tag --delete v4.22.0 //delete local tag +git push origin :v4.22.0 # delete remote tag +git tag --delete v4.22.0 # delete local tag ``` Recreating the `v4.22.0` tag locally and pushing to origin will now trigger the new deployment: ``` -git tag v4.22.0 //create new tag locally -git push origin v4.22.0 //push tag to remote +git tag v4.22.0 # create new tag locally +git push origin v4.22.0 # push tag to remote ```