refactor: touchup require syntax & docs (#4496)
A set of general tweaks of the `require` syntax and docs that provide a base for #4495. The sole significant behavioral change is that the `name` field of a `require` in TOML now falls back to being interpreted as a simple string name if the value is not a valid Lean identifier. This means that a require for a package like `doc-gen4` can be written without French quotes.
This commit is contained in:
Mac Malone
GitHub
parent
1b5b91cccf
commit
f9952e8c39
5 changed files with 158 additions and 76 deletions
|
|
@ -163,15 +163,16 @@ protected def LeanExeConfig.mkSyntax
|
|||
`(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name):ident $[$declVal?]?)
|
||||
|
||||
protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic.run do
|
||||
let src ←
|
||||
match cfg.src with
|
||||
| .path dir =>
|
||||
`(fromSource|$(quote dir):term)
|
||||
| .git url rev? subDir? =>
|
||||
`(fromSource|git $(quote url) $[@ $(rev?.map quote)]? $[/ $(subDir?.map quote)]?)
|
||||
let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
|
||||
cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>
|
||||
`($stx |>.insert $(quote opt) $(quote val))
|
||||
match cfg.src with
|
||||
| .path dir =>
|
||||
`(requireDecl|require $(mkIdent cfg.name) from $(quote dir):term $[with $opts?]?)
|
||||
| .git url rev? subDir? =>
|
||||
`(requireDecl|require $(mkIdent cfg.name) from git $(quote url)
|
||||
$[@ $(rev?.map quote)]? $[/ $(subDir?.map quote)]? $[with $opts?]?)
|
||||
`(requireDecl|require $(mkIdent cfg.name):ident from $src $[with $opts?]?)
|
||||
|
||||
/-! ## Root Encoder -/
|
||||
|
||||
|
|
|
|||
|
|
@ -5,34 +5,46 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
|||
-/
|
||||
import Lean.Data.NameMap
|
||||
|
||||
/- # Package Dependency Configuration
|
||||
|
||||
This module the defines the data types which encode a dependency of a
|
||||
Lake package (i.e., the information contained in the `require` DSL syntax).
|
||||
-/
|
||||
|
||||
open System Lean
|
||||
|
||||
namespace Lake
|
||||
open Lean System
|
||||
|
||||
/--
|
||||
The `src` of a `Dependency`.
|
||||
|
||||
In Lake, dependency sources currently come into flavors:
|
||||
* Local `path`s relative to the package's directory.
|
||||
* Remote `git` repositories that are download from a given `url`
|
||||
into the workspace's `packagesDir`.
|
||||
The source of a `Dependency`.
|
||||
That is, where Lake should look to materialize the dependency.
|
||||
-/
|
||||
inductive Source where
|
||||
inductive DependencySrc where
|
||||
/- A package located a fixed path relative to the dependent package's directory. -/
|
||||
| path (dir : FilePath)
|
||||
/- A package cloned from a Git repository available at a fixed Git `url`. -/
|
||||
| git (url : String) (rev : Option String) (subDir : Option FilePath)
|
||||
deriving Inhabited, Repr
|
||||
|
||||
/-- A `Dependency` of a package. -/
|
||||
|
||||
/--
|
||||
A `Dependency` of a package.
|
||||
It specifies a package which another package depends on.
|
||||
This encodes the information contained in the `require` DSL syntax.
|
||||
-/
|
||||
structure Dependency where
|
||||
/--
|
||||
A `Name` for the dependency.
|
||||
The names of a package's dependencies cannot clash.
|
||||
The package name of the dependency.
|
||||
This name must match the one declared in its configuration file,
|
||||
as that name is used to index its target data types. For this reason,
|
||||
the package name must also be unique across packages in the dependency graph.
|
||||
-/
|
||||
name : Name
|
||||
/--
|
||||
The source of a dependency.
|
||||
See the documentation of `Source` for more information.
|
||||
See the documentation of `DependencySrc` for supported sources.
|
||||
-/
|
||||
src : Source
|
||||
src : DependencySrc
|
||||
/--
|
||||
Arguments to pass to the dependency's package configuration.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -8,54 +8,96 @@ import Lake.Config.Dependency
|
|||
import Lake.DSL.Extensions
|
||||
import Lake.DSL.DeclUtil
|
||||
|
||||
namespace Lake.DSL
|
||||
/-! # The `require` syntax
|
||||
|
||||
This module contains the macro definition of the `require` DSL syntax
|
||||
used to specify package dependencies.
|
||||
-/
|
||||
|
||||
open Lean Parser Command
|
||||
|
||||
namespace Lake.DSL
|
||||
|
||||
syntax fromPath :=
|
||||
term
|
||||
|
||||
syntax fromGit :=
|
||||
&" git " term:max ("@" term:max)? ("/" term)?
|
||||
&"git " term:max ("@" term:max)? ("/" term)?
|
||||
|
||||
syntax depSpec :=
|
||||
ident " from " (fromGit <|> fromPath) (" with " term)?
|
||||
|
||||
def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
|
||||
let depTy := mkCIdent ``Dependency
|
||||
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 : $depTy := {
|
||||
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 : $depTy := {
|
||||
name := $(quote name.getId),
|
||||
src := Source.path $path,
|
||||
opts := $opts
|
||||
})
|
||||
| _ => Macro.throwErrorAt stx "ill-formed require syntax"
|
||||
syntax fromSource :=
|
||||
fromGit <|> fromPath
|
||||
|
||||
/--
|
||||
Adds a new package dependency to the workspace. Has two forms:
|
||||
Specifies a specific source from which to draw the package dependency.
|
||||
Dependencies that are downloaded from a remote source will be placed
|
||||
into the workspace's `packagesDir`.
|
||||
|
||||
```lean
|
||||
require foo from "path"/"to"/"local"/"package" with NameMap.empty
|
||||
require bar from git "url.git"@"rev"/"optional"/"path-to"/"dir-with-pkg"
|
||||
**Path Dependencies**
|
||||
|
||||
```
|
||||
from <path>
|
||||
```
|
||||
|
||||
Either form supports the optional `with` clause.
|
||||
The `@"rev"` and `/"path"/"dir"` parts of the git form of `require`
|
||||
are optional.
|
||||
Lake loads the package located a fixed `path` relative to the
|
||||
requiring package's directory.
|
||||
|
||||
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).
|
||||
**Git Dependencies**
|
||||
|
||||
```
|
||||
from git <url> [@ <rev>] [/ <subDir>]
|
||||
```
|
||||
|
||||
Lake clones the Git repository available at the specified fixed Git `url`,
|
||||
and checks out the specified revision `rev`. The revision can be a commit hash,
|
||||
branch, or tag. If none is provided, Lake defaults to `master`. After checkout,
|
||||
Lake loads the package located in `subDir` (or the repository root if no
|
||||
subdirectory is specified).
|
||||
-/
|
||||
syntax fromClause :=
|
||||
" from " fromSource
|
||||
|
||||
syntax withClause :=
|
||||
" with " term
|
||||
|
||||
syntax depSpec :=
|
||||
identOrStr 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)
|
||||
|
||||
def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
|
||||
let `(depSpec| $nameStx from $src $[with $opts?]?) := stx
|
||||
| Macro.throwErrorAt stx "ill-formed require syntax"
|
||||
let src ←
|
||||
match src with
|
||||
| `(fromSource|git%$tk $url $[@ $rev?]? $[/ $subDir?]?) => withRef tk do
|
||||
let rev ← quoteOptTerm rev?
|
||||
let subDir ← quoteOptTerm subDir?
|
||||
``(DependencySrc.git $url $rev $subDir)
|
||||
| `(fromSource|$path:term) => withRef src do
|
||||
``(DependencySrc.path $path)
|
||||
| _ => Macro.throwErrorAt src "ill-formed from syntax"
|
||||
let name := expandIdentOrStrAsIdent nameStx
|
||||
`($[$doc?:docComment]? @[package_dep] def $name : $(mkCIdent ``Dependency) := {
|
||||
name := $(quote name.getId),
|
||||
src := $src,
|
||||
opts := $(opts?.getD <| ← `({})),
|
||||
})
|
||||
|
||||
/--
|
||||
Adds a new package dependency to the workspace. The general syntax is:
|
||||
|
||||
```
|
||||
require <pkg-name> from <source> [with <options>]
|
||||
```
|
||||
|
||||
The `from` clause tells Lake where to locate the dependency.
|
||||
See the `fromClause` syntax documentation (e.g., hover over it) to see
|
||||
the different forms this clause can take.
|
||||
|
||||
The `with` clause specifies 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.
|
||||
-/
|
||||
scoped macro (name := requireDecl)
|
||||
doc?:(docComment)? kw:"require " spec:depSpec : command => withRef kw do
|
||||
|
|
|
|||
|
|
@ -221,29 +221,29 @@ protected def LeanExeConfig.decodeToml (t : Table) (ref := Syntax.missing) : Exc
|
|||
|
||||
instance : DecodeToml LeanExeConfig := ⟨fun v => do LeanExeConfig.decodeToml (← v.decodeTable) v.ref⟩
|
||||
|
||||
protected def Source.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Source := do
|
||||
protected def DependencySrc.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) DependencySrc := do
|
||||
let typeVal ← t.decodeValue `type
|
||||
match (← typeVal.decodeString) with
|
||||
| "path" =>
|
||||
return Source.path (← t.decode `dir)
|
||||
return .path (← t.decode `dir)
|
||||
| "git" => ensureDecode do
|
||||
return Source.git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
|
||||
return .git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
|
||||
| _ =>
|
||||
throw #[DecodeError.mk typeVal.ref "expected one of 'path' or 'git'"]
|
||||
|
||||
instance : DecodeToml Source := ⟨fun v => do Source.decodeToml (← v.decodeTable) v.ref⟩
|
||||
instance : DecodeToml DependencySrc := ⟨fun v => do DependencySrc.decodeToml (← v.decodeTable) v.ref⟩
|
||||
|
||||
protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Dependency := ensureDecode do
|
||||
let name ← t.tryDecode `name ref
|
||||
let src ← id do
|
||||
let name ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
|
||||
let src : DependencySrc ← id do
|
||||
if let some dir ← t.tryDecode? `path then
|
||||
return Source.path dir
|
||||
return .path dir
|
||||
else if let some g := t.find? `git then
|
||||
match g with
|
||||
| .string _ url =>
|
||||
return Source.git url (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
|
||||
return .git url (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
|
||||
| .table ref t =>
|
||||
return Source.git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
|
||||
return .git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
|
||||
| _ =>
|
||||
modify (·.push <| .mk g.ref "expected string or table")
|
||||
return default
|
||||
|
|
|
|||
|
|
@ -24,7 +24,9 @@ Each `lakefile.lean` includes a `package` declaration (akin to `main`) which def
|
|||
+ [Custom Targets](#custom-targets)
|
||||
* [Defining New Facets](#defining-new-facets)
|
||||
* [Adding Dependencies](#adding-dependencies)
|
||||
+ [Syntax of `require`](#syntax-of-require)
|
||||
+ [Lean `require`](#lean-require)
|
||||
+ [Supported Sources](#supported-sources)
|
||||
+ [TOML `require`](#toml-require)
|
||||
* [GitHub Release Builds](#github-release-builds)
|
||||
* [Writing and Running Scripts](#writing-and-running-scripts)
|
||||
* [Building and Running Lake from the Source](#building-and-running-lake-from-the-source)
|
||||
|
|
@ -336,30 +338,55 @@ For theorem proving packages which depend on `mathlib`, you can also run `lake n
|
|||
|
||||
**NOTE:** For mathlib in particular, you should run `lake exe cache get` prior to a `lake build` after adding or updating a mathlib dependency. Otherwise, it will be rebuilt from scratch (which can take hours). For more information, see mathlib's [wiki page](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency) on using it as a dependency.
|
||||
|
||||
### Syntax of `require`
|
||||
## Lean `require`
|
||||
|
||||
The `require` command has two forms:
|
||||
The `require` command in Lean Lake configuration follows the general syntax:
|
||||
|
||||
```lean
|
||||
require foo from "path"/"to"/"local"/"package" with NameMap.empty
|
||||
require bar from git "url.git"@"rev"/"optional"/"path-to"/"dir-with-pkg"
|
||||
require <pkg-name> from <source> [with <options>]
|
||||
```
|
||||
|
||||
The first form adds a local dependency and the second form adds a Git dependency. For a Git dependency, the revision can be a commit hash, branch, or tag. Also, the `@"rev"` and `/"path-to"/"term"` parts of the `require` are optional.
|
||||
The `from` clause tells Lake where to locate the dependency.
|
||||
The `with` clause specifies 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.
|
||||
|
||||
Both forms also support an optional `with` clause to specify arguments to pass to the dependency's package configuration (i.e., same as `args` in a `lake build -- <args...>` invocation). 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).
|
||||
## Supported Sources
|
||||
|
||||
To `require` a package in a TOML configuration, the equivalent syntax is:
|
||||
Lake supports the following types of dependencies as sources in a `from` clause.
|
||||
|
||||
### Path Dependencies
|
||||
|
||||
```
|
||||
from <path>
|
||||
```
|
||||
|
||||
Lake loads the package located a fixed `path` relative to the requiring package's directory.
|
||||
|
||||
### Git Dependencies
|
||||
|
||||
```
|
||||
from git <url> [@ <rev>] [/ <subDir>]
|
||||
```
|
||||
|
||||
Lake clones the Git repository available at the specified fixed Git `url`, and checks out the specified revision `rev`. The revision can be a commit hash, branch, or tag. If none is provided, Lake defaults to `master`. After checkout, Lake loads the package located in `subDir` (or the repository root if no subdirectory is specified).
|
||||
|
||||
## TOML `require`
|
||||
|
||||
To `require` a package in a TOML configuration, the parallel syntax for the above examples is:
|
||||
|
||||
```toml
|
||||
# A path dependency
|
||||
[[require]]
|
||||
path = "path/to/local/package"
|
||||
options = {}
|
||||
name = "<pkg-name>"
|
||||
path = "<path>"
|
||||
options = {<options>}
|
||||
|
||||
# A Git dependency
|
||||
[[require]]
|
||||
git = "url.git"
|
||||
rev = "rev"
|
||||
subDir = "optional/path-to/dir-with-pkg"
|
||||
name = "<pkg-name>"
|
||||
git = "<url>"
|
||||
rev = "<rev>"
|
||||
subDir = "<subDir>"
|
||||
options = {<options>}
|
||||
```
|
||||
|
||||
## GitHub Release Builds
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue