Skip to content

Commit 12ff2d8

Browse files
chore: remove old documentation site (#7974)
This PR removes the old documentation overview site, as its content has moved to the main Lean website infrastructure. This should be merged when the new website section is deployed, after installing appropriate redirects. Developer documentation is remaining in Markdown form, but it will no longer be part of the documentation hosted on the Lean website. Example code stays here for CI, but it is now rendered via a Verso plugin.
1 parent 8807893 commit 12ff2d8

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

61 files changed

+24
-7442
lines changed

.github/workflows/nix-ci.yml

Lines changed: 0 additions & 112 deletions
This file was deleted.

README.md

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,25 +2,24 @@ This is the repository for **Lean 4**.
22

33
# About
44

5-
- [Quickstart](https://lean-lang.org/lean4/doc/quickstart.html)
5+
- [Quickstart](https://lean-lang.org/documentation/setup/)
66
- [Homepage](https://lean-lang.org)
77
- [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
88
- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
9-
- [Documentation Overview](https://lean-lang.org/lean4/doc/)
9+
- [Documentation Overview](https://lean-lang.org/documentation/)
1010
- [Language Reference](https://lean-lang.org/doc/reference/latest/)
1111
- [Release notes](RELEASES.md) starting at v4.0.0-m3
12-
- [Examples](https://lean-lang.org/lean4/doc/examples.html)
12+
- [Examples](https://lean-lang.org/documentation/examples/)
1313
- [External Contribution Guidelines](CONTRIBUTING.md)
14-
- [FAQ](https://lean-lang.org/lean4/doc/faq.html)
1514

1615
# Installation
1716

18-
See [Setting Up Lean](https://lean-lang.org/lean4/doc/setup.html).
17+
See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
1918

2019
# Contributing
2120

2221
Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
2322

2423
# Building from Source
2524

26-
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).
25+
See [Building Lean](doc/make/index.md).

doc/README.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
# Developer Documentation and Examples
2+
3+
This directory contains documentation that describes how to work on
4+
Lean itself, as well as examples that are included in documentation
5+
that's hosted on the Lean website. The `make` directory contains
6+
information on building Lean, and the `dev` directory describes how to
7+
work on Lean.
8+
9+
The [documentation section](https://lean-lang.org/documentation) has
10+
links to documentation that describes how to use Lean itself.

doc/SUMMARY.md

Lines changed: 0 additions & 46 deletions
This file was deleted.

0 commit comments

Comments
 (0)