From 4520e5bbfa611f320fd0583a79c2b86c3f43c527 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 30 Sep 2024 20:29:00 -0400 Subject: [PATCH] doc: update README w/ Reservoir package options (#5546) Adds the new Reservoir-related package configuration options to Lake's README. (cherry picked from commit 4771741fa288466a2de48569483205ad0690c8ef) --- src/lake/Lake/Config/Package.lean | 13 ++++++++----- src/lake/README.md | 17 +++++++++++++++++ 2 files changed, 25 insertions(+), 5 deletions(-) diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 54e6f6f6fbda..ed208476f199 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -283,7 +283,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where the Git revisions corresponding to released versions. Defaults to tags that are "version-like". - That is, start with a `v` and are followed by a digit. + That is, start with a `v` followed by a digit. -/ versionTags : StrPat := defaultVersionTags @@ -299,7 +299,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where `devtool`), specific subtopics (e.g., `topology`, `cryptology`), and significant implementation details (e.g., `dsl`, `ffi`, `cli`). For instance, Lake's keywords could be `devtool`, `cli`, `dsl`, - `package-manager`, `build-system`. + `package-manager`, and `build-system`. -/ keywords : Array String := #[] @@ -308,7 +308,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where Reservoir will already include a link to the package's GitHub repository (if the package is sourced from there). Thus, users are advised to specify - something else for this link (if anything). + something else for this (if anything). -/ homepage : String := "" @@ -340,8 +340,11 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where /-- The path to the package's README. - A README should be a markdown file containing an overview of the package. - Reservoir displays the rendered HTML of this README on a package's page. + + A README should be a Markdown file containing an overview of the package. + Reservoir displays the rendered HTML of this file on a package's page. + A nonstandard location can be used to provide a different README for Reservoir + and GitHub. Defaults to `README.md`. -/ diff --git a/src/lake/README.md b/src/lake/README.md index 26ac5940a38e..746f8f0a0d71 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -13,6 +13,7 @@ Each `lakefile.lean` includes a `package` declaration (akin to `main`) which def * [Creating and Building a Package](#creating-and-building-a-package) * [Glossary of Terms](#glossary-of-terms) * [Package Configuration Options](#package-configuration-options) + + [Metadata](#metadata) + [Layout](#layout) + [Build & Run](#build--run) + [Test & Lint](#test--lint) @@ -165,6 +166,22 @@ Lake uses a lot of terms common in software development -- like workspace, packa Lake provides a large assortment of configuration options for packages. +### Metadata + +These options describe the package. They are used by Lake's package registry, [Reservoir](https://reservoir.lean-lang.org/), to index and display packages. If a field is left out, Reservoir may use information from the package's GitHub repository to fill in details. + +* `name`: The name of the package. Set by `package ` in Lean configuration files. +* `version`: The version of the package. A 3-point version identifier with an optional `-` suffix. +* `versionTags`: Git tags of this package's repository that should be treated as versions. Reservoir makes use of this information to determine the Git revisions corresponding to released versions. Defaults to tags that are "version-like". That is, start with a `v` followed by a digit. +* `description`: A short description for the package. +* `keywords`: An `Array` of custom keywords that identify key aspects of the package. Reservoir can make use of these to group packages and make it easier for potential users to discover them. For example, Lake's keywords could be `devtool`, `cli`, `dsl`, `package-manager`, and `build-system`. +* `homepage`: A URL to information about the package. Reservoir will already include a link to the package's GitHub repository. Thus, users are advised to specify something else for this. +* `license`: An [SPFX license identifier](https://spdx.org/licenses/) for the package's license. For example, `Apache-2.0` or `MIT`. +* `licenseFiles`: An `Array` of files that contain license information. For example, `#["LICENSE", "NOTICE"]` for Apache 2.0. Defaults to `#["LICENSE"]`, +* `readmeFile`: The relative path to the package's README. It should be a Markdown file containing an overview of the package. A nonstandard location can be used to provide a different README for Reservoir and GitHub. Defaults to `README.md`. +* `reservoir`: Whether Reservoir should index the package. Defaults to `true`. Set this to `false` to have Reservoir exclude the package from its index. + + ### Layout These options control the top-level directory layout of the package and its build directory. Further paths specified by libraries, executables, and targets within the package are relative to these directories.