Merge pull request #52 from lean-dojo/dev

Fix minor bugs
lean-dojo · Sep 5, 2023 · 310e896 · 310e896
2 parents 362428c + f474520
commit 310e896
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 95 deletions.
diff --git a/pyproject.toml b/pyproject.toml
@@ -13,7 +13,7 @@ exclude = [
 
 [project]
 name = "lean-dojo"
-version = "1.2.2"
+version = "1.2.4"
 authors = [
   { name="Kaiyu Yang", email="[email protected]" },
 ]

diff --git a/scripts/demo-lean4.ipynb b/scripts/demo-lean4.ipynb
@@ -97,9 +97,9 @@
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "\u001b[32m2023-08-13 15:02:44.367\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m163\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib4-355541ae7a2455222f179dcf7f074aa2c45eb8aa/mathlib4\u001b[0m\n",
-      "2023-08-13 15:02:46,441\tINFO worker.py:1627 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
-      "100%|████████████████████████████████████████| 4264/4264 [07:58<00:00,  8.91it/s]\n"
+      "\u001b[32m2023-09-05 16:11:21.442\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m163\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib4-355541ae7a2455222f179dcf7f074aa2c45eb8aa/mathlib4\u001b[0m\n",
+      "2023-09-05 16:11:23,966\tINFO worker.py:1612 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
+      "100%|██████████████████████████████████| 4264/4264 [07:46<00:00,  9.14it/s]\n"
      ]
     }
    ],
@@ -117,7 +117,7 @@
     {
      "data": {
       "text/plain": [
-       "<networkx.classes.digraph.DiGraph at 0x7f08ea31df00>"
+       "<networkx.classes.digraph.DiGraph at 0x7f2049695f60>"
       ]
      },
      "execution_count": 6,
@@ -1907,7 +1907,7 @@
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "\u001b[32m2023-08-13 15:11:47.807\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m172\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n"
+      "\u001b[32m2023-09-05 16:20:35.194\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m173\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n"
      ]
     }
    ],
@@ -2063,7 +2063,7 @@
       "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
       "\u001b[0;31mRuntimeError\u001b[0m                              Traceback (most recent call last)",
       "Cell \u001b[0;32mIn[27], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mdojo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mrun_tac\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstate_2\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mskip\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m)\u001b[49m\n",
-      "File \u001b[0;32m~/LeanDojo/src/lean_dojo/interaction/dojo.py:474\u001b[0m, in \u001b[0;36mDojo.run_tac\u001b[0;34m(self, state, tactic)\u001b[0m\n\u001b[1;32m    472\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrun_tac\u001b[39m(\u001b[38;5;28mself\u001b[39m, state: TacticState, tactic: \u001b[38;5;28mstr\u001b[39m) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m TacticResult:\n\u001b[1;32m    473\u001b[0m     \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(state, TacticState):\n\u001b[0;32m--> 474\u001b[0m         \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\n\u001b[1;32m    475\u001b[0m             \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mAttempting to run a tactic on an invalid state \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mstate\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m.\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m    476\u001b[0m         )\n\u001b[1;32m    477\u001b[0m     \u001b[38;5;28;01massert\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(tactic, \u001b[38;5;28mstr\u001b[39m), \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mInvalid tactic \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mtactic\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m    479\u001b[0m     tsid \u001b[38;5;241m=\u001b[39m state\u001b[38;5;241m.\u001b[39mid\n",
+      "File \u001b[0;32m~/LeanDojo/src/lean_dojo/interaction/dojo.py:478\u001b[0m, in \u001b[0;36mDojo.run_tac\u001b[0;34m(self, state, tactic)\u001b[0m\n\u001b[1;32m    476\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrun_tac\u001b[39m(\u001b[38;5;28mself\u001b[39m, state: TacticState, tactic: \u001b[38;5;28mstr\u001b[39m) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m TacticResult:\n\u001b[1;32m    477\u001b[0m     \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(state, TacticState):\n\u001b[0;32m--> 478\u001b[0m         \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\n\u001b[1;32m    479\u001b[0m             \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mAttempting to run a tactic on an invalid state \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mstate\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m.\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m    480\u001b[0m         )\n\u001b[1;32m    481\u001b[0m     \u001b[38;5;28;01massert\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(tactic, \u001b[38;5;28mstr\u001b[39m), \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mInvalid tactic \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mtactic\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m    483\u001b[0m     tsid \u001b[38;5;241m=\u001b[39m state\u001b[38;5;241m.\u001b[39mid\n",
       "\u001b[0;31mRuntimeError\u001b[0m: Attempting to run a tactic on an invalid state LeanError(error='<stdin>:1:1: unknown tactic')."
      ]
     }
