From e733149134a9fa9e92bc589afbe6c2cbb665835c Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 2 May 2024 21:08:18 -0400
Subject: [PATCH] feat: lake: `require` doc comments (#4057)

Lake now supports docstrings on `require` commands:

```lean
/-- This is a docstring for a require statement. -/
require std from ...
```

Closes #2898.
---
 src/lake/Lake/DSL/Require.lean           | 43 +++++++++++++-----------
 src/lake/examples/deps/bar/lakefile.lean |  1 +
 2 files changed, 24 insertions(+), 20 deletions(-)

diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean
index 0db58f28c5..18b0560c87 100644
--- a/src/lake/Lake/DSL/Require.lean
+++ b/src/lake/Lake/DSL/Require.lean
@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lean.Parser.Command
 import Lake.DSL.Extensions
+import Lake.DSL.DeclUtil
 
 namespace Lake.DSL
 open Lean Parser Command
@@ -18,24 +19,25 @@ syntax fromGit :=
 syntax depSpec :=
   ident " from " (fromGit <|> fromPath) (" with " term)?
 
-def expandDepSpec : TSyntax ``depSpec → MacroM Command
-| `(depSpec| $name:ident from git $url $[@ $rev?]? $[/ $path?]? $[with $opts?]?) => do
-  let rev ← match rev? with | some rev => `(some $rev) | none => `(none)
-  let path ← match path? with | some path => `(some $path) | none => `(none)
-  let opts := opts?.getD <| ← `({})
-  `(@[package_dep] def $name : Dependency := {
-    name := $(quote name.getId),
-    src := Source.git $url $rev $path,
-    opts := $opts
-  })
-| `(depSpec| $name:ident from $path:term $[with $opts?]?) => do
-  let opts := opts?.getD <| ← `({})
-  `(@[package_dep] def $name : Dependency := {
-    name :=  $(quote name.getId),
-    src := Source.path $path,
-    opts := $opts
-  })
-| _ => Macro.throwUnsupported
+def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
+  match stx with
+  | `(depSpec| $name:ident from git $url $[@ $rev?]? $[/ $path?]? $[with $opts?]?) =>
+    let rev ← match rev? with | some rev => `(some $rev) | none => `(none)
+    let path ← match path? with | some path => `(some $path) | none => `(none)
+    let opts := opts?.getD <| ← `({})
+    `($[$doc?:docComment]? @[package_dep] def $name : Dependency := {
+      name := $(quote name.getId),
+      src := Source.git $url $rev $path,
+      opts := $opts
+    })
+  | `(depSpec| $name:ident from $path:term $[with $opts?]?) => do
+    let opts := opts?.getD <| ← `({})
+    `($[$doc?:docComment]? @[package_dep] def $name : Dependency := {
+      name :=  $(quote name.getId),
+      src := Source.path $path,
+      opts := $opts
+    })
+  | _ => Macro.throwUnsupported
 
 /--
 Adds a new package dependency to the workspace. Has two forms:
@@ -53,8 +55,9 @@ The elements of both the `from` and `with` clauses are proper terms so
 normal computation is supported within them (though parentheses made be
 required to disambiguate the syntax).
 -/
-scoped macro (name := requireDecl) "require " spec:depSpec : command =>
-  expandDepSpec spec
+scoped macro (name := requireDecl)
+doc?:(docComment)? "require " spec:depSpec : command =>
+  expandDepSpec spec doc?
 
 @[inherit_doc requireDecl] abbrev RequireDecl := TSyntax ``requireDecl
 
diff --git a/src/lake/examples/deps/bar/lakefile.lean b/src/lake/examples/deps/bar/lakefile.lean
index a180b75b23..3f9ee16503 100644
--- a/src/lake/examples/deps/bar/lakefile.lean
+++ b/src/lake/examples/deps/bar/lakefile.lean
@@ -3,6 +3,7 @@ open System Lake DSL
 
 package bar
 
+/-- Require statements can have doc comments. -/
 require foo from ".."/"foo"
 
 lean_lib Bar