feat: promote scripts from PackageConifg to top level commands

Lake/Attributes.lean

@@ -4,7 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lean
+
 open Lean
+namespace Lake
 
 initialize packageAttr : TagAttribute ←
   registerTagAttribute `package "Lake package attribute"
+
+initialize scriptAttr : TagAttribute ←
+  registerTagAttribute `script "Lake script attribute"

Lake/DSL.lean

@@ -10,16 +10,21 @@ import Lake.Attributes
 open Lean Parser Command
 namespace Lake.DSL
 
-syntax packageStruct :=
+syntax structVal :=
   "{" manyIndent(group(Term.structInstField optional(", "))) "}"
 
-syntax packageDeclValSpecial :=
-  (packageStruct <|> (ppSpace Term.do)) (Term.whereDecls)?
+syntax declValDo :=
+  ppSpace Term.do (Term.whereDecls)?
+
+syntax declValStruct :=
+  ppSpace structVal (Term.whereDecls)?
+
+-- # Packages
 
 syntax packageDeclWithBinders :=
   (ppSpace "(" Term.simpleBinder ")")? -- dir
   (ppSpace "(" Term.simpleBinder ")")? -- args
-  ppSpace (declValSimple <|> packageDeclValSpecial)
+  (declValSimple <|> declValStruct <|> declValDo)
 
 syntax packageDeclTyped :=
   Term.typeSpec declValSimple
@@ -28,7 +33,7 @@ syntax packageDeclSpec :=
   ident (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders)?
 
 scoped syntax (name := packageDecl)
-(docComment)? "package "  packageDeclSpec : command
+(docComment)? "package " packageDeclSpec : command
 
 def expandPackageBinders
 : (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax)
@@ -64,3 +69,21 @@ def expandPackageDecl : Macro
   `($[$doc?:docComment]? @[«package»] def $id : IOPackager :=
       (fun $dir $args => do $seq) $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed package declaration"
+
+-- # Scripts
+
+syntax scriptDeclSpec :=
+  ident (ppSpace "(" Term.simpleBinder ")")? (declValSimple <|> declValDo)
+
+scoped syntax (name := scriptDecl)
+(docComment)? "script " scriptDeclSpec : command
+
+@[macro scriptDecl]
+def expandScriptDecl : Macro
+| `($[$doc?:docComment]? script $id:ident $[($args?)]? do $seq $[$wds?]?) => do
+  let args := args?.getD (← `(_))
+  `($[$doc?:docComment]? @[«script»] def $id : Script := fun $args => do $seq $[$wds?]?)
+| `($[$doc?:docComment]? script $id:ident $[($args?)]? := $defn $[$wds?]?) => do
+  let args := args?.getD (← `(_))
+  `($[$doc?:docComment]? @[«script»] def $id : Script := fun $args => $defn $[$wds?]?)
+| stx => Macro.throwErrorAt stx "ill-formed script declaration"

Lake/LeanConfig.lean

@@ -33,6 +33,12 @@ unsafe def evalPackageDecl (env : Environment) (declName : Name)
     s!"unexpected type at `{declName}`, " ++
       "`Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected"
 
+/-- Evaluate a `script` declaration to its respective `Script`. -/
+unsafe def evalScriptDecl
+(env : Environment) (declName : Name) (leanOpts := Options.empty) : IO Script :=
+  IO.ofExcept <| Id.run <| ExceptT.run <|
+    env.evalConstCheck Script leanOpts ``Script declName
+
 namespace Package
 
 /-- Unsafe implementation of `load`. -/
@@ -48,7 +54,9 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
         s!"configuration file is missing a `package` declaration"
     | [pkgDeclName] =>
       let config ← evalPackageDecl env pkgDeclName dir args leanOpts
-      return Package.mk dir config
+      let scripts ← scriptAttr.ext.getState env |>.foldM (init := {})
+        fun m d => do m.insert d <| ← evalScriptDecl env d
+      return Package.mk dir config scripts
     | _ =>
       throw <| IO.userError
         s!"configuration file has multiple `package` declarations"

Lake/Package.lean

@@ -11,7 +11,7 @@ import Lake.BuildTarget
 import Lake.Glob
 
 open Std System
