merge no-import matcher info

Author: Kha

.claude/CLAUDE.md

@@ -46,6 +46,21 @@ This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
 leading quantifiers are stripped when creating a pattern.
 ```
 
+**Changelog labels:** Add one `changelog-*` label to categorize the PR for release notes:
+- `changelog-language` - Language features and metaprograms
+- `changelog-tactics` - User facing tactics
+- `changelog-server` - Language server, widgets, and IDE extensions
+- `changelog-pp` - Pretty printing
+- `changelog-library` - Library
+- `changelog-compiler` - Compiler, runtime, and FFI
+- `changelog-lake` - Lake
+- `changelog-doc` - Documentation
+- `changelog-ffi` - FFI changes
+- `changelog-other` - Other changes
+- `changelog-no` - Do not include this PR in the release changelog
+
+If you're unsure which label applies, it's fine to omit the label and let reviewers add it.
+
 ## CI Log Retrieval
 
 When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.

.github/workflows/pr-release.yml

@@ -43,6 +43,19 @@ jobs:
           name: build-.*
           name_is_regexp: true
 
+      # Verify artifacts were downloaded before any side effects (tag creation, release deletion).
+      - name: Verify release artifacts exist
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        run: |
+          shopt -s nullglob
+          files=(artifacts/*/*)
+          if [ ${#files[@]} -eq 0 ]; then
+            echo "::error::No artifacts found matching artifacts/*/*"
+            exit 1
+          fi
+          echo "Found ${#files[@]} artifacts to upload:"
+          printf '%s\n' "${files[@]}"
+
       - name: Push tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
@@ -74,18 +87,6 @@ jobs:
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
-      # Verify artifacts were downloaded (equivalent to fail_on_unmatched_files in the old action).
-      - name: Verify release artifacts exist
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          shopt -s nullglob
-          files=(artifacts/*/*)
-          if [ ${#files[@]} -eq 0 ]; then
-            echo "::error::No artifacts found matching artifacts/*/*"
-            exit 1
-          fi
-          echo "Found ${#files[@]} artifacts to upload:"
-          printf '%s\n' "${files[@]}"
       # We use `gh release create` instead of `softprops/action-gh-release` because
       # the latter enumerates all releases to check for existing ones, which fails
       # when the repository has more than 10000 releases (GitHub API pagination limit).

CMakeLists.txt

@@ -10,22 +10,22 @@ option(USE_MIMALLOC "use mimalloc" ON)
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
-  if("${var}" MATCHES "STAGE0_(.*)")
+  if(var MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif("${var}" MATCHES "STAGE1_(.*)")
+  elseif(var MATCHES "STAGE1_(.*)")
     list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
+  elseif(currentHelpString MATCHES "No help, variable specified on the command line." OR currentHelpString STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
+    if(var MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
+    elseif(var MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
-  elseif("${var}" MATCHES "USE_MIMALLOC")
+  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"))
+  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()
 endforeach()
@@ -34,15 +34,15 @@ include(ExternalProject)
 project(LEAN CXX C)
 
 if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
-    set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
+  set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
 
 # Don't do anything with cadical on wasm
-if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   find_program(CADICAL cadical)
   if(NOT CADICAL)
     set(CADICAL_CXX c++)
-    if (CADICAL_USE_CUSTOM_CXX)
+    if(CADICAL_USE_CUSTOM_CXX)
       set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
       # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
       # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
@@ -54,81 +54,101 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
       set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
     endif()
     # missing stdio locking API on Windows
-    if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
       string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
     endif()
     string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
-    ExternalProject_add(cadical
+    ExternalProject_Add(
+      cadical
       PREFIX cadical
       GIT_REPOSITORY https://github.com/arminbiere/cadical
       GIT_TAG rel-2.1.2
       CONFIGURE_COMMAND ""
-      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
-        CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-        CXX=${CADICAL_CXX}
-        CXXFLAGS=${CADICAL_CXXFLAGS}
-        LDFLAGS=${CADICAL_LDFLAGS}
+      BUILD_COMMAND
+        $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
+        CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS} LDFLAGS=${CADICAL_LDFLAGS}
       BUILD_IN_SOURCE ON
-      INSTALL_COMMAND "")
-    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
+      INSTALL_COMMAND ""
+    )
+    set(
+      CADICAL
+      ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX}
+      CACHE FILEPATH
+      "path to cadical binary"
+      FORCE
+    )
     list(APPEND EXTRA_DEPENDS cadical)
   endif()
   list(APPEND CL_ARGS -DCADICAL=${CADICAL})
 endif()
 
-if (USE_MIMALLOC)
-  ExternalProject_add(mimalloc
+if(USE_MIMALLOC)
+  ExternalProject_Add(
+    mimalloc
     PREFIX mimalloc
     GIT_REPOSITORY https://github.com/microsoft/mimalloc
     GIT_TAG v2.2.3
     # just download, we compile it as part of each stage as it is small
     CONFIGURE_COMMAND ""
     BUILD_COMMAND ""
-    INSTALL_COMMAND "")
+    INSTALL_COMMAND ""
+  )
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-if (NOT STAGE1_PREV_STAGE)
-  ExternalProject_add(stage0
+if(NOT STAGE1_PREV_STAGE)
+  ExternalProject_Add(
+    stage0
     SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
     SOURCE_SUBDIR src
     BINARY_DIR stage0
     # do not rebuild stage0 when git hash changes; it's not from this commit anyway
     # (however, CI will override this as we need to embed the githash into the stage 1 library built
     # by stage 0)
     CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
-    INSTALL_COMMAND ""  # skip install
+    BUILD_ALWAYS
+      ON # cmake doesn't auto-detect changes without a download method
+    INSTALL_COMMAND
+      "" # skip install
     DEPENDS ${EXTRA_DEPENDS}
   )
   list(APPEND EXTRA_DEPENDS stage0)
 endif()
-ExternalProject_add(stage1
+ExternalProject_Add(
+  stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
+  CMAKE_ARGS
+    -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0
+    -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS ${EXTRA_DEPENDS}
   STEP_TARGETS configure
 )
-ExternalProject_add(stage2
+ExternalProject_Add(
+  stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
+  CMAKE_ARGS
+    -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
+    ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage1
   EXCLUDE_FROM_ALL ON
   STEP_TARGETS configure
 )
-ExternalProject_add(stage3
+ExternalProject_Add(
+  stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
+  CMAKE_ARGS
+    -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
+    ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2
@@ -137,24 +157,14 @@ ExternalProject_add(stage3
 
 # targets forwarded to appropriate stages
 
-add_custom_target(update-stage0
-  COMMAND $(MAKE) -C stage1 update-stage0
-  DEPENDS stage1)
+add_custom_target(update-stage0 COMMAND $(MAKE) -C stage1 update-stage0 DEPENDS stage1)
 
-add_custom_target(update-stage0-commit
-  COMMAND $(MAKE) -C stage1 update-stage0-commit
-  DEPENDS stage1)
+add_custom_target(update-stage0-commit COMMAND $(MAKE) -C stage1 update-stage0-commit DEPENDS stage1)
 
-add_custom_target(test
-  COMMAND $(MAKE) -C stage1 test
-  DEPENDS stage1)
+add_custom_target(test COMMAND $(MAKE) -C stage1 test DEPENDS stage1)
 
-add_custom_target(clean-stdlib
-  COMMAND $(MAKE) -C stage1 clean-stdlib
-  DEPENDS stage1)
+add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 
-add_custom_target(check-stage3
-  COMMAND diff "stage2/bin/lean" "stage3/bin/lean"
-  DEPENDS stage3)
+add_custom_target(check-stage3 COMMAND diff "stage2/bin/lean" "stage3/bin/lean" DEPENDS stage3)

script/fmt

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# This script expects to be run from the repo root.
+
+# Format cmake files
+find -regex '.*/CMakeLists\.txt\(\.in\)?\|.*\.cmake\(\.in\)?' \
+  ! -path './build/*' \
+  ! -path "./stage0/*" \
+  -exec \
+    uvx gersemi --in-place --line-length 120 --indent 2 \
+    --definitions src/cmake/Modules/ src/CMakeLists.txt \
+    -- {} +