@@ -2074,64 +2074,20 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": null,
    "id": "65bae6ea",
    "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "ProofGivenUp()"
-      ]
-     },
-     "execution_count": 28,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
+   "outputs": [],
    "source": [
     "dojo.run_tac(state_0, \"sorry\")"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
+   "execution_count": null,
    "id": "c373865a",
    "metadata": {},
-   "outputs": [
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "R✝ : Type u_1\n",
-      "R₁ : Type u_2\n",
-      "R₂ : Type u_3\n",
-      "R₃ : Type u_4\n",
-      "R₄ : Type u_5\n",
-      "S : Type u_6\n",
-      "K : Type u_7\n",
-      "K₂ : Type u_8\n",
-      "M : Type u_9\n",
-      "M' : Type u_10\n",
-      "M₁ : Type u_11\n",
-      "M₂ : Type u_12\n",
-      "M₃ : Type u_13\n",
-      "M₄ : Type u_14\n",
-      "N : Type u_15\n",
-      "N₂ : Type u_16\n",
-      "ι✝ : Type u_17\n",
-      "V : Type u_18\n",
-      "V₂ : Type u_19\n",
-      "ι : Type u_20\n",
-      "inst✝² : Fintype ι\n",
-      "inst✝¹ : DecidableEq ι\n",
-      "R : Type u_21\n",
-      "inst✝ : Semiring R\n",
-      "x : ι → R\n",
-      "⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n"
-     ]
-    }
-   ],
+   "outputs": [],
    "source": [
     "print(state_0.pp)"
    ]
@@ -2234,15 +2190,15 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 33,
+   "execution_count": 34,
    "id": "243ea43c",
    "metadata": {},
    "outputs": [
     {
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "\u001b[32m2023-08-13 15:13:17.383\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m172\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n"
+      "\u001b[32m2023-09-05 06:39:10.260\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m173\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n"
      ]
     }
    ],
@@ -2253,7 +2209,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 34,
+   "execution_count": 35,
    "id": "5ebd615c",
    "metadata": {},
    "outputs": [
@@ -2263,7 +2219,7 @@
        "CommandState(id=0, message=None)"
       ]
      },
-     "execution_count": 34,
+     "execution_count": 35,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2274,7 +2230,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 36,
    "id": "b1e079fa",
    "metadata": {},
    "outputs": [
@@ -2284,7 +2240,7 @@
        "CommandState(id=1, message='1')"
       ]
      },
-     "execution_count": 35,
+     "execution_count": 36,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2295,7 +2251,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 36,
+   "execution_count": 37,
    "id": "31c9bada",
    "metadata": {},
    "outputs": [
@@ -2305,7 +2261,7 @@
        "LeanError(error=\"unknown identifier 'x'\")"
       ]
      },
-     "execution_count": 36,
+     "execution_count": 37,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2316,7 +2272,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 37,
+   "execution_count": 38,
    "id": "b638bfbf",
    "metadata": {},
    "outputs": [
@@ -2326,7 +2282,7 @@
        "CommandState(id=3, message='')"
       ]
      },
-     "execution_count": 37,
+     "execution_count": 38,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2339,7 +2295,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 38,
+   "execution_count": 39,
    "id": "bdc4f14d",
    "metadata": {},
    "outputs": [
@@ -2349,7 +2305,7 @@
        "CommandState(id=4, message='1')"
       ]
      },
