refactor: use import Lake in package configurations
This commit is contained in:
parent
efadebd5ef
commit
a9c0210ef3
12 changed files with 12 additions and 19 deletions
|
|
@ -26,7 +26,7 @@ def mainFileContents :=
|
|||
"
|
||||
|
||||
def pkgFileContents (pkgName : String) :=
|
||||
s!"import Lake.Package
|
||||
s!"import Lake
|
||||
|
||||
def package : Lake.PackageConfig := \{
|
||||
name := \"{pkgName}\"
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -1,5 +1,4 @@
|
|||
import Lake.Package
|
||||
|
||||
import Lake
|
||||
open Lake System
|
||||
|
||||
def package : PackageConfig := {
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import Lake.Package
|
||||
import Lake
|
||||
|
||||
def package : Lake.PackageConfig := {
|
||||
name := "a"
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import Lake.Package
|
||||
import Lake
|
||||
|
||||
def package : Lake.PackageConfig := {
|
||||
name := "b"
|
||||
|
|
|
|||
|
|
@ -1,5 +1,4 @@
|
|||
import Lake.Package
|
||||
|
||||
import Lake
|
||||
open Lake System
|
||||
|
||||
def package : PackageConfig := {
|
||||
|
|
|
|||
|
|
@ -1,6 +1,4 @@
|
|||
import Lake.Package
|
||||
import Lake.BuildTargets
|
||||
|
||||
import Lake
|
||||
open Lake System
|
||||
|
||||
def package : PackageConfig := {
|
||||
|
|
|
|||
|
|
@ -1,6 +1,4 @@
|
|||
import Lake.Package
|
||||
import Lake.BuildTargets
|
||||
|
||||
import Lake
|
||||
open Lake System
|
||||
|
||||
def cDir : FilePath := "c"
|
||||
|
|
|
|||
|
|
@ -1,5 +1,4 @@
|
|||
import Lake.Package
|
||||
|
||||
import Lake
|
||||
open Lake System
|
||||
|
||||
def package : PackageConfig := {
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import Lake.Package
|
||||
import Lake
|
||||
|
||||
def package : Lake.PackageConfig := {
|
||||
name := "hello"
|
||||
|
|
|
|||
|
|
@ -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} ..."
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
import Lake.Package
|
||||
import Lake
|
||||
|
||||
def package : Lake.PackageConfig := {
|
||||
name := "foo"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue