feat: add new and run commands

Lake/Cli.lean

@@ -10,6 +10,7 @@ import Lake.Help
 import Lake.LeanConfig
 
 namespace Lake
+
 def getCwdPkg (args : List String) : IO Package := do
   let pkg ← Package.fromDir "." args
   if pkg.leanVersion ≠ leanVersionString then
@@ -17,8 +18,16 @@ def getCwdPkg (args : List String) : IO Package := do
       leanVersionString ++ ", but package requires " ++ pkg.leanVersion ++ "\n"
   return pkg
 
+def Package.run (script : String) (args : List String) (self : Package) : IO PUnit :=
+  if let some script := self.scripts.find? script then
+    script args
+  else
+    self.scripts.forM fun name _ => IO.println name
+
 def cli : (cmd : String) → (lakeArgs pkgArgs : List String) → IO Unit
+| "new",          [name],   []      => new name
 | "init",         [name],   []      => init name
+| "run",          [script], args    => do (← getCwdPkg []).run script args
 | "configure",    [],       pkgArgs => do configure (← getCwdPkg pkgArgs)
 | "print-paths",  imports,  pkgArgs => do printPaths (← getCwdPkg pkgArgs) imports
 | "build",        [],       pkgArgs => do build (← getCwdPkg pkgArgs)

Lake/Help.lean

@@ -13,7 +13,9 @@ def usage :=
 Usage:
   lake <command>
 
+new <name>       create a Lean package in a new directory
 init <name>      create a Lean package in the current directory
+run <script>     run arbitrary package scripts
 configure        download and build dependencies
 build            configure and build *.olean files
 build-lib        configure and build a static library
@@ -21,51 +23,83 @@ build-bin        configure and build a native binary executable
 
 See `lake help <command>` for more information on a specific command."
 
+def helpNew :=
+"Create a Lean package in a new directory
+
+Usage:
+  lake new <name>
+
+This command creates a new Lean package with the given name in
+a new directory with the same name."
+
+def helpInit :=
+"Create a Lean package in the current directory
+
+Usage:
+  lake init <name>
+
+This command creates a new Lean package with the given name in
+the current directory."
+
+def helpRun :=
+"Run arbitrary package scripts
+
+Usage:
+  lake run <script> [-- <args>...]
+
+This command runs the given script from the package configuration's
+`scripts` field, passing `args` to it. If the given script does not exist,
+it will list the available scripts."
+
 def helpConfigure :=
 "Download and build dependencies
 
 Usage:
-  lake configure
+  lake configure [-- <args>...]
 
-This command sets up the `build/deps` directory.
+This command sets up the directory with the package's dependencies
+(i.e., by default, `lean_packages`). Passes `args` to the `Packager`
+if specified.
 
 For each (transitive) git dependency, the specified commit is checked out
-into a sub-directory of `build/deps`. If there are dependencies on multiple
-versions of the same package, the version materialized is undefined. No copy
-is made of local dependencies."
+into a sub-directory of `depsDir`. If there are dependencies on multiple
+versions of the same package, the version materialized is undefined.
+No copy is made of local dependencies."
 
 def helpBuild :=
 "Configure this package and build *.olean files
 
 Usage:
-  lake build
+  lake build [-- <args>...]
 
 This command configures the package's dependencies and then builds the package
 with `lean`. Additional arguments can be passed to `lean` by setting the
-`leanArgs` field in the package's configuration."
+`leanArgs` field in the package's configuration. Arguments to the `Packager`
+itself can be specified with `args`."
 
 def helpBuildLib :=
 "Configure this package and build a static library
 
 Usage:
-  lake build-lib
+  lake build-lib [-- <args>...]
 
-This command configures this package's dependencies, builds the package itself,
+This command configures this package's dependencies, builds the package,
 compiles the extracted C code with `leanc`, and uses `ar` to produce a static
-library in  `build/lib`.
+library.
 
 Additional arguments can be passed to `lean` or `leanc` by setting the
