Skip to content

Commit

Permalink
minor fix
Browse files Browse the repository at this point in the history
  • Loading branch information
yangky11 committed Sep 18, 2024
1 parent cef522f commit 6db9fc7
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions src/lean_dojo/data_extraction/lean.py
Original file line number Diff line number Diff line change
Expand Up @@ -447,10 +447,7 @@ def get_lean4_commit_from_config(config_dict: Dict[str, Any]) -> str:
if LEAN4_REPO is None:
LEAN4_REPO = GITHUB.get_repo("leanprover/lean4")
assert "content" in config_dict, "config_dict must have a 'content' field"
config = config_dict["content"].strip()
prefix = "leanprover/lean4:"
assert config.startswith(prefix), f"Invalid Lean 4 version: {config}"
version = config[len(prefix) :]
version = get_lean4_version_from_config(config_dict["content"].strip())
if version.startswith("nightly-"):
global LEAN4_NIGHTLY_REPO
if LEAN4_NIGHTLY_REPO is None:
Expand Down

0 comments on commit 6db9fc7

Please sign in to comment.