Spaces:
Running
Running
File size: 1,092 Bytes
3ac681e 6cf7e7c 3ac681e | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 | #!/usr/bin/env python3
import argparse
import os
import sys
sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
from langgraph_agent import LangGraphAgent
def main():
parser = argparse.ArgumentParser(description="Run the LangGraph Lean Proof Agent on a file.")
parser.add_argument("file", help="Path to the .lean file to solve")
parser.add_argument("--model", default="qwen3-vl:4b", help="Ollama model name")
parser.add_argument("--retries", type=int, default=5, help="Max retries")
parser.add_argument("--index-dir", default=None, help="Path to pre-built FAISS index directory")
args = parser.parse_args()
print(f"Starting LangGraph Proof Agent with model: {args.model}")
agent = LangGraphAgent(
model_name=args.model,
max_retries=args.retries,
index_dir=args.index_dir,
)
success = agent.solve_file(args.file)
if success:
print("\nSuccess! The proof has been verified.")
else:
print("\nFailed to verify the proof.")
if __name__ == "__main__":
main()
|