Turn this into a failing status

I took the liberty to rename the workflow file and name, so that one
doesn't have to look inside to guess what the workflow is doing.

.github/workflows/pr-title.yml

@@ -0,0 +1,17 @@
+name: Check PR title for commit convention
+
+on:
+  pull_request:
+    types: [opened, edited]
+
+jobs:
+  check-pr-title:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check PR title
+        uses: actions/github-script@v6
+        with:
+          script: |
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(context.payload.pull_request.title)) {
+              core.setFailed('the PR title does not follow the [Commit Convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).'),
+            }

.github/workflows/pr.yml

@@ -1,31 +0,0 @@
-name: sanity-check opened PRs
-
-on:
-  # needs read/write GH token, do *not* execute arbitrary code from PR
-  pull_request_target:
-    types: [opened]
-
-jobs:
-  check-pr:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check Commit Message
-        uses: actions/github-script@v6
-        with:
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            const { data: commits } = await github.rest.pulls.listCommits({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              pull_number: context.issue.number,
-            });
-            console.log(commits[0].commit.message);
-            // check first commit only (and only once) since later commits might be intended to be squashed away
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(commits[0].commit.message)) {
-              await github.rest.issues.createComment({
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                issue_number: context.issue.number,
-                body: 'Thanks for your contribution! Please make sure to follow our [Commit Convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).',
-              });
-            }