Merge tag 'nightly-2025-04-02' into releases/v4.19.0

Author: kim-em

CMakeLists.txt

@@ -20,6 +20,9 @@ foreach(var ${vars})
     elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
+  elseif("${var}" MATCHES "USE_MIMALLOC")
+    list(APPEND CL_ARGS "-D${var}=${${var}}")
+    list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
   elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()

CMakePresets.json

@@ -30,6 +30,7 @@
         "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
         "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
         "SMALL_ALLOCATOR": "OFF",
+        "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
         "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
       },

script/merge_remote.py

@@ -0,0 +1,165 @@
+#!/usr/bin/env python3
+
+"""
+Merge a tag into a branch on a GitHub repository.
+
+This script checks if a specified tag can be merged cleanly into a branch and performs
+the merge if possible. If the merge cannot be done cleanly, it prints a helpful message.
+
+Usage:
+    python3 merge_remote.py <org/repo> <branch> <tag>
+
+Arguments:
+    org/repo: GitHub repository in the format 'organization/repository'
+    branch: The target branch to merge into
+    tag: The tag to merge from
+
+Example:
+    python3 merge_remote.py leanprover/mathlib4 stable v4.6.0
+
+The script uses the GitHub CLI (`gh`), so make sure it's installed and authenticated.
+"""
+
+import argparse
+import subprocess
+import sys
+import tempfile
+import os
+import shutil
+
+
+def run_command(command, check=True, capture_output=True):
+    """Run a shell command and return the result."""
+    try:
+        result = subprocess.run(
+            command,
+            check=check,
+            shell=True,
+            text=True,
+            capture_output=capture_output
+        )
+        return result
+    except subprocess.CalledProcessError as e:
+        if capture_output:
+            print(f"Command failed: {command}")
+            print(f"Error: {e.stderr}")
+        return e
+
+
+def clone_repo(repo, temp_dir):
+    """Clone the repository to a temporary directory using shallow clone."""
+    print(f"Shallow cloning {repo}...")
+    # Use --depth=1 for shallow clone
+    clone_result = run_command(f"gh repo clone {repo} {temp_dir} -- --depth=1", check=False)
+    if clone_result.returncode != 0:
+        print(f"Failed to clone repository {repo}.")
+        print(f"Error: {clone_result.stderr}")
+        return False
+    return True
+
+
+def check_and_merge(repo, branch, tag, temp_dir):
+    """Check if tag can be merged into branch and perform the merge if possible."""
+    # Change to the temporary directory
+    os.chdir(temp_dir)
+    
+    # Fetch only the specific branch and tag we need
+    print(f"Fetching branch '{branch}' and tag '{tag}'...")
+    fetch_branch = run_command(f"git fetch origin {branch}")
+    if fetch_branch.returncode != 0:
+        print(f"Error: Failed to fetch branch '{branch}'.")
+        return False
+        
+    fetch_tag = run_command(f"git fetch origin tag {tag}")
+    if fetch_tag.returncode != 0:
+        print(f"Error: Failed to fetch tag '{tag}'.")
+        return False
+
+    # Check if branch exists
+    branch_check = run_command(f"git branch -r | grep origin/{branch}")
+    if branch_check.returncode != 0:
+        print(f"Error: Branch '{branch}' does not exist in repository.")
+        return False
+
+    # Check if tag exists
+    tag_check = run_command(f"git tag -l {tag}")
+    if tag_check.returncode != 0 or not tag_check.stdout.strip():
+        print(f"Error: Tag '{tag}' does not exist in repository.")
+        return False
+
+    # Checkout the branch
+    print(f"Checking out branch '{branch}'...")
+    checkout_result = run_command(f"git checkout -b {branch} origin/{branch}")
+    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)
+    
+    if merge_check.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:
+        print(f"Failed to push changes to remote.")
+        return False
+    
+    print(f"Successfully merged {tag} into {branch} and pushed to remote.")
+    return True
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Merge a tag into a branch on a GitHub repository.",
+        formatter_class=argparse.RawDescriptionHelpFormatter,
+        epilog="""
+Examples:
+  %(prog)s leanprover/mathlib4 stable v4.6.0    Merge tag v4.6.0 into stable branch
+
+The script will:
+1. Clone the repository
+2. Check if the tag and branch exist
+3. Check if the tag can be merged cleanly into the branch
+4. Perform the merge and push to remote if possible
+        """
+    )
+    parser.add_argument("repo", help="GitHub repository in the format 'organization/repository'")
+    parser.add_argument("branch", help="The target branch to merge into")
+    parser.add_argument("tag", help="The tag to merge from")
+    
+    args = parser.parse_args()
+    
+    # Create a temporary directory for the repository
+    temp_dir = tempfile.mkdtemp()
+    try:
+        # Clone the repository
+        if not clone_repo(args.repo, temp_dir):
+            sys.exit(1)
+        
+        # Check if the tag can be merged and perform the merge
+        if not check_and_merge(args.repo, args.branch, args.tag, temp_dir):
+            sys.exit(1)
+        
+    finally:
+        # Clean up the temporary directory
+        print(f"Cleaning up temporary files...")
+        shutil.rmtree(temp_dir)
+
+
+if __name__ == "__main__":
+    main() 

