RFC: Add CSLib template for lake

[Shreyas4991]

Proposal

Create a cslib project template in lean. Such a template should create a project with CSLib as the toplevel dependency.

Clear and detailed description of the proposal. Consider the following questions:

• User Experience: How does this feature improve the user experience?
  Allows users to create project using CSLib definitions, and maybe use mathlib's cache and the future lake cache.

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?
  Computer Scientists who wish to use the foundational material being built in CSLib. Currently, those who want to build Free Monad DSLs, or use the formalizations of Labelled-Transition-Systems or typed Lambda Calculi

• Maintainability: Will this change streamline code maintenance or simplify its structure?
  Its effect is orthogonal.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

• The idea came up on Office hours Feb 19th 2026, and was approved by @kim-em

• Zulip thread here

Impact

Add 👍 to issues you consider important.