Disable most documentation notifications on GitHub #37740
Conversation
Previously, the documentation comment on GitHub would be removed and then recreated which creates notification emails and to some feels like it's polluting their GitHub inbox. Here, we change this behavior so that only the initial build of the documentation causes such a notification. Further updates to the documentation, do update the links in the comment but do not trigger a notification. This is meant as an alternative to sagemath#37387. See sagemath#37739 for futher ideas about a smarter behavior here.
saraedum
added
s: needs review
disputed
|
@tornaria @kwankyu @mantepse @tobiasdiez feel free to have a look :) |
|
I think this is a reasonable compromise so 👍 Alternatively: is the bot able to edit the description of the PR? Wouldn't it make more sense to put the link at the end of the description (and update it there every time)? This could be a more visible location for the link. Maybe easier: is there an easy URL that will redirect to the latest version of the documentation for a given PR? Maybe this link could be added statically into the PR template? |
|
|
+1, please. Preferably I want to get 0 email notifications from github-actions[bot] for documentations. |
|
Another option is to learn from how Gitpod does it. For example, see this Mathlib issue. They have a button that redirects to Gitpod, then (I think) Gitpod checks the referral header to see which repo & issue it comes from. We can do something similar, have an endpoint that takes the issue number and redirect to the built documentation. |
Is it possible to have a static file in a single fixed URL that will read the PR from the referrer and redirect to the correct link? I assume this is what happens with the With some luck, this can be done in javascript without server side involvement. |
|
Here's a test: https://www.cmat.edu.uy/~tornaria/ref.html Let's try the link to see if javascript can figure out the PR number. EDIT: it seems we only get |
|
Documentation preview for this PR (built with commit 7dcf495; changes) is ready! 🎉 |
|
I tested that this actually works on saraedum#2. (The link there is broken because there is no netlify configured.) But the notification updates correctly and looks correct to me. |
|
I certainly want to wait for a week or so before I tally the votes here. But if you'd like to, I would appreciate a formal review of this PR. |
I get 
|
Browsers (and their privacy extensions) can decide not to send the referer at all or mangle it. From my understanding of how this works, I think this has not much hope to lead to a robust solution. |
|
Of this change Before this change, I can easily see that the doc build workflow is completed since the comment reappears at the bottom of the thread but others get annoyed by the useless notifications in github inbox (assuming they have email filters). After this change, I would be annoyed for the need to look into the Checks list to see that the doc build workflow is completed but others won't receive the useless notifications in github inbox. I vote -1 because I want this PR to get merged only if there are many people to care about the github inbox (I don't). |
|
Before this change, I can easily see that the doc build workflow is completed since the comment reappears at the bottom of the thread but others get annoyed by the useless notifications in github inbox (assuming they have email filters).
Maybe it's possible to move up the "deploy documentation" so it's the first thing visible there ? An advantage of the check box is that it will always be there as the last thing in the PR, while the comment by the bot gets lost if there are other comments after. |
Will it be reasonable to have a giant box just for the user to type the PR number in manually? I mean, if you click that "open PR" button or whatever, it'll open a new tab, so the GitHub PR page is still open, and you can copy the PR number over easily. |
Maybe we can use the referrer url, which will work for most people (e.g. for @kwankyu as shown in #37740 (comment)). But when the referrer url is mangled (for people like me, using privacy plugins) show a box to let me input the PR number. There's possibly some (mild) correlation between people that get annoyed by spam bots and people that use privacy plugins. I wouldn't mind at all that the link in the PR comment doesn't work for me without manual intervention, typing the PR number is nil compared to receiving lots of spam from the bot which hides relevant notifications. |
|
That sounds great! Just to enlarge the sample size, referral doesn't show PR number for me. |
|
+1 here |
|
+1 This is a simple solution that eliminates most of the noise. For what it's worth, I blocked these in my mail system to see how hard it would be. It's not terribly easy, and I'm the mail server administrator. The notifications come from the usual github address, with all of the same headers that accompany any other comment. To dig into the body using server-side filtering, you need the sieve body extension. Then of course you want to test it by filtering the messages into junk for a while before you discard them entirely. All of this takes time, multiplied by the apparently large number of users who hate these notifications. In the future, I would remain open to any of the better solutions that have been proposed but not implemented yet. |
|
Wait, so are we disabling the notifications without a replacement (e.g. the redirection button or whatever)? |
|
Please do counting of votes before status labelling. That's the rule for disputed PRs. |
you'll get one notification, 1st time docs are/attempted to be built. You can revisit the PR if you want to see how it's going. |
I had initially placed him on the -1 side. However, I couldn't find his vote on this PR. He was tagged in the first comment, and also this PR was mentioned in the other PR he was participating in, so I would say he was given reasonable notification. The vote would still be 5 to 2, so it wouldn't make a difference. |
@dimpase Well, how would you know this? As a matter of fact, I do get the email notifications, and they are exactly what I use in my notification-driven workflow. I said this clearly in the original discussion - #37387 (comment) |
|
My vote is -1. I have already explained clearly why in #37387 (comment): "This proposal is not suitable as a compromise -- because it completely ignores the use of this notification as a workflow management tool. #37387 (comment)" |
|
+1, people interested in getting notifications when the doc workflow is finished can subscribe via built-in github functionality (https://docs.github.com/en/actions/monitoring-and-troubleshooting-workflows/notifications-for-workflow-runs) or by quickly hacking together there own notification system using the public and easy-to-use github api (https://docs.github.com/en/rest/actions/workflow-runs?apiVersion=2022-11-28#about-workflow-runs-in-github-actions) |
|
by the way, these notifications appear to be broken, e.g. I got dimpase#6 (comment) |
that's what you suggested in a discussion around #36803 - to disable email notifications (IIRC). This assumes that you eat your own dog food, certainly. |
Most likely you do not have netlify credentials configured. When creating a PR into a fork where these are not configured, the notification gets created but is not functional. While that could be fixed, I don't really think it's relevant at the moment since I don't think anybody is creating PRs into other forks regularly. |
Previously, the documentation comment on GitHub would be removed and then recreated whenever there is a change to a PR which creates notification emails and to some feels like it's polluting their GitHub inbox.
Here, we change this behavior so that only the initial build of the documentation causes such a notification. Further updates to the documentation do update the links in the comment but do not trigger a notification.
This is meant as an alternative to #37387. See #37739 for futher ideas about a smarter behavior here.
An actual preview of the result can be seen here: saraedum#2
Note that the links on that PR do not work because my fork does not have netlify credentials configured.
📝 Checklist