relevant `master` changes notifier

Stream: general

[Arthur Paulino]

Do you guys think it would be useful to have a post-merge script that posts notifications on open PRs about changes (lines removal only) on master that involve the files the PR is changing or the files that those files import? Example:

Commit <commit hash hyperlink> removed line(s) on the file(s) that are related to this PR.

[Eric Wieser]

What situation do you have in mind where that's useful?

[Eric Wieser]

Often the presence of a merge conflict is enough information

[Arthur Paulino]

Just being notified about times I'd really need to manage a master merge into my branch because some API changed

[Arthur Paulino]

Because some changes that don't cause conflicts can also make my branch break silently, especially if they happen on a file that my file imports

[Yaël Dillies]

I can list you the recent changes that broke stuff.

[Yaël Dillies]

The biggest is nat lemmas and more generally has_ordered_sub lemmas that got their sub renamed to tsub (for truncated subtraction). There are some more and the best way to be aware of them is to watch the queue, but that's definitely some attention drain.

[Yaël Dillies]

But your suggestion doesn't fix that anyway. A best solution would be a "What broke" stream where people create topics for what they broke/renamed when they PR and what suddenly got broked in their branch when they merge master.

[Yaël Dillies]

But also you can solve most problems yourself by knowing where to look.

[Eric Wieser]

Note that bors already protects against silently broken branches

[Eric Wieser]

If it's broken once merged into master, bors will reject it

[Kevin Buzzard]

Just to put this into some context Arthur, you have leapt into Lean in this amazing way, trying to resurrect a stale branch by creating some other branch in some area where other people are working at the same time, are running into all kinds of problems, are gritting your teeth and solving them in this incredibly tenacious way, at a time where the rate of merged PRs is for some reason extremely high. Many of the maintainers and other people writing "competing" code right now are very active on Zulip and if at the end of it you come out unscathed it will be a tribute to both your tenacity and that of the community for helping you through. I have seen many people start on Lean and honestly I don't think any of them started with a project which was so technically complex in terms of the sheer number of issues which you are faced with, and are solving. I would just keep asking questions because in almost every case if you say "look at this branch, this line used to work and now it didn't" you might well get a quick answer from Yael or Kyle or one of the other experts of the form "oh yeah, this happened, fix it like this"

[Kevin Buzzard]

I was initially frustrated with the branch you were working on because it had errors unrelated to what you were doing and I was too lazy to think about how to fix them, but now these are fixed, questions of the form "this line on this branch no longer works after I merged master, help!" will probably be answered effectively -- you have got the community's attention.

[Yaël Dillies]

Also I want to note that this branch is very much not stale but rather "thought about without actively modifying it" :stuck_out_tongue:
You just happen to arrive when I don't have time to sink in that branch, and that's great that you're making it work!

[Kevin Buzzard]

Welcome aboard Arthur. It is not usually a baptism of fire like this!

[Eric Wieser]

(I'm out of the loop; which branch is Arthur trying to revive?)

[Yaël Dillies]

walks_and_trees, the branch where Kyle compiled all the graph theory stuff people wrote in branches when I asked about what was the state of paths and such.

[Yaël Dillies]

#8737

[Kevin Buzzard]

It's back on track now, initially it was a branch that changed multiple files and wasn't even compiling

[Yaël Dillies]

Btw, I will soon need connectivity and hamiltonian cycles.

[Yaël Dillies]

Would be great to see them land in mathlib.

[Arthur Paulino]

I see. Thanks for the clarifications! Yeah it's been a thrilling experience learning Lean while trying to solve already existing issues. I like to learn stuff with a very hands on approach. This time around I was a bit unlucky that I wasn't aware the branch was not working properly. But I appreciate all the support and patience from the community. :pray:

[Kyle Miller]

It's somewhat frustrating to keep hearing how my branch was broken and had compiler errors -- it would be nice if whomever decides to merge master into someone else's branch would make sure they didn't break anything. I had a PR in the meantime renaming simple_graph.sym to simple_graph.symm (and similarly for subgraphs), which affects most simple graph branches pre Sep 10.

[Yaël Dillies]

Uh, I temporarily broke it, but then fixed it until sorryland. And I killed all remaining broken stuff when remerging for Arthur.

[Kyle Miller]

(22 days is certainly temporary :wink: thanks for getting it all up to date)