add notes about verso/reference-manual

doc/dev/release_checklist.md

@@ -144,6 +144,10 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     - Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` 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.
@@ -151,7 +155,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
       - 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.
+    - 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.

script/merge_remote.py

@@ -47,10 +47,10 @@ def run_command(command, check=True, capture_output=True):
 
 
 def clone_repo(repo, temp_dir):
-    """Clone the repository to a temporary directory using shallow clone."""
-    print(f"Shallow cloning {repo}...")
-    # Keep the shallow clone for efficiency
-    clone_result = run_command(f"gh repo clone {repo} {temp_dir} -- --depth=1", check=False)
+    """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}")
@@ -95,26 +95,16 @@ def check_and_merge(repo, branch, tag, temp_dir):
     if checkout_result.returncode != 0:
         return False
 
-    # Try merging the tag in a dry-run to check if it can be merged cleanly
-    print(f"Checking if {tag} can be merged cleanly into {branch}...")
-    merge_check = run_command(f"git merge --no-commit --no-ff {tag}", check=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_check.returncode != 0:
+    if merge_result.returncode != 0:
         print(f"Cannot merge {tag} cleanly into {branch}.")
         print("Merge conflicts would occur. Aborting merge.")
         run_command("git merge --abort")
         return False
     
-    # Abort the test merge
-    run_command("git reset --hard HEAD")
-    
-    # Now perform the actual merge and push to remote
-    print(f"Merging {tag} into {branch}...")
-    merge_result = run_command(f"git merge {tag} --no-edit")
-    if merge_result.returncode != 0:
-        print(f"Failed to merge {tag} into {branch}.")
-        return False
-    
     print(f"Pushing changes to remote...")
     push_result = run_command(f"git push origin {branch}")
     if push_result.returncode != 0:

script/release_checklist.py

@@ -255,6 +255,7 @@ def main():
     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")
@@ -360,10 +361,24 @@ def main():
         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)
-                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
+                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:

script/release_repos.yml

@@ -21,12 +21,19 @@ repositories:
     branch: master
     dependencies: []
 
+  - name: lean4-cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: doc-gen4
     url: https://github.com/leanprover/doc-gen4
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: []
+    dependencies: [lean4-cli]
 
   - name: verso
     url: https://github.com/leanprover/verso
@@ -42,20 +49,13 @@ repositories:
     branch: main
     dependencies: [verso]
 
-  - name: lean4-cli
-    url: https://github.com/leanprover/lean4-cli
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: ProofWidgets4
     url: https://github.com/leanprover-community/ProofWidgets4
     toolchain-tag: false
     stable-branch: false
     branch: main
     dependencies:
-      - Batteries
+      - batteries
 
   - name: aesop
     url: https://github.com/leanprover-community/aesop
@@ -63,7 +63,7 @@ repositories:
     stable-branch: true
     branch: master
     dependencies:
-      - Batteries
+      - batteries
 
   - name: import-graph
     url: https://github.com/leanprover-community/import-graph
@@ -71,8 +71,8 @@ repositories:
     stable-branch: false
     branch: main
     dependencies:
-      - Cli
-      - Batteries
+      - lean4-cli
+      - batteries
 
   - name: plausible
     url: https://github.com/leanprover-community/plausible
@@ -88,10 +88,11 @@ repositories:
     branch: master
     bump-branch: true
     dependencies:
-      - Aesop
+      - aesop
       - ProofWidgets4
       - lean4checker
-      - Batteries
+      - batteries
+      - lean4-cli
       - doc-gen4
       - import-graph
       - plausible
@@ -102,4 +103,4 @@ repositories:
     stable-branch: true
     branch: master
     dependencies:
-      - Mathlib
+      - mathlib4

script/release_steps.py

@@ -68,7 +68,7 @@ def generate_script(repo, version, config):
     ]
 
     # Special cases for specific repositories
-    if repo_name == "REPL":
+    if repo_name == "repl":
         script_lines.extend([
             "lake update",
             "cd test/Mathlib",
@@ -79,7 +79,7 @@ def generate_script(repo, version, config):
             "./test.sh"
         ])
     elif dependencies:
-        script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"')
+        script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
         script_lines.append("lake update")
 
     script_lines.append("")
@@ -89,13 +89,20 @@ def generate_script(repo, version, config):
         ""
     ])
 
-    if re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
+    if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
         script_lines.extend([
             "echo 'This repo has nightly-testing infrastructure'",
             f"git merge origin/bump/{version.split('-rc')[0]}",
             "echo 'Please resolve any conflicts.'",
             ""
         ])
+    if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:
+        script_lines.extend([
+            "echo 'This repo does development on nightly-testing: remember to rebase merge the PR.'",
+            f"git merge origin/nightly-testing",
+            "echo 'Please resolve any conflicts.'",
+            ""
+        ])
     if repo_name != "Mathlib":
         script_lines.extend([
             "lake build && if lake check-test; then lake test; fi",
@@ -104,7 +111,7 @@ def generate_script(repo, version, config):
 
     script_lines.extend([
         'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
-        "echo 'Please review the PR and merge it.'",
+        "echo 'Please review the PR and merge or rebase it.'",
         ""
     ])