import argparse
import json
from pathlib import Path
from .core import HTTPProvider, CommandProvider, LeanVerifier, solve

def options(parser):
    parser.add_argument('--model', default='local-model')
    parser.add_argument('--base-url', default='http://localhost:8000/v1')
    parser.add_argument('--api-key-env', default='LLM_API_KEY')
    parser.add_argument('--provider-command', help='JSON argv array; stdin JSON messages, stdout proof')
    parser.add_argument('--lean-command', default='["lean"]', help='JSON argv array; e.g. ["lake","env","lean"]')
    parser.add_argument('--lean-project', help='Lean/Lake project working directory')
    parser.add_argument('--attempts', type=int, default=3)
    parser.add_argument('--lean-timeout', type=float, default=30)
    parser.add_argument('--llm-timeout', type=float, default=120)

def components(args):
    provider = (CommandProvider(json.loads(args.provider_command), args.llm_timeout)
        if args.provider_command else HTTPProvider(args.model, args.base_url, args.api_key_env, args.llm_timeout))
    return provider, LeanVerifier(json.loads(args.lean_command), args.lean_project, args.lean_timeout)

def main():
    parser = argparse.ArgumentParser(description='Prove one Lean theorem with any LLM')
    parser.add_argument('task', type=Path, help='JSON with id, statement, optional prelude')
    options(parser)
    args = parser.parse_args()
    result = solve(*components(args), json.loads(args.task.read_text()), args.attempts)
    print(json.dumps(result, ensure_ascii=False, indent=2))
    raise SystemExit(0 if result['success'] else 1)

if __name__ == '__main__': main()