update

src/lean_dojo/data_extraction/ast.py

@@ -1179,7 +1179,7 @@ def is_private(self) -> bool:
 
     def get_proof_node(self) -> Node:
         decl_val_node = self.children[3]
-        if isinstnace(
+        if isinstance(
             decl_val_node,
             (
                 CommandDeclvalsimpleNode,

tests/conftest.py

@@ -3,7 +3,7 @@
 from lean_dojo import *
 
 
-BATTERIES_URL = "https://github.com/leanprover/batteries"
+BATTERIES_URL = "https://github.com/leanprover-community/batteries"
 AESOP_URL = "https://github.com/leanprover-community/aesop"
 MATHLIB4_URL = "https://github.com/leanprover-community/mathlib4"
 LEAN4_EXAMPLE_URL = "https://github.com/yangky11/lean4-example"

tests/interaction/test_tactics.py

@@ -36,7 +36,7 @@ def test_example_pow_two_pow_sub_pow_two_pow(mathlib4_repo: LeanGitRepo) -> None
 def test_example_mem_nil_iff(batteries_repo: LeanGitRepo) -> None:
     thm = Theorem(
         batteries_repo,
-        "Std/Data/List/Lemmas.lean",
+        "Batteries/Data/List/Lemmas.lean",
         "List.mem_nil_iff",
     )
     with Dojo(thm) as (dojo, s0):
@@ -141,7 +141,7 @@ def test_example_coe_monoidHom_mk(mathlib4_repo: LeanGitRepo) -> None:
 def test_example_length_le(batteries_repo: LeanGitRepo) -> None:
     thm = Theorem(
         batteries_repo,
-        "Std/Data/List/Lemmas.lean",
+        "Batteries/Data/List/Lemmas.lean",
         "List.IsSuffix.length_le",
     )
     with Dojo(thm) as (dojo, s0):
@@ -282,7 +282,7 @@ def test_example_mem_eqLocus(mathlib4_repo: LeanGitRepo) -> None:
 def test_example_neg_lt_sub_right_of_lt_add(batteries_repo: LeanGitRepo) -> None:
     thm = Theorem(
         batteries_repo,
-        "Std/Data/Int/Order.lean",
+        "Batteries/Data/Int/Order.lean",
         "Int.neg_lt_sub_right_of_lt_add",
     )
     with Dojo(thm) as (dojo, s0):