-open Lean (Name)
+open Lean (Name NameMap)
 
 namespace Lake
 
@@ -111,14 +111,6 @@ structure PackageConfig where
   -/
   name : Name
 
-  /--
-    A `HashMap` of scripts for the package.
-
-    A `Script` is an arbitrary `(args : List String) → IO UInt32` function that
-    is indexed by a `String` key and can be be run by `lake run <key> [-- <args>]`.
-  -/
-  scripts : HashMap String Script := HashMap.empty
-
   /-
     An `Array` of the package's dependencies.
     See the documentation of `Dependency` for more information.
@@ -263,6 +255,13 @@ structure Package where
   dir : FilePath
   /-- The package's configuration. -/
   config : PackageConfig
+  /--
+    A `NameMap` of scripts for the package.
+
+    A `Script` is a `(args : List String) → IO UInt32` definition with
+    a `@[script]` tag that can be run by `lake run <script> [-- <args>]`.
+  -/
+  scripts : NameMap Script := {}
   deriving Inhabited
 
 /--
@@ -283,10 +282,6 @@ namespace Package
 def name (self : Package) : Name :=
   self.config.name
 
-/-- The package's `scripts` configuration. -/
-def scripts (self : Package) : HashMap String Script :=
-  self.config.scripts
-
 /-- The package's `dependencies` configuration. -/
 def dependencies (self : Package) : Array Dependency :=
   self.config.dependencies

README.md

@@ -87,7 +87,6 @@ Lake provides a large assortment of configuration options for packages.
 ### General
 
 * `name` **(Required)**: The `Name` of the package.
-* `scripts`: A `HashMap` of scripts for the package. A `Script` is an arbitrary `(args : List String) → IO UInt32` function that is indexed by a `String` key and can be be run by `lake run <key> [-- <args>]`.
 * `dependencies`: An `Array` of the package's dependencies.
 * `depsDir`: The directory to which Lake should download dependencies. Defaults to `lean_packages`.
 * `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package.
@@ -109,3 +108,29 @@ Lake provides a large assortment of configuration options for packages.
 * `binRoot`: The root module of the package's binary executable. Defaults to `Main`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper.
 * `moreLibTargets`: Additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables).
 * `linkArgs`: Additional arguments to pass to `leanc` while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`.
+
+## Scripts
+
+A configuration file can also contain a number of `scripts` declaration. A script is an arbitrary `(args : List String) → IO UInt32` definition that can be run by `lake run <script> [-- <args>]`. For example, given the following `lakefile.lean`:
+
+```lean
+import Lake
+open Lake DSL
+
+package scripts
+
+script greet (args) do
+  if h : 0 < args.length then
+    IO.println s!"Hello, {args.get 0 h}!"
+  else
+    IO.println "Hello, world!"
+  pure 0
+```
+
+The script `greet` can be run like so:
+```
+$ lake run greet
+Hello, world!
+$ lake run greet -- me
+Hello, me!
+```

examples/Makefile

@@ -3,7 +3,7 @@ LAKE ?= ../build/bin/lake
 all: check-lake test time-bootstrap check-bootstrap test-bootstrapped
 
 test: test-init test-hello test-io test-deps\
-	test-git test-ffi test-ffi-dep
+	test-git test-ffi test-ffi-dep test-scripts
 
 clean: clean-init clean-hello clean-io clean-deps\
 	clean-git clean-ffi clean-ffi-dep clean-bootstrap
@@ -53,6 +53,9 @@ test-ffi-dep:
 clean-ffi-dep:
 	cd ffi-dep && ./clean.sh
 
+test-scripts:
+	cd scripts && ./test.sh
+
 test-bootstrap:
 	cd bootstrap && ./test.sh
 

examples/scripts/lakefile.lean

@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+package scripts
+
+script greet (args) do
+  if h : 0 < args.length then
+    IO.println s!"Hello, {args.get 0 h}!"
+  else
+    IO.println "Hello, world!"
+  pure 0

examples/scripts/test.sh

@@ -0,0 +1,3 @@
+set -ex
+${LAKE:-../../build/bin/lake} run greet
+${LAKE:-../../build/bin/lake} run greet -- me