Conflict in Mathlib.lean

Stream: mathlib4

[Johan Commelin]

Problem: bors occasionally fails because multiple files in a batch add lines to Mathlib.lean and the staging branch doesn't merge them in alphabetical order (or there is simply a conflict).

Proposal:

• Configure CI to check that all files are imported, but don't require the lines in Mathlib.lean to be sorted
• Add a .gitattributes file to the root of the repo with

Mathlib.lean merge=union

• Occasionally sort Mathlib.lean. This could be done by a bot.

[Arthur Paulino]

Related: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60leanproject.20build.60.20equivalent/near/329456004

[Arthur Paulino]

However, dropping Mathlib.lean will require a fix on cache

[Floris van Doorn]

Note: Johan is not suggesting to drop Mathlib.lean

[Eric Wieser]

I think there's a way to define a custom merge handler that does union then sort? https://stackoverflow.com/a/13000959/102441

[Arthur Paulino]

Floris van Doorn said:

Note: Johan is not suggesting to drop Mathlib.lean

I understand, but dropping it sounds like a similar effort that will avoid future maintenance issues altogether (including this one)

[Gabriel Ebner]

In any case we need a file that imports everything because we need to check that there are no two definitions with the same name. And the linter also needs to import all of mathlib4.

[Sebastian Ullrich]

Though if those checks are the only use cases, the file could be generated on demand or the metaprograms adjusted correspondingly. The crucial question is whether import Mathlib should be supported - if it is considered an antipattern, then avoiding the file would be preferable.

[Eric Wieser]

Is it possible to write a metaprogram that intercepts import Mathlib and imports every file in the directory tree? That is, is there a hook along the lines of Python's sys.meta_path, or a function along the lines of Python's __import__?

[James Gallicchio]

if the language server supported auto-import-finding along the lines of what other language servers have, then import Mathlib definitely becomes an anti-pattern :P

[James Gallicchio]

but that seems like way more work than we are willing to put into this right now...

[Eric Wieser]

Auto-import wouldn't really work for things like instances, simp lemmas, or tactic extensions

[Arthur Paulino]

Here's an idea to maintain Mathlib.lean without a bot: you can call the creation/sorting command with a Git pre-commit hook. You would barely notice it doing it's job.

[Eric Wieser]

That would only help if bors runs the commit hook during a rebase

[Eric Wieser]

Although based on this README, using a custom merge driver has a similar problem

[Arthur Paulino]

My comment was in the spirit of "Occasionally sort Mathlib.lean. This could be done by a bot.", but removing the bot part. The contributors themselves would sort it without even noticing

[Jireh Loreaux]

(deleted)

[Chris Hughes]

Is there an easy fix to these merge conflicts we keep getting in Mathlib.lean? I guess it just requires someone who knows the CI setup to add find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean somewhere.

[Chris Hughes]

I see that maybe this is not that simple after trying to figure out how to do it

[Chris Hughes]

The only fix I can think of is to get rid of it from the github repository, add it to .gitignore and have lake exe cache get make it.

[Pol'tta / Miyahara Kō]

@Chris Hughes My ported files seems easy to make many conflicts in Mathlib.lean.
For now, please consider delegating me to merge reviewed files, and I merge branches gradually not to make merge conflicts.

[Chris Hughes]

Done this with all the measure theory PRs except AEMeasurableOrder which is currently on the staging branch

[Arthur Paulino]

(deleted because my memory wasn't accurate)

[Eric Wieser]

We can write a custom merge driver to automatically merge this the right way, as mentioned last time this came up

[Notification Bot]

17 messages were moved here from #mathlib4 > check all files imported by Eric Wieser.

[Eric Wieser]

(I just merged the threads)

[Chris Hughes]

Another question is, if there is a merge conflict in bors, can I see what it was so I can take something off the queue. It's not easy to figure out which of the current PRs conflict with each other

[Eric Wieser]

There's no point taking it off the queue, is there? Bors does that for you when it reaches the top

[Chris Hughes]

Yeah, but it doesn't identify which one causes the failure, so it just keeps splitting stuff in half and you end up with really small batches.

[Eric Wieser]

My understanding is that when that happens it means that every PR works fine on its own, but two in the batch conflict with each other

[Chris Hughes]

Yes, I want to figure what those two are so I can take one of them off the queue.

[Eric Wieser]

I suspect the bors algorithm is just "cherry-pick one at a time until you get a merge conflict, then split the batch at that point"

[Eric Wieser]

So it doesn't even know which two conflicted, it just knows that the first one to be cut from the batch conflicts with one in it

[Eric Wieser]

But maybe it's doing the stupider "throw the whole batch away and bisect"

[Chris Hughes]

It's doing the stupider thing