From 9afa3042f960ff4bf7110f342afedbd38f39266a Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 20 Dec 2023 12:37:08 -0800 Subject: [PATCH 1/2] minor edits --- src/lean_dojo/constants.py | 4 ++-- src/lean_dojo/container.py | 8 -------- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py index 8c9cd98..d62d966 100644 --- a/src/lean_dojo/constants.py +++ b/src/lean_dojo/constants.py @@ -98,11 +98,11 @@ """ TACTIC_CPU_LIMIT = int(os.getenv("TACTIC_CPU_LIMIT", 1)) -"""Number of CPUs for executing tactics when interacting with Lean. +"""Number of CPUs for executing tactics when interacting with Lean (only useful when running within Docker). """ TACTIC_MEMORY_LIMIT = os.getenv("TACTIC_MEMORY_LIMIT", "32g") -"""Maximum memory when interacting with Lean. +"""Maximum memory when interacting with Lean (only useful when running within Docker). """ CONTAINER = os.getenv("CONTAINER", "native") diff --git a/src/lean_dojo/container.py b/src/lean_dojo/container.py index ab912d5..f23e5fd 100644 --- a/src/lean_dojo/container.py +++ b/src/lean_dojo/container.py @@ -205,14 +205,6 @@ def run_interactive( work_dir: Optional[str] = None, ) -> subprocess.Popen: assert as_current_user, "NativeContainer can only run as the current user." - if cpu_limit is not None: - logger.warning( - f"Disregarding `cpu_limit = {cpu_limit} since NativeContainer does not support CPU limit.`" - ) - if memory_limit is not None: - logger.warning( - f"Disregarding `memory_limit = {memory_limit}` since NativeContainer does not support memory limit." - ) self._mount_files(mounts) self.mounts = mounts From 0400d8507e9d81a1f984bb58b0c7164e84fef58e Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 20 Dec 2023 12:37:47 -0800 Subject: [PATCH 2/2] bump --- pyproject.toml | 2 +- src/lean_dojo/constants.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 6caa669..2e7f4f4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -13,7 +13,7 @@ exclude = [ [project] name = "lean-dojo" -version = "1.4.4" +version = "1.4.5rc" authors = [ { name="Kaiyu Yang", email="kaiyuy@caltech.edu" }, ] diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py index 0c8c876..c710c42 100644 --- a/src/lean_dojo/constants.py +++ b/src/lean_dojo/constants.py @@ -15,7 +15,7 @@ load_dotenv() -__version__ = "1.4.4" +__version__ = "1.4.5rc" logger.remove() if "VERBOSE" in os.environ or "DEBUG" in os.environ: