chore: update release_checklist.py to check new release notes page (#8235)

script/release_checklist.py

@@ -7,6 +7,7 @@ import base64
 import subprocess
 import sys
 import os
+import re # Import re module
 # Import run_command from merge_remote.py
 from merge_remote import run_command
 
@@ -58,13 +59,29 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
-def get_release_notes(repo_url, tag_name, github_token):
-    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/releases/tags/{tag_name}"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    response = requests.get(api_url, headers=headers)
-    if response.status_code == 200:
-        return response.json().get("body", "").strip()
-    return None
+def get_release_notes(tag_name):
+    """Fetch release notes page title from lean-lang.org."""
+    # Strip -rcX suffix if present for the URL
+    base_tag = tag_name.split('-')[0]
+    reference_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+    try:
+        response = requests.get(reference_url)
+        response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
+        
+        # Extract title using regex
+        match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
+        if match:
+            return match.group(1).strip()
+        else:
+            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
+            return None
+            
+    except requests.exceptions.RequestException as e:
+        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
+        return None
+    except Exception as e:
+        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
+        return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
@@ -275,14 +292,22 @@ def main():
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-        release_notes = get_release_notes(lean_repo_url, toolchain, github_token)
-        if not (release_notes and toolchain in release_notes.splitlines()[0].strip()):
-            previous_minor_version = version_minor - 1
-            previous_release = f"v{version_major}.{previous_minor_version}.0"
-            print(f"  ❌ Release notes not published. Please run `script/release_notes.py --since {previous_release}` on branch `{branch_name}`.")
-            lean4_success = False
-        else:
-            print(f"  ✅ Release notes look good.")
+        
+    # Check the actual release notes page title
+    actual_title = get_release_notes(toolchain)
+    expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
+
+    if actual_title is None:
+        # Error already printed by get_release_notes
+        lean4_success = False
+    elif not actual_title.startswith(expected_title_prefix):
+        # Construct URL for the error message (using the base tag)
+        base_tag = toolchain.split('-')[0]
+        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
+        lean4_success = False
+    else:
+        print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
     repo_status["lean4"] = lean4_success