feat: lake: Reservoir-related configuration for packages

debug.log

@@ -0,0 +1 @@
+[0829/202002.254:ERROR:crashpad_client_win.cc(868)] not connected

src/lake/Lake/CLI/Help.lean

@@ -18,6 +18,7 @@ COMMANDS:
   init <name> <temp>    create a Lean package in the current directory
   build <targets>...    build targets
   exe <exe> <args>...   build an exe and run it in Lake's environment
+  check-build           check if any default build targets are configured
   test                  test the package using the configured test driver
   check-test            check if there is a properly configured test driver
   lint                  lint the package using the configured lint driver
@@ -126,6 +127,19 @@ TARGET EXAMPLES:        build the ...
 A bare `lake build` command will build the default facet of the root package.
 Package dependencies are not updated during a build."
 
+def helpCheckBuild :=
+"Check if any default build targets are configured
+
+USAGE:
+  lake check-build
+
+Exits with code 0 if the workspace's root package has any
+default targets configured. Errors (with code 1) otherwise.
+
+Does NOT verify that the configured default targets are valid.
+It merely verifies that some are specified.
+"
+
 def helpUpdate :=
 "Update dependencies and save them to the manifest
 
@@ -375,6 +389,7 @@ def help : (cmd : String) → String
 | "new"                 => helpNew
 | "init"                => helpInit
 | "build"               => helpBuild
+| "check-build"         => helpCheckBuild
 | "update" | "upgrade"  => helpUpdate
 | "pack"                => helpPack
 | "unpack"              => helpUnpack

src/lake/Lake/CLI/Init.lean

@@ -52,7 +52,7 @@ s!"import Lake
 open Lake DSL
 
 package {repr pkgName} where
-  -- add package configuration options here
+  version := v!\"0.1.0\"
 
 lean_lib {libRoot} where
   -- add library configuration options here
@@ -64,6 +64,7 @@ lean_exe {repr exeName} where
 
 def stdTomlConfigFileContents (pkgName libRoot exeName : String) :=
 s!"name = {repr pkgName}
+version = \"0.1.0\"
 defaultTargets = [{repr exeName}]
 
 [[lean_lib]]
@@ -79,7 +80,7 @@ s!"import Lake
 open Lake DSL
 
 package {repr pkgName} where
-  -- add package configuration options here
+  version := v!\"0.1.0\"
 
 @[default_target]
 lean_exe {repr exeName} where
@@ -88,6 +89,7 @@ lean_exe {repr exeName} where
 
 def exeTomlConfigFileContents (pkgName exeName : String) :=
 s!"name = {repr pkgName}
+version = \"0.1.0\"
 defaultTargets = [{repr exeName}]
 
 [[lean_exe]]
@@ -100,7 +102,7 @@ s!"import Lake
 open Lake DSL
 
 package {repr pkgName} where
-  -- add package configuration options here
+  version := v!\"0.1.0\"
 
 @[default_target]
 lean_lib {libRoot} where
@@ -109,6 +111,7 @@ lean_lib {libRoot} where
 
 def libTomlConfigFileContents (pkgName libRoot : String) :=
 s!"name = {repr pkgName}
+version = \"0.1.0\"
 defaultTargets = [{repr libRoot}]
 
 [[lean_lib]]
@@ -120,11 +123,11 @@ s!"import Lake
 open Lake DSL
 
 package {repr pkgName} where
-  -- Settings applied to both builds and interactive editing
+  version := v!\"0.1.0\"
+  keywords := #[\"math\"]
   leanOptions := #[
     ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
   ]
-  -- add any additional package configuration options here
 
 require \"leanprover-community\" / \"mathlib\"
 
@@ -135,6 +138,8 @@ lean_lib {libRoot} where
 
 def mathTomlConfigFileContents (pkgName libRoot : String) :=
 s!"name = {repr pkgName}
