chore: lake: simplify config decl syntax

* deprecate `:=` syntax in config decls
* standardize field syntax across `where` and `{...}`

RELEASES.md

@@ -10,6 +10,8 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f
 v4.3.0 (development in progress)
 ---------
 
+* **Lake:** The `:=` syntax for configuration declarations (i.e., `package`, `lean_lib`, and `lean_exe`) has been deprecated. For example, `package foo := {...}` is deprecated.
+
 v4.2.0
 ---------
 

src/lake/Lake/DSL/DeclUtil.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.DSL.Config
 import Lake.Util.Binder
 import Lean.Parser.Command
 
@@ -24,8 +25,11 @@ def expandAttrs (attrs? : Option Attributes) : Array AttrInstance :=
   else
     #[]
 
+syntax declField :=
+  ident ":=" term
+
 syntax structVal :=
-  "{" manyIndent(group(Term.structInstField ", "?)) "}"
+  "{" manyIndent(group(declField ", "?)) "}"
 
 syntax declValDo :=
   ppSpace Term.do (Term.whereDecls)?
@@ -33,6 +37,9 @@ syntax declValDo :=
 syntax declValStruct :=
   ppSpace structVal (Term.whereDecls)?
 
+syntax declValWhere :=
+  " where " sepByIndentSemicolon(declField) (Term.whereDecls)?
+
 syntax declValTyped :=
   Term.typeSpec declValSimple
 
@@ -43,7 +50,7 @@ syntax simpleDeclSig :=
   ident Term.typeSpec declValSimple
 
 syntax structDeclSig :=
-  ident (Command.whereStructInst <|> declValOptTyped <|> declValStruct)?
+  ident (declValWhere <|> declValOptTyped <|> declValStruct)?
 
 syntax bracketedSimpleBinder :=
   "(" ident (" : " term)? ")"
@@ -69,18 +76,25 @@ def fixName (id : Ident) : Option Name → Ident
 | some n => mkIdentFrom id n
 | none => id
 
-def mkConfigStructDecl (name? : Option Name)
+def expandDeclField : TSyntax ``declField → MacroM (TSyntax ``Term.structInstField)
+| `(declField| $id :=%$tk $val) => `(Term.structInstField| $id:ident :=%$tk $val)
+| x => Macro.throwErrorAt x "ill-formed field declaration"
+
+def mkConfigDecl (name? : Option Name)
 (doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term)
 : (spec : Syntax) → MacroM Syntax.Command
 | `(structDeclSig| $id:ident) =>
   `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
     {name := $(quote id.getId)})
-| `(structDeclSig| $id:ident where $ds;* $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty where
-      name := $(quote id.getId); $ds;* $[$wds?]?)
-| `(structDeclSig| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $(ty?.getD ty) := $defn $[$wds?]?)
+| `(structDeclSig| $id:ident where $fs;* $[$wds?]?) => do
+  let fields ← fs.getElems.mapM expandDeclField
+  let defn ← `({ name := $(quote id.getId), $fields,* })
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
+| `(structDeclSig| $id:ident $[: $ty?]? :=%$defTk $defn $[$wds?]?) => do
+  let notice ← withRef defTk `(#eval IO.eprintln s!" warning: {__dir__}: `:=` syntax for configurations has been deprecated")
+  `($notice $[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
 | `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $fs,* })
+  let fields ← fs.mapM expandDeclField
+  let defn ← `({ name := $(quote id.getId), $fields,* })
   `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed configuration syntax"

src/lake/Lake/DSL/Package.lean

@@ -20,7 +20,6 @@ Defines the configuration of a Lake package.  Has many forms:
 package «pkg-name»
 package «pkg-name» { /- config opts -/ }
 package «pkg-name» where /- config opts -/
-package «pkg-name» : PackageConfig := /- config -/
 ```
 
 There can only be one `package` declaration per Lake configuration file.
@@ -32,4 +31,4 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
   let attr ← `(Term.attrInstance| «package»)
   let ty := mkCIdentFrom (← getRef) ``PackageConfig
   let attrs := #[attr] ++ expandAttrs attrs?
-  mkConfigStructDecl packageDeclName doc? attrs ty sig
+  mkConfigDecl packageDeclName doc? attrs ty sig

src/lake/Lake/DSL/Targets.lean

@@ -153,7 +153,6 @@ Has many forms:
 lean_lib «target-name»
 lean_lib «target-name» { /- config opts -/ }
 lean_lib «target-name» where /- config opts -/
-lean_lib «target-name» := /- config -/
 ```
 -/
 scoped macro (name := leanLibDecl)
@@ -162,7 +161,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
   let attr ← `(Term.attrInstance| lean_lib)
   let ty := mkCIdentFrom (← getRef) ``LeanLibConfig
   let attrs := #[attr] ++ expandAttrs attrs?
-  mkConfigStructDecl none doc? attrs ty sig
+  mkConfigDecl none doc? attrs ty sig
 
 /--
 Define a new Lean binary executable target for the package.
@@ -173,7 +172,6 @@ Has many forms:
 lean_exe «target-name»
 lean_exe «target-name» { /- config opts -/ }
 lean_exe «target-name» where /- config opts -/
-lean_exe «target-name» := /- config -/
 ```
 -/
 scoped macro (name := leanExeDecl)
@@ -182,7 +180,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
   let attr ← `(Term.attrInstance| lean_exe)
   let ty := mkCIdentFrom (← getRef) ``LeanExeConfig
   let attrs := #[attr] ++ expandAttrs attrs?
-  mkConfigStructDecl none doc? attrs ty sig
+  mkConfigDecl none doc? attrs ty sig
 
 
 --------------------------------------------------------------------------------

src/lake/README.md

@@ -194,9 +194,8 @@ A Lean library target defines a set of Lean modules available to `import` and ho
 **Syntax**
 
 ```lean
-lean_lib «target-name» {
+lean_lib «target-name» where
   -- configuration options go here
-}
 ```
 
 **Configuration Options**
@@ -217,9 +216,8 @@ A Lean executable target builds a binary executable from a Lean module with a `m
 **Syntax**
 
 ```lean
-lean_exe «target-name» {
+lean_exe «target-name» where
   -- configuration options go here
-}
 ```
 
 **Configuration Options**