-     "execution_count": 38,
+     "execution_count": 39,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2360,7 +2316,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 39,
+   "execution_count": 40,
    "id": "ef47afb8",
    "metadata": {},
    "outputs": [
@@ -2370,7 +2326,7 @@
        "CommandState(id=5, message='Finsupp.smul_sum.{u_23, u_22, u_21, u_20} {α : Type u_20} {β : Type u_21} {R : Type u_22} {M : Type u_23}\\n[inst✝ : Zero β] [inst✝¹ : AddCommMonoid M] [inst✝² : DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} :\\nc • sum v h = sum v fun a b => c • h a b')"
       ]
      },
-     "execution_count": 39,
+     "execution_count": 40,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2381,7 +2337,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 40,
+   "execution_count": 41,
    "id": "c6b8b9a5",
    "metadata": {},
    "outputs": [
@@ -2391,7 +2347,7 @@
        "LeanError(error=\"unknown identifier 'sum_smul_index_linearMap''\")"
       ]
      },
-     "execution_count": 40,
+     "execution_count": 41,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -2403,7 +2359,7 @@
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "173f21d8",
+   "id": "c67d7931",
    "metadata": {},
    "outputs": [],
    "source": []

diff --git a/src/lean_dojo/__init__.py b/src/lean_dojo/__init__.py
@@ -12,7 +12,6 @@
     TracedTheorem,
     TracedTactic,
 )
-from .utils import set_lean_dojo_logger
 from .interaction.dojo import (
     CommandState,
     TacticState,
@@ -30,10 +29,5 @@
 from .data_extraction.lean import LeanGitRepo, LeanFile, Theorem, Pos
 from .constants import __version__
 
-if "VERBOSE" in os.environ or "DEBUG" in os.environ:
-    set_lean_dojo_logger(verbose=True)
-else:
-    set_lean_dojo_logger(verbose=False)
-
 if os.geteuid() == 0:
     raise RuntimeError("LeanDojo should not be run as root.")
diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py
@@ -3,6 +3,7 @@
 """
 import os
 import re
+import sys
 import subprocess
 import multiprocessing
 from github import Auth
@@ -12,7 +13,13 @@
 from loguru import logger
 
 
-__version__ = "1.2.2"
+__version__ = "1.2.4"
+
+logger.remove()
+if "VERBOSE" in os.environ or "DEBUG" in os.environ:
+    logger.add(sys.stderr, level="DEBUG")
+else:
+    logger.add(sys.stderr, level="INFO")
 
 CACHE_DIR = (
     Path(os.environ["CACHE_DIR"])

diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py
@@ -282,7 +282,7 @@ def get_lean4_commit_from_config(config: str) -> str:
     prefix = "leanprover/lean4:"
 
     if config == f"{prefix}nightly":
-        latest_tag = next(LEAN4_NIGHTLY_REPO.get_tags())
+        latest_tag = LEAN4_NIGHTLY_REPO.get_tags()[0]
         return latest_tag.commit.sha
 
     assert config.startswith(prefix), f"Invalid Lean 4 version: {config}"

diff --git a/src/lean_dojo/utils.py b/src/lean_dojo/utils.py
@@ -144,21 +144,6 @@ def camel_case(s: str) -> str:
     return _CAMEL_CASE_REGEX.sub(" ", s).title().replace(" ", "")
 
 
-def set_lean_dojo_logger(verbose: bool) -> None:
-    """Set loguru's logging level.
-
-    The effect of this function is global, and it should be called only once in the main function.
-
-    Args:
-        verbose (bool): Whether to print debug information.
-    """
-    logger.remove()
-    if verbose:
-        logger.add(sys.stderr, level="DEBUG")
-    else:
-        logger.add(sys.stderr, level="INFO")
-
-
 def get_repo_info(path: Path) -> Tuple[str, str]:
     """Get the URL and commit hash of the Git repo at ``path``.