no-eval-in-source.yml

name: "No #eval in source files"

on: [pull_request, merge_group]

jobs:
    check-no-eval:
        name: "Check no #eval in source files"
        runs-on: ubuntu-latest
        steps:
            - uses: actions/checkout@v7

            - name: Check for #eval in source files
              run: |
                  # Find #eval statements in module source files (excluding tests and test-projects)
                  # Non-module files are allowed to have #eval since their private/scoped definitions
                  # cannot be tested externally, and there's no phase issue with builds.
                  OFFENDING_FILES=()
                  while IFS= read -r -d '' file; do
                    # Check if file contains #eval
                    if grep -qE '^[[:space:]]*#eval([[:space:]]|$)' "$file"; then
                      # Check if file is a module file (has 'module' on its own line)
                      if grep -q '^module$' "$file"; then
                        OFFENDING_FILES+=("$file")
                      fi
                    fi
                  done < <(find ./src -path ./src/tests -prune -o \
                    -path ./src/test-projects -prune -o \
                    -path ./src/errata-tests -prune -o \
                    -name "*.lean" -type f -print0)

                  if [ ${#OFFENDING_FILES[@]} -gt 0 ]; then
                    echo "Found #eval statements in module source files (should be in src/tests/ or src/errata-tests/):"
                    printf '%s\n' "${OFFENDING_FILES[@]}"
                    echo ""
                    echo "Offending lines:"
                    grep -nE '^[[:space:]]*#eval([[:space:]]|$)' "${OFFENDING_FILES[@]}" || true
                    exit 1
                  else
                    echo "No #eval statements found in module source files."
                  fi