Do we still have plenty of time before the port?

Stream: mathlib4

[Patrick Stevens]

I've got a big PR which I'm very slowly pulling apart and adding to mathlib, and I just wanted to check the mathlib4 port wasn't too imminent; I started this PR well over a year ago and am just doing bits of it in the rare weekends when I get time, so would like to not get caught by surprise with a sudden deadline. (I had a bit of a look round and I couldn't immediately find a progress update on the port or anything.)

[Gabriel Ebner]

I think you've got more than a month and less than a year. We'll announce the end of mathlib in time for people to finish their PRs.

[Fernando Chu]

I hope it's fine to bump old topics, is the timeframe Gabriel mentioned still the same? Or will the port get delayed a bit? Asking because I'm new to Lean and not sure in which style I should be writing

[Mario Carneiro]

the end of this year seems like a more accurate estimate at this point