docs/PLAN_CORRECCIONES.md

# Plan de corrección — hallazgos de la auditoría del 2026-09-23

> Documento de ejecución para el agente implementador. Fuente de los hallazgos (IDs SEC-, VER-, BUG-, …): [`AUDIT_2026-09-23.md`](AUDIT_2026-09-23.md).
> Fecha: 2026-09-23. Idioma de trabajo: español; código, prompts y comentarios de código siguen en el idioma que ya usa cada archivo.

---

## 0. Cómo usar este documento

- Plan **por fases**. Cada fase trae objetivo, hallazgos que cierra, tareas numeradas, archivos, criterios de aceptación medibles, plan B, esfuerzo y costo en US$. No se pasa a la siguiente fase sin cumplir los criterios de aceptación, salvo que la sección 7 marque que dos fases son independientes.
- **Reglas de trabajo** (valen para todas las fases):
  1. **Corrección mínima en el lugar correcto.** Rige la misma regla de `PLAN_RAG.md §0` (sin sobreingeniería, sin abstracciones de una sola implementación). Un arreglo va en la función por la que pasan todos los llamadores, no en cada llamador.
  2. **Todo bug empieza con un test de regresión que falla**; después viene el arreglo.
  3. **Toda decisión o desvío se registra en `docs/DECISIONS.md`**, con el formato existente y numeración a partir de **#69**.
  4. **Si cambia un contrato Pydantic**, se regeneran los JSON Schema con `python scripts/export_schemas.py` y se comprueba que siguen sincronizados.
  5. **Los resultados ya reportados de `eval-v1` no se reescriben en su sitio.** Si un arreglo cambia una cifra publicada, se recalcula desde los datos guardados (0 llamadas LLM), se escribe en un archivo nuevo y se actualiza el informe con una nota del cambio.
  6. **Ninguna llamada de pago sin aprobación explícita del usuario.** La key tiene un tope de US$2,00 y quedan unos US$0,42.
  7. **Operación en esta máquina** (7,5 GB de RAM, repo en `/mnt/c`):
     - Un solo proceso con modelos cargados a la vez.
     - Corridas largas con `setsid nohup … < /dev/null &` y log persistente en `data/eval/results/`.
     - Nunca `uv add` ni `uv sync` con una corrida en marcha. Siempre `uv sync --extra dev --extra ingest` (más `--extra demo` desde la Fase 3).
     - El REPL de Lean se usa desde `~/ragsolver_cache/lean_project`.
  8. **Después de cambiar código**, ejecutar `graphify update .` (lo pide `CLAUDE.md`).
  9. **No hacer commit ni push** salvo que el usuario lo pida explícitamente.
  10. **Cierre de cada fase:** la suite pasa (`uv run pytest -q --deselect tests/test_retriever_integration.py`, más la integración cuando aplique) y la documentación afectada queda actualizada en la misma fase.

---

## 1. Decisiones que necesita el usuario

| # | Decisión | Se necesita en | Opción recomendada |
|---|---|---|---|
| D1 | Licencia del repositorio | Fase 9 (antes del commit) | Apache-2.0, coherente con `CITATION.cff`, Mathlib, miniF2F-v2 y Qwen3 |
| D2 | Commit y push de la rama (habilita el CI) | Fase 6.4 y Fase 9 | Tras cerrar las Fases 1–3 |
| D3 | Qué hacer con `blobs/` (caché de MinerU con el texto del PDF) | Fase 2 | Ignorarlo en git; borrarlo sólo si el usuario lo confirma |
| D4 | Alcance de la ingesta informal | Fase 5 | Guard de un solo documento con metadatos correctos; multidocumento sólo si hay un segundo PDF real |
| D5 | Replan | Fase 7 | Pasar el feedback del Crítico al Planificador (0 llamadas extra); alternativa: `max_replans: 0` |
| D6 | Gasto | Fases 4.8, 7.1 y 9.4 | Smoke de 5 problemas triviales (≈ US$0,001); `eval-v1-full` (≈ US$0,30) |
| D7 | `HF_TOKEN` y nombres de los repos | Fase 9.3 | — |
| D8 | Sandbox a nivel de sistema operativo | Fase 10 | Obligatorio antes de exponer la demo fuera de localhost |

---

## 2. Estado del arte consultado y decisiones

