@[reducible, inline]

abbrev Lake.ScriptM (α : Type) : Type

The type of a Script's monad.

It is an IO monad equipped information about the Lake configuration.

Equations

• Lake.ScriptM = Lake.LakeT IO

@[reducible, inline]

abbrev Lake.ScriptFn : Type

The type of a Script's function.

It is similar to the main function's signature, except the monad is also equipped with information about the Lake configuration.

Equations

• Lake.ScriptFn = (List String → Lake.ScriptM Lake.ExitCode)

@[implicit_reducible]

instance Lake.instTypeNameScriptFn : TypeName ScriptFn

Equations

• Lake.instTypeNameScriptFn = Lake.instTypeNameScriptFn.unsafe_impl_2

structure Lake.Script : Type

A package Script is a named ScriptFn definition with a some optional documentation.

It can be run by lake run <name> [-- <args>].

• name : String

  The full name of the Script (e.g., pkg/script).

• fn : ScriptFn
• doc? : Option String

def Lake.instInhabitedScript.default : Script

Equations

• Lake.instInhabitedScript.default = { name := default, fn := default, doc? := default }

@[implicit_reducible]

instance Lake.instInhabitedScript : Inhabited Script

Equations

• Lake.instInhabitedScript = { default := Lake.instInhabitedScript.default }

def Lake.Script.run (args : List String) (self : Script) : ScriptM ExitCode

Run the script with the specified CLI args.

Equations

• Lake.Script.run args self = self.fn args