From 9da32ce7ebdc463bf2b88f5c4d1e6c525a717703 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 10 Jul 2021 12:21:52 -0400 Subject: [PATCH] chore: add Packager test --- Lake/LeanConfig.lean | 3 ++- examples/io/.gitignore | 1 + examples/io/Io.lean | 2 ++ examples/io/clean.sh | 1 + examples/io/package.lean | 8 ++++++++ examples/io/package.sh | 1 + examples/io/test.sh | 3 +++ 7 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 examples/io/.gitignore create mode 100644 examples/io/Io.lean create mode 100644 examples/io/clean.sh create mode 100644 examples/io/package.lean create mode 100644 examples/io/package.sh create mode 100644 examples/io/test.sh 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