test: add tests for several Lean versions

LeanUtilsTest.lean

@@ -0,0 +1,2 @@
+import LeanUtilsTest.LeanFileWithSorries
+import LeanUtilsTest.TestExtractSorry

LeanUtilsTest/PROCESS.md

@@ -0,0 +1,8 @@
+0. Loop over toolchains in the testable_toolchain.txt file
+1. Create temporary directory with project to test on with the current toolchain
+2. run lake update, lake build, lake test
+3. Surface errors to the user. 
+4. Clean up temporary directory. 
+5. In a future where we need different versions of the repo for different
+   intervals of toolchains, of course only test on the interval of toolchains
+   corresponding to the current version.

LeanUtilsTest/TestExtractSorry.lean

@@ -1,4 +1,4 @@
-import LeanUtils.ExtractSorry
+import bins.ExtractSorry
 
 /--
 info: Running sorry extraction.

LeanUtilsTest/run_tests.sh

@@ -0,0 +1,162 @@
+#!/usr/bin/env bash
+
+# Test suite for LeanUtils across multiple Lean toolchains
+# Usage: ./run_tests.sh [path_to_testable_toolchains.txt]
+
+set -e
+
+# Colors for output
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[1;33m'
+NC='\033[0m' # No Color
+
+# Get the directory where this script is located
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"
+
+# Path to toolchains file
+TOOLCHAINS_FILE="${1:-$SCRIPT_DIR/testable_toolchains.txt}"
+
+if [[ ! -f "$TOOLCHAINS_FILE" ]]; then
+    echo -e "${RED}Error: Toolchains file not found: $TOOLCHAINS_FILE${NC}"
+    exit 1
+fi
+
+echo "Testing LeanUtils across multiple toolchains"
+echo "=============================================="
+echo ""
+
+# Statistics
+TOTAL_TESTS=0
+PASSED_TESTS=0
+FAILED_TESTS=0
+declare -a FAILED_TOOLCHAINS
+
+# Read toolchains from file
+while IFS= read -r toolchain || [[ -n "$toolchain" ]]; do
+    # Skip empty lines and comments
+    [[ -z "$toolchain" || "$toolchain" =~ ^[[:space:]]*# ]] && continue
+
+    TOTAL_TESTS=$((TOTAL_TESTS + 1))
+
+    echo -e "${YELLOW}Testing toolchain: $toolchain${NC}"
+    echo "-------------------------------------------"
+
+    # Create temporary directory
+    TEMP_DIR=$(mktemp -d -t lean-test-XXXXXXXXXX)
+
+    # Cleanup function
+    cleanup() {
+        if [[ -d "$TEMP_DIR" ]]; then
+            echo "  Cleaning up temporary directory..."
+            rm -rf "$TEMP_DIR"
+        fi
+    }
+
+    # Set trap to cleanup on exit
+    trap cleanup EXIT
+
+    # Copy project to temp directory
+    echo "  Creating temporary test environment..."
+    cp -r "$PROJECT_ROOT"/* "$TEMP_DIR/" 2>/dev/null || true
+    cp -r "$PROJECT_ROOT"/.git "$TEMP_DIR/" 2>/dev/null || true
+    cd "$TEMP_DIR"
+
+    # Update lean-toolchain file
+    echo "$toolchain" > lean-toolchain
+
+    # Run tests
+    TEST_FAILED=0
+
+    # Step 1: lake update
+    echo "  Running: lake update"
+    set +e  # Temporarily disable exit on error to capture it ourselves
+    lake update > /tmp/lake-update.log 2>&1
+    UPDATE_EXIT=$?
+    set -e
+
+    if [[ $UPDATE_EXIT -ne 0 ]]; then
+        echo -e "${RED}  ✗ lake update failed (exit code: $UPDATE_EXIT)${NC}"
+        echo "  Error output:"
+        tail -20 /tmp/lake-update.log | sed 's/^/    /'
+        TEST_FAILED=1
+    else
+        echo -e "${GREEN}  ✓ lake update succeeded${NC}"
+    fi
+
+    # Step 2: lake build (only if update succeeded)
+    if [[ $TEST_FAILED -eq 0 ]]; then
+        echo "  Running: lake build"
+        set +e
+        lake build > /tmp/lake-build.log 2>&1
+        BUILD_EXIT=$?
+        set -e
+
+        if [[ $BUILD_EXIT -ne 0 ]]; then
+            echo -e "${RED}  ✗ lake build failed (exit code: $BUILD_EXIT)${NC}"
+            echo "  Error output:"
+            tail -20 /tmp/lake-build.log | sed 's/^/    /'
+            TEST_FAILED=1
+        else
+            echo -e "${GREEN}  ✓ lake build succeeded${NC}"
+        fi
+    fi
+
+    # Step 3: lake test (only if build succeeded)
+    if [[ $TEST_FAILED -eq 0 ]]; then
+        echo "  Running: lake test"
+        set +e
+        lake test > /tmp/lake-test.log 2>&1
+        TEST_EXIT=$?
+        set -e
+
+        if [[ $TEST_EXIT -ne 0 ]]; then
+            echo -e "${RED}  ✗ lake test failed (exit code: $TEST_EXIT)${NC}"
+            echo "  Error output:"
+            tail -20 /tmp/lake-test.log | sed 's/^/    /'
+            TEST_FAILED=1
+        else
+            echo -e "${GREEN}  ✓ lake test succeeded${NC}"
+        fi
+    fi
+
+    # Update statistics
+    if [[ $TEST_FAILED -eq 0 ]]; then
+        PASSED_TESTS=$((PASSED_TESTS + 1))
+        echo -e "${GREEN}✓ Toolchain $toolchain: PASSED${NC}"
+    else
+        FAILED_TESTS=$((FAILED_TESTS + 1))
+        FAILED_TOOLCHAINS+=("$toolchain")
+        echo -e "${RED}✗ Toolchain $toolchain: FAILED${NC}"
+    fi
+
+    echo ""
+
+    # Cleanup
+    cleanup
+    trap - EXIT
+
+done < "$TOOLCHAINS_FILE"
+
+# Print summary
+echo ""
+echo "=============================================="
+echo "Test Summary"
+echo "=============================================="
+echo "Total toolchains tested: $TOTAL_TESTS"
+echo -e "${GREEN}Passed: $PASSED_TESTS${NC}"
+echo -e "${RED}Failed: $FAILED_TESTS${NC}"
+
+if [[ $FAILED_TESTS -gt 0 ]]; then
+    echo ""
+    echo "Failed toolchains:"
+    for tc in "${FAILED_TOOLCHAINS[@]}"; do
+        echo -e "  ${RED}✗ $tc${NC}"
+    done
+    exit 1
+else
+    echo ""
+    echo -e "${GREEN}All tests passed!${NC}"
+    exit 0
+fi

LeanUtilsTest/testable_toolchains.txt

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.0-rc1

README.md

@@ -1,2 +1,29 @@
 # LeanUtils
-Lean scripts for indexing sorries and verifying proofs
+Lean scripts for indexing sorries and verifying proofs. 
+
+## Testing
+The repository can be tested in two separate ways. 
+1. On a specific Lean version: by running `lake test`
+2. Across several Lean versions: by running `LeanUtilsTest/run_tests.sh`. The
+   toolchains tested against are stored in `testable_toolchains.txt`. 
+
+## Lean versions
+
+This repository will eventually contain releases tagged with lean version
+strings (e.g. v4.17.0). The user (sorry indexer, proof checker, ...) should 
+use the most recent version tag which is less than or equal to the version tag
+for the Lean repository being indexed/tested/...
+
+### Bumping lean versions
+
+When a new major Lean version is released, add the corresponding toolchain to
+`LeanUtilsTest/testable_toolchain.txt`. If this does not break any unit tests,
+we are good to go. Otherwise fix the test, and create a new
+release with the current version tag (if necessary, the fixed version might be
+backwards compatible with the current range of toolchains).
+
+
+## Current Lean versions covered
+
+Currently, the tests seem to pass on all Lean versions from `v4.9.0` to `v4.25.0-rc1`.
+TODO(Paul-Lez): increase test coverage.

lakefile.toml

@@ -1,14 +1,22 @@
 name = "LeanUtils"
 version = "0.1.0"
-defaultTargets = ["KernelCheck", "ExtractSorry"]
+defaultTargets = ["KernelCheck", "ExtractSorry", "LeanUtils"]
+testDriver = "LeanUtilsTest"
 
 [[lean_lib]]
 name = "LeanUtils"
 
+[[lean_lib]]
+name = "LeanUtilsTest"
+root = "LeanUtilsTest"
+
+[[lean_lib]]
+name = "bins"
+
 [[lean_exe]]
 name = "KernelCheck"
 root = "bins.KernelCheck"
 
 [[lean_exe]]
 name = "ExtractSorry"
-root = "bins.KernelCheck"
+root = "bins.ExtractSorry"