Thank you for nice package management!

Stream: lean4

[Geoffrey Irving]

I wanted to say thank you to the Lean devs responsible for the nice package management story. When fiddling around with the Mandelbrot set these days I've split the related code into 5 different repos, and it's quite pleasant to keep them synced, update some but not others if there are temporary incompatibilities, moving code around and re-sync in stages if that's easiest. I originally split interval out of ray when someone asked if they could use it standalone, then later I split out the interval-using parts of ray into a ray-render repo so that I can sync the mathematical parts without syncing the computational parts, and now there are two more (series and bottcher), and jumping around between all of these remains very pleasant.

Screenshot 2025-11-12 at 11.17.24 PM.png

[Kim Morrison]

Just pinging @Mac Malone. :heart:

[Max Nowak 🐉]

Lean tooling is absolutely amazing and very modern in general. :)

[metakuntyyy]

Yeah, also big thanks from me. I remember I had issues with updating mathlib and I had to recreate a repository everytime I wanted to use a new version. Now I can just update it.