From c751b63d0850041d89c5316cc580a72026551371 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 24 Sep 2026 03:55:46 +0000 Subject: [PATCH 1/3] refactor: split lake docs into focused modules --- Manual/BuildTools/Lake.lean | 1507 +----------------- Manual/BuildTools/Lake/API.lean | 147 ++ Manual/BuildTools/Lake/Builds.lean | 432 +++++ Manual/BuildTools/Lake/CLI.lean | 4 +- Manual/BuildTools/Lake/Cache.lean | 108 ++ Manual/BuildTools/Lake/Drivers.lean | 789 +++++++++ Manual/BuildTools/Lake/PackageOverrides.lean | 96 ++ Manual/BuildTools/Lake/Scripts.lean | 67 + 8 files changed, 1653 insertions(+), 1497 deletions(-) create mode 100644 Manual/BuildTools/Lake/API.lean create mode 100644 Manual/BuildTools/Lake/Builds.lean create mode 100644 Manual/BuildTools/Lake/Cache.lean create mode 100644 Manual/BuildTools/Lake/Drivers.lean create mode 100644 Manual/BuildTools/Lake/PackageOverrides.lean create mode 100644 Manual/BuildTools/Lake/Scripts.lean diff --git a/Manual/BuildTools/Lake.lean b/Manual/BuildTools/Lake.lean index 278f6b40b..b0262d8a6 100644 --- a/Manual/BuildTools/Lake.lean +++ b/Manual/BuildTools/Lake.lean @@ -13,8 +13,14 @@ import Lake.Build.Module import Manual.Meta +import Manual.BuildTools.Lake.API +import Manual.BuildTools.Lake.Builds +import Manual.BuildTools.Lake.Cache import Manual.BuildTools.Lake.CLI import Manual.BuildTools.Lake.Config +import Manual.BuildTools.Lake.Drivers +import Manual.BuildTools.Lake.PackageOverrides +import Manual.BuildTools.Lake.Scripts open Manual open Verso.Genre @@ -165,1507 +171,18 @@ By default, trace messages are hidden and the others are shown. The threshold can be adjusted using the {lakeOpt}`--log-level` option, the {lakeOpt}`--verbose` flag, or the {lakeOpt}`--quiet` flag. ::: -## Package Overrides -%%% -tag := "package-overrides" -%%% - -Together, the {tech}[package configuration] and {tech}[manifest] describe the exact manner by which Lake expects to acquire dependencies. -Usually, this involves making a local copy of a remote Git repository over the network. -Lake terminates with an error if the remote repository cannot be accessed. -Because the sources of dependencies are predictable, builds are reproducible across systems; packages are retrieved in the same way from the same sources on all machines. - -Nonetheless, there are situations where it is infeasible to acquire package dependencies the same way the original developers did. -For example, some companies require that all dependencies are audited prior to use, and not everyone always has access to the Internet while working. -In these situations, it is necessary to acquire packages in some other way. - -Lake's {deftech}_package overrides_ allow a package dependency to be redirected from one source to another without modifying any {tech}[package configurations] or {tech}[manifests]. -They do not allow packages to be added to or removed from the {tech}[workspace]. -All transitive dependencies in the workspace respect the redirection. -The package overrides file is a JSON file that contains an alternate list of package entries. -These entries will take precedence over those in the package's {tech}[manifest]. -This file can be provided to Lake either via the {lakeOpt}`--packages` option or by placing it at a fixed path within the Lake workspace: `.lake/package-overrides.json`. - -The syntax of package entries in the package overrides file mirrors that of the {tech}[manifest]. -Thus, it is possible to copy an entry from a manifest into a package overrides file (and vice versa). -One way to determine the necessary syntax for a package entry is to add a temporary dependency to a {tech}[package configuration] that matches the desired configuration, run {lake}`update` to generate a manifest with that dependency, and then copy the entry from the manifest into the package overrides file. - -:::example "Making Remote Dependencies Local" - -Consider a use case where programs are being developed in a restricted enviroment without network access (e.g., for security reasons). -The team wishes to compile a small tool written in Lean that depends on the [`@leanprover/Cli`](https://reservoir.lean-lang.org/@leanprover/Cli) library to provide a simple command-line interface. -That tool's {tech}[manifest] thus looks something like this: - -```lakeManifest -{ - "version": "1.3.0", - "packagesDir": ".lake/packages", - "packages": [{ - "url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "0000000000000000000000000000000000000000", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.toml" - }], - "name": "myTool", - "lakeDir": ".lake", - "fixedToolchain": false -} -``` - -This manifest would instruct Lake to download the `Cli` package from the indicated GitHub URL when building this tool. -However, the restricted environment does not have network access, so the build will fail unless Lake uses a local copy instead. -This can be done with the following {tech}[package overrides] file: - -```lakePackageOverrides -{ - "version": "1.3.0", - "packages": [{ - "type": "path", - "dir": "/etc/lean-packages/Cli", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inherited": false, - "configFile": "lakefile.toml" - }] -} -``` - -With this, Lake will instead resolve the `Cli` dependency to the local package located at the path `/etc/lean-packages/Cli`. - -::: - -## Builds - -:::paragraph -Producing a desired {tech}[artifact], such as a {tech}[`.olean` file] or an executable binary, is called a {deftech}_build_. -Builds are triggered by the {lake}`build` command or by other commands that require an artifact to be present, such as {lake}`exe`. -A build consists of the following steps: - -: {deftech (key := "configure package")}[Configuring] the package - - If {tech}[package configuration] file is newer than the cached configuration file `lakefile.olean`, then the package configuration is re-elaborated. - This also occurs when the cached file is missing or when the {lakeOpt}`--reconfigure` or {lakeOpt}`-R` flag is provided. - Changes to options using {lakeOpt}`-K` do not trigger re-elaboration of the configuration file; {lakeOpt}`-R` is necessary in these cases. - -: Computing dependencies - - The set of artifacts that are required to produce the desired output are determined, along with the {tech}[targets] and {tech}[facets] that produce them. - This process is recursive, and the result is a _graph_ of dependencies. - The dependencies in this graph are distinct from those declared for a package: packages depend on other packages, while build targets depend on other build targets, which may be in the same package or in a different one. - One facet of a given target may depend on other facets of the same target. - Lake automatically analyzes the imports of Lean modules to discover their dependencies, and the {tomlField Lake.LeanLibConfig}`extraDepTargets` field can be used to add additional dependencies to a target. - -: Replaying traces - - Rather than rebuilding everything in the dependency graph from scratch, Lake uses saved {deftech}_trace files_ to determine which artifacts require building. - During a build, Lake records which source files or other artifacts were used to produce each artifact, saving a hash of each input; these {deftech}_traces_ are saved in the {tech}[build directory].{margin}[More specifically, each artifact's trace file contains a Merkle tree hash mixture of its inputs' hashes.] - If the inputs are all unmodified, then the corresponding artifact is not rebuilt. - Trace files additionally record the {tech}[log] from each build task; these outputs are replayed as if the artifact had been built anew. - Reusing prior build products when possible is called an {deftech}_incremental build_. - -: Building artifacts - - When all unmodified dependencies in the dependency graph have been replayed from their trace files, Lake proceeds to build each artifact. - This involves running the appropriate build tool on the input files and saving the artifact and its trace file, as specified in the corresponding facet. -::: - -Lake uses two separate hash algorithms. -Text files are hashed after normalizing newlines, so that files that differ only by platform-specific newline conventions are hashed identically. -Other files are hashed without any normalization. - -Along with the trace files, Lean caches input hashes. -Whenever an artifact is built, its hash is saved in a separate file that can be re-read instead of computing the hash from scratch. -This is a performance optimization. -This feature can be disabled, causing all hashes to be recomputed from their inputs, using the {lakeOpt}`--rehash` command-line option. - -:::paragraph -During a build, the following directories are provided to the underlying build tools: - * The {deftech}_source directory_ contains Lean source code that is available for import. - * The {deftech}_library directories_ contain {tech}[`.olean` files] along with the shared and static libraries that are available for linking; it normally consists of the {tech}[root package]'s library directory (found in `.lake/build/lib`), the library directories for the other packages in the workspace, the library directory for the current Lean toolchain, and the system library directory. - * The {deftech}_Lake home_ is the directory in which Lake is installed, including binaries, source code, and libraries. - The libraries in the Lake home are needed to elaborate Lake configuration files, which have access to the full power of Lean. -::: - -## Facets -%%% -tag := "lake-facets" -%%% - -A {deftech}_facet_ describes the production of a target from another. -Conceptually, any target may have facets. -However, executables, external libraries, and custom targets provide only a single implicit facet. -Packages, libraries, and modules have multiple facets that can be requested by name when invoking {lake}`build` to select the corresponding target. - -When no facet is explicitly requested, but an initial target is designated, {lake}`build` produces the initial target's {deftech}_default facet_. -Each type of initial target has a corresponding default facet (e.g. producing an executable binary from an executable target or building a package's {tech}[default targets]); other facets may be explicitly requested in the {tech}[package configuration] or via Lake's {ref "lake-cli"}[command-line interface]. -Lake's internal API may be used to write custom facets. - - -```lakeHelp "build" -Build targets - -USAGE: - lake build [...] [-o ] [--package ] - -A target is specified with a string of the form: - - [@[]/][|[+]][:] - -You can also use the source path of a module as a target. For example, - - lake build Foo/Bar.lean:o - -will build the Lean module (within the workspace) whose source file is -`Foo/Bar.lean` and compile the generated C file into a native object file. - -The `@` and `+` markers can be used to disambiguate packages and modules -from file paths or other kinds of targets (e.g., executables or libraries). - -LIBRARY FACETS: build the library's ... - elabArts elaboration artifacts (*.olean, *.ilean files) - irArts (default) compilation artifacts (*.ir, *.ir.sig, *.c files) - static static artifact (*.a file) - shared shared artifact (*.so, *.dll, or *.dylib file) - -MODULE FACETS: build the module's ... - deps dependencies (e.g., imports, shared libraries, etc.) - elabArts elaboration artifacts (*.olean, *.ilean files) - irArts (default) compilation artifacts (*.ir, *.ir.sig, *.c files) - olean OLean (binary blob of Lean data for importers) - ilean ILean (binary blob of metadata for the Lean LSP server) - c compiled C file - bc compiled LLVM bitcode file - c.o compiled object file (of its C file) - bc.o compiled object file (of its LLVM bitcode file) - o compiled object file (of its configured backend) - dynlib shared library (e.g., for `--load-dynlib`) - -TARGET EXAMPLES: build the ... - a default facet(s) of target `a` - @a default target(s) of package `a` - +A default facet(s) of module `A` - @/a default facet(s) of target `a` of the root package - @a/b default facet(s) of target `b` of package `a` - @a/+A:c C file of module `A` of package `a` - :foo facet `foo` of the root package - -A bare `lake build` command will build the default target(s) of the root -package. Package dependencies are not updated during a build. - -With the Lake cache enabled, Lake can track the targets the build covers -(both those up-to-date and those newly built) and write the input-to-outputs -mappings of each to a file specified by the `-o` option. By default, with `-o`, -Lake will track the targets of the root package, use `--package` to select a -different one. These mappings can then be used to upload the build artifacts -to a remote cache with `lake cache put`. This will only include the artifacts -from the covered targets. Other targets in the package will not be tracked. -``` - - -::::paragraph - -The facets available for packages are: - -```lean -show --- Always keep this in sync with the description below. It ensures that the list is complete. -/-- -info: #[`package.barrel, `package.cache, `package.defaultModules, `package.deps, `package.extraDep, `package.optBarrel, - `package.optCache, `package.optRelease, `package.release, `package.transDeps] --/ -#guard_msgs in -#eval Lake.initPackageFacetConfigs.toList.map (·.1) |>.toArray |>.qsort (·.toString < ·.toString) -``` -: `extraDep` - - The default facets of the package's extra dependency targets, specified in the {tomlField Lake.PackageConfig}`extraDepTargets` field. - -: `deps` - - The package's {tech}[direct dependencies]. - -: `transDeps` - - The package's {tech}[transitive dependencies], topologically sorted. - -: `defaultModules` - - The Lean modules of the package's {tech}[default targets]: every module of each default library, and the root module of each default executable together with the modules it transitively imports from the workspace. - Other default targets, such as {ref "lake-config-custom-target"}[custom targets], are not included. - - -: `optCache` - - A package's optional cached build archive (e.g., from Reservoir or GitHub). - Will *not* cause the whole build to fail if the archive cannot be fetched. - -: `cache` - - A package's cached build archive (e.g., from Reservoir or GitHub). - Will cause the whole build to fail if the archive cannot be fetched. - -: `optBarrel` - - A package's optional cached build archive (e.g., from Reservoir or GitHub). - Will *not* cause the whole build to fail if the archive cannot be fetched. - -: `barrel` - - A package's cached build archive (e.g., from Reservoir or GitHub). - Will cause the whole build to fail if the archive cannot be fetched. - -: `optRelease` - - A package's optional build archive from a GitHub release. - Will *not* cause the whole build to fail if the release cannot be fetched. - -: `release` - - A package's build archive from a GitHub release. - Will cause the whole build to fail if the archive cannot be fetched. - - -:::: - -```lean -show --- Always keep this in sync with the description below. It ensures that the list is complete. -/-- -info: [`lean_lib.elabArts, `lean_lib.extraDep, `lean_lib.leanArts, `lean_lib.irArts, `lean_lib.static.export, - `lean_lib.shared, `lean_lib.modules, `lean_lib.static, `lean_lib.default] --/ -#guard_msgs in -#eval Lake.initLibraryFacetConfigs.toList.map (·.1) -``` - -:::paragraph - -The facets available for libraries are: +{include 2 Manual.BuildTools.Lake.PackageOverrides} -: `elabArts` +{include 0 Manual.BuildTools.Lake.Builds} - The library's elaboration artifacts (`*.olean` and `*.ilean` files). +{include 0 Manual.BuildTools.Lake.Cache} -: `irArts` (default) +{include 0 Manual.BuildTools.Lake.Scripts} - The library's code-generation artifacts (`*.ir`, `*.ir.sig`, and `*.c` files). - -: `leanArts` - - The artifacts that the Lean compiler produces for the library or executable ({tech (key := ".olean files")}`*.olean`, `*.ilean`, and `*.c` files). - -: `static` - - The static library produced by the C compiler from the `leanArts` (that is, a `*.a` file). - -: `static.export` - - The static library produced by the C compiler from the `leanArts` (that is, a `*.a` file), with exported symbols. - -: `shared` - - The shared library produced by the C compiler from the `leanArts` (that is, a `*.so`, `*.dll`, or `*.dylib` file, depending on the platform). - -: `extraDep` - - A Lean library's {tomlField Lake.LeanLibConfig}`extraDepTargets` and those of its package. - -::: - -:::paragraph - -Executables have a single `exe` facet that consists of the executable binary. - -::: - -```lean -show --- Always keep this in sync with the description below. It ensures that the list is complete. -/-- -info: module.bc -module.bc.o -module.c -module.c.o -module.c.o.export -module.c.o.noexport -module.depHash -module.depTrace -module.deps -module.dynlib -module.elabArts -module.exportInfo -module.header -module.ilean -module.importAllArts -module.importArts -module.importInfo -module.imports -module.input -module.ir -module.ir.sig -module.irArts -module.lean -module.leanArts -module.linkInfoExport -module.linkInfoNoExport -module.ltar -module.metaExportInfo -module.o -module.o.export -module.o.noexport -module.olean -module.olean.private -module.olean.server -module.precompileImports -module.presetup -module.setup -module.transImports --/ -#guard_msgs in -#eval Lake.initModuleFacetConfigs.toList.toArray.map (·.1) |>.qsort (·.toString < ·.toString) |>.forM (IO.println) -``` - -:::paragraph -The facets available for modules are: - -: `lean` - - The module's Lean source file. - -: `elabArts` - - The module's elaboration artifacts (`*.olean` and `*.ilean` files). - -: `irArts` (default) - - The module's code-generation artifacts (`*.ir`, `*.ir.sig`, and `*.c` files). - -: `leanArts` - - All artifacts produced by elaboration and code generation. - -: `deps` - - The module's dependencies (e.g., imports or shared libraries). - -: `depHash` - - A hash of a module's build dependencies (e.g., imports, source, plugins). - -: `depTrace` - - A Lake build trace data structure (i.e., composite hash and modification time) of a module's build dependencies (e.g., imports, source, plugins). - -: `olean` - - The module's {tech}[`.olean` file]. {TODO}[Once module system lands fully, add docs for `olean.private` and `olean.server`] - -: `ilean` - - The module's `.ilean` file, which is metadata used by the Lean language server. - -: `header` - - The parsed module header of the module's source file. - -: `input` - - The module's processed Lean source file. Combines tracing the file with parsing its header. - -: `imports` - - The immediate imports of the Lean module, but not the full set of transitive imports. {TODO}[Once the module system lands fully, add docs here for `module.importAllArts`, `module.importArts`] - -: `precompileImports` - - The transitive imports of the Lean module, compiled to object code. - -: `transImports` - - The transitive imports of the Lean module, as {tech}[`.olean` files]. - -: `allImports` - - Both the immediate and transitive imports of the Lean module. - -: `setup` - - All of a module's dependencies: transitive local imports and shared libraries to be loaded with `--load-dynlib`. - Returns the list of shared libraries to load along with their search path. - -: `ir` - - The `.ir` file produced for modules that use the {ref "module-structure"}[module system]. - - -: `ir.sig` - - The `.ir.sig` file produced for modules that use the {ref "module-structure"}[module system]. - -: `c` - - The C file produced by the Lean compiler. - -: `bc` - - LLVM bitcode file, produced by the Lean compiler. - -: `c.o` - - The compiled object file, produced from the C file. On Windows, this is equivalent to `.c.o.noexport`, while it is equivalent to `.c.o.export` on other platforms. - -: `c.o.export` - - The compiled object file, produced from the C file, with Lean symbols exported. - -: `c.o.noexport` - - The compiled object file, produced from the C file, without Lean symbols exported. - -: `bc.o` - - The compiled object file, produced from the LLVM bitcode file. - -: `o` - - The compiled object file for the configured backend. - -: `dynlib` - - A shared library (e.g., for the Lean option `--load-dynlib`){TODO}[Document Lean command line options, and cross-reference from here]. - -: `ltar` - - A compressed archive (produced via `leantar`) of the module's build artifacts. {TODO}[Document `leantar` in the manual as well] - -: `linkInfoExport` - - A structured representation of the linker arguments, static objects, and dynamic libraries needed to link a module and its dependencies. Objects have Lean symbols exported. - -: `linkInfoNoExport` - - A structured representation of the linker arguments, static objects, and dynamic libraries needed to link a module and its dependencies. Objects do not Lean symbols exported. - -::: - - -## Scripts -%%% -tag := "lake-scripts" -%%% - -Lake {tech}[package configuration] files may include {deftech}_Lake scripts_, which are embedded programs that can be executed from the command line. -Scripts are intended to be used for project-specific tasks that are not already well-served by Lake's other features. -While ordinary executable programs are run in the {name}`IO` {tech}[monad], scripts are run in {name Lake.ScriptM}`ScriptM`, which extends {name}`IO` with information about the workspace. -Because they are Lean definitions, Lake scripts can only be defined in the Lean configuration format. - -:::::TODO - -Restore the following once we can import enough of Lake to elaborate it - -```` -```lean -show -section -open Lake DSL -``` - -:::example "Listing Dependencies" - -This Lake script lists all the transitive dependencies of the root package, along with their Git URLs, in alphabetical order. -Similar scripts could be used to check declared licenses, discover which dependencies have test drivers configured, or compute metrics about the transitive dependency set over time. - -```lean -script "list-deps" := do - let mut results := #[] - for p in (← getWorkspace).packages do - if p.name ≠ (← getWorkspace).root.name then - results := results.push (p.name.toString, p.remoteUrl) - results := results.qsort (·.1 < ·.1) - IO.println "Dependencies:" - for (name, url) in results do - IO.println s!"{name}:\t{url}" - return 0 -``` -::: - -```lean -show -end -``` -```` - -::::: - -## Test and Lint Drivers -%%% -tag := "test-lint-drivers" -%%% - -A {deftech}_test driver_ runs the tests for a package. -It can be an executable target, a {tech}[Lake script], or a library. -Lake itself isn't a test framework: the {lake}`test` command just locates the configured target, builds it, and (for executables and scripts) runs it. -Library drivers are exercised purely by elaboration, so they aren't run as a separate step. -Assertions, test discovery, and reporting are up to the target itself, whether that's a third-party testing library or hand-written checks. - -For executables and scripts, Lake treats a nonzero exit code as a test failure. -For libraries, any elaboration error counts as a test failure, including failures of {keyword}`#guard`-style commands. - -A {deftech}_lint driver_ is similar, but it's run by {lake}`lint` and checks the package for stylistic issues and other problems that aren't _errors_ but indicate likely problems. -Lint drivers can only be executables or scripts, not libraries. - -### Configuring a Test Driver -%%% -tag := "lake-test-driver-config" -%%% - -In a `lakefile.toml`, set {tomlField Lake.PackageConfig}`testDriver` to the name of an executable target, library target, or script defined in the same configuration: - -:::::example "Test Driver (`lakefile.toml`)" - -::::lakeToml Lake.PackageConfig _root_ -```toml -name = "my-package" -testDriver = "my-package-tests" - -[[lean_exe]] -name = "my-package-tests" -root = "Tests" -``` -```expected -{wsIdx := 0, - baseName := `«my-package», - keyName := `«my-package», - origName := `«my-package», - dir := FilePath.mk ".", - relDir := FilePath.mk ".", - config := - {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, - toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - bootstrap := false, - extraDepTargets := #[], - precompileModules := false, - moreGlobalServerArgs := #[], - srcDir := FilePath.mk ".", - buildDir := FilePath.mk ".lake/build", - leanLibDir := FilePath.mk "lib/lean", - nativeLibDir := FilePath.mk "lib", - binDir := FilePath.mk "bin", - irDir := FilePath.mk "ir", - releaseRepo := none, - buildArchive := ELIDED, - preferReleaseBuild := false, - testDriver := "my-package-tests", - testDriverArgs := #[], - lintDriver := "", - lintDriverArgs := #[], - version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, - versionTags := { filter := #, name := `default, descr? := none}, - description := "", - keywords := #[], - homepage := "", - license := "", - licenseFiles := #[FilePath.mk "LICENSE"], - readmeFile := FilePath.mk "README.md", - reservoir := true, - enableArtifactCache? := none, - restoreAllArtifacts? := none, - libPrefixOnWindows := false, - allowImportAll := false, - builtinLint? := none, - checks := #[], - fixedToolchain := false}, - configFile := FilePath.mk "lakefile", - relConfigFile := FilePath.mk "lakefile", - relManifestFile := FilePath.mk "lake-manifest.json", - scope := "", - remoteUrl := "", - depConfigs := #[], - depIdxs := #[], - depPkgs := #[], - targetDecls := - #[{toConfigDecl := - {pkg := `«my-package», - name := `«my-package-tests», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Tests, - exeName := "my-package-tests", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}], - targetDeclMap := - {`«my-package-tests» ↦ - {toPConfigDecl := - {toConfigDecl := - {pkg := `«my-package», - name := `«my-package-tests», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Tests, - exeName := "my-package-tests", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}, - name_eq := …}, - }, - defaultTargets := #[], - scripts := {}, - defaultScripts := #[], - postUpdateHooks := #[], - buildArchive := ELIDED, - testDriver := "my-package-tests", - lintDriver := ""} -``` -:::: -::::: - -In a `lakefile.lean`, either set the {name Lake.Package.testDriver}`testDriver` field on the {keyword}`package` declaration (as above), or tag a script, executable, or library declaration with the {attr}`test_driver` attribute. -The attribute form is often convenient because it places the marker next to the target. - -:::::example "Test Driver (`lakefile.lean`)" - -::::lakeLean -```lean -import Lake -open Lake DSL - -package «my-package» where - testDriver := "my-package-tests" - -lean_exe «my-package-tests» where - root := `Tests -``` -```expected -{wsIdx := 0, - baseName := `«my-package», - keyName := Lean.Name.mkNum `«my-package» 0, - origName := `«my-package», - dir := FilePath.mk ".", - relDir := FilePath.mk ".", - config := - {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, - toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - bootstrap := false, - extraDepTargets := #[], - precompileModules := false, - moreGlobalServerArgs := #[], - srcDir := FilePath.mk ".", - buildDir := FilePath.mk ".lake/build", - leanLibDir := FilePath.mk "lib/lean", - nativeLibDir := FilePath.mk "lib", - binDir := FilePath.mk "bin", - irDir := FilePath.mk "ir", - releaseRepo := none, - buildArchive := ELIDED, - preferReleaseBuild := false, - testDriver := "my-package-tests", - testDriverArgs := #[], - lintDriver := "", - lintDriverArgs := #[], - version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, - versionTags := { filter := #, name := `default, descr? := none}, - description := "", - keywords := #[], - homepage := "", - license := "", - licenseFiles := #[FilePath.mk "LICENSE"], - readmeFile := FilePath.mk "README.md", - reservoir := true, - enableArtifactCache? := none, - restoreAllArtifacts? := none, - libPrefixOnWindows := false, - allowImportAll := false, - builtinLint? := none, - checks := #[], - fixedToolchain := false}, - configFile := FilePath.mk "lakefile.lean", - relConfigFile := FilePath.mk "lakefile.lean", - relManifestFile := FilePath.mk "lake-manifest.json", - scope := "", - remoteUrl := "", - depConfigs := #[], - depIdxs := #[], - depPkgs := #[], - targetDecls := - #[{toConfigDecl := - {pkg := Lean.Name.mkNum `«my-package» 0, - name := `«my-package-tests», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Tests, - exeName := "my-package-tests", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}], - targetDeclMap := - {`«my-package-tests» ↦ - {toPConfigDecl := - {toConfigDecl := - {pkg := Lean.Name.mkNum `«my-package» 0, - name := `«my-package-tests», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Tests, - exeName := "my-package-tests", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}, - name_eq := …}, - }, - defaultTargets := #[], - scripts := {}, - defaultScripts := #[], - postUpdateHooks := #[], - buildArchive := ELIDED, - testDriver := "my-package-tests", - lintDriver := ""} -``` -:::: -::::: - -Only one declaration per package can be tagged with {attr}`test_driver`. -It is an error to use both the {attr}`test_driver` attribute and a non-empty {name Lake.Package.testDriver}`testDriver` field in the same Lake configuration file. - -A test driver may also be a target in a package dependency that is transitively {tech (key:="require")}[required]. -To use a target from another package, use `/` as the value of `testDriver`, where `` is the name of the package in which the target is found.. - -### Running Tests -%%% -tag := "lake-test-running" -%%% - -The {lake}`test` command runs the configured driver for the {tech}[root package] only. -Test drivers for dependencies are not run. - -:::paragraph -If the test driver is an executable or a script, Lake passes the arguments from {tomlField Lake.PackageConfig}`testDriverArgs` first, then anything after `--` on the command line. -For example, - -``` -lake test -- --filter Foo --verbose -``` - -passes `--filter Foo --verbose` to the driver after whatever {tomlField Lake.PackageConfig}`testDriverArgs` is already configured. -Lake builds executable drivers before running them. -::: - -If the test driver is a library, arguments are not accepted. -Lake reports an error if {tomlField Lake.PackageConfig}`testDriverArgs` is non-empty or if any arguments follow `--`. -To run the tests, the library is just {tech (key:="Lean elaborator")}[elaborated]. - -{lake}`check-test` terminates with exit code 0 (that is, successfully) if a test driver is configured for the root package. -It doesn't check that the named target actually exists. - -### Lint Drivers -%%% -tag := "lake-lint-drivers" -%%% - -Lint drivers are configured and run similarly to {ref "lake-test-driver-config"}[test drivers]. -The Lake configuration file specifies a target that serves as the lint driver, and {lake}`lint` runs it. -This target must be an executable or a script; unlike test drivers, lint drivers may not be libraries. - -In a TOML-format Lake configuration file, the package-level field {tomlField Lake.PackageConfig}`lintDriver` specifies the name of the lint driver target. - -:::::example "Lint Driver (`lakefile.toml`)" -This minimal `lakefile.toml` configures a lint driver: - -::::lakeToml Lake.PackageConfig _root_ -```toml -name = "my-package" -lintDriver = "my-package-lint" - -[[lean_exe]] -name = "my-package-lint" -root = "Lint" -``` -```expected -{wsIdx := 0, - baseName := `«my-package», - keyName := `«my-package», - origName := `«my-package», - dir := FilePath.mk ".", - relDir := FilePath.mk ".", - config := - {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, - toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - bootstrap := false, - extraDepTargets := #[], - precompileModules := false, - moreGlobalServerArgs := #[], - srcDir := FilePath.mk ".", - buildDir := FilePath.mk ".lake/build", - leanLibDir := FilePath.mk "lib/lean", - nativeLibDir := FilePath.mk "lib", - binDir := FilePath.mk "bin", - irDir := FilePath.mk "ir", - releaseRepo := none, - buildArchive := ELIDED, - preferReleaseBuild := false, - testDriver := "", - testDriverArgs := #[], - lintDriver := "my-package-lint", - lintDriverArgs := #[], - version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, - versionTags := { filter := #, name := `default, descr? := none}, - description := "", - keywords := #[], - homepage := "", - license := "", - licenseFiles := #[FilePath.mk "LICENSE"], - readmeFile := FilePath.mk "README.md", - reservoir := true, - enableArtifactCache? := none, - restoreAllArtifacts? := none, - libPrefixOnWindows := false, - allowImportAll := false, - builtinLint? := none, - checks := #[], - fixedToolchain := false}, - configFile := FilePath.mk "lakefile", - relConfigFile := FilePath.mk "lakefile", - relManifestFile := FilePath.mk "lake-manifest.json", - scope := "", - remoteUrl := "", - depConfigs := #[], - depIdxs := #[], - depPkgs := #[], - targetDecls := - #[{toConfigDecl := - {pkg := `«my-package», - name := `«my-package-lint», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Lint, - exeName := "my-package-lint", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}], - targetDeclMap := - {`«my-package-lint» ↦ - {toPConfigDecl := - {toConfigDecl := - {pkg := `«my-package», - name := `«my-package-lint», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Lint, - exeName := "my-package-lint", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}, - name_eq := …}, - }, - defaultTargets := #[], - scripts := {}, - defaultScripts := #[], - postUpdateHooks := #[], - buildArchive := ELIDED, - testDriver := "", - lintDriver := "my-package-lint"} -``` -:::: -::::: - - -In a `lakefile.lean`, either set the {name Lake.Package.lintDriver}`lintDriver` field on the {keyword}`package` declaration, or tag a script or executable declaration with the {attr}`lint_driver` attribute. -The attribute form is often convenient because it places the marker next to the target. - -:::::example "Lint Driver (`lakefile.lean`)" - -::::lakeLean -```lean -import Lake -open Lake DSL - -package «my-package» where - lintDriver := "my-package-lint" - -lean_exe «my-package-lint» where - root := `Lint -``` -```expected -{wsIdx := 0, - baseName := `«my-package», - keyName := Lean.Name.mkNum `«my-package» 0, - origName := `«my-package», - dir := FilePath.mk ".", - relDir := FilePath.mk ".", - config := - {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, - toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - bootstrap := false, - extraDepTargets := #[], - precompileModules := false, - moreGlobalServerArgs := #[], - srcDir := FilePath.mk ".", - buildDir := FilePath.mk ".lake/build", - leanLibDir := FilePath.mk "lib/lean", - nativeLibDir := FilePath.mk "lib", - binDir := FilePath.mk "bin", - irDir := FilePath.mk "ir", - releaseRepo := none, - buildArchive := ELIDED, - preferReleaseBuild := false, - testDriver := "", - testDriverArgs := #[], - lintDriver := "my-package-lint", - lintDriverArgs := #[], - version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, - versionTags := { filter := #, name := `default, descr? := none}, - description := "", - keywords := #[], - homepage := "", - license := "", - licenseFiles := #[FilePath.mk "LICENSE"], - readmeFile := FilePath.mk "README.md", - reservoir := true, - enableArtifactCache? := none, - restoreAllArtifacts? := none, - libPrefixOnWindows := false, - allowImportAll := false, - builtinLint? := none, - checks := #[], - fixedToolchain := false}, - configFile := FilePath.mk "lakefile.lean", - relConfigFile := FilePath.mk "lakefile.lean", - relManifestFile := FilePath.mk "lake-manifest.json", - scope := "", - remoteUrl := "", - depConfigs := #[], - depIdxs := #[], - depPkgs := #[], - targetDecls := - #[{toConfigDecl := - {pkg := Lean.Name.mkNum `«my-package» 0, - name := `«my-package-lint», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Lint, - exeName := "my-package-lint", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}], - targetDeclMap := - {`«my-package-lint» ↦ - {toPConfigDecl := - {toConfigDecl := - {pkg := Lean.Name.mkNum `«my-package» 0, - name := `«my-package-lint», - kind := `lean_exe, - config := - {toLeanConfig := - { buildType := Lake.BuildType.release, - leanOptions := #[], - moreLeanArgs := #[], - weakLeanArgs := #[], - moreLeancArgs := #[], - moreServerOptions := #[], - weakLeancArgs := #[], - moreLinkObjs := #[], - moreLinkLibs := #[], - moreLinkArgs := #[], - weakLinkArgs := #[], - backend := Lake.Backend.default, - platformIndependent := none, - precompileImports := false, - dynlibs := #[], - plugins := #[], - requiresModuleSystem := false, - allowNonModules := false }, - srcDir := FilePath.mk ".", - root := `Lint, - exeName := "my-package-lint", - needs := #[], - extraDepTargets := #[], - supportInterpreter := false, - nativeFacets := #}, - wf_data := …}, - pkg_eq := …}, - name_eq := …}, - }, - defaultTargets := #[], - scripts := {}, - defaultScripts := #[], - postUpdateHooks := #[], - buildArchive := ELIDED, - testDriver := "", - lintDriver := "my-package-lint"} -``` -:::: -::::: - -Only one declaration per package can be tagged with {attr}`lint_driver`. -It is an error to use both the {attr}`lint_driver` attribute and a non-empty {name Lake.Package.lintDriver}`lintDriver` field in the same Lake configuration file. - -:::lakeSession -show -```lean +lakefile -import Lake -open Lake DSL -package p - -@[lint_driver] -lean_exe Foo where - -@[lint_driver] -lean_exe Bar where -``` -```lakeCmd "lake build" +error -error: p: only one script or executable can be tagged @[lint_driver] -``` -::: - -A lint driver in a dependency package can be referenced with the same `/` syntax used for test drivers. - -{lake}`lint` runs the configured driver, passing {tomlField Lake.PackageConfig}`lintDriverArgs` first, then anything after `--` on the command line: - -``` -lake lint -- --warnings-as-errors -``` - -Lake also has a separate {deftech}_builtin linter_ that operates on Lean modules directly, independent of any configured driver. -Builtin linting is enabled by the `--builtin-lint` and related flags (see {lake}`lint`), or by setting {tomlField Lake.PackageConfig}`builtinLint` to `true` in the package configuration. -When builtin linting is active, positional `MODULE` arguments before `--` select which modules to lint, and they are _not_ passed to the configured driver. -So `lake lint Mathlib` triggers builtin linting on `Mathlib`, whereas `lake lint -- Mathlib` passes `Mathlib` to the driver. -The two mechanisms are independent and can run together: when both apply, Lake runs the builtin linter first and then the driver. - -{lake}`check-lint` exits with code 0 (that is, successfully) if a lint driver is configured for the root package or if {tomlField Lake.PackageConfig}`builtinLint` is set to `true` in its configuration. - - -## GitHub Release Builds -%%% -tag := "lake-github" -%%% - -Lake supports uploading and downloading build artifacts (i.e., the archived build directory) to/from the GitHub releases of packages. -This enables end users to fetch pre-built artifacts from the cloud without needed to rebuild the package from source themselves. -The {envVar}`LAKE_NO_CACHE` environment variable can be used to disable this feature. - -### Downloading - -To download artifacts, one should configure the package options `releaseRepo` and `buildArchive` to point to the GitHub repository hosting the release and the correct artifact name within it (if the defaults are not sufficient). -Then, set `preferReleaseBuild := true` to tell Lake to fetch and unpack it as an extra package dependency. - -Lake will only fetch release builds as part of its standard build process if the package wanting it is a dependency (as the root package is expected to modified and thus not often compatible with this scheme). -However, should one wish to fetch a release for a root package (e.g., after cloning the release's source but before editing), one can manually do so via `lake build :release`. - -Lake internally uses `curl` to download the release and `tar` to unpack it, so the end user must have both tools installed in order to use this feature. -If Lake fails to fetch a release for any reason, it will move on to building from the source. -This mechanism is not technically limited to GitHub: any Git host that uses the same URL scheme works as well. - -### Uploading - -To upload a built package as an artifact to a GitHub release, Lake provides the {lake}`upload` command as a convenient shorthand. -This command uses `tar` to pack the package's build directory into an archive and uses `gh release upload` to attach it to a pre-existing GitHub release for the specified tag. -Thus, in order to use it, the package uploader (but not the downloader) needs to have `gh`, the GitHub CLI, installed and in `PATH`. - -## Artifact Caches -%%% -tag := "lake-cache" -%%% - -*This is an experimental feature that is still undergoing development.* - -Lake supports a {deftech (key := "local cache")}_local artifact cache_ that stores individual build products, tracking the complete set of inputs that gave rise to them. -Each {tech}[toolchain] has its own cache because intermediate build products are not compatible between toolchain versions. -However, a toolchain's cache is shared between all local {tech}[workspaces] that use it, so common dependencies don't need to be rebuilt. -If two separate workspaces with the same toolchain depend on the same package, then they can share each others' build products. - -Because it is an experimental feature, the local cache is disabled by default. -It is only enabled when the {envVar}`LAKE_ARTIFACT_CACHE` environment variable is set to `true` or when the {TODO}[ref] `enableArtifactCache` field is set to `true` in the {ref "lake-config"}[configuration file]. - - -### Remote Artifact Caches -%%% -tag := "lake-cache-remote" -%%% - -Build products can be retrieved from remote cache servers and placed into the local cache. -This makes it possible to completely avoid local builds. -The {lake}`cache get` command is used to download artifacts into the local cache. - -Compared to {ref "lake-github"}[GitHub release builds], the remote artifact cache is much more fine-grained. -It tracks build products at the level of individual source files, {tech}[`.olean` files], and object code, rather than at the level of entire packages. - -### Mappings - -When passed the `-o` option, {lake}`build` tracks the inputs used to generate each build product. -These are stored to a {deftech}_mappings file_ in JSON lines format, where each line of the file must be a valid JSON object. -A mappings file tracks a single package within a build, and includes all intermediate and final build products from the package that are part of the build. - -By default, {lake}`build` saves the workspace's {tech}[root package]'s mappings. -The {lakeOpt}`--package` option selects a different package in the workspace, such as a dependency, saving its mappings instead. -The tracked build products include those that were already up to date and not regenerated, but not the package's targets that the build did not cover. -The {lake}`cache put` command uploads the build products in the mappings file from the local cache to the remote cache. - -### Configuration - -:::paragraph -Remote artifact caches are configured using the following environment variables: - * {envVar}`LAKE_CACHE_KEY` - * {envVar}`LAKE_CACHE_ARTIFACT_ENDPOINT` - * {envVar}`LAKE_CACHE_REVISION_ENDPOINT` -::: +{include 0 Manual.BuildTools.Lake.Drivers} {include 0 Manual.BuildTools.Lake.CLI} {include 0 Manual.BuildTools.Lake.Config} -# Script API Reference -%%% -tag := "lake-api" -%%% - -In addition to ordinary {lean}`IO` effects, Lake scripts have access to the Lake environment (which provides information about the current toolchain, such as the location of the Lean compiler) and the current workspace. -This access is provided in {name Lake.ScriptM}`ScriptM`. - -{docstring Lake.ScriptM} - -## Accessing the Environment - -Monads that provide access to information about the current Lake environment (such as the locations of Lean, Lake, and other tools) have {name Lake.MonadLakeEnv}`MonadLakeEnv` instances. -This is true for all of the monads in the Lake API, including {name Lake.ScriptM}`ScriptM`. - -{docstring Lake.MonadLakeEnv} - -{docstring Lake.getLakeEnv} - -{docstring Lake.getNoCache} - -{docstring Lake.getTryCache} - -{docstring Lake.getPkgUrlMap} - -{docstring Lake.getElanToolchain} - -### Search Path Helpers - -{docstring Lake.getEnvLeanPath} - -{docstring Lake.getEnvLeanSrcPath} - -{docstring Lake.getEnvSharedLibPath} - -### Elan Install Helpers - -{docstring Lake.getElanInstall?} - -{docstring Lake.getElanHome?} - -{docstring Lake.getElan?} - -### Lean Install Helpers - -{docstring Lake.getLeanInstall} - -{docstring Lake.getLeanSysroot} - -{docstring Lake.getLeanSrcDir} - -{docstring Lake.getLeanLibDir} - -{docstring Lake.getLeanIncludeDir} - -{docstring Lake.getLeanSystemLibDir} - -{docstring Lake.getLean} - -{docstring Lake.getLeanc} - -{docstring Lake.getLeanSharedLib} - -{docstring Lake.getLeanAr} - -{docstring Lake.getLeanCc} - -{docstring Lake.getLeanCc?} - -### Lake Install Helpers - -{docstring Lake.getLakeInstall} - -{docstring Lake.getLakeHome} - -{docstring Lake.getLakeSrcDir} - -{docstring Lake.getLakeLibDir} - -{docstring Lake.getLake} - -## Accessing the Workspace - -Monads that provide access to information about the current Lake workspace have {name Lake.MonadWorkspace}`MonadWorkspace` instances. -In particular, there are instances for {name Lake.ScriptM}`ScriptM` and {name Lake.LakeM}`LakeM`. - -```lean -show -section -open Lake -#synth MonadWorkspace ScriptM - -end -``` - -{docstring Lake.MonadWorkspace} - -{docstring Lake.getRootPackage} - -{docstring Lake.findPackageByName?} - -{docstring Lake.findPackageByKey?} - -{docstring Lake.findModule?} - -{docstring Lake.findLeanExe?} - -{docstring Lake.findLeanLib?} - -{docstring Lake.findExternLib?} - -{docstring Lake.getLeanPath} - -{docstring Lake.getLeanSrcPath} - -{docstring Lake.getSharedLibPath} - -{docstring Lake.getAugmentedLeanPath} - -{docstring Lake.getAugmentedLeanSrcPath } - -{docstring Lake.getAugmentedSharedLibPath} - -{docstring Lake.getAugmentedEnv} +{include 0 Manual.BuildTools.Lake.API} diff --git a/Manual/BuildTools/Lake/API.lean b/Manual/BuildTools/Lake/API.lean new file mode 100644 index 000000000..a4e31c27e --- /dev/null +++ b/Manual/BuildTools/Lake/API.lean @@ -0,0 +1,147 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual + +import Lean.Parser.Command +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Module + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Verso.Genre.Manual.InlineLean + +set_option guard_msgs.diff true + +open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode + +#doc (Manual) "Script API Reference" => +%%% +tag := "lake-api" +%%% + +In addition to ordinary {lean}`IO` effects, Lake scripts have access to the Lake environment (which provides information about the current toolchain, such as the location of the Lean compiler) and the current workspace. +This access is provided in {name Lake.ScriptM}`ScriptM`. + +{docstring Lake.ScriptM} + +# Accessing the Environment + +Monads that provide access to information about the current Lake environment (such as the locations of Lean, Lake, and other tools) have {name Lake.MonadLakeEnv}`MonadLakeEnv` instances. +This is true for all of the monads in the Lake API, including {name Lake.ScriptM}`ScriptM`. + +{docstring Lake.MonadLakeEnv} + +{docstring Lake.getLakeEnv} + +{docstring Lake.getNoCache} + +{docstring Lake.getTryCache} + +{docstring Lake.getPkgUrlMap} + +{docstring Lake.getElanToolchain} + +## Search Path Helpers + +{docstring Lake.getEnvLeanPath} + +{docstring Lake.getEnvLeanSrcPath} + +{docstring Lake.getEnvSharedLibPath} + +## Elan Install Helpers + +{docstring Lake.getElanInstall?} + +{docstring Lake.getElanHome?} + +{docstring Lake.getElan?} + +## Lean Install Helpers + +{docstring Lake.getLeanInstall} + +{docstring Lake.getLeanSysroot} + +{docstring Lake.getLeanSrcDir} + +{docstring Lake.getLeanLibDir} + +{docstring Lake.getLeanIncludeDir} + +{docstring Lake.getLeanSystemLibDir} + +{docstring Lake.getLean} + +{docstring Lake.getLeanc} + +{docstring Lake.getLeanSharedLib} + +{docstring Lake.getLeanAr} + +{docstring Lake.getLeanCc} + +{docstring Lake.getLeanCc?} + +## Lake Install Helpers + +{docstring Lake.getLakeInstall} + +{docstring Lake.getLakeHome} + +{docstring Lake.getLakeSrcDir} + +{docstring Lake.getLakeLibDir} + +{docstring Lake.getLake} + +# Accessing the Workspace + +Monads that provide access to information about the current Lake workspace have {name Lake.MonadWorkspace}`MonadWorkspace` instances. +In particular, there are instances for {name Lake.ScriptM}`ScriptM` and {name Lake.LakeM}`LakeM`. + +```lean -show +section +open Lake +#synth MonadWorkspace ScriptM + +end +``` + +{docstring Lake.MonadWorkspace} + +{docstring Lake.getRootPackage} + +{docstring Lake.findPackageByName?} + +{docstring Lake.findPackageByKey?} + +{docstring Lake.findModule?} + +{docstring Lake.findLeanExe?} + +{docstring Lake.findLeanLib?} + +{docstring Lake.findExternLib?} + +{docstring Lake.getLeanPath} + +{docstring Lake.getLeanSrcPath} + +{docstring Lake.getSharedLibPath} + +{docstring Lake.getAugmentedLeanPath} + +{docstring Lake.getAugmentedLeanSrcPath } + +{docstring Lake.getAugmentedSharedLibPath} + +{docstring Lake.getAugmentedEnv} diff --git a/Manual/BuildTools/Lake/Builds.lean b/Manual/BuildTools/Lake/Builds.lean new file mode 100644 index 000000000..f2d92b838 --- /dev/null +++ b/Manual/BuildTools/Lake/Builds.lean @@ -0,0 +1,432 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual + +import Lean.Parser.Command +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Module + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Verso.Genre.Manual.InlineLean + +set_option guard_msgs.diff true + +#doc (Manual) "Builds" => + +:::paragraph +Producing a desired {tech}[artifact], such as a {tech}[`.olean` file] or an executable binary, is called a {deftech}_build_. +Builds are triggered by the {lake}`build` command or by other commands that require an artifact to be present, such as {lake}`exe`. +A build consists of the following steps: + +: {deftech (key := "configure package")}[Configuring] the package + + If {tech}[package configuration] file is newer than the cached configuration file `lakefile.olean`, then the package configuration is re-elaborated. + This also occurs when the cached file is missing or when the {lakeOpt}`--reconfigure` or {lakeOpt}`-R` flag is provided. + Changes to options using {lakeOpt}`-K` do not trigger re-elaboration of the configuration file; {lakeOpt}`-R` is necessary in these cases. + +: Computing dependencies + + The set of artifacts that are required to produce the desired output are determined, along with the {tech}[targets] and {tech}[facets] that produce them. + This process is recursive, and the result is a _graph_ of dependencies. + The dependencies in this graph are distinct from those declared for a package: packages depend on other packages, while build targets depend on other build targets, which may be in the same package or in a different one. + One facet of a given target may depend on other facets of the same target. + Lake automatically analyzes the imports of Lean modules to discover their dependencies, and the {tomlField Lake.LeanLibConfig}`extraDepTargets` field can be used to add additional dependencies to a target. + +: Replaying traces + + Rather than rebuilding everything in the dependency graph from scratch, Lake uses saved {deftech}_trace files_ to determine which artifacts require building. + During a build, Lake records which source files or other artifacts were used to produce each artifact, saving a hash of each input; these {deftech}_traces_ are saved in the {tech}[build directory].{margin}[More specifically, each artifact's trace file contains a Merkle tree hash mixture of its inputs' hashes.] + If the inputs are all unmodified, then the corresponding artifact is not rebuilt. + Trace files additionally record the {tech}[log] from each build task; these outputs are replayed as if the artifact had been built anew. + Reusing prior build products when possible is called an {deftech}_incremental build_. + +: Building artifacts + + When all unmodified dependencies in the dependency graph have been replayed from their trace files, Lake proceeds to build each artifact. + This involves running the appropriate build tool on the input files and saving the artifact and its trace file, as specified in the corresponding facet. +::: + +Lake uses two separate hash algorithms. +Text files are hashed after normalizing newlines, so that files that differ only by platform-specific newline conventions are hashed identically. +Other files are hashed without any normalization. + +Along with the trace files, Lean caches input hashes. +Whenever an artifact is built, its hash is saved in a separate file that can be re-read instead of computing the hash from scratch. +This is a performance optimization. +This feature can be disabled, causing all hashes to be recomputed from their inputs, using the {lakeOpt}`--rehash` command-line option. + +:::paragraph +During a build, the following directories are provided to the underlying build tools: + * The {deftech}_source directory_ contains Lean source code that is available for import. + * The {deftech}_library directories_ contain {tech}[`.olean` files] along with the shared and static libraries that are available for linking; it normally consists of the {tech}[root package]'s library directory (found in `.lake/build/lib`), the library directories for the other packages in the workspace, the library directory for the current Lean toolchain, and the system library directory. + * The {deftech}_Lake home_ is the directory in which Lake is installed, including binaries, source code, and libraries. + The libraries in the Lake home are needed to elaborate Lake configuration files, which have access to the full power of Lean. +::: + +# Facets +%%% +tag := "lake-facets" +%%% + +A {deftech}_facet_ describes the production of a target from another. +Conceptually, any target may have facets. +However, executables, external libraries, and custom targets provide only a single implicit facet. +Packages, libraries, and modules have multiple facets that can be requested by name when invoking {lake}`build` to select the corresponding target. + +When no facet is explicitly requested, but an initial target is designated, {lake}`build` produces the initial target's {deftech}_default facet_. +Each type of initial target has a corresponding default facet (e.g. producing an executable binary from an executable target or building a package's {tech}[default targets]); other facets may be explicitly requested in the {tech}[package configuration] or via Lake's {ref "lake-cli"}[command-line interface]. +Lake's internal API may be used to write custom facets. + + +```lakeHelp "build" +Build targets + +USAGE: + lake build [...] [-o ] [--package ] + +A target is specified with a string of the form: + + [@[]/][|[+]][:] + +You can also use the source path of a module as a target. For example, + + lake build Foo/Bar.lean:o + +will build the Lean module (within the workspace) whose source file is +`Foo/Bar.lean` and compile the generated C file into a native object file. + +The `@` and `+` markers can be used to disambiguate packages and modules +from file paths or other kinds of targets (e.g., executables or libraries). + +LIBRARY FACETS: build the library's ... + elabArts elaboration artifacts (*.olean, *.ilean files) + irArts (default) compilation artifacts (*.ir, *.ir.sig, *.c files) + static static artifact (*.a file) + shared shared artifact (*.so, *.dll, or *.dylib file) + +MODULE FACETS: build the module's ... + deps dependencies (e.g., imports, shared libraries, etc.) + elabArts elaboration artifacts (*.olean, *.ilean files) + irArts (default) compilation artifacts (*.ir, *.ir.sig, *.c files) + olean OLean (binary blob of Lean data for importers) + ilean ILean (binary blob of metadata for the Lean LSP server) + c compiled C file + bc compiled LLVM bitcode file + c.o compiled object file (of its C file) + bc.o compiled object file (of its LLVM bitcode file) + o compiled object file (of its configured backend) + dynlib shared library (e.g., for `--load-dynlib`) + +TARGET EXAMPLES: build the ... + a default facet(s) of target `a` + @a default target(s) of package `a` + +A default facet(s) of module `A` + @/a default facet(s) of target `a` of the root package + @a/b default facet(s) of target `b` of package `a` + @a/+A:c C file of module `A` of package `a` + :foo facet `foo` of the root package + +A bare `lake build` command will build the default target(s) of the root +package. Package dependencies are not updated during a build. + +With the Lake cache enabled, Lake can track the targets the build covers +(both those up-to-date and those newly built) and write the input-to-outputs +mappings of each to a file specified by the `-o` option. By default, with `-o`, +Lake will track the targets of the root package, use `--package` to select a +different one. These mappings can then be used to upload the build artifacts +to a remote cache with `lake cache put`. This will only include the artifacts +from the covered targets. Other targets in the package will not be tracked. +``` + + +::::paragraph + +The facets available for packages are: + +```lean -show +-- Always keep this in sync with the description below. It ensures that the list is complete. +/-- +info: #[`package.barrel, `package.cache, `package.defaultModules, `package.deps, `package.extraDep, `package.optBarrel, + `package.optCache, `package.optRelease, `package.release, `package.transDeps] +-/ +#guard_msgs in +#eval Lake.initPackageFacetConfigs.toList.map (·.1) |>.toArray |>.qsort (·.toString < ·.toString) +``` +: `extraDep` + + The default facets of the package's extra dependency targets, specified in the {tomlField Lake.PackageConfig}`extraDepTargets` field. + +: `deps` + + The package's {tech}[direct dependencies]. + +: `transDeps` + + The package's {tech}[transitive dependencies], topologically sorted. + +: `defaultModules` + + The Lean modules of the package's {tech}[default targets]: every module of each default library, and the root module of each default executable together with the modules it transitively imports from the workspace. + Other default targets, such as {ref "lake-config-custom-target"}[custom targets], are not included. + + +: `optCache` + + A package's optional cached build archive (e.g., from Reservoir or GitHub). + Will *not* cause the whole build to fail if the archive cannot be fetched. + +: `cache` + + A package's cached build archive (e.g., from Reservoir or GitHub). + Will cause the whole build to fail if the archive cannot be fetched. + +: `optBarrel` + + A package's optional cached build archive (e.g., from Reservoir or GitHub). + Will *not* cause the whole build to fail if the archive cannot be fetched. + +: `barrel` + + A package's cached build archive (e.g., from Reservoir or GitHub). + Will cause the whole build to fail if the archive cannot be fetched. + +: `optRelease` + + A package's optional build archive from a GitHub release. + Will *not* cause the whole build to fail if the release cannot be fetched. + +: `release` + + A package's build archive from a GitHub release. + Will cause the whole build to fail if the archive cannot be fetched. + + +:::: + +```lean -show +-- Always keep this in sync with the description below. It ensures that the list is complete. +/-- +info: [`lean_lib.elabArts, `lean_lib.extraDep, `lean_lib.leanArts, `lean_lib.irArts, `lean_lib.static.export, + `lean_lib.shared, `lean_lib.modules, `lean_lib.static, `lean_lib.default] +-/ +#guard_msgs in +#eval Lake.initLibraryFacetConfigs.toList.map (·.1) +``` + +:::paragraph + +The facets available for libraries are: + +: `elabArts` + + The library's elaboration artifacts (`*.olean` and `*.ilean` files). + +: `irArts` (default) + + The library's code-generation artifacts (`*.ir`, `*.ir.sig`, and `*.c` files). + +: `leanArts` + + The artifacts that the Lean compiler produces for the library or executable ({tech (key := ".olean files")}`*.olean`, `*.ilean`, and `*.c` files). + +: `static` + + The static library produced by the C compiler from the `leanArts` (that is, a `*.a` file). + +: `static.export` + + The static library produced by the C compiler from the `leanArts` (that is, a `*.a` file), with exported symbols. + +: `shared` + + The shared library produced by the C compiler from the `leanArts` (that is, a `*.so`, `*.dll`, or `*.dylib` file, depending on the platform). + +: `extraDep` + + A Lean library's {tomlField Lake.LeanLibConfig}`extraDepTargets` and those of its package. + +::: + +:::paragraph + +Executables have a single `exe` facet that consists of the executable binary. + +::: + +```lean -show +-- Always keep this in sync with the description below. It ensures that the list is complete. +/-- +info: module.bc +module.bc.o +module.c +module.c.o +module.c.o.export +module.c.o.noexport +module.depHash +module.depTrace +module.deps +module.dynlib +module.elabArts +module.exportInfo +module.header +module.ilean +module.importAllArts +module.importArts +module.importInfo +module.imports +module.input +module.ir +module.ir.sig +module.irArts +module.lean +module.leanArts +module.linkInfoExport +module.linkInfoNoExport +module.ltar +module.metaExportInfo +module.o +module.o.export +module.o.noexport +module.olean +module.olean.private +module.olean.server +module.precompileImports +module.presetup +module.setup +module.transImports +-/ +#guard_msgs in +#eval Lake.initModuleFacetConfigs.toList.toArray.map (·.1) |>.qsort (·.toString < ·.toString) |>.forM (IO.println) +``` + +:::paragraph +The facets available for modules are: + +: `lean` + + The module's Lean source file. + +: `elabArts` + + The module's elaboration artifacts (`*.olean` and `*.ilean` files). + +: `irArts` (default) + + The module's code-generation artifacts (`*.ir`, `*.ir.sig`, and `*.c` files). + +: `leanArts` + + All artifacts produced by elaboration and code generation. + +: `deps` + + The module's dependencies (e.g., imports or shared libraries). + +: `depHash` + + A hash of a module's build dependencies (e.g., imports, source, plugins). + +: `depTrace` + + A Lake build trace data structure (i.e., composite hash and modification time) of a module's build dependencies (e.g., imports, source, plugins). + +: `olean` + + The module's {tech}[`.olean` file]. {TODO}[Once module system lands fully, add docs for `olean.private` and `olean.server`] + +: `ilean` + + The module's `.ilean` file, which is metadata used by the Lean language server. + +: `header` + + The parsed module header of the module's source file. + +: `input` + + The module's processed Lean source file. Combines tracing the file with parsing its header. + +: `imports` + + The immediate imports of the Lean module, but not the full set of transitive imports. {TODO}[Once the module system lands fully, add docs here for `module.importAllArts`, `module.importArts`] + +: `precompileImports` + + The transitive imports of the Lean module, compiled to object code. + +: `transImports` + + The transitive imports of the Lean module, as {tech}[`.olean` files]. + +: `allImports` + + Both the immediate and transitive imports of the Lean module. + +: `setup` + + All of a module's dependencies: transitive local imports and shared libraries to be loaded with `--load-dynlib`. + Returns the list of shared libraries to load along with their search path. + +: `ir` + + The `.ir` file produced for modules that use the {ref "module-structure"}[module system]. + + +: `ir.sig` + + The `.ir.sig` file produced for modules that use the {ref "module-structure"}[module system]. + +: `c` + + The C file produced by the Lean compiler. + +: `bc` + + LLVM bitcode file, produced by the Lean compiler. + +: `c.o` + + The compiled object file, produced from the C file. On Windows, this is equivalent to `.c.o.noexport`, while it is equivalent to `.c.o.export` on other platforms. + +: `c.o.export` + + The compiled object file, produced from the C file, with Lean symbols exported. + +: `c.o.noexport` + + The compiled object file, produced from the C file, without Lean symbols exported. + +: `bc.o` + + The compiled object file, produced from the LLVM bitcode file. + +: `o` + + The compiled object file for the configured backend. + +: `dynlib` + + A shared library (e.g., for the Lean option `--load-dynlib`){TODO}[Document Lean command line options, and cross-reference from here]. + +: `ltar` + + A compressed archive (produced via `leantar`) of the module's build artifacts. {TODO}[Document `leantar` in the manual as well] + +: `linkInfoExport` + + A structured representation of the linker arguments, static objects, and dynamic libraries needed to link a module and its dependencies. Objects have Lean symbols exported. + +: `linkInfoNoExport` + + A structured representation of the linker arguments, static objects, and dynamic libraries needed to link a module and its dependencies. Objects do not Lean symbols exported. + +::: diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index 0952a3cba..3f4a29ae0 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -553,7 +553,7 @@ Module targets may also be specified by their filename, with an optional facet a The available {tech}[facets] depend on whether a package, library, executable, or module is to be built. They are listed in {ref "lake-facets"}[the section on facets]. -When using the {ref "lake-cache"}[local artifact cache], the {lakeOptDef option}`-o` option saves a {tech}[mappings file] that tracks the inputs and outputs of each step in the build. +When using the {ref "lake-cache-local"}[local artifact cache], the {lakeOptDef option}`-o` option saves a {tech}[mappings file] that tracks the inputs and outputs of each step in the build. The mappings file describes the targets from one package that are included in the build, restricted to the {tech}[root package] by default. Targets that were already up to date are included in the mappings file. The {lakeOptDef option}`--package` option causes the named package's targets to be written to the mappings file instead of the root package's targets, which makes it possible to upload build outputs for a dependency. @@ -1563,7 +1563,7 @@ If {lakeMeta}`archive.tgz` is not specified, the package's `buildArchive` settin # Local Caches {lake}`cache get`, {lake}`cache put`, and {lake}`cache add` are used to interact with remote cache servers. -These commands are *experimental*, and are only useful if the {ref "lake-cache"}[local cache] is enabled. +These commands are *experimental*, and are only useful if the {ref "lake-cache-local"}[local cache] is enabled. These commands can be configured to use a {deftech}[cache scope], which is a server-specific identifier for a set of build outputs for a package. On Reservoir, scopes are currently identical with GitHub repositories, but may include toolchain and platform information in the future. diff --git a/Manual/BuildTools/Lake/Cache.lean b/Manual/BuildTools/Lake/Cache.lean new file mode 100644 index 000000000..a29bb5ae4 --- /dev/null +++ b/Manual/BuildTools/Lake/Cache.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen, Mac Malone +-/ + +import VersoManual + +import Lean.Parser.Command +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Module + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Verso.Genre.Manual.InlineLean + +set_option guard_msgs.diff true + +#doc (Manual) "Caching Builds" => +%%% +tag := "lake-cache" +%%% + +Builds of large packages can consume significant time. +Compounding this, switching between local development branches can cause Lake to rebuild the same code many times. +To address these problems, Lake provides a number of ways to {deftech (key := "build cache")}_cache_ builds for later reuse. +Lake's {ref "lake-cache-local"}[local artifact cache] enables reuse of builds when switching between branches and across multiple local copies of the same package. +The {ref "lake-cache-remote"}[remote artifact cache] expands this to sharing artifact caches across machines. However, it requires the package developers to own cloud storage. +As an alternative for developers without cloud storage but already using GitHub, {ref "lake-github"}[release builds] provide a low-setup way to ship complete builds to users. + +# Artifact Caches +%%% +tag := "lake-cache-local" +%%% + +*This is an experimental feature that is still undergoing development.* + +Lake supports a {deftech (key := "local cache")}_local artifact cache_ that stores individual build products, tracking the complete set of inputs that gave rise to them. +Each {tech}[toolchain] has its own cache because intermediate build products are not compatible between toolchain versions. +However, a toolchain's cache is shared between all local {tech}[workspaces] that use it, so common dependencies don't need to be rebuilt. +If two separate workspaces with the same toolchain depend on the same package, then they can share each others' build products. + +Because it is an experimental feature, the local cache is disabled by default. +It is only enabled when the {envVar}`LAKE_ARTIFACT_CACHE` environment variable is set to `true` or when the {TODO}[ref] `enableArtifactCache` field is set to `true` in the {ref "lake-config"}[configuration file]. + + +# Remote Artifact Caches +%%% +tag := "lake-cache-remote" +%%% + +Build products can be retrieved from remote cache servers and placed into the local cache. +This makes it possible to completely avoid local builds. +The {lake}`cache get` command is used to download artifacts into the local cache. + +Compared to {ref "lake-github"}[GitHub release builds], the remote artifact cache is much more fine-grained. +It tracks build products at the level of individual source files, {tech}[`.olean` files], and object code, rather than at the level of entire packages. + +## Mappings + +When passed the `-o` option, {lake}`build` tracks the inputs used to generate each build product. +These are stored to a {deftech}_mappings file_ in JSON lines format, where each line of the file must be a valid JSON object. +A mappings file tracks a single package within a build, and includes all intermediate and final build products from the package that are part of the build. + +By default, {lake}`build` saves the workspace's {tech}[root package]'s mappings. +The {lakeOpt}`--package` option selects a different package in the workspace, such as a dependency, saving its mappings instead. +The tracked build products include those that were already up to date and not regenerated, but not the package's targets that the build did not cover. +The {lake}`cache put` command uploads the build products in the mappings file from the local cache to the remote cache. + +## Configuration + +:::paragraph +Remote artifact caches are configured using the following environment variables: + * {envVar}`LAKE_CACHE_KEY` + * {envVar}`LAKE_CACHE_ARTIFACT_ENDPOINT` + * {envVar}`LAKE_CACHE_REVISION_ENDPOINT` +::: + +# GitHub Release Builds +%%% +tag := "lake-github" +%%% + +Lake supports uploading and downloading the complete set of build artifacts (i.e., the archived build directory) to/from the GitHub releases of packages. +This enables end users to fetch pre-built artifacts from the cloud without needed to rebuild the package from source themselves. +The {envVar}`LAKE_NO_CACHE` environment variable can be used to disable this feature. + +## Downloading + +To download artifacts, one should configure the package options `releaseRepo` and `buildArchive` to point to the GitHub repository hosting the release and the correct artifact name within it (if the defaults are not sufficient). +Then, set `preferReleaseBuild := true` to tell Lake to fetch and unpack it as an extra package dependency. + +Lake will only fetch release builds as part of its standard build process if the package wanting it is a dependency (as the root package is expected to modified and thus not often compatible with this scheme). +However, should one wish to fetch a release for a root package (e.g., after cloning the release's source but before editing), one can manually do so via `lake build :release`. + +Lake internally uses `curl` to download the release and `tar` to unpack it, so the end user must have both tools installed in order to use this feature. +If Lake fails to fetch a release for any reason, it will move on to building from the source. +This mechanism is not technically limited to GitHub: any Git host that uses the same URL scheme works as well. + +## Uploading + +To upload a built package as an artifact to a GitHub release, Lake provides the {lake}`upload` command as a convenient shorthand. +This command uses `tar` to pack the package's build directory into an archive and uses `gh release upload` to attach it to a pre-existing GitHub release for the specified tag. +Thus, in order to use it, the package uploader (but not the downloader) needs to have `gh`, the GitHub CLI, installed and in `PATH`. diff --git a/Manual/BuildTools/Lake/Drivers.lean b/Manual/BuildTools/Lake/Drivers.lean new file mode 100644 index 000000000..7d8ba5c91 --- /dev/null +++ b/Manual/BuildTools/Lake/Drivers.lean @@ -0,0 +1,789 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual + +import Lean.Parser.Command +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Module + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Verso.Genre.Manual.InlineLean + +set_option guard_msgs.diff true + +#doc (Manual) "Test and Lint Drivers" => +%%% +tag := "test-lint-drivers" +%%% + +A {deftech}_test driver_ runs the tests for a package. +It can be an executable target, a {tech}[Lake script], or a library. +Lake itself isn't a test framework: the {lake}`test` command just locates the configured target, builds it, and (for executables and scripts) runs it. +Library drivers are exercised purely by elaboration, so they aren't run as a separate step. +Assertions, test discovery, and reporting are up to the target itself, whether that's a third-party testing library or hand-written checks. + +For executables and scripts, Lake treats a nonzero exit code as a test failure. +For libraries, any elaboration error counts as a test failure, including failures of {keyword}`#guard`-style commands. + +A {deftech}_lint driver_ is similar, but it's run by {lake}`lint` and checks the package for stylistic issues and other problems that aren't _errors_ but indicate likely problems. +Lint drivers can only be executables or scripts, not libraries. + +# Configuring a Test Driver +%%% +tag := "lake-test-driver-config" +%%% + +In a `lakefile.toml`, set {tomlField Lake.PackageConfig}`testDriver` to the name of an executable target, library target, or script defined in the same configuration: + +:::::example "Test Driver (`lakefile.toml`)" + +::::lakeToml Lake.PackageConfig _root_ +```toml +name = "my-package" +testDriver = "my-package-tests" + +[[lean_exe]] +name = "my-package-tests" +root = "Tests" +``` +```expected +{wsIdx := 0, + baseName := `«my-package», + keyName := `«my-package», + origName := `«my-package», + dir := FilePath.mk ".", + relDir := FilePath.mk ".", + config := + {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, + toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + bootstrap := false, + extraDepTargets := #[], + precompileModules := false, + moreGlobalServerArgs := #[], + srcDir := FilePath.mk ".", + buildDir := FilePath.mk ".lake/build", + leanLibDir := FilePath.mk "lib/lean", + nativeLibDir := FilePath.mk "lib", + binDir := FilePath.mk "bin", + irDir := FilePath.mk "ir", + releaseRepo := none, + buildArchive := ELIDED, + preferReleaseBuild := false, + testDriver := "my-package-tests", + testDriverArgs := #[], + lintDriver := "", + lintDriverArgs := #[], + version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, + versionTags := { filter := #, name := `default, descr? := none}, + description := "", + keywords := #[], + homepage := "", + license := "", + licenseFiles := #[FilePath.mk "LICENSE"], + readmeFile := FilePath.mk "README.md", + reservoir := true, + enableArtifactCache? := none, + restoreAllArtifacts? := none, + libPrefixOnWindows := false, + allowImportAll := false, + builtinLint? := none, + checks := #[], + fixedToolchain := false}, + configFile := FilePath.mk "lakefile", + relConfigFile := FilePath.mk "lakefile", + relManifestFile := FilePath.mk "lake-manifest.json", + scope := "", + remoteUrl := "", + depConfigs := #[], + depIdxs := #[], + depPkgs := #[], + targetDecls := + #[{toConfigDecl := + {pkg := `«my-package», + name := `«my-package-tests», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Tests, + exeName := "my-package-tests", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}], + targetDeclMap := + {`«my-package-tests» ↦ + {toPConfigDecl := + {toConfigDecl := + {pkg := `«my-package», + name := `«my-package-tests», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Tests, + exeName := "my-package-tests", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}, + name_eq := …}, + }, + defaultTargets := #[], + scripts := {}, + defaultScripts := #[], + postUpdateHooks := #[], + buildArchive := ELIDED, + testDriver := "my-package-tests", + lintDriver := ""} +``` +:::: +::::: + +In a `lakefile.lean`, either set the {name Lake.Package.testDriver}`testDriver` field on the {keyword}`package` declaration (as above), or tag a script, executable, or library declaration with the {attr}`test_driver` attribute. +The attribute form is often convenient because it places the marker next to the target. + +:::::example "Test Driver (`lakefile.lean`)" + +::::lakeLean +```lean +import Lake +open Lake DSL + +package «my-package» where + testDriver := "my-package-tests" + +lean_exe «my-package-tests» where + root := `Tests +``` +```expected +{wsIdx := 0, + baseName := `«my-package», + keyName := Lean.Name.mkNum `«my-package» 0, + origName := `«my-package», + dir := FilePath.mk ".", + relDir := FilePath.mk ".", + config := + {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, + toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + bootstrap := false, + extraDepTargets := #[], + precompileModules := false, + moreGlobalServerArgs := #[], + srcDir := FilePath.mk ".", + buildDir := FilePath.mk ".lake/build", + leanLibDir := FilePath.mk "lib/lean", + nativeLibDir := FilePath.mk "lib", + binDir := FilePath.mk "bin", + irDir := FilePath.mk "ir", + releaseRepo := none, + buildArchive := ELIDED, + preferReleaseBuild := false, + testDriver := "my-package-tests", + testDriverArgs := #[], + lintDriver := "", + lintDriverArgs := #[], + version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, + versionTags := { filter := #, name := `default, descr? := none}, + description := "", + keywords := #[], + homepage := "", + license := "", + licenseFiles := #[FilePath.mk "LICENSE"], + readmeFile := FilePath.mk "README.md", + reservoir := true, + enableArtifactCache? := none, + restoreAllArtifacts? := none, + libPrefixOnWindows := false, + allowImportAll := false, + builtinLint? := none, + checks := #[], + fixedToolchain := false}, + configFile := FilePath.mk "lakefile.lean", + relConfigFile := FilePath.mk "lakefile.lean", + relManifestFile := FilePath.mk "lake-manifest.json", + scope := "", + remoteUrl := "", + depConfigs := #[], + depIdxs := #[], + depPkgs := #[], + targetDecls := + #[{toConfigDecl := + {pkg := Lean.Name.mkNum `«my-package» 0, + name := `«my-package-tests», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Tests, + exeName := "my-package-tests", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}], + targetDeclMap := + {`«my-package-tests» ↦ + {toPConfigDecl := + {toConfigDecl := + {pkg := Lean.Name.mkNum `«my-package» 0, + name := `«my-package-tests», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Tests, + exeName := "my-package-tests", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}, + name_eq := …}, + }, + defaultTargets := #[], + scripts := {}, + defaultScripts := #[], + postUpdateHooks := #[], + buildArchive := ELIDED, + testDriver := "my-package-tests", + lintDriver := ""} +``` +:::: +::::: + +Only one declaration per package can be tagged with {attr}`test_driver`. +It is an error to use both the {attr}`test_driver` attribute and a non-empty {name Lake.Package.testDriver}`testDriver` field in the same Lake configuration file. + +A test driver may also be a target in a package dependency that is transitively {tech (key:="require")}[required]. +To use a target from another package, use `/` as the value of `testDriver`, where `` is the name of the package in which the target is found.. + +# Running Tests +%%% +tag := "lake-test-running" +%%% + +The {lake}`test` command runs the configured driver for the {tech}[root package] only. +Test drivers for dependencies are not run. + +:::paragraph +If the test driver is an executable or a script, Lake passes the arguments from {tomlField Lake.PackageConfig}`testDriverArgs` first, then anything after `--` on the command line. +For example, + +``` +lake test -- --filter Foo --verbose +``` + +passes `--filter Foo --verbose` to the driver after whatever {tomlField Lake.PackageConfig}`testDriverArgs` is already configured. +Lake builds executable drivers before running them. +::: + +If the test driver is a library, arguments are not accepted. +Lake reports an error if {tomlField Lake.PackageConfig}`testDriverArgs` is non-empty or if any arguments follow `--`. +To run the tests, the library is just {tech (key:="Lean elaborator")}[elaborated]. + +{lake}`check-test` terminates with exit code 0 (that is, successfully) if a test driver is configured for the root package. +It doesn't check that the named target actually exists. + +# Lint Drivers +%%% +tag := "lake-lint-drivers" +%%% + +Lint drivers are configured and run similarly to {ref "lake-test-driver-config"}[test drivers]. +The Lake configuration file specifies a target that serves as the lint driver, and {lake}`lint` runs it. +This target must be an executable or a script; unlike test drivers, lint drivers may not be libraries. + +In a TOML-format Lake configuration file, the package-level field {tomlField Lake.PackageConfig}`lintDriver` specifies the name of the lint driver target. + +:::::example "Lint Driver (`lakefile.toml`)" +This minimal `lakefile.toml` configures a lint driver: + +::::lakeToml Lake.PackageConfig _root_ +```toml +name = "my-package" +lintDriver = "my-package-lint" + +[[lean_exe]] +name = "my-package-lint" +root = "Lint" +``` +```expected +{wsIdx := 0, + baseName := `«my-package», + keyName := `«my-package», + origName := `«my-package», + dir := FilePath.mk ".", + relDir := FilePath.mk ".", + config := + {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, + toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + bootstrap := false, + extraDepTargets := #[], + precompileModules := false, + moreGlobalServerArgs := #[], + srcDir := FilePath.mk ".", + buildDir := FilePath.mk ".lake/build", + leanLibDir := FilePath.mk "lib/lean", + nativeLibDir := FilePath.mk "lib", + binDir := FilePath.mk "bin", + irDir := FilePath.mk "ir", + releaseRepo := none, + buildArchive := ELIDED, + preferReleaseBuild := false, + testDriver := "", + testDriverArgs := #[], + lintDriver := "my-package-lint", + lintDriverArgs := #[], + version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, + versionTags := { filter := #, name := `default, descr? := none}, + description := "", + keywords := #[], + homepage := "", + license := "", + licenseFiles := #[FilePath.mk "LICENSE"], + readmeFile := FilePath.mk "README.md", + reservoir := true, + enableArtifactCache? := none, + restoreAllArtifacts? := none, + libPrefixOnWindows := false, + allowImportAll := false, + builtinLint? := none, + checks := #[], + fixedToolchain := false}, + configFile := FilePath.mk "lakefile", + relConfigFile := FilePath.mk "lakefile", + relManifestFile := FilePath.mk "lake-manifest.json", + scope := "", + remoteUrl := "", + depConfigs := #[], + depIdxs := #[], + depPkgs := #[], + targetDecls := + #[{toConfigDecl := + {pkg := `«my-package», + name := `«my-package-lint», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Lint, + exeName := "my-package-lint", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}], + targetDeclMap := + {`«my-package-lint» ↦ + {toPConfigDecl := + {toConfigDecl := + {pkg := `«my-package», + name := `«my-package-lint», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Lint, + exeName := "my-package-lint", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}, + name_eq := …}, + }, + defaultTargets := #[], + scripts := {}, + defaultScripts := #[], + postUpdateHooks := #[], + buildArchive := ELIDED, + testDriver := "", + lintDriver := "my-package-lint"} +``` +:::: +::::: + + +In a `lakefile.lean`, either set the {name Lake.Package.lintDriver}`lintDriver` field on the {keyword}`package` declaration, or tag a script or executable declaration with the {attr}`lint_driver` attribute. +The attribute form is often convenient because it places the marker next to the target. + +:::::example "Lint Driver (`lakefile.lean`)" + +::::lakeLean +```lean +import Lake +open Lake DSL + +package «my-package» where + lintDriver := "my-package-lint" + +lean_exe «my-package-lint» where + root := `Lint +``` +```expected +{wsIdx := 0, + baseName := `«my-package», + keyName := Lean.Name.mkNum `«my-package» 0, + origName := `«my-package», + dir := FilePath.mk ".", + relDir := FilePath.mk ".", + config := + {toWorkspaceConfig := { packagesDir := FilePath.mk ".lake/packages" }, + toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + bootstrap := false, + extraDepTargets := #[], + precompileModules := false, + moreGlobalServerArgs := #[], + srcDir := FilePath.mk ".", + buildDir := FilePath.mk ".lake/build", + leanLibDir := FilePath.mk "lib/lean", + nativeLibDir := FilePath.mk "lib", + binDir := FilePath.mk "bin", + irDir := FilePath.mk "ir", + releaseRepo := none, + buildArchive := ELIDED, + preferReleaseBuild := false, + testDriver := "", + testDriverArgs := #[], + lintDriver := "my-package-lint", + lintDriverArgs := #[], + version := { toSemVerCore := { major := 0, minor := 0, patch := 0 }, specialDescr := "" }, + versionTags := { filter := #, name := `default, descr? := none}, + description := "", + keywords := #[], + homepage := "", + license := "", + licenseFiles := #[FilePath.mk "LICENSE"], + readmeFile := FilePath.mk "README.md", + reservoir := true, + enableArtifactCache? := none, + restoreAllArtifacts? := none, + libPrefixOnWindows := false, + allowImportAll := false, + builtinLint? := none, + checks := #[], + fixedToolchain := false}, + configFile := FilePath.mk "lakefile.lean", + relConfigFile := FilePath.mk "lakefile.lean", + relManifestFile := FilePath.mk "lake-manifest.json", + scope := "", + remoteUrl := "", + depConfigs := #[], + depIdxs := #[], + depPkgs := #[], + targetDecls := + #[{toConfigDecl := + {pkg := Lean.Name.mkNum `«my-package» 0, + name := `«my-package-lint», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Lint, + exeName := "my-package-lint", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}], + targetDeclMap := + {`«my-package-lint» ↦ + {toPConfigDecl := + {toConfigDecl := + {pkg := Lean.Name.mkNum `«my-package» 0, + name := `«my-package-lint», + kind := `lean_exe, + config := + {toLeanConfig := + { buildType := Lake.BuildType.release, + leanOptions := #[], + moreLeanArgs := #[], + weakLeanArgs := #[], + moreLeancArgs := #[], + moreServerOptions := #[], + weakLeancArgs := #[], + moreLinkObjs := #[], + moreLinkLibs := #[], + moreLinkArgs := #[], + weakLinkArgs := #[], + backend := Lake.Backend.default, + platformIndependent := none, + precompileImports := false, + dynlibs := #[], + plugins := #[], + requiresModuleSystem := false, + allowNonModules := false }, + srcDir := FilePath.mk ".", + root := `Lint, + exeName := "my-package-lint", + needs := #[], + extraDepTargets := #[], + supportInterpreter := false, + nativeFacets := #}, + wf_data := …}, + pkg_eq := …}, + name_eq := …}, + }, + defaultTargets := #[], + scripts := {}, + defaultScripts := #[], + postUpdateHooks := #[], + buildArchive := ELIDED, + testDriver := "", + lintDriver := "my-package-lint"} +``` +:::: +::::: + +Only one declaration per package can be tagged with {attr}`lint_driver`. +It is an error to use both the {attr}`lint_driver` attribute and a non-empty {name Lake.Package.lintDriver}`lintDriver` field in the same Lake configuration file. + +:::lakeSession -show +```lean +lakefile +import Lake +open Lake DSL +package p + +@[lint_driver] +lean_exe Foo where + +@[lint_driver] +lean_exe Bar where +``` +```lakeCmd "lake build" +error +error: p: only one script or executable can be tagged @[lint_driver] +``` +::: + +A lint driver in a dependency package can be referenced with the same `/` syntax used for test drivers. + +{lake}`lint` runs the configured driver, passing {tomlField Lake.PackageConfig}`lintDriverArgs` first, then anything after `--` on the command line: + +``` +lake lint -- --warnings-as-errors +``` + +Lake also has a separate {deftech}_builtin linter_ that operates on Lean modules directly, independent of any configured driver. +Builtin linting is enabled by the `--builtin-lint` and related flags (see {lake}`lint`), or by setting {tomlField Lake.PackageConfig}`builtinLint` to `true` in the package configuration. +When builtin linting is active, positional `MODULE` arguments before `--` select which modules to lint, and they are _not_ passed to the configured driver. +So `lake lint Mathlib` triggers builtin linting on `Mathlib`, whereas `lake lint -- Mathlib` passes `Mathlib` to the driver. +The two mechanisms are independent and can run together: when both apply, Lake runs the builtin linter first and then the driver. + +{lake}`check-lint` exits with code 0 (that is, successfully) if a lint driver is configured for the root package or if {tomlField Lake.PackageConfig}`builtinLint` is set to `true` in its configuration. diff --git a/Manual/BuildTools/Lake/PackageOverrides.lean b/Manual/BuildTools/Lake/PackageOverrides.lean new file mode 100644 index 000000000..ed1293413 --- /dev/null +++ b/Manual/BuildTools/Lake/PackageOverrides.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen, Mac Malone +-/ + +import VersoManual + +import Lean.Parser.Command +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Module + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Verso.Genre.Manual.InlineLean + +set_option guard_msgs.diff true + +#doc (Manual) "Package Overrides" => +%%% +tag := "package-overrides" +%%% + +Together, the {tech}[package configuration] and {tech}[manifest] describe the exact manner by which Lake expects to acquire dependencies. +Usually, this involves making a local copy of a remote Git repository over the network. +Lake terminates with an error if the remote repository cannot be accessed. +Because the sources of dependencies are predictable, builds are reproducible across systems; packages are retrieved in the same way from the same sources on all machines. + +Nonetheless, there are situations where it is infeasible to acquire package dependencies the same way the original developers did. +For example, some companies require that all dependencies are audited prior to use, and not everyone always has access to the Internet while working. +In these situations, it is necessary to acquire packages in some other way. + +Lake's {deftech}_package overrides_ allow a package dependency to be redirected from one source to another without modifying any {tech}[package configurations] or {tech}[manifests]. +They do not allow packages to be added to or removed from the {tech}[workspace]. +All transitive dependencies in the workspace respect the redirection. +The package overrides file is a JSON file that contains an alternate list of package entries. +These entries will take precedence over those in the package's {tech}[manifest]. +This file can be provided to Lake either via the {lakeOpt}`--packages` option or by placing it at a fixed path within the Lake workspace: `.lake/package-overrides.json`. + +The syntax of package entries in the package overrides file mirrors that of the {tech}[manifest]. +Thus, it is possible to copy an entry from a manifest into a package overrides file (and vice versa). +One way to determine the necessary syntax for a package entry is to add a temporary dependency to a {tech}[package configuration] that matches the desired configuration, run {lake}`update` to generate a manifest with that dependency, and then copy the entry from the manifest into the package overrides file. + +:::example "Making Remote Dependencies Local" + +Consider a use case where programs are being developed in a restricted enviroment without network access (e.g., for security reasons). +The team wishes to compile a small tool written in Lean that depends on the [`@leanprover/Cli`](https://reservoir.lean-lang.org/@leanprover/Cli) library to provide a simple command-line interface. +That tool's {tech}[manifest] thus looks something like this: + +```lakeManifest +{ + "version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [{ + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0000000000000000000000000000000000000000", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.toml" + }], + "name": "myTool", + "lakeDir": ".lake", + "fixedToolchain": false +} +``` + +This manifest would instruct Lake to download the `Cli` package from the indicated GitHub URL when building this tool. +However, the restricted environment does not have network access, so the build will fail unless Lake uses a local copy instead. +This can be done with the following {tech}[package overrides] file: + +```lakePackageOverrides +{ + "version": "1.3.0", + "packages": [{ + "type": "path", + "dir": "/etc/lean-packages/Cli", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inherited": false, + "configFile": "lakefile.toml" + }] +} +``` + +With this, Lake will instead resolve the `Cli` dependency to the local package located at the path `/etc/lean-packages/Cli`. + +::: diff --git a/Manual/BuildTools/Lake/Scripts.lean b/Manual/BuildTools/Lake/Scripts.lean new file mode 100644 index 000000000..815f6d82a --- /dev/null +++ b/Manual/BuildTools/Lake/Scripts.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual + +import Lean.Parser.Command +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Module + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Verso.Genre.Manual.InlineLean + +set_option guard_msgs.diff true + +#doc (Manual) "Scripts" => +%%% +tag := "lake-scripts" +%%% + +Lake {tech}[package configuration] files may include {deftech}_Lake scripts_, which are embedded programs that can be executed from the command line. +Scripts are intended to be used for project-specific tasks that are not already well-served by Lake's other features. +While ordinary executable programs are run in the {name}`IO` {tech}[monad], scripts are run in {name Lake.ScriptM}`ScriptM`, which extends {name}`IO` with information about the workspace. +Because they are Lean definitions, Lake scripts can only be defined in the Lean configuration format. + +:::::TODO + +Restore the following once we can import enough of Lake to elaborate it + +```` +```lean -show +section +open Lake DSL +``` + +:::example "Listing Dependencies" + +This Lake script lists all the transitive dependencies of the root package, along with their Git URLs, in alphabetical order. +Similar scripts could be used to check declared licenses, discover which dependencies have test drivers configured, or compute metrics about the transitive dependency set over time. + +```lean +script "list-deps" := do + let mut results := #[] + for p in (← getWorkspace).packages do + if p.name ≠ (← getWorkspace).root.name then + results := results.push (p.name.toString, p.remoteUrl) + results := results.qsort (·.1 < ·.1) + IO.println "Dependencies:" + for (name, url) in results do + IO.println s!"{name}:\t{url}" + return 0 +``` +::: + +```lean -show +end +``` +```` + +::::: From 143714a2df2a8c0efd40b6c9d229ba119013822b Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 24 Sep 2026 19:05:19 +0000 Subject: [PATCH 2/3] doc: intro each new top-level section & demote scripts --- Manual/BuildTools/Lake.lean | 8 ++++---- Manual/BuildTools/Lake/Builds.lean | 3 +++ 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Manual/BuildTools/Lake.lean b/Manual/BuildTools/Lake.lean index b0262d8a6..c24c1485f 100644 --- a/Manual/BuildTools/Lake.lean +++ b/Manual/BuildTools/Lake.lean @@ -47,8 +47,8 @@ Lake is extensible. It provides a rich API that can be used to define incremental build tasks for software artifacts that are not written in Lean, to automate administrative tasks, and to integrate with external workflows. For build configurations that do not need these features, Lake provides a declarative configuration language that can be written either in TOML or as a Lean file. -This section describes Lake's {ref "lake-cli"}[command-line interface], {ref "lake-config"}[configuration files], and {ref "lake-api"}[internal API]. -All three share a set of concepts and terminology. +This section describes Lake's {ref "lake-builds"}[builds], {ref "lake-cache"}[cache], {ref "test-lint-drivers"}[workflow drivers], {ref "lake-cli"}[command-line interface], {ref "lake-config"}[configuration files], and {ref "lake-api"}[internal API]. +They all share a set of concepts and terminology. # Concepts and Terminology @@ -173,12 +173,12 @@ The threshold can be adjusted using the {lakeOpt}`--log-level` option, the {lake {include 2 Manual.BuildTools.Lake.PackageOverrides} +{include 2 Manual.BuildTools.Lake.Scripts} + {include 0 Manual.BuildTools.Lake.Builds} {include 0 Manual.BuildTools.Lake.Cache} -{include 0 Manual.BuildTools.Lake.Scripts} - {include 0 Manual.BuildTools.Lake.Drivers} {include 0 Manual.BuildTools.Lake.CLI} diff --git a/Manual/BuildTools/Lake/Builds.lean b/Manual/BuildTools/Lake/Builds.lean index f2d92b838..5dd35e91c 100644 --- a/Manual/BuildTools/Lake/Builds.lean +++ b/Manual/BuildTools/Lake/Builds.lean @@ -21,6 +21,9 @@ open Verso.Genre.Manual.InlineLean set_option guard_msgs.diff true #doc (Manual) "Builds" => +%%% +tag := "lake-builds" +%%% :::paragraph Producing a desired {tech}[artifact], such as a {tech}[`.olean` file] or an executable binary, is called a {deftech}_build_. From 53d630448953566f3d403651d82dea710c806202 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 24 Sep 2026 19:59:34 +0000 Subject: [PATCH 3/3] doc:: bundle scripts & drivers into workflows + link intro to terms --- Manual/BuildTools/Lake.lean | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/Manual/BuildTools/Lake.lean b/Manual/BuildTools/Lake.lean index c24c1485f..3c82d4aee 100644 --- a/Manual/BuildTools/Lake.lean +++ b/Manual/BuildTools/Lake.lean @@ -38,16 +38,16 @@ tag := "lake" Lake is the standard Lean build tool. It is responsible for: - * Configuring builds and building Lean code - * Fetching and building external dependencies - * Integrating with Reservoir, the Lean package server - * Running tests, linters, and other development workflows + * Configuring {tech}[builds] and building Lean code + * Fetching and building external {tech}[dependencies] + * Integrating with [Reservoir](https://reservoir.lean-lang.org/){TODO}[xref chapter], the Lean package server + * Running tests, linters, and other {tech}[development workflows] Lake is extensible. It provides a rich API that can be used to define incremental build tasks for software artifacts that are not written in Lean, to automate administrative tasks, and to integrate with external workflows. For build configurations that do not need these features, Lake provides a declarative configuration language that can be written either in TOML or as a Lean file. -This section describes Lake's {ref "lake-builds"}[builds], {ref "lake-cache"}[cache], {ref "test-lint-drivers"}[workflow drivers], {ref "lake-cli"}[command-line interface], {ref "lake-config"}[configuration files], and {ref "lake-api"}[internal API]. +This section describes Lake's {ref "lake-builds"}[builds], {ref "lake-cache"}[cache], {ref "lake-workflows"}[workflows], {ref "lake-cli"}[command-line interface], {ref "lake-config"}[configuration files], and {ref "lake-api"}[internal API]. They all share a set of concepts and terminology. @@ -59,7 +59,7 @@ tag := "lake-vocab" A {deftech}_package_ is the basic unit of Lean code distribution. A single package may contain multiple libraries or executable programs. A package consist of a directory that contains a {tech}[package configuration] file together with source code. -Packages may {deftech}_require_ other packages, in which case those packages' code (more specifically, their {tech}[targets]) are made available. +Packages may {deftech}_require_ other packages as {deftech}_dependencies_, in which case those packages' code (more specifically, their {tech}[targets]) are made available. The {deftech}_direct dependencies_ of a package are those that it requires, and the {deftech}_transitive dependencies_ are the direct dependencies of a package together with their transitive dependencies. Packages may either be obtained from [Reservoir](https://reservoir.lean-lang.org/){TODO}[xref chapter], the Lean package repository, or from a manually-specified location. {deftech}_Git dependencies_ are specified by a Git repository URL along with a revision (branch, tag, or hash) and must be cloned locally prior to build, while local {deftech}_path dependencies_ are specified by a path relative to the package's directory. @@ -173,13 +173,22 @@ The threshold can be adjusted using the {lakeOpt}`--log-level` option, the {lake {include 2 Manual.BuildTools.Lake.PackageOverrides} -{include 2 Manual.BuildTools.Lake.Scripts} - {include 0 Manual.BuildTools.Lake.Builds} {include 0 Manual.BuildTools.Lake.Cache} -{include 0 Manual.BuildTools.Lake.Drivers} +# Development Workflows +%%% +tag := "lake-workflows" +%%% + +Lake provides tools to execute standard {deftech}_development workflows_ for a package through its own CLI. +For the common cases of testing and linting, Lake provides builtin support through the {lake}`test` and {lake}`lint` commands, which use the {ref "test-lint-drivers"}[test and lint drivers] configured on the package. +For other workflows, Lake provides {ref "lake-scripts"}[scripts], custom programs with ready access to the {ref "lake-api"}[Lake API], defined in the Lean configuration format and run through the {lake}`scripts` CLI. + +{include 2 Manual.BuildTools.Lake.Drivers} + +{include 2 Manual.BuildTools.Lake.Scripts} {include 0 Manual.BuildTools.Lake.CLI}