From 8852c5e2369583c95833cfdb3d0ed1dfb31dffa1 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 3 Oct 2021 14:13:49 -0400 Subject: [PATCH] feat: use an attribute to identify packages in lakefile --- Lake/Attributes.lean | 10 ++++++++++ Lake/DSL.lean | 44 +++++++++++++++++++++++++------------------- Lake/LeanConfig.lean | 38 +++++++++++++++++++++++--------------- 3 files changed, 58 insertions(+), 34 deletions(-) create mode 100644 Lake/Attributes.lean diff --git a/Lake/Attributes.lean b/Lake/Attributes.lean new file mode 100644 index 0000000000..8597985cd7 --- /dev/null +++ b/Lake/Attributes.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lean +open Lean + +initialize packageAttr : TagAttribute ← + registerTagAttribute `package "Lake package attribute" diff --git a/Lake/DSL.lean b/Lake/DSL.lean index c261966800..51da208f5e 100644 --- a/Lake/DSL.lean +++ b/Lake/DSL.lean @@ -1,7 +1,13 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ import Lean.Parser import Lake.Package +import Lake.Attributes -open Lean Parser +open Lean Parser Command namespace Lake.DSL syntax packageStruct := @@ -13,16 +19,16 @@ syntax packageDeclValSpecial := syntax packageDeclWithBinders := (ppSpace "(" Term.simpleBinder ")")? -- dir (ppSpace "(" Term.simpleBinder ")")? -- args - ppSpace (Command.declValSimple <|> packageDeclValSpecial) + ppSpace (declValSimple <|> packageDeclValSpecial) syntax packageDeclTyped := - Term.typeSpec Command.declValSimple + Term.typeSpec declValSimple syntax packageDeclSpec := ident (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders)? scoped syntax (name := packageDecl) -declModifiers "package " packageDeclSpec : command +(docComment)? "package " packageDeclSpec : command def expandPackageBinders : (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax) @@ -31,30 +37,30 @@ def expandPackageBinders | none, some args => do (true, ← `(_), args) | some dir, some args => do (true, dir, args) -def mkPackageDef (defn : Syntax) (mods : Syntax) +def mkPackageDef (id : Syntax) (defn : Syntax) (doc? : Option Syntax) (dir? : Option Syntax) (args? : Option Syntax) (wds? : Option Syntax) : MacroM Syntax := do let (hasBinders, dir, args) ← expandPackageBinders dir? args? if hasBinders then - `($mods:declModifiers def $(mkIdent `package) : Packager := + `($[$doc?:docComment]? @[«package»] def $id : Packager := (fun $dir $args => $defn) $[$wds?]?) else - `($mods:declModifiers def $(mkIdent `package) : PackageConfig := $defn $[$wds?]?) + `($[$doc?:docComment]? @[«package»] def $id : PackageConfig := $defn $[$wds?]?) @[macro packageDecl] def expandPackageDecl : Macro -| `($mods:declModifiers package $id:ident) => - `($mods:declModifiers def $(mkIdent `package) : PackageConfig := {name := $(quote id.getId)}) -| `($mods:declModifiers package $id:ident where $[$ds]*) => - `($mods:declModifiers def $(mkIdent `package) : PackageConfig where +| `($[$doc?:docComment]? package $id:ident) => + `($[$doc?:docComment]? @[«package»] def $id : PackageConfig := {name := $(quote id.getId)}) +| `($[$doc?:docComment]? package $id:ident where $[$ds]*) => + `($[$doc?:docComment]? @[«package»] def $id : PackageConfig where name := $(quote id.getId) $[$ds]*) -| `($mods:declModifiers package $id:ident : $ty := $defn $[$wds?]?) => - `($mods:declModifiers def $(mkIdent `package) : $ty := $defn $[$wds?]?) -| `($mods:declModifiers package $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) => - mkPackageDef defn mods dir? args? wds? -| `($mods:declModifiers package $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do - mkPackageDef (← `({ name := $(quote id.getId), $[$fs]* })) mods dir? args? wds? -| `($mods:declModifiers package $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do +| `($[$doc?:docComment]? package $id:ident : $ty := $defn $[$wds?]?) => + `($[$doc?:docComment]? @[«package»] def $id : $ty := $defn $[$wds?]?) +| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) => + mkPackageDef id defn doc? dir? args? wds? +| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do + mkPackageDef id (← `({ name := $(quote id.getId), $[$fs]* })) doc? dir? args? wds? +| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do let (_, dir, args) ← expandPackageBinders dir? args? - `($mods:declModifiers def $(mkIdent `package) : IOPackager := + `($[$doc?:docComment]? @[«package»] def $id : IOPackager := (fun $dir $args => do $seq) $[$wds?]?) | stx => Macro.throwErrorAt stx "ill-formed package declaration" diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean index 4b6c07515f..8cb69fde49 100644 --- a/Lake/LeanConfig.lean +++ b/Lake/LeanConfig.lean @@ -3,15 +3,15 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lean.Elab.Frontend +import Lean import Lake.Package +import Lake.Attributes open Lean System namespace Lake -def pkgModName : Name := `package -def pkgDefName : Name := `package +def configModName : Name := `lakefile /-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/ def defaultConfigFile : FilePath := "lakefile.lean" @@ -23,19 +23,27 @@ unsafe def fromLeanFileUnsafe : IO Package := do let opts := Options.empty let input ← IO.FS.readFile path - let (env, ok) ← Elab.runFrontend input opts path.toString pkgModName + let (env, ok) ← Elab.runFrontend input opts path.toString configModName if ok then - let m := env.evalConstCheck IOPackager opts ``IOPackager pkgDefName - if let Except.ok ioPackager := m.run.run then - return Package.mk dir (← ioPackager dir args) - let m := env.evalConstCheck Packager opts ``Packager pkgDefName - if let Except.ok packager := m.run.run then - return Package.mk dir (packager dir args) - let m := env.evalConstCheck PackageConfig opts ``PackageConfig pkgDefName - if let Except.ok config := m.run.run then - return Package.mk dir config - throw <| IO.userError - s!"unexpected type at 'package', `Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected" + match packageAttr.ext.getState env |>.toList with + | [] => + throw <| IO.userError + s!"configuration file is missing a `package` declaration" + | [pkgDeclName] => + let m := env.evalConstCheck IOPackager opts ``IOPackager pkgDeclName + if let Except.ok ioPackager := m.run.run then + return Package.mk dir (← ioPackager dir args) + let m := env.evalConstCheck Packager opts ``Packager pkgDeclName + if let Except.ok packager := m.run.run then + return Package.mk dir (packager dir args) + let m := env.evalConstCheck PackageConfig opts ``PackageConfig pkgDeclName + if let Except.ok config := m.run.run then + return Package.mk dir config + throw <| IO.userError + s!"unexpected type at 'package', `Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected" + | _ => + throw <| IO.userError + s!"configuration file has multiple `package` declarations" else throw <| IO.userError s!"package configuration (at {path}) has errors"