-`leanArgs` or `leancArgs` fields in the package's configuration."
+`leanArgs` or `leancArgs` fields in the package's configuration. Arguments
+to the `Packager` itself can be specified with `args`."
 
 def helpBuildBin :=
 "Configure the package and build a native binary executable
 
 Usage:
-  lake build-bin
+  lake build-bin [-- <args>...]
 
-This command configures this package's dependencies, builds the package itself,
-compiles the extracted C code `leannc`, and then links the object files with
-`leanc` to produce a native binary executable in `build/bin`.
+This command configures this package's dependencies, builds the package,
+compiles the extracted C code `leanc`, and then links the results together
+with `leanc` to produce a native binary executable.
 
 This requires a declaration of name `main` in the root namespace, which must
 return `IO Unit` or `IO UInt32` (the exit code) and may accept the program's
@@ -73,19 +107,13 @@ command line arguments as a `List String` parameter.
 
 Additional  arguments can be passed to `lean`, the  `leanc` compiler, or the
 `leanc` linker by setting the `leanArgs`, `leancArgs`, or `linkArgs` fields in
-the package's configuration."
-
-def helpInit :=
-"Create a new Lean package in the current directory
-
-Usage:
-  lake init <name>
-
-This command creates a new Lean package with the given name in the current
-directory."
+the package's configuration. Arguments to the  `Packager` itself can be
+specified with `args`."
 
 def help : (cmd : String) → String
+| "new"       => helpNew
 | "init"      => helpInit
+| "run"       => helpRun
 | "configure" => helpConfigure
 | "build"     => helpBuild
 | "build-lib" => helpBuildLib

Lake/Init.lean

@@ -27,16 +27,24 @@ def package : Lake.PackageConfig := \{
 }
 "
 
-open Git in
-def init (pkgName : String) : IO Unit := do
-  IO.FS.writeFile leanPkgFile (leanPkgFileContents pkgName)
-  IO.FS.writeFile ⟨s!"{pkgName.capitalize}.lean"⟩ mainFileContents
-  let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false)
+open Git System
+
+def initPkg (dir : FilePath) (pkgName : String) : IO PUnit := do
+  IO.FS.writeFile (dir / leanPkgFile) (leanPkgFileContents pkgName)
+  IO.FS.writeFile (dir / s!"{pkgName.capitalize}.lean") mainFileContents
+  let h ← IO.FS.Handle.mk (dir / ".gitignore") IO.FS.Mode.append (bin := false)
   h.putStr initGitignoreContents
-  unless ← System.FilePath.isDir ⟨".git"⟩ do
-    (do
+  unless ← FilePath.isDir (dir /".git") do
+    try
       quietInit
       unless upstreamBranch = "master" do
         checkoutBranch upstreamBranch
-    ) <|>
+    catch _ =>
       IO.eprintln "WARNING: failed to initialize git repository"
+
+def init (pkgName : String) : IO PUnit :=
+  initPkg "." pkgName
+
+def new (pkgName : String) : IO PUnit := do
+  IO.FS.createDir pkgName
+  initPkg pkgName pkgName

Lake/Package.lean

@@ -5,10 +5,11 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lean.Data.Name
 import Lean.Elab.Import
+import Std.Data.HashMap
 import Lake.LeanVersion
 import Lake.BuildTarget
 
-open Lean System
+open Lean Std System
 
 namespace Lake
 
@@ -29,6 +30,8 @@ structure Dependency where
   src  : Source
   args : List String := []
 
+abbrev Script := List String → IO PUnit
+
 structure PackageConfig where
   name : String
   version : String
@@ -47,6 +50,7 @@ structure PackageConfig where
   depsDir : FilePath := defaultDepsDir
   dependencies : List Dependency := []
   moreDepsTarget : BuildTarget LeanTrace PUnit := BuildTarget.nil
+  scripts : HashMap String Script := HashMap.empty
   deriving Inhabited
 
 structure Package where
@@ -67,6 +71,9 @@ def version (self : Package) : String :=
 def leanVersion (self : Package) : String :=
   self.config.leanVersion
 
+def scripts (self : Package) : HashMap String Script :=
+  self.config.scripts
+
 def moduleRoot (self : Package) : Name :=
   self.config.moduleRoot