+version = \"0.1.0\"
+keywords = [\"math\"]
 defaultTargets = [{repr libRoot}]
 
 [leanOptions]

src/lake/Lake/CLI/Main.lean

@@ -316,6 +316,11 @@ protected def build : CliM PUnit := do
   if showProgress then
     IO.println "Build completed successfully."
 
+protected def checkBuild : CliM PUnit := do
+  processOptions lakeOption
+  let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
+  noArgsRem do exit <| if pkg.defaultTargets.isEmpty then 1 else 0
+
 protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
@@ -478,6 +483,66 @@ protected def translateConfig : CliM PUnit := do
   if outFile?.isNone then
     IO.FS.rename pkg.configFile (pkg.configFile.addExtension "bak")
 
+def ReservoirConfig.currentSchemaVersion : StdVer := v!"1.0.0"
+
+structure ReservoirConfig where
+  name : String
+  version : StdVer
+  versionTags : List String
+  description : String
+  keywords : Array String
+  homepage : String
+  platformIndependent : Option Bool
+  license : String
+  licenseFiles : Array FilePath
+  readmeFile : Option FilePath
+  doIndex : Bool
+  schemaVersion := ReservoirConfig.currentSchemaVersion
+  deriving Lean.ToJson
+
+protected def reservoirConfig : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let cfg ← mkLoadConfig opts
+  let _ ← id do
+    let some verStr ← takeArg?
+      | return ReservoirConfig.currentSchemaVersion
+    match StdVer.parse verStr with
+    | .ok ver => return ver
+    | .error e => error s!"invalid target version: {e}"
+  noArgsRem do
+  let pkg ← loadPackage cfg
+  let repoTags ← GitRepo.getTags pkg.dir
+  let licenseFiles ← pkg.licenseFiles.filterMapM fun relPath => do
+    return if (← (pkg.dir / relPath).pathExists) then some relPath else none
+  let readmeFile :=
+    if (← pkg.readmeFile.pathExists) then some pkg.relReadmeFile else none
+  let cfg : ReservoirConfig := {
+    name := pkg.name.toString
+    version := pkg.version
+    versionTags := repoTags.filter pkg.versionTags.matches
+    description := pkg.description
+    homepage := pkg.homepage
+    keywords := pkg.keywords
+    platformIndependent := pkg.platformIndependent
+    license := pkg.license
+    licenseFiles := licenseFiles
+    readmeFile := readmeFile
+    doIndex := pkg.reservoir
+  }
+  IO.println (toJson cfg).pretty
+
+protected def versionTags : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let cfg ← mkLoadConfig opts
+  noArgsRem do
+  let pkg ← loadPackage cfg
+  let tags ← GitRepo.getTags pkg.dir
+  for tag in tags do
+    if pkg.versionTags.matches tag then
+      IO.println tag
+
 protected def selfCheck : CliM PUnit := do
   processOptions lakeOption
   noArgsRem do verifyInstall (← getThe LakeOptions)
@@ -491,6 +556,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "new"                 => lake.new
 | "init"                => lake.init
 | "build"               => lake.build
+| "check-build"         => lake.checkBuild
 | "update" | "upgrade"  => lake.update
 | "resolve-deps"        => lake.resolveDeps
 | "pack"                => lake.pack
@@ -510,6 +576,8 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "exe" | "exec"        => lake.exe
 | "lean"                => lake.lean
 | "translate-config"    => lake.translateConfig
+| "reservoir-config"    => lake.reservoirConfig
+| "version-tags"        => lake.versionTags
 | "self-check"          => lake.selfCheck
 | "help"                => lake.help
 | cmd                   => throw <| CliError.unknownCommand cmd

src/lake/Lake/CLI/Translate/Lean.lean

@@ -20,6 +20,9 @@ open DSL System Lean Syntax Parser Module
 private local instance : Quote FilePath where
   quote path := quote path.toString
 
+private local instance [Quote α] : Quote (Array α) where
+  quote xs := let xs : Array Term := xs.map quote; Unhygienic.run `(#[$xs,*])
+
 private local instance : BEq FilePath where
   beq a b := a.normalize == b.normalize
 
@@ -67,6 +70,13 @@ def quoteLeanOption (opt : LeanOption) : Term := Unhygienic.run do
 
 private local instance : Quote LeanOption := ⟨quoteLeanOption⟩
 
+protected def LeanVer.quote (v : LeanVer) : Term := Unhygienic.run do
+  let lit := Syntax.mkLit interpolatedStrLitKind  v.toString.quote
+  let stx := mkNode interpolatedStrKind #[lit]
+  `(v!$stx)
+
+private local instance : Quote LeanVer := ⟨LeanVer.quote⟩
+
 /-! ## Configuration Encoders -/
 
 def WorkspaceConfig.addDeclFields (cfg : WorkspaceConfig) (fs : Array DeclField) : Array DeclField :=
@@ -91,7 +101,8 @@ def LeanConfig.addDeclFields (cfg : LeanConfig) (fs : Array DeclField) : Array D
 
 def PackageConfig.mkSyntax (cfg : PackageConfig)
   (testDriver := cfg.testDriver) (lintDriver := cfg.lintDriver)
-  : PackageDecl := Unhygienic.run do
+: PackageDecl := Unhygienic.run do
+  have : Quote Term := ⟨id⟩
   let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `precompileModules cfg.precompileModules false
     |> addDeclFieldD `moreGlobalServerArgs cfg.moreGlobalServerArgs #[]
@@ -108,9 +119,26 @@ def PackageConfig.mkSyntax (cfg : PackageConfig)
     |> addDeclFieldD `testDriverArgs cfg.testDriverArgs #[]
     |> addDeclFieldD `lintDriver lintDriver ""
     |> addDeclFieldD `lintDriverArgs cfg.lintDriverArgs #[]
+    |> addDeclFieldD `version cfg.version v!"0.0.0"
+    |> addDeclField? `versionTags (quoteVerTags? cfg.versionTags)
+    |> addDeclFieldD `description cfg.description ""
+    |> addDeclFieldD `keywords cfg.keywords #[]
+    |> addDeclFieldD `homepage cfg.homepage ""
+    |> addDeclFieldD `license cfg.license ""
+    |> addDeclFieldD `licenseFiles cfg.licenseFiles #["LICENSE"]
+    |> addDeclFieldD `readmeFile cfg.readmeFile "README.md"
+    |> addDeclFieldD `reservoir cfg.reservoir true
     |> cfg.toWorkspaceConfig.addDeclFields
     |> cfg.toLeanConfig.addDeclFields
   `(packageDecl|package $(mkIdent cfg.name):ident $[$declVal?]?)
+  where
+    quoteVerTags? (pat : StrPat) : Option Term :=
+      match pat with
+      | .mem xs => if xs.isEmpty then Unhygienic.run `(∅) else some (quote xs)
+      | .startsWith pre => Unhygienic.run `(.$(mkIdent `startsWith) $(quote pre))
+      | .satisfies _ n =>
+        if n.isAnonymous || n == `default then none else
+        Unhygienic.run `(.$(mkIdent n))
 
 private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
   | Name.anonymous => if acc.isEmpty then none else some acc

