Error when entering theorem with doc comment

[vasnesterov]

It seems that LeanDojo cannot enter a theorem if there is a documentation comment above it. I found out that this occurs because writing anything between the doc comment and the definition in Lean causes an error. For example, we cannot write

/--
Some docs
-/
set_option maxHeartbeats 0 in
theorem foo : 1 = 1 := by sorry

and after modifying the .lean file this way Lake is unable to build it.

Minimal example:

from lean_dojo import *

repo = LeanGitRepo(
    "https://github.com/leanprover-community/mathlib4",
    "3c307701fa7e9acbdc0680d7f3b9c9fed9081740",
)

theorem = Theorem(repo, "Mathlib/Topology/Order/Basic.lean", "TFAE_mem_nhdsWithin_Iio")

dojo, state_0 = Dojo(theorem).__enter__()

This code raises the exception

DojoCrashError: Mathlib/Topology/Order/Basic.lean:926:2: error: [fatal] not_a_theorem

[yangky11]

Thanks for reporting this bug. I just fixed it in the latest version (v1.8.0). Could you please try and let me know?

[yangky11]

Closing due to inactivity.