remove lean 3

README.md

@@ -3,11 +3,12 @@ LeanDojo: Machine Learning for Theorem Proving in Lean
 
 ![LeanDojo](https://github.com/lean-dojo/LeanDojo/blob/main/images/LeanDojo.jpg)
 
-[LeanDojo](https://leandojo.org/) is a Python library for learning–based theorem provers in Lean, supporting both [Lean 3](https://github.com/leanprover-community/lean) and [Lean 4](https://leanprover.github.io/). It provides two main features:
+[LeanDojo](https://leandojo.org/) is a Python library for learning–based theorem provers in Lean, providing two main features:
 
 * Extracting data (proof states, tactics, premises, etc.) from Lean repos.
 * Interacting with Lean programmatically.
 
+LeanDojo's current version is compatible with Lean 4 `v4.3.0-rc2` or later. We strongly suggest using the current version. However, you may use the [`legacy`](https://github.com/lean-dojo/LeanDojo/tree/legacy) branch if you want to work with earlier versions (including Lean 3).
 
 [![Documentation Status](https://readthedocs.org/projects/leandojo/badge/?version=latest)](https://leandojo.readthedocs.io/en/latest/?badge=latest) [![PyPI](https://img.shields.io/pypi/v/lean-dojo)](https://pypi.org/project/lean-dojo/) [![GitHub license](https://img.shields.io/github/license/lean-dojo/LeanDojo)](https://github.com/lean-dojo/LeanDojo/blob/main/LICENSE) [![Code style: black](https://img.shields.io/badge/code%20style-black-000000.svg)](https://github.com/psf/black) 
 
@@ -20,7 +21,6 @@ ______________________________________________________________________
 * 3.9 <= Python < 3.11
 * wget
 * [elan](https://github.com/leanprover/elan)
-* Docker is strongly recommended when using LeanDojo with Lean 3
 * Recommended: Generate a [GitHub personal access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens#personal-access-tokens-classic) and set the environment variable `GITHUB_ACCESS_TOKEN` to it
 
 

docs/source/conf.py

@@ -13,7 +13,7 @@
 project = "LeanDojo"
 copyright = "2023, LeanDojo Team"
 author = "Kaiyu Yang"
-release = "1.6.0"
+release = "1.7.0rc"
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyproject.toml

@@ -13,7 +13,7 @@ exclude = [
 
 [project]
 name = "lean-dojo"
-version = "1.6.0"
+version = "1.7.0rc"
 authors = [
   { name="Kaiyu Yang", email="[email protected]" },
 ]

src/lean_dojo/constants.py

@@ -14,7 +14,7 @@
 
 load_dotenv()
 
-__version__ = "1.6.0"
+__version__ = "1.7.0rc"
 
 logger.remove()
 if "VERBOSE" in os.environ or "DEBUG" in os.environ:
@@ -49,18 +49,9 @@
 
 NUM_WORKERS = NUM_PROCS - 1
 
-LEAN3_URL = "https://github.com/leanprover-community/lean"
-"""The URL of the Lean 3 repo."""
-
-LEAN3_PACKAGES_DIR = Path("_target/deps")
-"""The directory where Lean 3 dependencies are stored."""
-
 LEAN4_URL = "https://github.com/leanprover/lean4"
 """The URL of the Lean 4 repo."""
 
-LEAN4_PACKAGES_DIR_OLD = Path("lake-packages")
-"""The directory where Lean 4 dependencies are stored (before v4.3.0-rc2)."""
-
 LEAN4_PACKAGES_DIR = Path(".lake/packages")
 """The directory where Lean 4 dependencies are stored (since v4.3.0-rc2)."""
 
@@ -69,12 +60,6 @@
 
 LEAN4_BUILD_DIR = Path(".lake/build")
 
-LEAN_BUILD_DIR_OLD = Path("build")
-
-TACTIC_TIMEOUT = int(os.getenv("TACTIC_TIMEOUT", 5000))
-"""Maximum time (in milliseconds) before interrupting a tactic when interacting with Lean (only for Lean 3).
-"""
-
 TACTIC_CPU_LIMIT = int(os.getenv("TACTIC_CPU_LIMIT", 1))
 """Number of CPUs for executing tactics when interacting with Lean (only useful when running within Docker).
 """
@@ -97,10 +82,6 @@
     ), "Failed to access Docker. Please make sure Docker is running and you have access. Alternatively, you can try to run without Docker by setting the `CONTAINER` environment variable to `native` (see https://leandojo.readthedocs.io/en/latest/user-guide.html#advanced-running-within-docker)."
     os.system(f"docker pull {DOCKER_TAG} 1>/dev/null 2>/dev/null")
 
-MIN_LEAN3_VERSION = "v3.42.1"
-"""The minimum version of Lean 3 that LeanDojo supports.
-"""
-
 
 def check_git_version(min_version: Tuple[int, int, int]) -> Tuple[int, int, int]:
     """Check the version of Git installed on the system."""