script/release_checklist.py

@@ -8,6 +8,11 @@
 import sys
 import os
 
+def debug(verbose, message):
+    """Print debug message if verbose mode is enabled."""
+    if verbose:
+        print(f"    [DEBUG] {message}")
+
 def parse_repos_config(file_path):
     with open(file_path, "r") as f:
         return yaml.safe_load(f)["repositories"]
@@ -90,14 +95,15 @@ def is_version_gte(version1, version2):
         return False
     return parse_version(version1) >= parse_version(version2)
 
-def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
+def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token, verbose=False):
     # First get the commit SHA for the tag
     api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
 
     # Get tag's commit SHA
     tag_response = requests.get(f"{api_base}/git/refs/tags/{tag_name}", headers=headers)
     if tag_response.status_code != 200:
+        debug(verbose, f"Could not fetch tag {tag_name}, status code: {tag_response.status_code}")
         return False
 
     # Handle both single object and array responses
@@ -106,22 +112,48 @@ def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
         # Find the exact matching tag in the list
         matching_tags = [tag for tag in tag_data if tag['ref'] == f'refs/tags/{tag_name}']
         if not matching_tags:
+            debug(verbose, f"No matching tag found for {tag_name} in response list")
             return False
         tag_sha = matching_tags[0]['object']['sha']
     else:
         tag_sha = tag_data['object']['sha']
-
+    
+    # Check if the tag is an annotated tag and get the actual commit SHA
+    if tag_data.get('object', {}).get('type') == 'tag' or (
+        isinstance(tag_data, list) and 
+        matching_tags and 
+        matching_tags[0].get('object', {}).get('type') == 'tag'):
+        
+        # Get the commit that this tag points to
+        tag_obj_response = requests.get(f"{api_base}/git/tags/{tag_sha}", headers=headers)
+        if tag_obj_response.status_code == 200:
+            tag_obj = tag_obj_response.json()
+            if 'object' in tag_obj and tag_obj['object']['type'] == 'commit':
+                commit_sha = tag_obj['object']['sha']
+                debug(verbose, f"Tag is annotated. Resolved commit SHA: {commit_sha}")
+                tag_sha = commit_sha  # Use the actual commit SHA
+    
     # Get commits on stable branch containing this SHA
     commits_response = requests.get(
         f"{api_base}/commits?sha={stable_branch}&per_page=100",
         headers=headers
     )
     if commits_response.status_code != 200:
+        debug(verbose, f"Could not fetch commits for branch {stable_branch}, status code: {commits_response.status_code}")
         return False
 
     # Check if any commit in stable's history matches our tag's SHA
     stable_commits = [commit['sha'] for commit in commits_response.json()]
-    return tag_sha in stable_commits
+    
+    is_merged = tag_sha in stable_commits
+    
+    debug(verbose, f"Tag SHA: {tag_sha}")
+    debug(verbose, f"First 5 stable commits: {stable_commits[:5]}")
+    debug(verbose, f"Total stable commits fetched: {len(stable_commits)}")
+    if not is_merged:
+        debug(verbose, f"Tag SHA not found in first {len(stable_commits)} commits of stable branch")
+    
+    return is_merged
 
 def is_release_candidate(version):
     return "-rc" in version
@@ -195,13 +227,15 @@ def pr_exists_with_title(repo_url, title, github_token):
     return None
 
 def main():
-    github_token = get_github_token()
+    parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
+    parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
+    parser.add_argument("--verbose", "-v", action="store_true", help="Enable verbose debugging output")
+    args = parser.parse_args()
 
