Zulip Chat Archive

Stream: Lean Together 2021

Topic: porting mathlib to Lean 4


view this post on Zulip Rob Lewis (Jan 05 2021 at 09:30):

On yesterday's schedule we had a time slot to discuss porting mathlib to Lean 4. We very happily yielded this time to Leo and Sebastian's Lean 4 presentation -- to discuss porting, we need as much information as we can get about the target of the port!

view this post on Zulip Rob Lewis (Jan 05 2021 at 09:31):

Our social time immediately crashed Wonder, so we reconvened on Zoom, and there was an impromptu porting discussion there.

view this post on Zulip Rob Lewis (Jan 05 2021 at 09:32):

This wasn't a guided discussion and certainly no plans or decisions were made, so don't feel that you missed out on anything juicy if you weren't there :)

view this post on Zulip Rob Lewis (Jan 05 2021 at 09:33):

We won't have time to reschedule a porting discussion during this workshop, but we'll come back to the idea after people have had some time to play around with the brand new Lean 4 release. Stay tuned.


Last updated: May 08 2021 at 22:13 UTC