os interface and regex

Stream: lean4

[Alexandre Rademaker]

Do we have any primitives for an OS interface? I am especially looking for a function that lists files in a folder, for example. Inspect the filenames etc. I am also curious about regex implementation; anything on that direction?

[Marcus Rossel]

Regex was recently discussed in Requirements for regex library.

[Marcus Rossel]

Regarding operations like listing files in a directory, you might find the things you need by poking around the IO.FS and System namespaces (you're looking for System.FilePath.readDir).

[Alexandre Rademaker]

Thank you @Marcus Rossel for the pointers.

[Ioannis Konstantoulas]

I have been able to go surprisingly far with the matching functions in Std.Data.String.

[Alexandre Rademaker]

good to know @Ioannis Konstantoulas ! Thank you

[Alexandre Rademaker]

Hum, Std is part of the math lib, right? I guess for me, depending on Mathlib can be too much...

[Johan Commelin]

Mathlib depends on Std. But they are separate packages.

[Johan Commelin]

You can depend on Std without depending on Mathlib

[Alexandre Rademaker]

Oh, great @Johan Commelin. Thank you

[Scott Morrison]

In particular, Std is intended to be the standard library for Lean, and our plan is that it is high enough quality (and small enough / fast enough to build) that almost all projects are comfortable depending on it.

[Scott Morrison]

If anyone has concerns in that direction (i.e. are hesitant to depend on it) please let us know sooner rather than later!

[Ioannis Konstantoulas]

Scott Morrison said:

If anyone has concerns in that direction (i.e. are hesitant to depend on it) please let us know sooner rather than later!

I have found Std very satisfactory so far, both in terms of size and code. Of course I would love to see many more features there, but everyone says that :laughing: