diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 0a2e91ec72..410c70aa1c 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/src/lake/Lake/CLI/Translate/Lean.lean @@ -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 -/ diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean index e41b9f1f83..59f6059566 100644 --- a/src/lake/Lake/Config/Dependency.lean +++ b/src/lake/Lake/Config/Dependency.lean @@ -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. -/ diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean index 5da81dd826..930ace7dc7 100644 --- a/src/lake/Lake/DSL/Require.lean +++ b/src/lake/Lake/DSL/Require.lean @@ -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 ``` -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 [@ ] [/ ] +``` + +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 from [with ] +``` + +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 diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index b345cad61b..85cf32d52a 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -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 diff --git a/src/lake/README.md b/src/lake/README.md index e08bf9e64e..fabfc9790c 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -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 from [with ] ``` -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 -- ` 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 +``` + +Lake loads the package located a fixed `path` relative to the requiring package's directory. + +### Git Dependencies + +``` +from git [@ ] [/ ] +``` + +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 = "" +path = "" +options = {} +# A Git dependency [[require]] -git = "url.git" -rev = "rev" -subDir = "optional/path-to/dir-with-pkg" +name = "" +git = "" +rev = "" +subDir = "" +options = {} ``` ## GitHub Release Builds