diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean index bb90519f06..9de4e609ac 100644 --- a/Lake/LeanConfig.lean +++ b/Lake/LeanConfig.lean @@ -29,7 +29,8 @@ unsafe def fromLeanFileUnsafe env.evalConstCheck PackageConfig Options.empty ``PackageConfig `package match configE with | Except.ok config => Package.mk root config - | Except.error error => throw <| IO.userError error + | Except.error error => throw <| IO.userError <| + s!"unexpected type at 'package', `Lake.Packager` or `Lake.PackageConfig` expected" else throw <| IO.userError <| s!"package configuration (at {path}) has errors" diff --git a/examples/io/.gitignore b/examples/io/.gitignore new file mode 100644 index 0000000000..796b96d1c4 --- /dev/null +++ b/examples/io/.gitignore @@ -0,0 +1 @@ +/build diff --git a/examples/io/Io.lean b/examples/io/Io.lean new file mode 100644 index 0000000000..00ac27245d --- /dev/null +++ b/examples/io/Io.lean @@ -0,0 +1,2 @@ +def main : IO Unit := + IO.println "Hello from Io!" diff --git a/examples/io/clean.sh b/examples/io/clean.sh new file mode 100644 index 0000000000..07cbd15340 --- /dev/null +++ b/examples/io/clean.sh @@ -0,0 +1 @@ +rm -r build diff --git a/examples/io/package.lean b/examples/io/package.lean new file mode 100644 index 0000000000..58ef709beb --- /dev/null +++ b/examples/io/package.lean @@ -0,0 +1,8 @@ +import Lake.Package + +def package : Lake.Packager := fun path args => do + IO.println s!"computing io package in {path} with args {args} ..." + return { + name := "io" + version := "1.0" + } diff --git a/examples/io/package.sh b/examples/io/package.sh new file mode 100644 index 0000000000..b6449c2dd0 --- /dev/null +++ b/examples/io/package.sh @@ -0,0 +1 @@ +../../build/bin/Lake build-bin diff --git a/examples/io/test.sh b/examples/io/test.sh new file mode 100644 index 0000000000..1872494d40 --- /dev/null +++ b/examples/io/test.sh @@ -0,0 +1,3 @@ +./clean.sh +./package.sh +./build/bin/io