Data.Finsupp.Defs mathlib4#1807

Stream: mathlib4

[Johan Commelin]

This file is terribly borken. It's using a rather technical mix of classical and decidable stuff. :fear:

[Eric Wieser]

Proposal: throw out all the classical stuff in the Lean 3 version of this file first ;)

[Johan Commelin]

Proposal: come up with a realistic strategy to make sure that the port is done before Christmas ;)

[Eric Wieser]

I have a half done branch already that tries the above...

[Johan Commelin]

@Eric Wieser What is the age of that branch?

[Eric Wieser]

A few days

[Johan Commelin]

And it half fixes that one file, or half fixes all of mathlib 3?

[Eric Wieser]

Well I can really comment if it fixes anything that's causing trouble in lean 4

[Eric Wieser]

Half-"fixes" mathlib 3 for some optimistic meaning of half

[Eric Wieser]

I think probably applying @Kyle Miller's classical hack to mathlib 3 would make things more amenable to porting

[Johan Commelin]

Which hack is that?

[Eric Wieser]

A vm_override of the tactic executor that prevents classical leaking

[Johan Commelin]

Is there a PR?

[Eric Wieser]

No, but there is a zulip thread with working code

[Johan Commelin]

Link?

[Eric Wieser]

Mobile makes it hard to get links I'm afraid

[Johan Commelin]

Aha: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60classical.60.20attribute.20leakage

[Johan Commelin]

Thanks for the ping

[Eric Wieser]

Johan Commelin said:

And it half fixes that one file, or half fixes all of mathlib 3?

#18274 is the PR, it currently applies to just data/finsupp/* (the optimistic half)

[Eric Wieser]

I don't think that PR is worth continuing with in it's current form

[Eric Wieser]

Eric Wieser said:

I think probably applying Kyle Miller's classical hack to mathlib 3 would make things more amenable to porting

But this change should be in mathport soon

[Johan Commelin]

Will that change the output of mathport by a lot?

[Johan Commelin]

Should we trigger a new mathport run?

[Eric Wieser]

What time of day does mathport run against mathlib3?

[Johan Commelin]

0 mod 12, I think

[Ruben Van de Velde]

Of whose day? :)

[Johan Commelin]

But I don't know which timezone. Probably UTC?

[Eric Wieser]

Johan Commelin said:

Will that change the output of mathport by a lot?

23 changes in that file, all of them the word classical and line wrapping

[Eric Wieser]

So could probably get away without it for that file

[Johan Commelin]

Eric Wieser said:

I don't think that PR is worth continuing with in it's current form

Do you have other reasons for :this: besides those classicals?

[Eric Wieser]

To be clear, that refers to a different PR

[Johan Commelin]

Then I don't understand this thread anymore :see_no_evil:

[Eric Wieser]

#18277 is the one in master adding 23 classicals that isn't quite in mathport

[Eric Wieser]

#18274 is the one that I think is junk

[Johan Commelin]

Ok, so I can manually add those 23 classicals now.

[Eric Wieser]

#18277 is definitely worth waiting for in downstream files, but the gains in finsupp/defs are marginal

[Eric Wieser]

It also has some fixes I need to forward-port

[Johan Commelin]

This PR is starting to converge

[Johan Commelin]

File is error-free

[Johan Commelin]

Fix most automatic stuff

[Johan Commelin]

Need to go to seminar now.

[Johan Commelin]

Fixed lints

[Johan Commelin]

CI is happy