From 9e9ddb134aba2e267c117455b13a0225bc31c5d8 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 21 Oct 2024 16:31:25 +0200 Subject: [PATCH] chore: README update (#97) Update README links and text --- README.md | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 65a3538..ad1139b 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,21 @@ # Lean Language Reference +The Lean Language Reference is intended as a comprehensive, precise description of Lean. It is first and foremost a reference work in which Lean users can look up detailed information, rather than a tutorial for new users. + +This new reference has been rebuilt from the ground up in Verso. This means that all example code is type checked, the source code contains tests to ensure that it stays up-to-date with respect to changes in Lean, and we can add any features that we need to improve the documentation. Verso also makes it easy to integrate tightly with Lean, so we can show function docstrings directly, mechanically check descriptions of syntax against the actual parser, and insert cross-references automatically. + + ## Reading the Manual -The output of building the current state of the `main` branch can be read at . +The latest release of this reference manual can be read [here](https://lean-lang.org/doc/reference/latest/). + +For developers: + * The output of building the current state of the `main` branch can be read [here](https://lean-reference-manual-review.netlify.app/). + * Each pull request in this repository causes two separate previews to be generated, one with extra information that's only useful to those actively working on the text, such as TODO notes and symbol coverage progress bars. These are posted by a bot to the PR after the first successful build. -## Building the Reference Manual +## Building the Reference Manual Locally -To read the manual, run the following command: +To build the manual, run the following command: ``` lake exe generate-manual --depth 2 @@ -18,3 +27,8 @@ python3 -m http.server 8880 --directory _out/html-multi & ``` Then open in your browser. + +## Contributing + +Please see [CONTRIBUTING.md](CONTRIBUTING.md) for more information. +