feat: use an attribute to identify packages in lakefile
This commit is contained in:
tydeu
parent
50f70712a8
commit
8852c5e236
3 changed files with 58 additions and 34 deletions
10
Lake/Attributes.lean
Normal file
10
Lake/Attributes.lean
Normal file
|
|
@ -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"
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue