From 05b08d91bcf9fdfe40c92fd6ce0f3621a95d159b Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Fri, 10 Oct 2025 11:22:15 +0100 Subject: [PATCH 1/4] Make search path backwards compatible --- LeanUtils/Utils.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/LeanUtils/Utils.lean b/LeanUtils/Utils.lean index 07d74bf..3064349 100644 --- a/LeanUtils/Utils.lean +++ b/LeanUtils/Utils.lean @@ -9,8 +9,6 @@ structure SorryData (Out : Type) where parentDecl : Name deriving BEq --- #check ContextInfo - /-- Visit a node in the info tree and apply function `x` if the node is a tactic info or term info. -/ def visitSorryNode {Out} (ctx : ContextInfo) (node : Info) From de81bd40a8b1de417d2178a0c24efddee5f3d27e Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Fri, 10 Oct 2025 15:11:14 +0100 Subject: [PATCH 2/4] Update search path --- LeanUtils/ExtractSorry.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/LeanUtils/ExtractSorry.lean b/LeanUtils/ExtractSorry.lean index e7b2105..45e3b14 100644 --- a/LeanUtils/ExtractSorry.lean +++ b/LeanUtils/ExtractSorry.lean @@ -126,8 +126,6 @@ def main (args : List String) : IO Unit := do IO.println "Running sorry extraction." unsafe enableInitializersExecution let path : System.FilePath := { toString := path } - let path ← IO.FS.realPath path - searchPathRef.set compile_time_search_path% let out := (← parseFile path).map ToJson.toJson IO.eprintln s!"File extraction yielded" IO.eprintln (toJson out) From 5420ffa1330c7ad2f560cd17efdba2846c8c5415 Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 5 Nov 2025 09:10:45 +0000 Subject: [PATCH 3/4] Add infrastructure to test on several Lean versions --- LeanUtilsTest/PROCESS.md | 8 ++ LeanUtilsTest/TestExtractSorry.lean | 2 +- LeanUtilsTest/run_tests.sh | 162 ++++++++++++++++++++++++++ LeanUtilsTest/testable_toolchains.txt | 1 + README.md | 29 ++++- lakefile.toml | 12 +- 6 files changed, 210 insertions(+), 4 deletions(-) create mode 100644 LeanUtilsTest/PROCESS.md create mode 100755 LeanUtilsTest/run_tests.sh create mode 100644 LeanUtilsTest/testable_toolchains.txt diff --git a/LeanUtilsTest/PROCESS.md b/LeanUtilsTest/PROCESS.md new file mode 100644 index 0000000..9f66756 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/LeanUtilsTest/TestExtractSorry.lean b/LeanUtilsTest/TestExtractSorry.lean index 4e0678c..7172e71 100644 --- a/LeanUtilsTest/TestExtractSorry.lean +++ b/LeanUtilsTest/TestExtractSorry.lean @@ -1,4 +1,4 @@ -import LeanUtils.ExtractSorry +import bins.ExtractSorry /-- info: Running sorry extraction. diff --git a/LeanUtilsTest/run_tests.sh b/LeanUtilsTest/run_tests.sh new file mode 100755 index 0000000..d15c0ee --- /dev/null +++ b/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 diff --git a/LeanUtilsTest/testable_toolchains.txt b/LeanUtilsTest/testable_toolchains.txt new file mode 100644 index 0000000..2264e7f --- /dev/null +++ b/LeanUtilsTest/testable_toolchains.txt @@ -0,0 +1 @@ +leanprover/lean4:v4.25.0-rc1 \ No newline at end of file diff --git a/README.md b/README.md index fb20642..3c7f4ee 100644 --- a/README.md +++ b/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. \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index e562581..e230349 100644 --- a/lakefile.toml +++ b/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" \ No newline at end of file +root = "bins.ExtractSorry" From e039eded2077efd820dfe5aaa8585a98fd7b9ec0 Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 5 Nov 2025 09:11:19 +0000 Subject: [PATCH 4/4] Add missing Lean file --- LeanUtilsTest.lean | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 LeanUtilsTest.lean diff --git a/LeanUtilsTest.lean b/LeanUtilsTest.lean new file mode 100644 index 0000000..0d076aa --- /dev/null +++ b/LeanUtilsTest.lean @@ -0,0 +1,2 @@ +import LeanUtilsTest.LeanFileWithSorries +import LeanUtilsTest.TestExtractSorry