def
Lake.exe
(name : Lean.Name)
(args : Array String := #[])
(buildConfig : Lake.BuildConfig :=
{ oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal,
failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr,
ansiMode := Lake.AnsiMode.auto })
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- pkg.unpack file = do Lake.logInfo (toString "unpacking " ++ toString file ++ toString "") Lake.untar file pkg.buildDir
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.Package.test
(pkg : Lake.Package)
(args : List String := [])
(buildConfig : Lake.BuildConfig :=
{ oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal,
failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr,
ansiMode := Lake.AnsiMode.auto })
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.Package.lint
(pkg : Lake.Package)
(args : List String := [])
(buildConfig : Lake.BuildConfig :=
{ oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal,
failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr,
ansiMode := Lake.AnsiMode.auto })
:
Equations
- One or more equations did not get rendered due to their size.