Data.Fintype.Quotient !4#2019

Stream: mathlib4

[Jireh Loreaux]

I've spent longer than I'd care to admit trying to fix the issue in this short file, and now I'm giving up. It's HEq hell unfortunately. Marked as help wanted

[Eric Wieser]

This one should be an easy port

[Eric Wieser]

You can just copy the lines from the PR where I deleted them

[Eric Wieser]

But also, we do not want to port this file yet, there is a mathlib3 refactor in progress

[Eric Wieser]

See this message

[Jireh Loreaux]

Shoot, I missed that message before. Thanks.

[Jireh Loreaux]

I'm just going to close it.

[Kyle Miller]

@Jireh Loreaux I've almost finished fixing it. I'll push my changes just for fun then.

[Jireh Loreaux]

well, I guess we should wait for the mathlib3 refactor, but fixing it is okay. You can reopen if you want. I'm not sure what the best decision is.

[Eric Wieser]

You should definitely not spend any effort fixing the broken proofs when there are fully working proofs in the git history for mathlib4

[Eric Wieser]

Is there something we can do to make the comments column on #port-status more visible? This contained a remark to not port the file.

[Jireh Loreaux]

Eric, I think I may have started porting it before the remark was there. I started yesterday afternoon, but didn't immediately create the PR because I thought I would be done in a few minutes, and then I wasn't.

[Johan Commelin]

@Eric Wieser was the mathlib3 refactor motivated by a porting problem?

[Eric Wieser]

No, but the file isn't high up on the dependency chain

[Eric Wieser]

So it seemed safe to freeze it for a bit

[Johan Commelin]

Well, if someone "freezes" a file, they should certainly check whether there is a port going on!

[Johan Commelin]

Refactoring files that are far away from the tide is fine. But this file was "ready to be ported" when the mathlib3 refactor began, and in fact, a port was in progress.

[Kyle Miller]

Incidentally, I've gotten stuck with the second error in the file (my commit)

[Kyle Miller]

It seems that there is some sort of bug in how motives are being computed and it reports an error in a mysterious way, right on the theorem name itself

[Eric Wieser]

This file was created specifically to allow the mathlib3 refactor. It was at no point ready to port

[Johan Commelin]

Then this should have been more clearly communicated.

[Eric Wieser]

I suspect the failure here was not updating #port-comments soon enough

[Eric Wieser]

I now see the comment was added only 3 hours ago, not the 24 hours ago that I posted my previous message

[Johan Commelin]

Eric Wieser said:

No, but the file isn't high up on the dependency chain

I also don't agree with this. Stuff touch list and quot is clearly either touching ported files, or very close to the tide.

[Johan Commelin]

If the refactor was not solving a porting problem, then it should have been postponed.

[Johan Commelin]

The port is hard enough already.

[Eric Wieser]

What I meant was that this file is practically a leaf

[Johan Commelin]

Eric Wieser said:

This file was created specifically to allow the mathlib3 refactor. It was at no point ready to port

But you also said :up:. If it is a leaf, but not ready to port, it shouldn't have been created as part of a very recent mathlib3 refactor.