| # Todo lo de la demo con un comando: demostrador en la GPU + demo Gradio en http://127.0.0.1:7860. | |
| # La demo precalienta Lean (`import Mathlib`, ~5 min) y el embedder en segundo plano al arrancar: | |
| # lánzala unos minutos antes de presentar. Ctrl+C cierra la demo; el demostrador sigue hasta | |
| # `bash scripts/prover_server.sh stop`. | |
| set -eu | |
| cd "$(dirname "$0")/.." | |
| bash scripts/prover_server.sh start | |
| export RAGSOLVER_MATHLIB_TABLE="${RAGSOLVER_MATHLIB_TABLE:-mathlib_full}" PYTHONUNBUFFERED=1 | |
| exec .venv/bin/python demo/app.py | |