diff --git a/Lake/Init.lean b/Lake/Init.lean index bf60404ff6..139e4b3621 100644 --- a/Lake/Init.lean +++ b/Lake/Init.lean @@ -26,7 +26,7 @@ def mainFileContents := " def pkgFileContents (pkgName : String) := -s!"import Lake.Package +s!"import Lake def package : Lake.PackageConfig := \{ name := \"{pkgName}\" diff --git a/README.md b/README.md index 6f1ff635e3..72d0551940 100644 --- a/README.md +++ b/README.md @@ -43,7 +43,7 @@ def main : IO Unit := Lake also creates a basic `package.lean` for the package: ```lean -import Lake.Package +import Lake def package : Lake.PackageConfig := { name := "hello" diff --git a/examples/bootstrap/package.lean b/examples/bootstrap/package.lean index 7d2dc38e83..5ad5da9dc4 100644 --- a/examples/bootstrap/package.lean +++ b/examples/bootstrap/package.lean @@ -1,5 +1,4 @@ -import Lake.Package - +import Lake open Lake System def package : PackageConfig := { diff --git a/examples/deps/a/package.lean b/examples/deps/a/package.lean index 5b84b81ccb..15ce8cbe26 100644 --- a/examples/deps/a/package.lean +++ b/examples/deps/a/package.lean @@ -1,4 +1,4 @@ -import Lake.Package +import Lake def package : Lake.PackageConfig := { name := "a" diff --git a/examples/deps/b/package.lean b/examples/deps/b/package.lean index f9108e340f..7fcd738693 100644 --- a/examples/deps/b/package.lean +++ b/examples/deps/b/package.lean @@ -1,4 +1,4 @@ -import Lake.Package +import Lake def package : Lake.PackageConfig := { name := "b" diff --git a/examples/deps/foo/package.lean b/examples/deps/foo/package.lean index fbd5cb70aa..76ea943e5d 100644 --- a/examples/deps/foo/package.lean +++ b/examples/deps/foo/package.lean @@ -1,5 +1,4 @@ -import Lake.Package - +import Lake open Lake System def package : PackageConfig := { diff --git a/examples/ffi-dep/package.lean b/examples/ffi-dep/package.lean index 23a2dcf7f6..503f8a833b 100644 --- a/examples/ffi-dep/package.lean +++ b/examples/ffi-dep/package.lean @@ -1,6 +1,4 @@ -import Lake.Package -import Lake.BuildTargets - +import Lake open Lake System def package : PackageConfig := { diff --git a/examples/ffi/package.lean b/examples/ffi/package.lean index a0b94fba2f..cdc48907bb 100644 --- a/examples/ffi/package.lean +++ b/examples/ffi/package.lean @@ -1,6 +1,4 @@ -import Lake.Package -import Lake.BuildTargets - +import Lake open Lake System def cDir : FilePath := "c" diff --git a/examples/git/package.lean b/examples/git/package.lean index 3430edbaea..2bb3bcf167 100644 --- a/examples/git/package.lean +++ b/examples/git/package.lean @@ -1,5 +1,4 @@ -import Lake.Package - +import Lake open Lake System def package : PackageConfig := { diff --git a/examples/hello/package.lean b/examples/hello/package.lean index 1b01a4fd3a..675cb37edf 100644 --- a/examples/hello/package.lean +++ b/examples/hello/package.lean @@ -1,4 +1,4 @@ -import Lake.Package +import Lake def package : Lake.PackageConfig := { name := "hello" diff --git a/examples/io/package.lean b/examples/io/package.lean index 9b7f6de88a..dc5a87c709 100644 --- a/examples/io/package.lean +++ b/examples/io/package.lean @@ -1,4 +1,4 @@ -import Lake.Package +import Lake def package : Lake.IOPackager := fun path args => do IO.println s!"computing io package in {path} with args {args} ..." diff --git a/examples/main/package.lean b/examples/main/package.lean index 0bc6d8e9fd..6a3ccb5cd4 100644 --- a/examples/main/package.lean +++ b/examples/main/package.lean @@ -1,4 +1,4 @@ -import Lake.Package +import Lake def package : Lake.PackageConfig := { name := "foo"