| Tema | Qué hacen los proyectos de referencia | Decisión para RagSolver | Por qué |
|---|---|---|---|
| Validar pruebas no confiables | La guía oficial de Lean ([Validating a Lean Proof](https://lean-lang.org/doc/reference/latest/ValidatingProofs/)) define niveles: (1) el kernel acepta; (2) `#print axioms` con sólo `propext`, `Classical.choice` y `Quot.sound` (avisa de que `Lean.trustCompiler` delata evaluación nativa); (3) replay con `lean4checker`; (4) `comparator` en sandbox. Advierte que "las tácticas y el metacódigo pueden realizar acciones arbitrarias". | **Ahora, nivel 2**: lista blanca de axiomas y rechazo de comandos y metaprogramación en las tácticas. **Nivel 3/4 opcional**, sólo para las pruebas que se publiquen (Fase 10). | Cierra SEC-1 y VER-1 con pocas líneas y sin infraestructura nueva. |
| Replay del entorno | [SafeVerify](https://github.com/GasStationManager/SafeVerify): `Environment.replay` más la lista blanca de los 3 axiomas; lo usa el leaderboard de PutnamBench, y Mistral mantiene un fork para su evaluación ([LeanstralSafeVerify](https://github.com/mistralai/LeanstralSafeVerify)). Rechaza `native_decide`. | La misma lista blanca. Replay con SafeVerify sólo como verificación opcional de las pruebas publicadas. | Reutiliza una herramienta estándar en lugar de escribir un replay propio. |
| Juez de referencia | [leanprover/comparator](https://github.com/leanprover/comparator) (Lean FRO, 2026): compila en un sandbox `landrun`, exporta con `lean4export` y hace replay con el kernel oficial y con kernels independientes. | No adoptarlo por ahora. | Necesita Landlock, que **no está activo** en este kernel de WSL2 (verificado: `landlock` no aparece en `/sys/kernel/security/lsm`), y un `.olean` por problema. |
| Precedente | En los artefactos miniF2F publicados de Kimina-Prover, [15/225 soluciones dependían de `Lean.ofReduceBool`](https://github.com/MoonshotAI/Kimina-Prover-Preview/issues/11). | VER-1 se trata como un riesgo real, no teórico. | Un prover publicado cayó exactamente en este fallo. |
| Sandbox en WSL2 | bubblewrap funciona en WSL2 porque usa namespaces de usuario, y Landlock es sólo una capa adicional ([Codex linux-sandbox](https://github.com/openai/codex/blob/main/codex-rs/linux-sandbox/README.md), [lince #356](https://github.com/RisorseArtificiali/lince/issues/356)). | bubblewrap mediante un script envoltorio pasado como `lake_path` de `lean-interact` (Fase 10). | Verificado aquí: `/usr/bin/bwrap` está instalado, `max_user_namespaces = 29869`, y `LeanREPLConfig(lake_path=…)` es configurable, así que no hay que parchear la librería. |
| Reintentos de LLM | Lección propia (DECISIONS #59): los reintentos invisibles gastaron unos US$0,9. | No reintentar timeouts de lectura (pueden haberse cobrado) y contar cada intento. | Mismo tipo de fallo que LLM-1. |
| Reranker con poca RAM (2026-09-23, a pedido del usuario) | llama.cpp sirve Qwen3-Reranker de forma nativa por `/v1/rerank` (`--reranking --pooling rank --embedding`), con conversión GGUF oficial ya publicada ([`ggml-org/Qwen3-Reranker-0.6B-Q8_0-GGUF`](https://huggingface.co/ggml-org/Qwen3-Reranker-0.6B-Q8_0-GGUF); confirmado funcionando en el hilo de la propia model card de Qwen, [discusión #22](https://huggingface.co/Qwen/Qwen3-Reranker-0.6B/discussions/22)). | Reranker de los agentes por GPU vía Vulkan (Fase 7.7), mismo patrón que el embedder (#48); no se espera a una máquina con más RAM. | `tools/llama-vulkan/llama-server.exe` ya instalado es un binario genérico de llama.cpp (sirve cualquier GGUF); `/dev/dxg` confirma el passthrough de GPU activo en esta máquina; el reranker (~1,8 GB) cabe junto al embedder en los 16 GB de VRAM de la RX 9060 XT sin tocar los 7,3 GB de RAM de WSL. |

---

## 3. Mapa hallazgo → fase

| Hallazgo | Severidad | Fase | Acción |
|---|---|---|---|
| SEC-1 | HIGH | 1 (y 10) | Validación de tácticas y del enunciado de la demo; sandbox de sistema operativo con disparador |
| VER-1 | HIGH | 1 | Auditoría de axiomas con lista blanca |
| SEC-2 | HIGH | 2 | `.gitignore` y publicación saneada |
| ING-1 | HIGH | 5 | Guard, metadatos reales, `section_path` real |
| BUG-1 | MEDIUM | 4 | IDs de cita estables |
| BUG-2 | MEDIUM | 1 | Una sola fuente Lean para el REPL y el reporte |
| BUG-3 | MEDIUM | 5 | CLI con `argparse` |
| BUG-4 | MEDIUM | 5 | Rutas ancladas a la raíz del repo |
| LLM-1 | MEDIUM | 4 | Política de reintentos |
| DES-1 | MEDIUM | 7 | Replan con feedback (D5) |
| TRZ-1 | MEDIUM | 4 | `run_id` en `RetrievalContext` |
| MET-1 | MEDIUM | 3 (doc), 4 (pin), 7 (tabla por defecto) | Documentar, registrar la tabla servida, `mathlib_full` por defecto |
| DATA-1 | MEDIUM | 3 (doc), 7 (medición), 10 (corpus) | Limitación documentada; disparador medido |
| DEP-1 | MEDIUM | 3 | `pyproject.toml` |
| TEST-1…4, CI-1 | MEDIUM/LOW | 1, 4, 5, 6 | Tests por fase y CI en funcionamiento |
| ACC-1, BUG-5, BUG-6 | LOW | 4 | Contabilidad completa |
| MET-2 | LOW | 7 | Redefinir la métrica |
| ARQ-2 | LOW | 5 | Versiones sólo desde `versions.yaml` |
| ARQ-3 | LOW | 8 | `channels` como parámetro del constructor |
| ARQ-4 | LOW | — | **No se corrige**: una reconstrucción atómica de `mathlib_full` (1,1 GB de vectores) no cabe cómodamente en 7,5 GB. Se documenta el riesgo; la tabla se puede regenerar desde el JSONL embebido |
| ARQ-5 y §9 (Ponytail) | INFO | 8 | Limpieza |
| ARQ-1 | LOW | 10 | Con disparador |
| SEC-3 | LOW | 3 (doc), 10 | Documentar el `llama-server` en `0.0.0.0` y cerrarlo con el sandbox |
| DES-2 | INFO | 7 | Sólo documentar |
| DES-3 | INFO | — | Ya reconocido en `final_report.md §7`; sin acción |
| DOC-1…12 | — | 3 y la fase que corresponda | Ver cada fase |
| Tareas del PLAN sin hacer (§3.A de la auditoría) | — | 1.5, 5, 7.3, 10 | Test índice ↔ Lean, etiqueta de cita, taxonomía del retriever; el resto con disparador |

---

## 4. Fases

### Fase 1 — Verificador seguro y sólido

**Cierra:** SEC-1, VER-1, BUG-2, TEST-1 y el test de arranque índice ↔ Lean de `PLAN_RAG §12`. **Esfuerzo:** M. **Costo:** US$0.

**Objetivo.** Que "verificado" signifique: el kernel aceptó la prueba usando sólo `propext`, `Classical.choice` y `Quot.sound`. Que el texto generado por el LLM no pueda ejecutar comandos. Y que el `lean_code` reportado sea exactamente el código que se verificó.

**Tareas**

1. **Una sola fuente Lean por intento** (`lean/verify.py`). Una función arma, a partir del problema y las tácticas, el texto que se envía al REPL: la cabecera `open …` sin imports, `set_option maxHeartbeats N in` y el enunciado con las tácticas empalmadas. Esa misma función la usan:
   - `LeanChecker.check`;
   - el `lean_code` del `SolutionReport`, tanto en el grafo (`graph.py:143`) como en las líneas base (`run.py:59`);
   - el backend `lake`, mientras exista.

   `lean_code` pasa a ser los imports de configuración seguidos de esa fuente: un archivo autocontenido que reproduce el entorno del REPL. Sobre `Problem.imports` adicionales: comprobar que ningún conjunto de problemas actual los usa y rechazar con un error explícito los problemas que los traigan, en lugar de ignorarlos en silencio.

2. **Validación previa de las tácticas.** Una función pura que reemplaza a `_FORBIDDEN`:
   - Quita antes los comentarios (`--` y `/- … -/`).
   - Compara tokens completos, con límites de palabra.
   - Rechaza:
     - comandos que empiezan por `#` (`#eval`, `#print`, `#exit`, `#check`, …);
     - metaprogramación: `run_tac`, `run_cmd`, `run_elab`, `elab`, `elab_rules`, `macro`, `macro_rules`, `syntax`, `notation`, `infix`, `infixl`, `infixr`, `prefix`, `postfix`;
     - atributos y código no confiable: `attribute`, `@[`, `unsafe`, `implemented_by`, `extern`;
     - cambios de entorno: `set_option` (el presupuesto de heartbeats lo fija el sistema), `import`;
     - declaraciones: `theorem`, `lemma`, `def`, `abbrev`, `instance`, `example`, `axiom`, `opaque`, `structure`, `inductive`, `class`, y `namespace` / `section` / `end` al principio de una línea;
     - pruebas no verificadas por el kernel: `native_decide`, `+native`, `ofReduceBool`, `trustCompiler`, `sorry`, `admit`;
     - `IO.`.
   - Se permite `open … in`, que es una táctica legítima.
   - El rechazo devuelve un `Verdict` con un error legible, para que el Crítico pueda corregirlo en el siguiente intento.

3. **Auditoría de axiomas.**
   - Cuando el veredicto sale sin errores, el sistema (no el LLM) ejecuta `#print axioms <nombre del teorema>` sobre el entorno que devolvió el REPL.
   - Se acepta sólo si los axiomas son un subconjunto de {`propext`, `Classical.choice`, `Quot.sound`}. Cualquier otro (`sorryAx`, `Lean.ofReduceBool`, `Lean.trustCompiler`, un axioma nuevo) da `ok=false` con el error "non-standard axioms: …".
   - El nombre del teorema se saca de `formal_statement`. Si el enunciado es un `example` sin nombre, al empalmar se declara como `theorem` con un nombre fijo; eso no debilita el enunciado.
   - `Verdict` gana el campo `axioms: list[str]`: regenerar los esquemas y registrar el cambio en DECISIONS.

4. **Demo** (`demo/app.py`).
   - El enunciado formal que escribe el usuario pasa por la misma validación y debe ser exactamente un `theorem` o `lemma` que termina en `:= by sorry`.
   - La pestaña "Resolver" se niega a ejecutar si el servidor escucha en una dirección que no es de loopback.

5. **Consistencia índice ↔ Lean** (`PLAN_RAG §12`).
   - En el precalentamiento del runner: `#check` de 20 `decl_name` elegidos al azar (semilla fija) de la tabla servida, excluyendo nombres privados y auxiliares.
   - Se escribe en el log cuántos existen. Si son menos de 19/20, se muestra un aviso, sin abortar.
   - Cuesta segundos, porque el REPL ya está caliente.

6. **Tests sin Lean** (`tests/test_verify.py`, archivo nuevo).
   - Deben rechazarse: la inyección exacta de la auditoría (`simp` seguido de `#eval IO.println …`), `decide +native`, `exact Lean.ofReduceBool _ _ rfl`, `run_tac`.
   - Deben aceptarse: un comentario que contiene la palabra "axiom"; tácticas legítimas como `nlinarith [sq_nonneg (a - b)]`, `norm_num [Nat.Prime] at h ⊢`, `decide`, `omega`, `interval_cases x <;> simp_all`.
   - Parseo de la salida de `#print axioms`, con fixtures de mensajes reales capturados una vez del REPL.
   - `lean_code` del reporte == texto recibido por un checker falso que registra lo que le llega.

7. **Test lento con Lean real.**
   - Marcador `slow`, registrado en `pytest.ini`; se salta si no existe la caché de Lean.
   - Comprueba que la inyección nunca llega al REPL y que `decide +native` sobre `2 ^ 10 = 1024` queda rechazado por la auditoría de axiomas.
   - Se ejecuta una vez en local y el resultado se anota en DECISIONS.

8. **Re-verificación offline de `eval-v1`** (0 llamadas LLM, sólo el REPL: unos 5 minutos de import más unos segundos).
   - Extraer las tácticas de los `lean_code` de las 27 filas `done` y verificarlas de nuevo con el verificador nuevo.
   - Pasar la validación de tácticas sobre los `lean_code` finales de las 300 filas, para medir falsos positivos.
   - Salida en un archivo nuevo, `data/eval/runs/eval-v1/reverify.json`; `results.jsonl` no se modifica.

9. **Documentación.**
   - Nueva sección "Modelo de amenazas del verificador" en `architecture.md`: qué se valida y qué no (no hay sandbox de sistema operativo hasta la Fase 10).
   - Entrada #69 en DECISIONS.

**Aceptación**
- Los tests nuevos pasan. El test lento se ejecutó una vez en local: la inyección fue rechazada y `+native` también.
- Re-verificación: **27/27 siguen aceptadas y sólo usan los 3 axiomas estándar**. Si alguna no pasa, la discrepancia queda en DECISIONS y en `final_report.md §6.3/§8` con las cifras corregidas.
- **0 falsos positivos** de la validación sobre las 27 pruebas aceptadas.
- Esquemas sincronizados y `graphify update .` ejecutado.

**Plan B**
- Si la salida de `#print axioms` no se puede leer de forma fiable del REPL, el sistema emite un `#eval` propio con `Lean.collectAxioms` sobre la constante. Es código del arnés, no del LLM, así que no contradice la tarea 2.
- Si la lista de rechazo bloquea tácticas legítimas en más del 1 % de los intentos de desarrollo, se afina la lista y se registra el cambio.

---

### Fase 2 — Licencias y datos, antes de cualquier commit

**Cierra:** SEC-2. **Esfuerzo:** S. **Costo:** US$0. **Depende de:** D3.

**Tareas**

1. **`.gitignore`.** Añadir:
   - `problemas resueltos olimpiadas.pdf`;
   - `blobs/`;
   - `lean_project/scratch/` y `lean_project.lock`;
   - `.claude/*.graphify-bak`;
   - `data/eval/runs/`: las corridas se publican ya saneadas en HF (tarea 3) y contienen 354 fragmentos del PDF.

   Preguntar al usuario si `Propuesta_Proyecto_Final_IA_UPTC.pdf`, que es suya, debe versionarse.

2. **Comprobación por contenido.**
   - Tomar los primeros 60 caracteres del `content_md` de cada una de las 153 filas de `informal.jsonl`.
   - Buscarlos en todos los archivos que se añadirían al repo: la lista de `git add --dry-run .` y los archivos de `data/eval/results/` y `data/eval/problems/`.
   - Resultado esperado: **0 coincidencias**.

3. **`scripts/publish_hf.py`.**
   - Cuando algún documento tenga `redistributable=false`, las carpetas de `runs` se suben desde una copia temporal saneada: `snippet` vacío en las citas del corpus informal, y nada del PDF en las trazas.
   - Los originales nunca se modifican.
   - Aplicar la misma comprobación de la tarea 2 sobre la copia saneada.

4. **Documentación.** DECISIONS #70 y una nota en `user_guide.md` ("Publicación").

**Aceptación**
- `git status --porcelain --ignored` muestra esos archivos como ignorados.
- La comprobación por contenido da 0 coincidencias, tanto en el repo como en la copia saneada que produce `publish_hf.py --dry-run`.

**Plan B.** Si el usuario quiere las corridas en git, se versiona una copia saneada generada por la misma función (por ejemplo `data/eval/runs_public/`).

---

### Fase 3 — Dependencias y documentación de estado

**Cierra:** DEP-1, DOC-1…3, DOC-5, DOC-7…10, DOC-12, la parte documental de MET-1 y DATA-1, y SEC-3 (documentación). **Esfuerzo:** M. **Costo:** US$0.

**Tareas**

1. **`pyproject.toml`.**
   - Declarar `httpx` y `tenacity`.
   - Nuevo extra `demo` con `gradio`, con cota inferior a la versión mayor instalada (6.x).
   - Pasar `ranx` a `dev`.
   - Quitar `pandas` y `accelerate` **sólo** si, sin ellos, cargan el embedder y el reranker (bf16 en CPU) y la suite pasa. Si falla algo, se restauran y se anota.
   - `uv lock` y `uv sync --extra dev --extra ingest --extra demo`, siempre sin corridas en marcha.

2. **Documentación inmediata.** Todo esto no depende de cambios de código:
   - `README.md`: `uv sync` con los extras.
   - `install.md`: GPU vía Vulkan (#48), número real de tests, y tabla única con las 9 variables de entorno (`RAGSOLVER_MATHLIB_TABLE`, `RAGSOLVER_EMBED_BACKEND`, `RAGSOLVER_EMBED_URL`, `RAGSOLVER_EMBED_BF16`, `RAGSOLVER_LEAN_PROJECT`, `RAGSOLVER_DB`, `RAGSOLVER_HF_DATASET`, `GRADIO_SERVER_NAME`, `HF_TOKEN`).
   - `PROGRESS.md`: reescritura. Una sección "Estado actual" al principio, sin contradicciones, y el material antiguo movido a "Historial". Se quita la tabla invalidada de la Fase 1, la sección "Sin GPU" y "Qué esperar cuando vuelvas".
   - `interfaces.md`: rango real de `subgoals`.
   - DECISIONS: tachar la #34 indicando que la reemplaza la #40.
   - Docstring de `evaluate.py`.
   - `versions.yaml`: el comentario de `provider_routing`.

3. **Limitaciones en `final_report.md` §8 (y §10 donde aplique).**
   - La tabla de 3.903 filas está sembrada con las premisas gold de miniF2F, lo que favorece al RAG (MET-1).
   - Hueco de cobertura: ninguna declaración `*.eq_*` ni del núcleo de Lean en el corpus (DATA-1).
   - `used_in_sketch` no es fiable en los 34 reportes con IDs repetidos (BUG-1, hasta la Fase 4).
   - RF-3 y RF-6 se aplican por problema, no por subobjetivo.
   - La frase "we release" pasa a indicar que la publicación está preparada pero pendiente.

4. **DECISIONS #71.** Una sola tabla con los desvíos del plan que no estaban registrados (§3.A de la auditoría): recuperación informal sólo en PLAN, sin boost por `math_area`, `_fts_text` en lugar de `name_tokens`, embeddings float32 en lugar de float16, `re_retrieve` implícito, sin tabla `documents`.

5. **`scripts/run_chain.sh`.** El resumen automático se escribe en `data/eval/results/chain_summary.md` en lugar de agregarse a `PROGRESS.md` (cambio de una línea).

6. **`llama-server` en `0.0.0.0` (SEC-3).** En `install.md` y en la cabecera de `embed_full_mathlib.sh`, indicar que se prefiera ligarlo a la IP de WSL, o apagarlo al terminar.

**Aceptación**
- `uv run python -c "import httpx, tenacity, gradio"` funciona en el entorno sincronizado con los extras; la suite pasa.
- Checklist de la auditoría §11 cerrado, cada punto contrastado con el código (con `grep` o `graphify explain`).
- Nada en `README`, `install.md`, `PROGRESS.md`, `architecture.md` ni `interfaces.md` contradice el código.

---

### Fase 4 — Citas, trazas y contabilidad

**Cierra:** BUG-1, TRZ-1, LLM-1, ACC-1, BUG-5, BUG-6 y el pin de tabla de MET-1. **Esfuerzo:** M. **Costo:** US$0, más un smoke opcional (D6).

**Tareas**

1. **IDs de cita estables.**
   - El estado del grafo guarda un mapa `chunk_id → citation_id`.
   - Los nodos `plan` y `retrieve` sólo asignan número a los chunks nuevos (el siguiente libre de cada prefijo, `M` o `I`) y reutilizan los existentes. Los prompts muestran esos IDs.
   - Test de regresión: un replan y una re-recuperación que devuelven chunks repetidos y nuevos no producen IDs duplicados, y `used_in_sketch` marca exactamente el chunk citado.
   - Los datos de `eval-v1` no se recalculan: no es reconstruible porque las trazas del retriever no se pueden atribuir a una configuración. Queda como limitación (Fase 3.3).

2. **Trazas del retriever por corrida.**
   - `RetrievalContext` gana `run_id`. El orquestador le pasa el identificador del par.
   - El `Retriever` escribe en el archivo de ese par cuando `run_id` está presente; si no, se mantiene el comportamiento actual (CLI, demo, evaluación).
   - El tratamiento de trazas interrumpidas del runner pasa a cubrir también las búsquedas.
   - Para las corridas nuevas, cambiar `:` por `__` en los nombres de archivo de traza, porque `/mnt/c` es NTFS. Registrarlo en DECISIONS.
   - Test: tras una corrida falsa, hay un archivo por par con los eventos de agentes y de búsquedas, y ningún archivo `<problema>:<uuid>`.

3. **Pin de tabla.** `VersionsPin` gana `mathlib_table`, con la tabla que realmente sirve el corpus `mathlib`. Regenerar esquemas.

4. **Política de reintentos** (`llm.py`).
   - Número de intentos configurable, por defecto 4.
   - Se reintenta ante error de conexión, timeout de conexión, 429 y 5xx. **No** se reintenta ante un timeout de lectura, porque el proveedor puede haber cobrado.
   - `timeout_s` de la sección `llm` baja a 300 s: 4.000 tokens de salida al proveedor más lento medido (19 tok/s, #62) son unos 210 s.
   - Cada intento fallido se registra con su código, y la respuesta lleva el número de intentos (`attempts`), que también va a la traza.
   - Tests con `httpx.MockTransport`, que viene con `httpx` (sin dependencias nuevas): 503, 503, 200 da 3 intentos registrados; un timeout de lectura no se reintenta.

5. **Contabilidad sin pérdidas.**
   - `_guard` captura cualquier excepción, salvo `DailyQuotaExhausted`, y la convierte en `status: error` dentro del grafo, conservando lo acumulado. Hoy `solve()` descarta el estado (`graph.py:222`).
   - El evento `invalid_json` registra `llm_calls`, tokens y `cost_usd`.
   - Las filas de error de las líneas base llevan el modelo.
   - Test: una excepción a mitad de corrida conserva los contadores (análogo al test existente de JSON inválido).

6. **Self-consistency.** Sumar `cost_usd` y el número real de llamadas de cada muestra (BUG-5).

7. **Caché de consultas.** Las escrituras y el desalojo de `_QUERY_CACHE` van bajo un lock (BUG-6).

8. **Smoke opcional (D6).** Los 5 problemas triviales con `full`, código nuevo, LLM real y REPL. Costo ≈ US$0,001.
   - Esperado: 5/5 resueltos; `axioms` informado; una traza por par con las búsquedas; `mathlib_table` en el pin.

9. **Documentación.** `architecture.md` (trazas), `reproduce.md` y `user_guide.md` (estructura de `traces/`), DECISIONS.

**Aceptación**
- Tests nuevos en verde.
- En una corrida falsa de 3 pares con replan: 0 IDs duplicados, 1 archivo de traza por par, y los contadores de llamadas, tokens y costo del reporte coinciden con la suma de los eventos de la traza.

---

### Fase 5 — Ingesta, CLI y configuración

**Cierra:** ING-1, BUG-3, BUG-4, ARQ-2 y la etiqueta de cita de `PLAN §7.5`. **Esfuerzo:** M (L si D4 = multidocumento). **Costo:** US$0, porque la caché de enriquecimiento evita llamadas.

**Tareas**

1. **Rutas ancladas a la raíz.** Una función que resuelve la raíz del repo a partir de `__file__` (válido con la instalación editable que hace `uv`). La usan todas las lecturas de `configs/`, `.env` y los valores por defecto de `data/`: `llm.py`, `agents/agents.py`, `rag/retrieve.py`, `rag/enrich.py`, `rag/ingest_*.py`, `rag/embed_corpus.py`, `orchestrator/run.py`, `logging/jsonl_writer.py`, `demo/app.py`.
   - Si algún día se distribuye como wheel no editable, añadir una variable de entorno para la raíz; hoy no hace falta.
   - Test: con otro directorio de trabajo, se cargan la configuración de `LLM` (con una clave falsa en el entorno) y la del `Retriever`.

2. **Versiones desde `versions.yaml`.** `index_version` y la versión del parser dejan de estar escritas en `ingest_informal.py` (4 sitios). `publish_space.py` cuenta las filas de la tabla, igual que `publish_hf.py`. El título de la demo toma la tag de `versions.yaml`.

3. **CLI.** `ragsolver ingest` delega en el `argparse` de `ingest_informal`, a través de un `main(argv)`. Test: las flags se interpretan igual en cualquier orden (`--skip-llm --pdf X` y `--pdf X --skip-llm`).

4. **Ingesta correcta (D4 = guard).**
   - Si `data/corpus/informal.jsonl` existe con otro `doc_id`, la ingesta aborta con un mensaje claro, salvo que se pase `--replace`.
   - Los metadatos del documento se construyen con el modelo `Document`, que así deja de estar muerto y además valida. Salen de `pymupdf` (`metadata`: title, author, creationDate) y los sobrescriben las flags `--title`, `--authors`, `--year`, `--license` y `--redistributable`.
   - `reproduce.md §2` pasa las flags del PDF de ejemplo, de modo que su `document.json` quede **idéntico** al actual.
   - `section_path` toma el título de sección que realmente detectó `parse_structure`, no el literal "Problemario".

5. **Etiqueta de cita** (`PLAN §7.5`).
   - Cada `InformalChunk` gana `source_label` (por ejemplo "Moreno Núñez & Tellechea Armenta (2002)"), escrito en la ingesta.
   - `_informal_citation_label` lo usa si existe; si no, el `doc_id`.
   - Hay que reingerir (0 llamadas por la caché), reembeber (≈ 215 s en CPU) y reconstruir las tablas `informal` y `figures`.

6. **Multidocumento, sólo si D4 = multi.** Archivos por documento (`data/corpus/informal/<doc_id>.jsonl` y sus figuras), `ragsolver ingest <dir>` que recorre los PDFs, y el CLI de `index` concatenando el directorio.

7. **Tests.** Guard de otro `doc_id`, metadatos desde flags, parseo del CLI, rutas desde otro directorio. La prueba de ingesta de extremo a extremo va en la Fase 6.

8. **Documentación.** `user_guide.md §4` (qué soporta y qué no), `reproduce.md §2`, DECISIONS.

**Aceptación**
- Reingerir el PDF de ejemplo da 153 chunks con los **mismos `content_sha`**, `document.json` sin cambios y 0 llamadas LLM.
- `ragsolver search … --corpus informal --mode exemplar` muestra la etiqueta con autor y año.
- `ragsolver ingest` desde otro directorio funciona.
- Ingerir un segundo PDF sin `--replace` aborta sin tocar el corpus.

**Plan B.** Si `pymupdf` no trae metadatos útiles para un PDF, las flags son obligatorias para ese documento (error explícito si faltan).

---

### Fase 6 — Tests de las zonas sin cobertura y CI

**Cierra:** TEST-2 (resto), TEST-3, TEST-4 y CI-1. **Esfuerzo:** M. **Costo:** US$0. **Depende de:** Fases 1, 4 y 5; D2 para el CI.

**Tareas**

1. **Fixture sintético.** Sin contenido con licencia:
   - un PDF de 2 páginas generado dentro del test con `pymupdf`, con una sección "Problemario" (2 problemas), otra "Soluciones" (2 soluciones) y un dibujo vectorial;
   - un JSON de bloques estilo MinerU mínimo en `tests/fixtures/`.

   Test: `ingest_informal.run(skip_llm=True)` de extremo a extremo, con directorios temporales. Esperado: 2 cards emparejadas, 1 figura recortada, archivos de corpus escritos.

2. **Tests con modelos falsos** (reutilizando el embedder falso y la LanceDB temporal de `test_retriever.py`):
   - `_cli` de búsqueda;
   - `evaluate_variants` sobre una tabla temporal;
   - `embed_corpus.run` con `embed_documents` sustituido.

3. **Integración con Lean real** (marcador `slow`; no se ejecuta en CI). Los 5 problemas triviales pasan por el `Orchestrator` con un LLM falso que devuelve tácticas correctas conocidas y el `LeanChecker` real. Esperado: 5/5 `done` con axiomas estándar. Tarda unos 5 minutos, casi todos del import.

4. **CI** (tras D2).
   - Se ejecuta en cada push con `-m "not slow"` y deseleccionando la integración con el índice.
   - Caché de `uv` en `setup-uv`.
   - Medir la duración. **Sólo si** supera 15 minutos, usar en CI el índice de ruedas de torch para CPU.

5. **Documentación.** En `install.md`, qué tests se saltan sin datos locales (15, según la auditoría) y cómo ejecutar los `slow`.

**Aceptación**
- Cobertura: `ingest_informal.py` ≥ 50 %, `cli.py` ≥ 80 %, `evaluate.py` y `embed_corpus.py` > 0 %, `lean/verify.py` ≥ 70 %, total ≥ 78 %.
- El CI termina en verde una vez en GitHub.

---

### Fase 7 — Diseño y métricas

**Cierra:** DES-1, MET-2, la taxonomía de errores del retriever (`PLAN F5 t5`), la medición de DATA-1, la tabla por defecto de MET-1, la documentación de DES-2 y el reranker para los agentes (restricción de capacidad del §8 de la auditoría). **Esfuerzo:** S–M. **Costo:** US$0, salvo la medición opcional.

> **Orden:** si se aprueba `eval-v1-full` (D6), debe ejecutarse **antes** de la tarea 7.1, con `prompt_version: "1"`, para no mezclar el cambio de prompt con el cambio de índice (ver Fase 9.4).

**Tareas**

1. **Replan con feedback (D5).**
   - El prompt del Planificador recibe `{feedback}`: la razón del Crítico y la estrategia anterior.
   - El grafo deja de vaciar `feedback` antes de replanificar; lo vacía después.
   - `prompt_version: "2"`.
   - Test con el LLM falso: el segundo prompt del planner contiene el feedback.
   - `eval-v1` no se repite; sus trazas registran `prompt_version: "1"`.
   - Medición opcional (con aprobación de gasto) sobre el split dev, **sin** afirmar una mejora: con n = 24, la variación entre corridas es del tamaño del efecto (informe §7).

2. **Métrica de re-recuperación (MET-2).** Se reemplaza `re_retrieval_success` por `re_retrieval_used`: la fracción de re-recuperaciones en modo `error` tras las cuales el siguiente intento usa (según `identifiers_used`) al menos una declaración que devolvió esa búsqueda, o se resuelve. Actualizar `eval_report.py` y `fill_final_report.py`. `eval-v1` sólo tiene 1 re-recuperación: se recalcula desde los datos si es trivial y, si no, se anota.

3. **Taxonomía de errores del retriever.** Se calcula desde los datos guardados, sin traza nueva y a US$0:
   - "Lema necesario no recuperado": premisas gold (`premises_gold.jsonl`) que no están entre las citas consultadas del par (`results.jsonl`).
   - "Nombre alucinado": identificadores de `unknown identifier` en los errores del verificador que no existen en el corpus.
   - "Ejemplar irrelevante": revisión manual de 20 listas de ejemplares, o se omite con una nota si no hay revisor.
   - "Figura mal descrita": no aplica a miniF2F.
   - Nueva sección en `eval_report.md`.

4. **Disparador de DATA-1.** A partir de la tarea 3, contar los identificadores desconocidos, y los `missing_identifiers` del Crítico, cuyo último componente empieza por `eq_` o que existen en Lean (se comprueba con `#check` en el REPL) pero no en el corpus. Si superan el **5 %** de los fallos por lema faltante, se activa la tarea de corpus de la Fase 10.

5. **Tabla por defecto (MET-1).** Si la tabla `mathlib_full` existe y `RAGSOLVER_MATHLIB_TABLE` no está definida, el corpus `mathlib` se sirve desde `mathlib_full` (el pin de la Fase 4.3 lo registra). `run_chain.sh` y `reproduce.md` fijan `RAGSOLVER_MATHLIB_TABLE=mathlib` de forma explícita para reproducir `eval-v1`.

6. **DES-2.** Documentar en `architecture.md` y en `final_report.md` que la crítica del último intento sólo alimenta la taxonomía (40 llamadas, 3,6 %). Sin cambio de código.

7. **Reranker para los agentes por GPU (revisado 2026-09-23 — ya no depende de más RAM).**
   - **Hallazgo:** el reranker no necesita más RAM del sistema, necesita correr en la GPU, igual que ya se hizo con el embedder (DECISIONS #48). `tools/llama-vulkan/llama-server.exe` es un binario genérico de llama.cpp: sirve cualquier GGUF, no sólo el embedder. llama.cpp soporta Qwen3-Reranker de forma nativa por el endpoint `/v1/rerank` (`--reranking --pooling rank --embedding`), con conversión GGUF oficial ya publicada y verificada (`ggml-org/Qwen3-Reranker-0.6B-Q8_0-GGUF`). La RX 9060 XT (16 GB VRAM) tiene sitio de sobra junto al embedder (~1,8 GB); el tráfico va por Vulkan, sin tocar los 7,3 GB de RAM de WSL. Verificado en esta máquina: `/dev/dxg` presente (passthrough de GPU activo), `tools/llama-vulkan/llama-server.exe` ya instalado.
   - **Tareas del lado del usuario** (Windows, fuera de este agente): descargar `Qwen3-Reranker-0.6B-Q8_0.gguf` (o el f16 si se prefiere) a `tools/llama-vulkan/models/`; arrancar un segundo `llama-server.exe` en un puerto distinto al del embedder (por ejemplo 8082) con `--reranking --pooling rank --embedding -ngl 99 --host 0.0.0.0 --port 8082`.
   - **Tareas de código** (este agente, en la Fase 7):
     - `rag/retrieve.py::Retriever._reranker()` gana un camino `RAGSOLVER_RERANK_BACKEND=llama` que llama a `POST {RAGSOLVER_RERANK_URL}/v1/rerank` con `{query, documents}` en vez de `CrossEncoder.predict()`, replicando el patrón de `embed.py::_llama_embed` (mismo `ThreadPoolExecutor`, mismo manejo de reintentos, `RAGSOLVER_RERANK_URL` con el mismo fallback de gateway que `_llama_url()`).
     - `configs/agents.yaml: retrieval.rerank: true`.
     - Nuevo script `scripts/rerank_llama.sh` (mismo formato que `embed_full_mathlib.sh`) con el comando exacto del servidor, para no depender de memoria.
     - Test con un servidor HTTP falso (`httpx.MockTransport`, sin dependencias nuevas) que verifica el payload y el parseo de la respuesta.
   - **Medición** (con el servidor arriba, 0 costo de LLM): repetir la Fase 5 de `PLAN_RAG.md` (evaluación sobre MathlibQR, variante `hibrido_rerank`) sobre el índice completo y comparar con los 0,45 de recall@10 ya medidos sin reranker de agentes (#56). Si la ganancia es ≥ 3 puntos, se documenta como confirmada y `retrieval.rerank: true` queda como valor por defecto también en un smoke de los 5 triviales.

**Aceptación**
- Tests del prompt y de la métrica en verde.
- Sección de taxonomía publicada en `eval_report.md`, con el cálculo reproducible con un comando.
- Resultado del disparador de DATA-1 registrado en DECISIONS.
- Con el servidor de reranking arriba: `RAGSOLVER_RERANK_BACKEND=llama ragsolver search "gcd is commutative" --corpus mathlib` devuelve resultados reordenados y el campo `scores.rerank` poblado, sin cargar el `CrossEncoder` de torch (verificable por RSS o por log).

**Plan B (tarea 7).** Si el usuario no tiene la máquina con la GPU disponible en el momento de esta fase, la tarea de código se implementa y se prueba con el servidor falso igual, y la medición y el `rerank: true` por defecto quedan pendientes de que el servidor esté arriba — no bloquean el resto de la fase.

---

### Fase 8 — Limpieza (Ponytail)

**Cierra:** la auditoría §9, ARQ-3, ARQ-5 y el código muerto de §3.D. **Esfuerzo:** S–M. **Costo:** US$0. **Depende de:** Fase 6 (red de tests) y D3.

**Tareas**

1. **Borrar código sin uso:** `render_pages`, `read_events` (sólo si ningún script lo necesita), `LLMResponse.json`, `Enricher.models` y `Enricher.model`, `QUERY_INSTRUCTION`, `VectorFigure.n_paths` y los tests que sólo prueban eso.

2. **Borrar scripts reemplazados:** `scripts/run_night.sh` y `scripts/run_eval_v1.sh` (los reemplaza `run_chain.sh`), y actualizar sus menciones en la documentación.

3. **Quitar el backend `lake`** (`verify()`, `run_lean()`, `parse_messages()`). El sandbox de la Fase 10 envuelve el REPL mediante `lake_path` y no necesita el camino por proceso. La función de fuente única de la Fase 1 sustituye a `build_file`.

4. **Deduplicar:**
   - despacho de verificación: `graph.verify` y `run_baseline` llaman a una sola función de chequeo;
   - un helper para construir `VersionsPin`.

5. **Estado del `Retriever` (ARQ-3):** `channels` pasa a ser parámetro del constructor. `evaluate.py` construye un `Retriever` por variante; el embedder ya está cacheado a nivel de módulo, así que es barato. La caché de tablas deja de ser `lru_cache` sobre un método y pasa a un dict por instancia.

6. **Artefactos (según D3):** `lean_project/scratch/`, `lean_project.lock` y `.claude/settings.json.graphify-bak`; `blobs/` sólo si el usuario lo confirma.

7. **`graphify update .`** y comprobar con `graphify explain` que no quedan nodos huérfanos de lo borrado.

**Aceptación**
- La suite pasa.
- Balance de líneas registrado en DECISIONS; la auditoría estimaba unas −150.
- Ningún `import` roto: `python -m compileall src scripts demo`.

---

### Fase 9 — Entregables (decisiones del usuario)

**Esfuerzo:** S. **Costo:** ≈ US$0,30 si se ejecuta `eval-v1-full`. **Depende de:** D1, D2, D6 y D7. **Obligatorio antes:** Fases 1 y 2.

**Tareas**

1. **Licencia (D1).** Archivo `LICENSE` y `CITATION.cff` con la URL real del repositorio.

2. **Commit (D2).**
   - Revisar la lista de archivos antes; la comprobación de la Fase 2.2 debe dar 0.
   - El commit y el push los ordena el usuario. El push dispara el CI (Fase 6.4).

3. **Hugging Face (D7).**
   - `publish_hf.py --dry-run` y revisión de la copia saneada; luego publicar el dataset y el Space.
   - Comprobar que el Space arranca y responde a una búsqueda, y que "Resolver" muestra el aviso de uso sólo local.

4. **`eval-v1-full` (D6).**
   - Se ejecuta con `run_chain.sh` después de las Fases 1 y 4 y **antes** de la Fase 7.1, con `prompt_version: "1"` y la misma configuración de agentes que `eval-v1`.
   - Los cambios de las Fases 1 y 4 no alteran los resultados, salvo lo que muestre la re-verificación (1.8): así, la única diferencia con `eval-v1` es el índice. Hay que declararlo así en el informe.

5. **Cierre.** Actualizar `final_report.md` (enlaces publicados, §6.3 con `eval-v1-full` si se ejecutó) y `PROGRESS.md`.

**Aceptación**
- Repo y dataset públicos sin texto del PDF (comprobación por contenido = 0).
- CI en verde.
- Informe con los enlaces reales.

---

### Fase 10 — Trabajo con disparador (sólo si se cumple la condición)

| Extensión | Disparador | Qué implica | Aceptación |
|---|---|---|---|
| Sandbox de sistema operativo para Lean (SEC-1 residual, SEC-3) | Antes de exponer la demo fuera de localhost, de procesar problemas o corpus de terceros, o de cambiar a un proveedor LLM no confiable | Script envoltorio pasado como `lake_path` de `lean-interact`: `bwrap` sin red (`--unshare-net`), bind de sólo lectura del proyecto Lean y del toolchain, `tmpfs` para lo temporal, sin acceso a `$HOME` ni al repo | Un `#eval IO.FS.readFile` sobre el `.env`, forzado con la validación desactivada en un test aislado, falla por permisos; el import de Mathlib tarda lo mismo (±10 %) |
| Replay de las pruebas publicadas (nivel 3) | Antes de presentar las pruebas como definitivas en HF o en el informe final | SafeVerify sobre las pruebas resueltas. `comparator` queda descartado mientras Landlock no esté activo | Todas pasan, o las discrepancias quedan documentadas |
| RF-1, RF-3 y RF-6 por subobjetivo | Si el curso exige el cumplimiento literal | Subobjetivos como lemas `have` o `lemma` verificados por separado, con reintentos por subobjetivo | Diseño propio (L) antes de implementar |
| Gold de OCR de 10 páginas | Cuando haya un anotador humano | Transcripción manual; métricas de `PLAN F2 t10` | Fórmulas ≥ 95 %, texto ≤ 3 % de distancia de edición |
| Completar el corpus (DATA-1) | Si el disparador de la Fase 7.4 supera el 5 % | Extraer las declaraciones que faltan (`eq_*` y núcleo de Lean) con el pipeline de LeanSearch v2 sin informalización (`PLAN F1`, plan B) y reindexar | El recall de premisas gold sube y se documenta |
| Multidocumento (si D4 = guard) | Un segundo documento real para ingerir | Fase 5.6 | Dos documentos conviven con citas correctas |
| Contratos transversales (ARQ-1) | El próximo cambio que toque contratos de dos paquetes | Mover `TraceEvent`, `VersionsPin`, `Citation` y `Verdict` a un único módulo de contratos | Sin dependencias `lean → agents` ni `logging ↔ rag` (verificado con Graphify) |
| Optimizaciones (auditoría §8) | Corridas en las que la recuperación supere el 10 % del tiempo de pared | Embeber las consultas de todos los subobjetivos en un lote; figuras en una sola consulta; embeddings en Arrow en lugar de JSONL | Latencia medida antes y después |
| PutnamBench | Trabajo futuro (#67) | Portar los enunciados al pin `v4.28.0-rc1` | — |

---

## 5. Esfuerzo y costo estimados

| Fase | Esfuerzo | Costo | Bloquea a |
|---|---|---|---|
| 1 Verificador | M (≈ 1 día) | US$0 | 3 (parcial), 4, 6, 9 |
| 2 Licencias | S | US$0 | 9 |
| 3 Dependencias y documentación | M | US$0 | 6 |
| 4 Citas, trazas y contabilidad | M | US$0 (+ US$0,001 opcional) | 6, 7, 9.4 |
| 5 Ingesta, CLI y configuración | M (L si hay multidocumento) | US$0 | 6 |
| 6 Tests y CI | M | US$0 | 8 |
| 7 Diseño y métricas | S–M | US$0 (+ medición opcional) | — |
| 8 Limpieza | S–M | US$0 | — |
| 9 Entregables | S | ≈ US$0,30 si hay `eval-v1-full` | — |

Total estimado del agente: **6 a 8 días de trabajo**, sin contar la Fase 10.

---

## 6. Definición de terminado (global)

1. Los 4 HIGH (SEC-1, VER-1, SEC-2, ING-1) están cerrados, con tests.
2. Cada MEDIUM está cerrado, o aplazado con su motivo registrado en DECISIONS.
3. `eval-v1` re-verificado con el verificador nuevo y el resultado documentado.
4. La documentación de estado es consistente con el código (checklist de la auditoría §11 cerrado).
5. La suite pasa (incluidos los tests nuevos); el test `slow` se ejecutó al menos una vez; el CI está en verde.
6. `graphify update .` ejecutado tras la última fase de código.

---

## 7. Orden de ejecución

1. **Fase 1** y **Fase 2** (independientes entre sí; ambas antes de cualquier commit).
2. **Fase 3** (depende de la Fase 1 sólo para la sección de amenazas; el resto puede ir en paralelo).
3. **Fase 4**. Si se aprueba, aquí va el smoke de D6.
4. **Fase 9.1–9.2**: licencia y commit, si el usuario lo decide. Habilita el CI.
5. **Fase 5**, luego **Fase 6**.
6. **Fase 9.4** (`eval-v1-full`, si se aprueba), **antes** de la Fase 7.1.
7. **Fase 7**, **Fase 8**, **Fase 9.3** (publicación en HF).
8. **Fase 10**, según los disparadores.

---

## 8. Referencias consultadas

- Lean FRO, *Validating a Lean Proof* (manual de referencia): https://lean-lang.org/doc/reference/latest/ValidatingProofs/
- leanprover/comparator (juez en sandbox para pruebas generadas por IA): https://github.com/leanprover/comparator
- GasStationManager/SafeVerify (replay más lista blanca de axiomas; leaderboard de PutnamBench): https://github.com/GasStationManager/SafeVerify · fork de Mistral: https://github.com/mistralai/LeanstralSafeVerify
- Kimina-Prover-Preview, issue #11 (15/225 soluciones de miniF2F dependían de `Lean.ofReduceBool`): https://github.com/MoonshotAI/Kimina-Prover-Preview/issues/11
- Kimina Lean Server: https://arxiv.org/abs/2504.21230
- OpenAI Codex, `linux-sandbox` (Landlock y bubblewrap): https://github.com/openai/codex/blob/main/codex-rs/linux-sandbox/README.md
- Sandbox en WSL (bubblewrap y namespaces de usuario): https://github.com/RisorseArtificiali/lince/issues/356
- Comprobaciones locales (2026-09-23): `/usr/bin/bwrap` presente; `max_user_namespaces = 29869`; Landlock ausente de `/sys/kernel/security/lsm`; `lean-interact` 0.11.5 admite `LeanREPLConfig(lake_path=…)`.
- llama.cpp, soporte de Qwen3-Reranker vía `/v1/rerank`: https://huggingface.co/ggml-org/Qwen3-Reranker-0.6B-Q8_0-GGUF · https://huggingface.co/Qwen/Qwen3-Reranker-0.6B/discussions/22 · issue de calidad del endpoint (usar la conversión oficial): https://github.com/ggml-org/llama.cpp/issues/16407
- Comprobación local (2026-09-23): `/dev/dxg` presente (passthrough de GPU activo en WSL2); `tools/llama-vulkan/llama-server.exe` ya instalado (mismo binario usado para el embedder, #48).