From f91b574c40ad862c5134d48995ad083fe48e4cd4 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Thu, 12 Oct 2023 16:35:07 -0400 Subject: [PATCH] Warn about deprecation in README (#815) Co-authored-by: Eric Wieser --- OLD_README.md | 52 ++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 55 ++++----------------------------------------------- 2 files changed, 56 insertions(+), 51 deletions(-) create mode 100644 OLD_README.md diff --git a/OLD_README.md b/OLD_README.md new file mode 100644 index 000000000..faa7f266c --- /dev/null +++ b/OLD_README.md @@ -0,0 +1,52 @@ +

logo

+ + + + + + + + + +
LicenseContinuous integrationChat
+ github actions + Bors enabled + Join the Zulip chat
+ +About +----- + +- **Important**: This is Lean 3.51.1c, a fork of Lean 3 maintained and updated by the Lean community. The last official release of Lean 3.x was Lean 3.4.2, which can be found [here](https://github.com/leanprover/lean). The Lean developers are currently developing [Lean 4](https://github.com/leanprover/lean4). +- [Lean Homepage](https://lean-lang.org) +- [Lean Prover Community Homepage](https://leanprover-community.github.io/lean3) +- [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/index.html) +- [Change Log](doc/changes.md) +- [Lean 3.4.2 FAQ](doc/faq.md) +- For HoTT mode, please use [Lean2](https://github.com/leanprover/lean2). + +Installation +------------ + +If you want to use Lean, the recommended way to install Lean is following [these instructions under Regular install](https://leanprover-community.github.io/lean3/get_started.html#regular-install). + +If you want to modify the code of Lean or the core library, the recommended way is to [build Lean from source](doc/make/index.md). + +If you want to modify *a single file* in the core library (not the C++ source), then instead of building Lean from scratch, you can run (in your local `lean/` directory) +``` +git checkout v3.xx.x +git checkout -b my-branch-name +elan override set leanprover-community/lean:3.xx.x +``` +You can now build the core library with `lean --make library` or open any Lean file is VSCode / Emacs and it will use the version of Lean you specified. You might have to restart Lean (in VScode: `ctrl+shift+P Lean: Restart`). Warning: all imported Lean files will be from the downloaded community version, *not* the version of the files in this repository. Therefore, this setup is not recommended if you modify more than one file. Moreover, editor features like `Go to Definition` will not behave correctly with this setup. For the best experience, [build Lean from source](doc/make/index.md). + +Stable binary releases of Lean are available on the [release page](https://github.com/leanprover-community/lean/releases). + +Miscellaneous +------------- + +- Building Doxygen Documentation: `doxygen src/Doxyfile` +- [Coding Style](doc/coding_style.md) +- [Library Style Conventions](doc/lean/library_style.org) +- [Git Commit Conventions](doc/commit_convention.md) +- [Syntax Highlight Lean Code in LaTeX](doc/syntax_highlight_in_latex.md) +- [Exporting, and reference type-checkers](doc/export_format.md) diff --git a/README.md b/README.md index 272e1c8d8..d21bbdecf 100644 --- a/README.md +++ b/README.md @@ -1,52 +1,5 @@ -

logo

- - - - - - - - - -
LicenseContinuous integrationChat
- github actions - Bors enabled - Join the Zulip chat
+> [!WARNING] +> Lean 3 is no longer actively maintained. +> It is strongly recommended that you use [Lean 4](https://lean-lang.org/) instead. -About ------ - -- **Important**: This is Lean 3.51.1c, a fork of Lean 3 maintained and updated by the Lean community. The last official release of Lean 3.x was Lean 3.4.2, which can be found [here](https://github.com/leanprover/lean). The Lean developers are currently developing [Lean 4](https://github.com/leanprover/lean4). -- [Lean Homepage](http://leanprover.github.io) -- [Lean Prover Community Homepage](https://leanprover-community.github.io/lean3) -- [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/index.html) -- [Change Log](doc/changes.md) -- [Lean 3.4.2 FAQ](doc/faq.md) -- For HoTT mode, please use [Lean2](https://github.com/leanprover/lean2). - -Installation ------------- - -If you want to use Lean, the recommended way to install Lean is following [these instructions under Regular install](https://leanprover-community.github.io/lean3/get_started.html#regular-install). - -If you want to modify the code of Lean or the core library, the recommended way is to [build Lean from source](doc/make/index.md). - -If you want to modify *a single file* in the core library (not the C++ source), then instead of building Lean from scratch, you can run (in your local `lean/` directory) -``` -git checkout v3.xx.x -git checkout -b my-branch-name -elan override set leanprover-community/lean:3.xx.x -``` -You can now build the core library with `lean --make library` or open any Lean file is VSCode / Emacs and it will use the version of Lean you specified. You might have to restart Lean (in VScode: `ctrl+shift+P Lean: Restart`). Warning: all imported Lean files will be from the downloaded community version, *not* the version of the files in this repository. Therefore, this setup is not recommended if you modify more than one file. Moreover, editor features like `Go to Definition` will not behave correctly with this setup. For the best experience, [build Lean from source](doc/make/index.md). - -Stable binary releases of Lean are available on the [release page](https://github.com/leanprover-community/lean/releases). - -Miscellaneous -------------- - -- Building Doxygen Documentation: `doxygen src/Doxyfile` -- [Coding Style](doc/coding_style.md) -- [Library Style Conventions](doc/lean/library_style.org) -- [Git Commit Conventions](doc/commit_convention.md) -- [Syntax Highlight Lean Code in LaTeX](doc/syntax_highlight_in_latex.md) -- [Exporting, and reference type-checkers](doc/export_format.md) +(If you need to read the old `README.md`, please see `OLD_README.md`.) \ No newline at end of file