Markus Himmel & Sofia Rodrigues - What's New In Lean

Stream: Lean Together 2026

[Ruchira S. Datta]

This talk about Std took place yesterday. I don't find that there was a topic made here for discussion.

I had live-tooted the talk on Mathstodon: https://mathstodon.xyz/@RuchiraSDatta/115933800499643137

[Ruchira S. Datta]

Pasting some of my toots.

Markus Himmel

Std.Iter allows efficient chained loops

Polymorphic ranges

Slices: combine a container and a range

Strings redefined to be byte arrays that are valid UTF-8

Improved the String API that uses C:

• use String.Slice to avoid intermediate copies
• polymorphic linear-time string search
• efficient positional operations

New tool Grove: interactive living design document including tests and tables

Check Markus Himmel's presentation on Proof Network Workshop for more

Sofia Rodrigues

Sofia Rodrigues presents on time manipulattion, concurrency, and https on top of Async

Date and time library:

Minutes, hours, etc are offsets and ordinals

Timestamp: single point of time

Duration: span of time (e.g., difference of timestamps)

Calendar time represented as PlainTime, PlainDate, PlainDateTime, and ZonedDateTime

Have parsing and formatting to interconvert with strings

Concurrency is built on libuv, an event library that allows receiving events and callbacks

Supports TCP, UDO, DNS, signals, timers, and process/system information

Selectors can efficiently wait for many asynchronous events at once

Uses the Async monad

The Async monad has high-level combinators like concurrently, race, and Selectable

Can cancel operations cooperatively using CancellationContext

Works with rich communication tools

Http server, based on Hyper, is built on Async using the same concurrency tools

Supports http/1.1

E.g., server blocks until shutdown

Handler receives a request and returns a respons

Not yet merged, PR #10478

There is an open PR for the http client; will be merged after the server

The http server is currently documented inside the module

Std has both tutorials and a reference manual, though both are a bit behind

[Joseph Tooby-Smith]

@Markus Himmel I'm sorry if this has been asked before: Is Grove currently something that is only internal to the FRO? Or is it something that (in practice) anyone can explore/use?

[Markus Himmel]

It's a similar situation to where Verso was 1.5 years or so ago: theoretically, everything is there for anyone to use it, but at the moment we're not investing anything into documentation or supporting external users before we have hardened the tool enough ourselves.

[Markus Himmel]

I hope that sometime this year we will be able to officially release it together with a nice tour of everything it can do and instructions on how to set up and use it.

[Joseph Tooby-Smith]

Great - many thanks! Looking forward to it.

[Michael Rothgang]

Me too. I believe I told you in person already (in Orsay, last September) - but for certain well-chosen corners of mathlib, I believe this can be quite useful.