From 5b51ddd2a6b9a4fa8b1ff0892705f75e9577fc0f Mon Sep 17 00:00:00 2001 From: Shreyas Date: Tue, 24 Feb 2026 19:56:11 +0100 Subject: [PATCH 1/4] Add cslib package template --- src/lake/Lake/CLI/Init.lean | 40 ++++++++++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 2af0cfd3a005..abc4021ee6a8 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -197,13 +197,51 @@ 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} " def readmeFileContents (pkgName : String) := s!"# {pkgName}" -def mathReadmeFileContents (pkgName : String) := s!"# {pkgName} +def mathReadmeFileContents (pkgName : String) := s!"# {pkgName}" + +def csReadmeFileContents (pkgName : String) := s!"# {pkgName}" ## GitHub configuration From 72c82c7541183c98a176e2768569335a6284d70e Mon Sep 17 00:00:00 2001 From: Shreyas Date: Tue, 24 Feb 2026 20:09:21 +0100 Subject: [PATCH 2/4] fix silly mistake --- src/lake/Lake/CLI/Init.lean | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index abc4021ee6a8..fb8c27b5b98a 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -230,7 +230,7 @@ weak.linter.mathlibStandardSet = true [[require]] name = \"cslib\" -scope = \"leanprover\" +scope = \"leanprover-community\" rev = {repr rev} [[lean_lib]] @@ -239,9 +239,21 @@ name = {repr libRoot} def readmeFileContents (pkgName : String) := s!"# {pkgName}" -def mathReadmeFileContents (pkgName : String) := s!"# {pkgName}" +def mathReadmeFileContents (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\". -def csReadmeFileContents (pkgName : String) := s!"# {pkgName}" +After following the steps above, you can remove this section from the README file. +" +def csReadmeFileContents (pkgName : String) := s!"# {pkgName} ## GitHub configuration @@ -256,6 +268,7 @@ 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 leanActionWorkflowContents := "name: Lean Action CI From 9fe5f27f6e522028cb2bb8dd47c24e807f332776 Mon Sep 17 00:00:00 2001 From: Shreyas Srinivas Date: Tue, 1 Sep 2026 15:30:55 +0200 Subject: [PATCH 3/4] More changes --- src/lake/Lake/CLI/Init.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index f2f4c0a4852f..9638eee9dba3 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -381,7 +381,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⟩ @@ -392,6 +392,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 := @@ -412,6 +413,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 @@ -423,6 +425,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 => cslibTomlConfigFileContents pkgNameStr (escapeName! root) cslibRev def createLeanActionWorkflow (dir : FilePath) (tmp : InitTemplate) : LogIO PUnit := do logVerbose "creating lean-action CI workflow" From d1511325989f911c253bed811d044623b5dd1a7c Mon Sep 17 00:00:00 2001 From: Shreyas Srinivas Date: Tue, 1 Sep 2026 15:41:39 +0200 Subject: [PATCH 4/4] changes complete. test CI --- src/lake/Lake/CLI/Help.lean | 1 + src/lake/Lake/CLI/Init.lean | 124 ++++++++++++++++++++++++++++----- tests/lake/tests/init/clean.sh | 2 + tests/lake/tests/init/test.sh | 29 ++++++++ 4 files changed, 140 insertions(+), 16 deletions(-) diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 6d1b2f7f9253..b951c2e633a3 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/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." diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 9638eee9dba3..5ba4ef5cd493 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -230,7 +230,7 @@ weak.linter.mathlibStandardSet = true [[require]] name = \"cslib\" -scope = \"leanprover-community\" +scope = \"leanprover\" rev = {repr rev} [[lean_lib]] @@ -354,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 @@ -426,7 +503,7 @@ def InitTemplate.configFileContents | .math, .lean => mathLeanConfigFileContents pkgNameStr (escapeName! root) mathRev | .math, .toml => mathTomlConfigFileContents pkgNameStr root.toString mathRev | .cslib, .toml => cslibTomlConfigFileContents pkgNameStr root.toString cslibRev - | .cslib, .lean => cslibTomlConfigFileContents pkgNameStr (escapeName! root) cslibRev + | .cslib, .lean => cslibLeanConfigFileContents pkgNameStr (escapeName! root) cslibRev def createLeanActionWorkflow (dir : FilePath) (tmp : InitTemplate) : LogIO PUnit := do logVerbose "creating lean-action CI workflow" @@ -437,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. -/ @@ -499,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 @@ -517,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 @@ -550,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 diff --git a/tests/lake/tests/init/clean.sh b/tests/lake/tests/init/clean.sh index 600dc0a6fbc0..c5d286a12592 100755 --- a/tests/lake/tests/init/clean.sh +++ b/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 diff --git a/tests/lake/tests/init/test.sh b/tests/lake/tests/init/test.sh index bcbebb59b813..30113494e169 100755 --- a/tests/lake/tests/init/test.sh +++ b/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 ."