!4#3106

Stream: mathlib4

[Newell Jensen]

I am hitting several errors (first one happens on line 36 after changing this line to use the Lean 4 #align name - Finset.mem_bunionᵢ):

failed to synthesize instance
  DecidableEq G

This indicates that the error is due to an overloaded operation that has not been implemented, and it describes the type class that must be implemented. However, this seems odd from my understanding as this instance implementation should already be present as it is relating to code that has already been ported to mathlib4? Am I thinking about this correctly? Any suggestions?

[Reid Barton]

I see classical is used in line 32, and the mathlib 3 version is similar.
I think mathlib 3's classical had a bug where classical in one tactic block could affect later tactic blocks as well. (Does anyone know if it is still the case?)
Maybe try adding a line classical between lines 35 and 36?

[Newell Jensen]

That fixed it, thanks!

[Newell Jensen]

@Eric Wieser was curious if you could take a quick look at the top error for what is currently pushed to !4#3106 as I think you wrote this earlier this year so you would most likely know what to do? Any other suggestions I am all ears as I continue learn. Thanks.

[Eric Wieser]

as I think you wrote this earlier this year

I think it was less than a week ago!

[Eric Wieser]

Looking at the PR, I think the difficulty is that ∃ m' ∈ s, p m' means ∃ m' (m' ∈ s), p m in Lean 3, and ∃ m', m' ∈ s \and p m' in Lean 4.
Perhaps someone else can advise on whether you're expected to rewrite the proofs, or just use the explicit spelling ∃ m' (_ : m' ∈ s), p m which means the same as the Lean 3 code

[Eric Wieser]

Either way, I fixed the build

[Eric Wieser]

It would be good to understand the porting notes before merging; this file is super-low priority, so we may as well use it to work out what's going on

[Yaël Dillies]

Why has bUnion turned into bunionᵢ, btw? The set incentive doesn't apply here.

[Eric Wieser]

docs4#Finset.bunionᵢ

[Newell Jensen]

I think this might be the error that I already fixed, I am on line 53 now refine' Ideal.span_le.2 _

[Eric Wieser]

Eric Wieser said:

Either way, I fixed the build

Note I pushed these fixes

[Eric Wieser]

That refine' error is weird

[Eric Wieser]

It seems to be confused by the implicit binders

[Newell Jensen]

Eric Wieser said:

It would be good to understand the porting notes before merging; this file is super-low priority, so we may as well use it to work out what's going on

Sounds good

[Newell Jensen]

So now that the rest of the errors are gone and it builds, does it get merged or because of the porting notes will this branch be held back till a later date?

[Eric Wieser]

Personally I think we should wait for someone to work out what's going on with the porting notes, since the file is really low priority

[Newell Jensen]

Speaking of priority, I know that the porting wiki says just pick one of the unported files to work on but if there really is some files that would help along the entire porting endeavor, what would be the best way to pick those out while looking for a file to work on?

[Eric Wieser]

#port-dashboard lists them by number of downstream files

[Eric Wieser]

So the one with the most dependents is the one that's going to free up the most things once its ported

[Eric Wieser]

Otherwise, pick a file you find interesting that's unported (or use one of the targets in #mathlib4 > port progress and look at the graph to work out which files it needs