src/lake/Lake/CLI/Translate/Toml.lean

@@ -61,6 +61,7 @@ def LeanConfig.toToml (cfg : LeanConfig) (t : Table := {}) : Table :=
   |>.smartInsert `weakLinkArgs cfg.weakLinkArgs
 
 instance : ToToml LeanConfig := ⟨(toToml ·.toToml)⟩
+instance : ToToml LeanVer := ⟨(toToml <| toString ·)⟩
 
 protected def PackageConfig.toToml (cfg : PackageConfig) (t : Table := {}) : Table :=
   t.insert `name cfg.name
@@ -75,8 +76,25 @@ protected def PackageConfig.toToml (cfg : PackageConfig) (t : Table := {}) : Tab
   |>.smartInsert `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
   |>.insertD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
   |>.insertD `preferReleaseBuild cfg.preferReleaseBuild false
+  |>.insertD `version cfg.version v!"0.0.0"
+  |> smartInsertVerTags cfg.versionTags
+  |>.smartInsert `keywords cfg.description
+  |>.smartInsert `keywords cfg.keywords
+  |>.smartInsert `homepage cfg.homepage
+  |>.smartInsert `license cfg.license
+  |>.insertD `licenseFiles cfg.licenseFiles #["LICENSE"]
+  |>.insertD `readmeFile cfg.readmeFile "README.md"
+  |>.insertD `reservoir cfg.reservoir true
   |> cfg.toWorkspaceConfig.toToml
   |> cfg.toLeanConfig.toToml
+where
+  smartInsertVerTags (pat : StrPat) (t : Table) : Table :=
+    match pat with
+    | .mem s => t.insert `versionTags (toToml s)
+    | .startsWith p => t.insert `versionTags.startsWith (toToml p)
+    | .satisfies _ n =>
+      if n.isAnonymous || n == `default then t else
+      t.insert `versionTags.preset (toToml n)
 
 instance : ToToml PackageConfig := ⟨(toToml ·.toToml)⟩