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 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"