split set_type_context: strict + update #362
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: PR Validation | |
| on: | |
| pull_request: | |
| branches: [ main ] | |
| types: | |
| - opened | |
| - edited | |
| - reopened | |
| - synchronize | |
| jobs: | |
| validate: | |
| name: Validate PR | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| with: | |
| # Checkout the merge commit that GitHub creates for PRs | |
| ref: ${{ github.sha }} | |
| # Fetch enough history to examine merge commit parents and find merge-base | |
| fetch-depth: 200 | |
| - name: Checkout PR head | |
| run: | | |
| # NB: this deserves an explanation. Caveat: this is just what dbentley | |
| # understands, and maybe I'm missing something. | |
| # We want to check changes: | |
| # from: merge-base(latest commit in PR, origin/main) | |
| # to: latest commit in PR | |
| # We could use github.event.pull_request.head.sha as ref to get head | |
| # But because of the way actions/checkout does fetching, | |
| # we won't have main, so there's no way to merge-base. | |
| # Instead, we use github.sha, which is a merge commit that merges: | |
| # * latest commit in PR | |
| # * latest commit in main | |
| # Which gives us what we need but requires a bit of work: | |
| # * find that commit's two parents | |
| # * find the merge-base of those two parents | |
| # * checkout the second parent (the latest commit in PR) | |
| # GitHub's merge commit has two parents: base branch (^1) and PR head (^2) | |
| base_sha=$(git rev-parse ${{ github.sha }}^1) | |
| head_sha=$(git rev-parse ${{ github.sha }}^2) | |
| merge_base=$(git merge-base "$base_sha" "$head_sha") | |
| echo "VILLINT_COMMIT=$merge_base" >> $GITHUB_ENV | |
| # Checkout PR head so villint diffs against the actual PR changes | |
| git checkout "$head_sha" | |
| - name: Validate PR title | |
| env: | |
| PR_TITLE: ${{ github.event.pull_request.title }} | |
| run: ./scripts/validate-pr-title.sh "$PR_TITLE" | |
| - name: Install clang-format | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y clang-format | |
| - name: Run villint linter | |
| run: | | |
| ./scripts/villint.sh --commit "$VILLINT_COMMIT" | |
| if ! git diff --quiet; then | |
| echo "" | |
| echo "ERROR: villint.sh found issues that need to be fixed" | |
| echo "" | |
| echo "Run './scripts/villint.sh' locally to fix these issues, then commit the changes." | |
| echo "" | |
| echo "To ignore specific files, add 'villint-ignore: path/to/file' to your commit message." | |
| echo "Multiple files can be comma-separated or in separate villint-ignore lines." | |
| echo "" | |
| echo "Changes needed:" | |
| git diff | |
| exit 1 | |
| fi | |
| echo "All linting checks passed" |