Zulip Chat Archive
Stream: mathlib4
Topic: Data.Fin.Tuple.Basic mathlib4#1516
Johan Commelin (Jan 16 2023 at 08:07):
#10346 is on the merge queue
Johan Commelin (Jan 17 2023 at 11:44):
This porting PR is rapidly becoming a roadblock for all progress towards order.filter.basic.
See https://tqft.net/mathlib4/latest/order.filter.basic.pdf
Ruben Van de Velde (Jan 17 2023 at 11:49):
Since mathlib3port isn't updating, can we do a oneshot translation of the latest mathlib3 code?
Johan Commelin (Jan 17 2023 at 11:49):
I've never gotten it to work
Ruben Van de Velde (Jan 17 2023 at 11:55):
Alternatively we can just finish the current PR and deal with the mathlib3 changes later - there's only 6 changed files anyway
Johan Commelin (Jan 17 2023 at 11:58):
I would be inclined to do that
Johan Commelin (Jan 17 2023 at 13:03):
The file now compiles
Johan Commelin (Jan 17 2023 at 13:14):
And CI is happy
Eric Wieser (Jan 17 2023 at 13:32):
I think mathlib3port not updating is going to become a bigger roadblock than this PR in the near future
Johan Commelin (Jan 17 2023 at 13:33):
I agree
Johan Commelin (Jan 17 2023 at 13:33):
Unfortunately mathlib3port and mathport have an extremely low bus factor.
Ruben Van de Velde (Jan 17 2023 at 13:35):
Looks like probably most of category theory is blocked on slice_lhs support, if we're talking blockers
Ruben Van de Velde (Jan 18 2023 at 09:21):
Submitted https://github.com/leanprover-community/mathlib4/pull/1637 to port the mathlib3 changes
Johan Commelin (Jan 18 2023 at 09:24):
@Ruben Van de Velde Did you use the mathport output of this morning?
Ruben Van de Velde (Jan 18 2023 at 09:28):
Yes
Johan Commelin (Jan 18 2023 at 09:33):
Great! (Wasn't clear from the commit history.)
Johan Commelin (Jan 18 2023 at 09:33):
Oh noes! Now we have repeat again
Johan Commelin (Jan 18 2023 at 09:34):
@Ruben Van de Velde Would you mind turning it into replicate?
Eric Wieser (Jan 18 2023 at 09:36):
I just left a comment on the PR
Eric Wieser (Jan 18 2023 at 09:36):
This repeat means something different to what list.repeat meant
Yaël Dillies (Jan 18 2023 at 09:36):
It's not the same repeat!
Johan Commelin (Jan 18 2023 at 09:37):
Then we need another name
Johan Commelin (Jan 18 2023 at 09:37):
repeat is a keyword in Lean 4
Yaël Dillies (Jan 18 2023 at 09:38):
Is that a problem? We already have docs4#Nat.repeat
Mario Carneiro (Jan 18 2023 at 09:38):
it's annoying to work with declarations which have keywords as names
Eric Wieser (Jan 18 2023 at 09:38):
This is the PR that links the definition with list.replicate
Eric Wieser said:
feat(data/list/of_fn): two lemmas about tuple concatenation #18192
Mario Carneiro (Jan 18 2023 at 09:39):
it's not impossible to refer to them but it does seem like a bad idea
Eric Wieser (Jan 18 2023 at 09:44):
Another way out of this would be to get rid of fin.repeat and define the more general fin.join, with repeat n a = join (λ i : fin n, a)
Johan Commelin (Jan 18 2023 at 10:15):
Ok, so shall we just merge this PR with repeat as name?
Johan Commelin (Jan 18 2023 at 10:15):
If it is too annoying, we can always rename it
Notification Bot (Jan 18 2023 at 11:04):
2 messages were moved from this topic to #mathlib4 > @[simp] on equation compiler definitions by Eric Wieser.
Chris Hughes (Jan 19 2023 at 09:10):
The port of data.fin.vec_notation is being made more difficult by the fact that mathlib#10346 has not been forward ported to mathlib4 yet.
Johan Commelin (Jan 19 2023 at 09:10):
It is, I think
Johan Commelin (Jan 19 2023 at 09:10):
But maybe not yet merged
Johan Commelin (Jan 19 2023 at 09:10):
https://github.com/leanprover-community/mathlib4/pull/1637
Last updated: Dec 20 2023 at 11:08 UTC