check if the traced repo is outdated

lean-dojo · Jul 17, 2024 · 2ff92a4 · 2ff92a4
1 parent 9fdb429
commit 2ff92a4
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/lean_dojo/interaction/dojo.py b/src/lean_dojo/interaction/dojo.py
@@ -160,6 +160,11 @@ def __enter__(self) -> Tuple["Dojo", State]:
 
         # Replace the human-written proof with a `repl` tactic.
         traced_repo_path = get_traced_repo_path(self.repo)
+        repl_path = traced_repo_path / "Lean4Repl.lean"
+        assert (
+            repl_path.exists()
+        ), "Unable to find Lean4Repl.lean in the traced repo. The traced repo was likely produced by an outdated version of LeanDojo. See https://github.com/lean-dojo/LeanDojo/releases/tag/v2.0.0."
+
         try:
             traced_file = self._locate_traced_file(traced_repo_path)
         except FileNotFoundError: