No #eval in source files #746
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 \ | |
| -name "*.lean" -type f -print0) | |
| if [ ${#OFFENDING_FILES[@]} -gt 0 ]; then | |
| echo "Found #eval statements in module source files (should be in src/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 |