From 2a4cb503191bc5fc38fa0554ae217f851ef5e2c7 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 22 May 2026 06:18:59 +0100
Subject: [PATCH] feat: Turn on and modify PR message

---
 .github/workflows/PRMessage.yml    | 32 ++++++++++++++++++
 .github/workflows/PR_checklist.yml | 54 ------------------------------
 2 files changed, 32 insertions(+), 54 deletions(-)
 create mode 100644 .github/workflows/PRMessage.yml
 delete mode 100644 .github/workflows/PR_checklist.yml

diff --git a/.github/workflows/PRMessage.yml b/.github/workflows/PRMessage.yml
new file mode 100644
index 000000000..b54c12a75
--- /dev/null
+++ b/.github/workflows/PRMessage.yml
@@ -0,0 +1,32 @@
+name: PR Comment
+
+on:
+  workflow_dispatch:
+  pull_request_target:
+    types: [opened]
+
+jobs:
+    build:
+        name: Comment a pull_request
+        runs-on: ubuntu-latest
+        permissions:
+            pull-requests: write
+
+        steps:
+            - name: Checkout
+              uses: actions/checkout@v2
+            - name: Comment a pull_request
+              uses: mb2dev/github-action-comment-pull-request@1.0.0
+              with:
+                message:  |
+                  Thank you for this PR, which will now be reviewed. Please 
+                  see our [review guidelines](https://github.com/leanprover-community/physlib/blob/master/docs/ReviewGuidelines.md) 
+                  if you are not familiar with the process. You should expect a back and forth 
+                  with a reviewer before your PR is merged. See also that link for how to 
+                  add appropriate labels to your PR. The PR will also go through a number 
+                  of automated checks. You can learn more about these [here](https://github.com/leanprover-community/physlib/blob/master/scripts/README.md), 
+                  including how to run them locally.
+
+                  If you want to bring attention to this PR, please write a message on this 
+                  [thread](https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/PR.20reviews/with/596447366) of the Lean Zulip.
+                GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.github/workflows/PR_checklist.yml b/.github/workflows/PR_checklist.yml
deleted file mode 100644
index d90b6a1fb..000000000
--- a/.github/workflows/PR_checklist.yml
+++ /dev/null
@@ -1,54 +0,0 @@
-name: PR Comment
-
-on: workflow_dispatch
-  #pull_request_target:
-  #  types:
-  #    - opened
-
-jobs:
-    build:
-        name: Comment a pull_request
-        runs-on: ubuntu-latest
-        permissions:
-            pull-requests: write
-
-        steps:
-            - name: Checkout
-              uses: actions/checkout@v2
-            - name: Comment a pull_request
-              uses: mb2dev/github-action-comment-pull-request@1.0.0
-              with:
-                message:  |
-                    Thank you for your PR! The following checklist can be used to ensure that the PR is as helpful as possible and to help maintain the quality of the project.
-
-                    *This checklist is experimental and can be ignored if you wish.
-                    Feel free to ask if anything is unclear, or make suggestions.*
-
-                    **Documentation**
-
-                    - [ ] I have updated the module doc-strings of any modules modified, or this comment is not relevant.
-                    - [ ] I created a new module doc-string for any new modules created, including an overall description of the module and the main results, or this comment is not relevant.
-                    - [ ] I have changed all doc-string occurances of declaration names which I have changed, or this comment is not relevant.
-                    - [ ] For definitions and key theorems I have added, I have added an english-readable statement of the result, which is as self-contained as possible, and where appropriate contain a readable UTF-8 version of the result.
-                    - [ ] Where appropriate and helpful I have included references to the original source of results in the module doc-string.
-
-                    **Lemmas and theorems**
-
-                    - [ ] I have ensured that the `theorem` key word is reserved for *important* theorems, and `lemma` is used for everything else.
-                    - [ ] I have ensured that no lemmas or definitions are duplications of other results.
-
-                    **Layout**
-
-                    - [ ] I have ensured that results are in the appropriate modules.
-
-                    **Usage of AI**
-
-                    Please tick one that applies to this PR:
-
-                    - [ ] I have not used any AI to generate code.
-                    - [ ] I have used basic AI coding assistance (e.g. Copilot) to generate repeative bits of code, but the lemmas and definitions are my own.
-                    - [ ] I used AI to generate the structure of the code and/or guide its organization, but I have checked it for corectness.
-                    - [ ] Other (please specify with a comment).
-
-
-                GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}