test.sh

#!/bin/bash
set -x

# Read lean-toolchain file
LEAN_VERSION=$(sed 's/.*lean4:\([^ ]*\).*/\1/' lean-toolchain 2>/dev/null | sed 's/^v//')

# Function to compare Lean versions
version_leq() {
    if [[ "$1" == "$2" ]]; then
        return 0
    fi
    local IFS=.
    local i ver1=($1) ver2=($2)
    # Remove -rc* suffix if present
    ver1=${ver1[0]//-rc*}
    ver2=${ver2[0]//-rc*}
    # Compare major and minor versions
    if [[ -z $ver1 || -z $ver2 ]]; then
        return 1
    fi
    for ((i=0; i<2; i++)); do
        if [[ -z ${ver1[i]} || -z ${ver2[i]} ]]; then
            return 1
        fi
        if ((10#${ver1[i]} > 10#${ver2[i]})); then
            return 1
        fi
        if ((10#${ver1[i]} < 10#${ver2[i]})); then
            return 0
        fi
    done
    return 0
}

# Determine if we need to adjust paths for Lean ≤ 4.17.0
ADJUST_PATHS=false
if [[ -n "$LEAN_VERSION" ]]; then
    if version_leq "$LEAN_VERSION" "4.17.0"; then
        ADJUST_PATHS=true
    fi
fi

# Build the project
lake build SafeVerifyTest || { echo "Build failed"; exit 1; }

# Base directory
BASE_DIR="SafeVerifyTest"

# Iterate over each test directory
for TEST_DIR in "$BASE_DIR"/*/; do
    TEST_NAME=$(basename "$TEST_DIR")
    # Adjust paths if needed
    if [ "$ADJUST_PATHS" = true ]; then
        TARGET_OLEAN=".lake/build/lib/$BASE_DIR/$TEST_NAME/Target.olean"
        GOOD_OLEAN=".lake/build/lib/$BASE_DIR/$TEST_NAME/Good.olean"
        BAD_OLEAN=".lake/build/lib/$BASE_DIR/$TEST_NAME/Bad.olean"
        HACK_OLEAN=".lake/build/lib/$BASE_DIR/$TEST_NAME/Hack.olean"
    else
        TARGET_OLEAN=".lake/build/lib/lean/$BASE_DIR/$TEST_NAME/Target.olean"
        GOOD_OLEAN=".lake/build/lib/lean/$BASE_DIR/$TEST_NAME/Good.olean"
        BAD_OLEAN=".lake/build/lib/lean/$BASE_DIR/$TEST_NAME/Bad.olean"
        HACK_OLEAN=".lake/build/lib/lean/$BASE_DIR/$TEST_NAME/Hack.olean"
    fi

    STATEMENTS_FILE="$TEST_DIR/statements.txt"
    # Check if statements.txt exists
    if [ ! -f "$STATEMENTS_FILE" ]; then
        statements=""
    else
        statements=$(cat "$STATEMENTS_FILE")
    fi

    FLAGS_FILE="$TEST_DIR/flags.txt"
    if [ ! -f "$FLAGS_FILE" ]; then
        flags=""
    else
        flags=$(cat "$FLAGS_FILE")
    fi

    # Skip directories without a Target.lean (e.g. unit test directories)
    if [ ! -f "$TEST_DIR/Target.lean" ]; then
        echo "Skipping $TEST_NAME (no Target.lean)"
        continue
    fi

    # Check if Target.olean exists
    if [ ! -f "$TARGET_OLEAN" ]; then
        echo "Error: $TARGET_OLEAN not found"
        exit 1
    fi

    # Test Good.lean
    if [ -f "$GOOD_OLEAN" ]; then
        echo "Testing $TEST_NAME/Good.lean..."
        if OUTPUT=$(lake exe safe_verify $flags "$TARGET_OLEAN" "$GOOD_OLEAN" $statements 2>&1); then
            echo "PASS: $TEST_NAME/Good.lean"
        else
            echo "FAIL: $TEST_NAME/Good.lean (expected to pass)"
            echo "Output:"
            echo "$OUTPUT"
            exit 1
        fi
    else
        echo "Warning: $GOOD_OLEAN not found, skipping..."
    fi

    # Test Bad.lean
    if [ -f "$BAD_OLEAN" ]; then
        echo "Testing $TEST_NAME/Bad.lean..."
        if ! OUTPUT=$(lake exe safe_verify $flags "$TARGET_OLEAN" "$BAD_OLEAN" 2>&1); then
            echo "PASS: $TEST_NAME/Bad.lean (expected to fail)"
        else
            # If Bad.lean passes, check if Hack.olean exists and fails
            if [ -f "$HACK_OLEAN" ]; then
                if ! HACK_OUTPUT=$(lake exe safe_verify "$HACK_OLEAN" 2>&1); then
                # Test multiple repo imports (BAD_OLEAN) has to import HACK_OLEAN from ../ search path
                    mkdir -p testtmp
                    cp -R .lake lakefile.lean lean-toolchain lake-manifest.json Main.lean SafeVerify testtmp/
                    cd testtmp
                    LAKE_OUTPUT=$(lake build 2>&1)
                    rm $HACK_OLEAN
                    if OUTPUT=$(lake exe safe_verify "$TARGET_OLEAN" "../$BAD_OLEAN" 2>&1); then
                        cd ..
                        rm -rf testtmp
                        echo "PASS: $TEST_NAME/Bad.lean (hack olean failed)"
                    else
                        cd ..
                        rm -rf testtmp
                        echo "FAIL: $TEST_NAME/Bad.lean (multi-repo test failed)"
                        echo "Output:"
                        echo "$OUTPUT"
                        exit 1
                    fi
                else
                    echo "FAIL: $TEST_NAME/Bad.lean (expected to fail, hack olean passed)"
                    echo "Output:"
                    echo "$OUTPUT"
                    exit 1
                fi
            else
                echo "FAIL: $TEST_NAME/Bad.lean (expected to fail but passed, no hack olean)"
                echo "Output:"
                echo "$OUTPUT"
                exit 1
            fi
        fi
    else
        echo "Warning: $BAD_OLEAN not found, skipping..."
    fi

done

echo "All tests completed successfully!"