String.Split and Acronym

Programming Lean
1

Hi, are these the maintainers for Lean4 language track?

I am doing this exercise: Acronym in Lean on Exercism.

In this case String.split returns List String, but the latest version of Lean returns Std.Iter String.Slice.

https://leanprover-community.github.io/mathlib4_docs/Init/Data/String/Search.html#String.split

Pedagogically this means that the user will be sidestepping the performance concerns that induced the Std.Iter framework for strings. For example, the following steps are interchangeable in creating the same result:

  1. mapping toUpper over the entire string
  2. splitting on whitespace and taking the first char

but 2 followed by 1 has different performance concerns from 1 followed by 2.

Thanks!

2

The track maintainers should be watching the track category. I moved your post to a new thread in the correct category.

3

Sounds like the start of an interesting article for that exercise if you and the maintainers are interested.

4

Hi! Right now Exercism is using Lean 4.25.2, which was launched at Nov 25, 2025, less than 4 months ago.

New releases are provided roughly each month, you can check them here: lean4/RELEASES.md at master · leanprover/lean4 · GitHub

There has been some important changes lately involving String and some of them have no backwards compatibility. For example, the track’s version uses String.ValidPos, which has since been deprecated in favor of String.Pos.

We will eventually update the track’s version, but it’s unlikely that we will be able to always use the latest version because we need to make sure nothing breaks in the process.

5

@daikonradish

We’ve just bumped the Lean version used by the track to 4.29.0, the current stable release.

I’ll try to keep the track updated to the latest stable version every 6 months or so.

Enjoy!

1 Like