feat: lake: require @ git (#4692)

Adds syntactic sugar specifying a git revision as a dependency version
in a `require` command. For example:

```
require "leanprover-community" / "proofwidgets" @ git "v0.0.39"
```

src/lake/Lake/CLI/Translate/Lean.lean

@@ -169,7 +169,14 @@ protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic
       `(fromSource|$(quote dir):term)
     | .git url rev? subDir? =>
       `(fromSource|git $(quote url) $[@ $(rev?.map quote)]? $[/ $(subDir?.map quote)]?)
-  let ver? := cfg.version?.map quote
+  let ver? ←
+    if let some ver := cfg.version? then
+      if ver.startsWith "git#" then
+        some <$> `(verSpec|git $(quote <| ver.drop 4))
+      else
+        some <$> `(verSpec|$(quote ver):term)
+    else
+      pure none
   let scope? := if cfg.scope.isEmpty then none else some (quote cfg.scope)
   let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
     cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>

src/lake/Lake/DSL/Require.lean

@@ -56,24 +56,31 @@ subdirectory is specified).
 syntax fromClause :=
   " from " fromSource
 
+/-
+A `NameMap String` of Lake options used to configure the dependency.
+This is equivalent to passing `-K` options to the dependency on the command line.
+-/
 syntax withClause :=
   " with " term
 
+syntax verSpec :=
+  &"git "? term:max
+
 /--
 The version of the package to lookup in Lake's package index.
-A Git revision can be specified via `"git#<rev>"`.
+A Git revision can be specified via `@ git "<rev>"`.
 -/
-syntax verSpec :=
-  " @ " term:max
+syntax verClause :=
+  " @ " verSpec
 
 syntax depName :=
   atomic(str " / ")? identOrStr
 
 syntax depSpec :=
-  depName (verSpec)? (fromClause)? (withClause)?
+  depName (verClause)? (fromClause)? (withClause)?
 
 @[inline] private def quoteOptTerm [Monad m] [MonadQuotation m] (term? : Option Term) : m Term :=
-  if let some term := term? then withRef term `(some $term) else `(none)
+  if let some term := term? then withRef term ``(some $term) else ``(none)
 
 def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
   let `(depSpec| $fullNameStx $[@ $ver?]? $[from $src?]? $[with $opts?]?) := stx
@@ -93,11 +100,19 @@ def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM
     match scope? with
     | some scope => scope
     | none => Syntax.mkStrLit "" (.fromRef fullNameStx)
+  let ver ←
+    if let some ver := ver? then withRef ver do
+      match ver with
+      | `(verSpec|git $ver) => ``(some ("git#" ++ $ver))
+      | `(verSpec|$ver:term) => ``(some $ver)
+      | _ => Macro.throwErrorAt ver "ill-formed version syntax"
+    else
+      ``(none)
   let name := expandIdentOrStrAsIdent nameStx
   `($[$doc?:docComment]? @[package_dep] def $name : $(mkCIdent ``Dependency) := {
     name :=  $(quote name.getId),
     scope := $scope,
-    version? := $(← quoteOptTerm ver?),
+    version? := $ver,
     src? := $(← quoteOptTerm src?),
     opts := $(opts?.getD <| ← `({})),
   })

src/lake/tests/translateConfig/out.expected.lean

@@ -9,7 +9,7 @@ package test where
   lintDriver := "b"
   platformIndependent := true
 
-require "foo" / baz @ "git#abcdef"
+require "foo" / baz @ git "abcdef"
 
 require foo from "-" with Lake.NameMap.empty |>.insert `foo "bar"