chore: add Packager test

This commit is contained in:
tydeu 2021-07-10 12:21:52 -04:00
parent 042353d862
commit 9da32ce7eb
7 changed files with 18 additions and 1 deletions

View file

@ -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"

1
examples/io/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
/build

2
examples/io/Io.lean Normal file
View file

@ -0,0 +1,2 @@
def main : IO Unit :=
IO.println "Hello from Io!"

1
examples/io/clean.sh Normal file
View file

@ -0,0 +1 @@
rm -r build

8
examples/io/package.lean Normal file
View file

@ -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"
}

1
examples/io/package.sh Normal file
View file

@ -0,0 +1 @@
../../build/bin/Lake build-bin

3
examples/io/test.sh Normal file
View file

@ -0,0 +1,3 @@
./clean.sh
./package.sh
./build/bin/io