DojoInitError: Cannot find the *.ast.json file for Theorem

[HorHang]

While I am trying to use LeanDjo to interact with LeanDojo programatically, below issue occurred. I think I don't have the *.ast.json file. How to get those files?

Run Code:

from lean_dojo import *
from ReProver.common import *
URL = "https://github.com/leanprover-community/mathlib4"
COMMIT = "20c73142afa995ac9c8fb80a9bb585a55ca38308"
repo = LeanGitRepo(URL, COMMIT)
theorem = Theorem(repo, thm.theorem.file_path, thm.theorem.full_name)
with Dojo(theorem) as (dojo, init_state):
       dojo.run_tac()

Error:

During handling of the above exception, another exception occurred:

DojoInitError                             Traceback (most recent call last)
Cell In[15], [line 25](vscode-notebook-cell:?execution_count=15&line=25)
     [21](vscode-notebook-cell:?execution_count=15&line=21)             unproof_theorems.append((thm_name, id))
     [23](vscode-notebook-cell:?execution_count=15&line=23)     return proof_theorems, unproof_theorems
---> [25](vscode-notebook-cell:?execution_count=15&line=25) proof_theorems, unproof_theorems = verified_all_theorems(dojo_matching_theorems[116:200])

Cell In[15], [line 16](vscode-notebook-cell:?execution_count=15&line=16)
     [13](vscode-notebook-cell:?execution_count=15&line=13) proof_ls = split_proof(commented_proof, pf_pattern)
     [14](vscode-notebook-cell:?execution_count=15&line=14) proof_steps = get_single_step_proof(proof_ls, pattern, tac_pattern)
---> [16](vscode-notebook-cell:?execution_count=15&line=16) thm_name, proof_finished = verified_single_theorem(theorem, proof_steps)
     [18](vscode-notebook-cell:?execution_count=15&line=18) if proof_finished:
     [19](vscode-notebook-cell:?execution_count=15&line=19)     proof_theorems.append((thm_name, id))

Cell In[10], [line 6](vscode-notebook-cell:?execution_count=10&line=6)
      [5](vscode-notebook-cell:?execution_count=10&line=5) def verified_single_theorem(theorem: Theorem, proof_steps: List[str]):
----> [6](vscode-notebook-cell:?execution_count=10&line=6)     with Dojo(theorem) as (dojo, init_state):
      [7](vscode-notebook-cell:?execution_count=10&line=7)       result = init_state
      [8](vscode-notebook-cell:?execution_count=10&line=8)       for t in proof_steps:

File ~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:165, in Dojo.__enter__(self)
    [163](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:163)     traced_file = self._locate_traced_file(traced_repo_path)
    [164](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:164) except FileNotFoundError:
--> [165](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:165)     raise DojoInitError(
    [166](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:166)         f"Cannot find the *.ast.json file for {self.entry} in {traced_repo_path}."
    [167](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:167)     )
    [169](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:169) self._modify_file(traced_file)
    [171](https://file+.vscode-resource.vscode-cdn.net/home/user/~/miniconda3/envs/ReProver/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py:171) # Run the modified file in a container.

DojoInitError: Cannot find the *.ast.json file for Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='20c73142afa995ac9c8fb80a9bb585a55ca38308'), file_path=PosixPath('src/lean/Init/Data/List/Erase.lean'), full_name='List.eraseP_cons_of_pos') in projects/.cache/lean_dojo/leanprover-community-mathlib4-20c73142afa995ac9c8fb80a9bb585a55ca38308/mathlib4.

System Version:

Lake version 5.0.0-306f361 (Lean version 4.17.0)
Lean (version 4.17.0, x86_64-unknown-linux-gnu, commit 306f36116535, Release)
lean-dojo v2.2.0
Python 3.11.8

[HorHang]

Another thing, how could we dojo.run_tac() on multiple tactics or single line contain ;? Some seems to work while other doesn't.

Example:

1. theorem Finset.map_nsmul_piAntidiag can run tactic \n classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn but if we split based on ; and run_tac separately, it going to run into error.
2. Conversely, theorem CommSemiring.toSemiring_injective cannot run tactic \n rintro ⟨⟩ ⟨⟩ _; congr. However, if we split it and run separately, it going to lead to Proof_Finished.
3. For theorem dist_le_Ico_sum_dist, how to run multiple line tactics like below:

  induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
  | succ n hle ihn =>
    calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
      { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }