"""Fase 6 / Objetivo 7 — publicar la demo como Space de Gradio en HF Hub. El Space sirve la pestaña **Buscar** sobre el índice publicado por `scripts/publish_hf.py` (se descarga al arrancar vía `RAGSOLVER_HF_DATASET`); **Resolver** necesita Lean 4 + Mathlib y una API key, así que en el Space muestra un aviso (sólo local). Sube `app.py`, el paquete `ragsolver/`, `configs/`, `requirements.txt` y la tarjeta del Space, y con ellos el resto del repositorio que pide la propuesta (docs, notebooks, tests, scripts, dependencias, LICENSE, CITATION), tras la misma comprobación de contenido del PDF que `publish_hf.py` (SEC-2). Desde 2026 los Spaces de Gradio en `cpu-basic` piden suscripción PRO (HTTP 402): con `--model` se sube lo mismo como repositorio de modelo (gratis) y la demo se corre en local (`bash scripts/demo_up.sh`). Uso: HF_TOKEN=... python scripts/publish_space.py --repo /ragsolver --dataset /ragsolver-index [--model] [--dry-run] """ from __future__ import annotations import argparse import json import os import sys import tempfile from pathlib import Path sys.path.insert(0, str(Path(__file__).resolve().parent)) from check_no_leaked_content import check as _check_leaks # noqa: E402 GRADIO = "6.28.0" # la versión con la que se probó demo/app.py REQUIREMENTS = """pydantic>=2.9 pyyaml>=6.0 lancedb>=0.17 pyarrow>=17.0 pandas>=2.2 sentence-transformers>=3.3 transformers>=4.51 torch>=2.4 accelerate>=1.0 huggingface_hub>=0.26 langgraph>=0.2 httpx tenacity """ SPACE_YAML = """--- title: RagSolver emoji: 🧮 colorFrom: indigo colorTo: green sdk: gradio sdk_version: {gradio} python_version: "3.12" app_file: app.py pinned: false license: apache-2.0 --- """ MODEL_YAML = """--- license: apache-2.0 tags: [lean4, mathlib, retrieval, rag, theorem-proving, olympiad, multi-agent] datasets: [{dataset}] --- """ CARD = """# RagSolver — búsqueda de lemas de Mathlib (Lean 4, v4.28.0-rc1) Recuperación híbrida (Qwen3-Embedding-0.6B + BM25, RRF) sobre {n_full} declaraciones de Mathlib informalizadas por LeanSearch v2, con citas (nombre, módulo, enlace a la documentación). Índice: [`{dataset}`](https://huggingface.co/datasets/{dataset}). El modo *Resolver* (agentes + verificación con el kernel de Lean) requiere una instalación local: `docs/install.md`. {demo} Este repositorio contiene el proyecto completo ([GitHub](https://github.com/camiloAndres11/RagSolver)): `ragsolver/` (agentes, orquestador, recuperación, Lean), `configs/`, `docs/` (arquitectura, instalación, guía de uso, interfaces, reproducción de cada ablación, informes de resultados e informe final), `notebooks/`, `tests/`, `scripts/`, `pyproject.toml` + `uv.lock`, `LICENSE` (Apache-2.0) y `CITATION.cff`. """ def main() -> None: ap = argparse.ArgumentParser() ap.add_argument("--repo", required=True, help="/ragsolver (Space)") ap.add_argument("--dataset", required=True, help="/ragsolver-index (publicado con publish_hf.py)") ap.add_argument("--model", action="store_true", help="repositorio de modelo en vez de Space (sin PRO)") ap.add_argument("--dry-run", action="store_true") args = ap.parse_args() n_full = "278 160" variables = {"RAGSOLVER_HF_DATASET": args.dataset, "RAGSOLVER_MATHLIB_TABLE": "mathlib_full", "GRADIO_SERVER_NAME": "0.0.0.0"} files = {"app.py": "demo/app.py", **{f: f for f in ("LICENSE", "CITATION.cff", "pyproject.toml", "uv.lock")}} folders = {"ragsolver": "src/ragsolver", "configs": "configs", **{d: d for d in ("docs", "notebooks", "tests", "scripts")}} upload = [Path(f) for f in files.values()] + [f for d in folders.values() for f in Path(d).rglob("*") if f.is_file() and "__pycache__" not in f.parts] leaks = _check_leaks(upload) if leaks: raise SystemExit("SEC-2: texto del corpus informal en lo que se iba a subir — publish abortado:\n" + "\n".join(leaks)) print(json.dumps({"space": args.repo, "variables": variables, "files": files, "folders": folders}, indent=2, ensure_ascii=False)) if args.dry_run: return from huggingface_hub import HfApi api = HfApi(token=os.environ.get("HF_TOKEN")) repo_type = "model" if args.model else "space" api.create_repo(args.repo, repo_type=repo_type, exist_ok=True, **({} if args.model else {"space_sdk": "gradio"})) demo = "La demo (`app.py`, Gradio) se corre en local: `bash scripts/demo_up.sh` (`docs/user_guide.md`)." if args.model else "" card = (MODEL_YAML if args.model else SPACE_YAML).format(dataset=args.dataset, gradio=GRADIO) + CARD.format(n_full=n_full, dataset=args.dataset, demo=demo) with tempfile.TemporaryDirectory() as tmp: (Path(tmp) / "README.md").write_text(card, encoding="utf-8") (Path(tmp) / "requirements.txt").write_text(REQUIREMENTS, encoding="utf-8") for name in ("README.md", "requirements.txt"): api.upload_file(path_or_fileobj=str(Path(tmp) / name), path_in_repo=name, repo_id=args.repo, repo_type=repo_type) for dst, src in files.items(): api.upload_file(path_or_fileobj=src, path_in_repo=dst, repo_id=args.repo, repo_type=repo_type) for dst, src in folders.items(): api.upload_folder(folder_path=src, path_in_repo=dst, repo_id=args.repo, repo_type=repo_type, ignore_patterns=["__pycache__/*", "*.pyc"]) for k, v in ({} if args.model else variables).items(): api.add_space_variable(args.repo, k, v) print("ok") if __name__ == "__main__": main()