-    if len(sys.argv) != 2:
-        print("Usage: python3 release_checklist.py <toolchain>")
-        sys.exit(1)
-
-    toolchain = sys.argv[1]
+    github_token = get_github_token()
+    toolchain = args.toolchain
+    verbose = args.verbose
+    
     stripped_toolchain = strip_rc_suffix(toolchain)
     lean_repo_url = "https://github.com/leanprover/lean4"
 
@@ -291,6 +325,7 @@ def main():
                 print(f"  ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})")
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
+                print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")
             repo_status[name] = False
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
@@ -303,8 +338,10 @@ def main():
             print(f"  ✅ Tag {toolchain} exists")
 
         if check_stable and not is_release_candidate(toolchain):
-            if not is_merged_into_stable(url, toolchain, "stable", github_token):
+            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
             print(f"  ✅ Tag {toolchain} is merged into stable")

script/release_repos.yml

@@ -85,6 +85,7 @@ repositories:
       - Batteries
       - doc-gen4
       - import-graph
+      - plausible
 
   - name: REPL
     url: https://github.com/leanprover-community/repl

script/release_steps.py

@@ -51,35 +51,40 @@ def find_repo(repo_substring, config):
 def generate_script(repo, version, config):
     repo_config = find_repo(repo, config)
     repo_name = repo_config['name']
+    repo_url = repo_config['url']
+    # Extract the last component of the URL, removing the .git extension if present
+    repo_dir = repo_url.split('/')[-1].replace('.git', '')
     default_branch = repo_config.get("branch", "main")
     dependencies = repo_config.get("dependencies", [])
     requires_tagging = repo_config.get("toolchain-tag", True)
     has_stable_branch = repo_config.get("stable-branch", True)
 
     script_lines = [
-        f"cd {repo_name}",
+        f"cd {repo_dir}",
         "git fetch",
-        f"git checkout {default_branch}",
+        f"git checkout {default_branch} && git pull",
         f"git checkout -b bump_to_{version}",
         f"echo leanprover/lean4:{version} > lean-toolchain",
     ]
 
     # Special cases for specific repositories
     if repo_name == "REPL":
         script_lines.extend([
+            "lake update",
             "cd test/Mathlib",
+            f"perl -pi -e 's/rev = \"v\\d+\\.\\d+\\.\\d+(-rc\\d+)?\"/rev = \"{version}\"/g' lakefile.toml",
             f"echo leanprover/lean4:{version} > lean-toolchain",
-            'echo "Please update the dependencies in lakefile.{lean,toml}"',
             "lake update",
-            "cd ../.."
+            "cd ../..",
+            "./test.sh"
         ])
     elif dependencies:
         script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"')
+        script_lines.append("lake update")
 
-    script_lines.append("lake update")
     script_lines.append("")
 
-    if not re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
+    if re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
         script_lines.extend([
             "echo 'This repo has nightly-testing infrastructure'",
             f"git merge bump/{version}",
@@ -98,13 +103,13 @@ def generate_script(repo, version, config):
     if repo_name == "ProofWidgets4":
         script_lines.append(f"echo 'Note: Follow the version convention of the repository for tagging.'")
     elif requires_tagging:
-        script_lines.append(f"git tag -a {version} -m 'Release {version}'")
-        script_lines.append("git push origin --tags")
+        script_lines.append(f"git checkout {default_branch} && git pull")
+        script_lines.append(f'[ "$(cat lean-toolchain)" = "leanprover/lean4:{version}" ] && git tag -a {version} -m \'Release {version}\' && git push origin --tags || echo "Error: lean-toolchain does not contain expected version {version}"')
 
     if has_stable_branch:
         script_lines.extend([
-            "git checkout stable",
-            f"git merge {version}",
+            "git checkout stable && git pull",
+            f"git merge {version} --no-edit",
             "git push origin stable"
         ])
 

src/Init/Data/BitVec/Bitblast.lean

@@ -1752,4 +1752,9 @@ theorem extractLsb'_mul {w len} {x y : BitVec w} (hlen : len ≤ w) :
     (x * y).extractLsb' 0 len = (x.extractLsb' 0 len) * (y.extractLsb' 0 len) := by
   simp [← setWidth_eq_extractLsb' hlen, setWidth_mul _ _ hlen]
 
+/-- Adding bitvectors that are zero in complementary positions equals concatenation. -/
+theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
+    (x ++ 0#w) + (0#v ++ y) = x ++ y := by
+  rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
+
 end BitVec