API Reference

This API reference is generated automatically from docstrings by autodoc.

• lean_dojo.data_extraction
  • lean_dojo.data_extraction.lean
    • GITHUB_ACCESS_TOKEN
    • LEAN4_NIGHTLY_REPO
    • LEAN4_REPO
    • LeanFile
    • LeanGitRepo
    • Pos
    • RepoInfoCache
    • RepoType
    • Theorem
    • cleanse_string()
    • get_latest_commit()
    • get_lean4_commit_from_config()
    • get_lean4_version_from_config()
    • get_repo_type()
    • is_commit_hash()
    • is_supported_version()
    • normalize_url()
    • ssh_to_https()
    • url_to_repo()
  • lean_dojo.data_extraction.trace
    • check_files()
    • get_lean_version()
    • get_traced_repo_path()
    • is_available_in_cache()
    • is_new_version()
    • launch_progressbar()
    • trace()
  • lean_dojo.data_extraction.traced_data
    • Comment
    • TracedFile
    • TracedRepo
    • TracedTactic
    • TracedTheorem
    • get_code_without_comments()
  • lean_dojo.data_extraction.ast
    • lean_dojo.data_extraction.ast
• lean_dojo.interaction
  • lean_dojo.interaction.dojo
    • CommandState
    • Dojo
    • DojoCrashError
    • DojoInitError
    • DojoTacticTimeoutError
    • LeanError
    • ProofFinished
    • ProofGivenUp
    • TacticState
    • kill_descendants()
  • lean_dojo.interaction.parse_goals
    • Declaration
    • Goal
    • parse_goals()
• lean_dojo.constants
  • CACHE_DIR
  • DISABLE_REMOTE_CACHE
  • LEAN4_PACKAGES_DIR
  • LEAN4_URL
  • LOAD_USED_PACKAGES_ONLY
  • NUM_PROCS
  • REMOTE_CACHE_URL
  • TACTIC_CPU_LIMIT
  • TACTIC_MEMORY_LIMIT
  • TMP_DIR
  • check_git_version()