feat: add cslib package template

src/lake/Lake/CLI/Help.lean

@@ -90,6 +90,7 @@ The initial configuration and starter files are based on the template:
   lib                   library only
   math-lax              library only with a Mathlib dependency
   math                  library with Mathlib standards for linting and workflows
+  cs                    library with CSLib standards and CSLib-specific workflows
 
 Templates can be suffixed with `.lean` or `.toml` to produce a Lean or TOML
 version of the configuration file, respectively. The default is TOML."

src/lake/Lake/CLI/Init.lean

@@ -197,6 +197,42 @@ name = \"mathlib\"
 scope = \"leanprover-community\"
 rev = {repr rev}
 
+[[lean_lib]]
+name = {repr libRoot}
+"
+def cslibLeanConfigFileContents (pkgName libRoot rev : String) :=
+s!"import Lake
+open Lake DSL
+
+package {repr pkgName} where
+  version := v!\"0.1.0\"
+  keywords := #[\"cs\"]
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`weak.linter.mathlibStandardSet, true⟩,
+  ]
+
+require \"leanprover\" / \"cslib\" @ git {repr rev}
+
+@[default_target]
+lean_lib {libRoot} where
+  -- add any library configuration options here
+"
+def cslibTomlConfigFileContents (pkgName libRoot rev : String) :=
+s!"name = {repr pkgName}
+version = \"0.1.0\"
+keywords = [\"cs\"]
+defaultTargets = [{repr libRoot}]
+
+[leanOptions]
+pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+weak.linter.mathlibStandardSet = true
+
+[[require]]
+name = \"cslib\"
+scope = \"leanprover\"
+rev = {repr rev}
+
 [[lean_lib]]
 name = {repr libRoot}
 "
@@ -217,6 +253,21 @@ To set up your new GitHub repository, follow these steps:
 
 After following the steps above, you can remove this section from the README file.
 "
+def csReadmeFileContents (pkgName : String) := s!"# {pkgName}
+
+## GitHub configuration
+
+To set up your new GitHub repository, follow these steps:
+
+* Under your repository name, click **Settings**.
+* In the **Actions** section of the sidebar, click \"General\".
+* Check the box **Allow GitHub Actions to create and approve pull requests**.
+* Click the **Pages** section of the settings sidebar.
+* In the **Source** dropdown menu, select \"GitHub Actions\".
+
+After following the steps above, you can remove this section from the README file.
+"
+
 
 def leanActionWorkflowContents :=
 "name: Lean Action CI
@@ -303,6 +354,83 @@ jobs:
           # END CONFIGURATION BLOCK 2
 "
 
+def cslibBuildActionWorkflowContents :=
+"name: CSLib CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read # Read access to repository contents
+  pages: write # Write access to GitHub Pages
+  id-token: write # Write access to ID tokens
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - name: Build project with CSLib
+        uses: leanprover/lean-action@v1
+      - name: Build and deploy documentation
+        uses: leanprover-community/docgen-action@v1
+"
+
+def cslibUpdateActionWorkflowContents :=
+"name: Update CSLib
+
+on:
+  # schedule:
+  #   - cron: \"0 8 * * *\" # Every day at 08:00 AM UTC
+  workflow_dispatch:
+
+jobs:
+  update-cslib:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+      issues: write
+      pull-requests: write
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v5
+      - name: Update CSLib and its Lean toolchain
+        uses: leanprover-community/lean-update@main
+        with:
+          update_if_modified: lake-manifest.json
+          on_update_succeeds: pr
+          on_update_fails: issue
+"
+
+def cslibCreateReleaseActionWorkflowContents :=
+"name: Create CSLib-compatible Release
+
+on:
+  push:
+    branches:
+      - 'main'
+      - 'master'
+    paths:
+      - 'lean-toolchain'
+
+jobs:
+  cslib-release-tag:
+    name: Add CSLib-compatible Lean release tag
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+    - name: Create release for the new CSLib toolchain
+      uses: leanprover-community/lean-release-tag@v1
+      with:
+        do-release: true
+        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+"
+
 def createReleaseActionWorkflowContents :=
 "name: Create Release
 
@@ -330,7 +458,7 @@ jobs:
 
 /-- Lake package template identifier. -/
 public inductive InitTemplate
-| std | exe | lib | mathLax | math
+| std | exe | lib | mathLax | math | cslib
 deriving Repr, DecidableEq
 
 public instance : Inhabited InitTemplate := ⟨.std⟩
@@ -341,6 +469,7 @@ public def InitTemplate.ofString? : String → Option InitTemplate
 | "lib" => some .lib
 | "math-lax" => some .mathLax
 | "math" => some .math
+| "cs" => some .cslib
 | _ => none
 
 def escapeIdent (id : String) : String :=
@@ -361,6 +490,7 @@ def InitTemplate.configFileContents
 : String :=
   let pkgNameStr := dotlessName pkgName
   let mathRev := leanVer?.elim "master" (s!"v{·.toString}")
+  let cslibRev := leanVer?.elim "main" (s!"v{·.toString}")
   match tmp, lang with
   | .std, .lean => stdLeanConfigFileContents pkgNameStr (escapeName! root) pkgNameStr.toLower
   | .std, .toml => stdTomlConfigFileContents pkgNameStr root.toString pkgNameStr.toLower
@@ -372,6 +502,8 @@ def InitTemplate.configFileContents
   | .mathLax, .toml => mathLaxTomlConfigFileContents pkgNameStr root.toString mathRev
   | .math, .lean => mathLeanConfigFileContents pkgNameStr (escapeName! root) mathRev
   | .math, .toml => mathTomlConfigFileContents pkgNameStr root.toString mathRev
+  | .cslib, .toml => cslibTomlConfigFileContents pkgNameStr root.toString cslibRev
+  | .cslib, .lean => cslibLeanConfigFileContents pkgNameStr (escapeName! root) cslibRev
 
 def createLeanActionWorkflow (dir : FilePath) (tmp : InitTemplate) : LogIO PUnit := do
   logVerbose "creating lean-action CI workflow"
@@ -382,26 +514,35 @@ def createLeanActionWorkflow (dir : FilePath) (tmp : InitTemplate) : LogIO PUnit
   if (← workflowFile.pathExists) then
     logVerbose "lean-action CI workflow already exists"
     return
-  if tmp = .math then
-    IO.FS.writeFile workflowFile mathBuildActionWorkflowContents
-  else
-    IO.FS.writeFile workflowFile leanActionWorkflowContents
+  let contents := match tmp with
+    | .math => mathBuildActionWorkflowContents
+    | .cslib => cslibBuildActionWorkflowContents
+    | _ => leanActionWorkflowContents
+  IO.FS.writeFile workflowFile contents
   logVerbose s!"created lean-action CI workflow at '{workflowFile}'"
 
-  if tmp = .math then
+  if tmp = .math || tmp = .cslib then
     -- A workflow for automatically creating update PRs/issues.
     let workflowFile := workflowDir / "update.yml"
     if (← workflowFile.pathExists) then
-      logVerbose "Mathlib update CI workflow already exists"
+      logVerbose "dependency update CI workflow already exists"
       return
-    IO.FS.writeFile workflowFile mathUpdateActionWorkflowContents
-    logVerbose s!"created Mathlib update CI workflow at '{workflowFile}'"
+    let contents := if tmp = .cslib then
+      cslibUpdateActionWorkflowContents
+    else
+      mathUpdateActionWorkflowContents
+    IO.FS.writeFile workflowFile contents
+    logVerbose s!"created dependency update CI workflow at '{workflowFile}'"
     -- A workflow for tagging commits that bump the Lean toolchain version.
     let workflowFile := workflowDir / "create-release.yml"
     if (← workflowFile.pathExists) then
       logVerbose "create-release CI workflow already exists"
       return
-    IO.FS.writeFile workflowFile createReleaseActionWorkflowContents
+    let contents := if tmp = .cslib then
+      cslibCreateReleaseActionWorkflowContents
+    else
+      createReleaseActionWorkflowContents
+    IO.FS.writeFile workflowFile contents
     logVerbose s!"created create-release CI workflow at '{workflowFile}'"
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
@@ -444,7 +585,7 @@ def initPkg
     unless (← basicFile.pathExists) do
       IO.FS.createDirAll libDir
       IO.FS.writeFile basicFile basicFileContents
-    let rootContents := if tmp = .math then
+    let rootContents := if tmp = .math || tmp = .cslib then
       mathLibRootFileContents root
     else
       libRootFileContents root.toString root
@@ -462,6 +603,8 @@ def initPkg
   unless (← readmeFile.pathExists) do
     let contents := if tmp = .math then
         mathReadmeFileContents <| dotlessName name
+      else if tmp = .cslib then
+        csReadmeFileContents <| dotlessName name
       else
         readmeFileContents <| dotlessName name
     IO.FS.writeFile readmeFile contents
@@ -495,12 +638,16 @@ def initPkg
             no known toolchain name for the current Elan/Lean/Lake"
     else
       IO.FS.writeFile toolchainFile <| env.toolchain ++ "\n"
-  if tmp matches .mathLax | .math then
+  if tmp matches .mathLax | .math | .cslib then
     if leanVer?.isNone then
-      logWarning "creating a new math package with a non-release Lean toolchain; \
-        Mathlib may not work properly"
+      if tmp = .cslib then
+        logWarning "creating a new cs package with a non-release Lean toolchain; \
+          CSLib may not work properly"
+      else
+        logWarning "creating a new math package with a non-release Lean toolchain; \
+          Mathlib may not work properly"
     unless offline do
-      -- Checkout mathlib and pin the version in the manifest
+      -- Checkout the template dependency and pin the version in the manifest
       updateManifest { lakeEnv := env, wsDir := dir, updateToolchain := false }
 
 def validatePkgName (pkgName : String) : LogIO PUnit := do

tests/lake/tests/init/clean.sh

@@ -10,4 +10,6 @@ rm -rf A-B-C-D
 rm -rf meta
 rm -rf qed-lax
 rm -rf qed
+rm -rf cs-lean
+rm -rf cs-toml
 rm -rf mathlib_standards

tests/lake/tests/init/test.sh

@@ -110,6 +110,35 @@ test_math_tmp () {
 test_math_tmp math-lax qed-lax QedLax
 test_math_tmp math qed Qed
 
+# Test cs template
+
+test_cs_tmp () {
+  local lang=$1; local pkg="cs-$lang"
+  local mod
+  if [ "$lang" = lean ]; then mod=CsLean; else mod=CsToml; fi
+  echo "# TEST: cs.$lang template"
+  # Use `--offline` and remove the `require`,
+  # since we do not wish to download CSLib during tests
+  ELAN_TOOLCHAIN="v4.0.0-test" test_run new $pkg cs.$lang --offline
+  test_cmd_out 'v4.0.0' grep -o 'v4.0.0' $pkg/lakefile.$lang
+  test_exp -f $pkg/.github/workflows/lean_action_ci.yml
+  test_exp -f $pkg/.github/workflows/update.yml
+  test_exp -f $pkg/.github/workflows/create-release.yml
+  test_cmd grep -F 'CSLib' $pkg/.github/workflows/lean_action_ci.yml
+  test_cmd grep -F 'cslib' $pkg/.github/workflows/update.yml
+  if [ "$lang" = lean ]; then
+    test_cmd grep -F 'require "leanprover" / "cslib"' $pkg/lakefile.lean
+    sed_i '/^require.*/{N;d;}' $pkg/lakefile.lean
+  else
+    test_cmd_out 'scope = "leanprover"' grep -F 'scope = "leanprover"' $pkg/lakefile.toml
+    sed_i '/^\[\[require\]\]/{N;N;N;d;}' $pkg/lakefile.toml
+  fi
+  test_lib $pkg $mod
+}
+
+test_cs_tmp lean
+test_cs_tmp toml
+
 # Test `init .`
 
 echo "# TEST: init ."