datetime

Stream: batteries

[Johan Commelin]

Is the a lib available for parsing / calculating with datetimes?

[Markus Himmel]

I know nothing about it except that it exists, but: https://github.com/ammkrn/timelib

[Kim Morrison]

A datetime library downstream of mathlib, eek!

[Patrick Massot]

Kim, you should see this as an indication that you are doing an important work when trying to upstream programmy stuff!

[Arthur Paulino]

It depends on Mathlib here: https://github.com/ammkrn/timelib/blob/main/Timelib/Util.lean

[Arthur Paulino]

I found another file that depends on Mathlib.
It raises an interesting question: how can one depend on Mathlib without depending on its entirety? This "lazy dependency" is something I haven't seen anywhere else

[Arthur Paulino]

Actually it's "possible" in Rust if the upstream project is structured with the right hierarchy of sub-crates.
For example, suppose I were able to depend on the Mathlib.Algebra.Order "submodule" and then Lake would download that for me, besides the transitive dependencies of Mathlib.Algebra.Order... and nothing else

[Ruben Van de Velde]

I guess some of Yaël's work might help with that. Also some kind of tree shaking algorithm could be interesting

[Yaël Dillies]

Ruben is right. See #11757, @Arthur Paulino

[Arthur Paulino]

So Lake already supports partial dependencies on a project?
Sorry for derailing the thread btw

[Ruben Van de Velde]

If you split the project, yes :)

[Mario Carneiro]

I would say that it doesn't really support this. You can't really split projects easily either because there are still reservoir-related constraints on having multiple projects in the same repo or a project in a subfolder, and as far as I know there is no way to depend on only one library in a package without depending on the whole package

[Mario Carneiro]

I have been arguing for better support for mathlib-style packages where the expectation is that you aren't depending on most of the files in the package, but currently you get all the sources downloaded no matter what, and lake exe cache get will download all the oleans unless you specifically ask otherwise. If lake was handling cache then it would be able to download the right files every time

[Moritz Firsching]

adding @Chris Bailey to the conversation

[Chris Bailey]

Johan Commelin said:

Is the a lib available for parsing / calculating with datetimes?

There's also this one which currently has more parsing/printing implemented but is more limited in scope. Just a heads up, it's GPL-3.

Arthur Paulino said:

I found another file that depends on Mathlib.
It raises an interesting question: how can one depend on Mathlib without depending on its entirety? This "lazy dependency" is something I haven't seen anywhere else

At least in the case of something like Timelib, authors can split their work into two packages, one has the core functionality (leaving out proofs and fancy typeclass instances) and another has the mathlib dependency and provides all of the proofs and fancier typeclass instances.

If users want a slim dependency that's just to do date arithmetic, they can take the basic dependency. If they want the full thing, they also import TimelibExtras or whatever.

Mathlib still holds a lot of important declarations and is pretty hard to get around in the wild.