A CSLib project template.

Stream: CSLib

[Shreyas Srinivas]

In yesterday's office hours, I brought up the idea of a CSLib project template. Concretely if a user starts a new project with lake new <ProjectName> cs or lake new <ProjectName> compsci, lake should set up a new project with the correct cslib toolchain as the toplevel dependency. Then it should fetch mathlib's cache (not sure how this should work until lake cache is ready, but maybe an alias lake executable?)

[Shreyas Srinivas]

Following lean contribution guidelines, I have created an RFC issue lean4#12592

[Shreyas Srinivas]

CC : @Kim Morrison

[Shreyas Srinivas]

I don't know if lake exe cache get will work in a project with cslib as the toplevel dependency

[Shreyas Srinivas]

If the RFC gets approval I will submit a PR.

[Chris Henson]

This has been discussed previously at #CSLib > `lake new` template for CSLib?. My reasoning against this remains the same:

Chris Henson said:

My thought is that it is simple enough to add CSLib as a dependency the standard way via the lakefile. I don't think we need to ask core to add any special support.

[Shreyas Srinivas]

I'd argue that this is only true if you have programming skills

[Shreyas Srinivas]

Most people just want the shortest way to create a project that gets them working on an editor

[Shreyas Srinivas]

And trust me, lots of CS folks have phobia of terminals, especially when one gets into the theoretical side.

[Shreyas Srinivas]

Also, one issue is, can we actually get mathlib cache this way:

Shreyas Srinivas said:

I don't know if lake exe cache get will work in a project with cslib as the toplevel dependency

[Chris Henson]

I am not convinced by these arguments. I have trouble imagining that the number of people formalizing computer science but unable to follow the lakefile instructions is very large.

[Chris Henson]

(Cache usage is an issue worth discussing separately.)

[Shreyas Srinivas]

I'd like to introduce you to the algorithms theory community

[Shreyas Srinivas]

But more importantly, I don't see why we can't have the same convenient out-of-the-box setup as math projects

[Shreyas Srinivas]

We should be striving for the best possible UX. Mathlib-downstream projects have this UX. We should get it for CSLib as well.

[Shreyas Srinivas]

Lastly, a CSLib template is a strict (Pareto?) improvement. It doesn’t detract from anything else.

[Ching-Tsun Chou]

I remember seeing the following announcement:
#announce > LeanProject repo template
Perhaps a small tweak would make it work for cslib as well:

[Shreyas Srinivas]

That’s different. That’s a project template on top of lake’s math template. It adds bells and whistles like the blueprint, extra CI stuff, a paper folder,and a github webpage

[Shreyas Srinivas]

And these days it also seems to include the project dashboard of the Equational theories project that I designed and Pietro implemented back in late 2024

[Shreyas Srinivas]

This is about the lake template itself