karlexmarin Claude Opus 4.7 (1M context) commited on
Commit
6e2328e
·
1 Parent(s): 28ac122

v0.6.1: 5 audit-driven gap fixes (privacy, exports, a11y, tooling)

Browse files

- meta tags: corrected to "8 recipes" (Help title already said 8; Profile-context retains "5" = profile chain count)
- submit-to-registry: clipboard + title-only URL replaces full-JSON-in-GET (privacy: was leaking body via GH server logs / referer headers)
- LaTeX/Markdown export: 6 new download buttons (3 share-bars × 2 formats); profileToLatex / compareToLatex / recipeToLatex serializers
- accessibility: ARIA roles on modal/tabs/lang-switcher, skip-to-main link, focus trap + Esc/Tab cycle in Help modal, aria-selected toggle on mode tabs
- new: scripts/check_lean_manifest.py — cross-checks lean_status.json against lean-taf source. Detects missing-in-source / line-drift / file-drift (errors) + new-in-source / commit-drift (info). --regenerate rewrites in-place. --strict for CI gate.
- i18n: 5 new keys × EN/ES/FR/ZH (parity 0 missing / 0 extra)
- 62/62 smoke tests passed locally

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Files changed (6) hide show
  1. index.html +20 -17
  2. js/i18n.js +20 -0
  3. js/main.js +192 -22
  4. scripts/README.md +38 -0
  5. scripts/check_lean_manifest.py +231 -0
  6. style.css +15 -0
index.html CHANGED
@@ -12,13 +12,13 @@
12
  <meta property="og:type" content="website" />
13
  <meta property="og:url" content="https://karlesmarin.github.io/tafagent/" />
14
  <meta property="og:title" content="TAF Agent — Test ANY Transformer LLM in Your Browser" />
15
- <meta property="og:description" content="Free, auditable transformer LLM diagnostic. 5 recipes, 5 modes, 4 languages. Runs in your browser. No server, no auth, $0/month forever." />
16
  <meta property="og:site_name" content="TAF Agent" />
17
 
18
  <!-- Twitter Card -->
19
  <meta name="twitter:card" content="summary_large_image" />
20
  <meta name="twitter:title" content="TAF Agent — Test ANY Transformer LLM in Your Browser" />
21
- <meta name="twitter:description" content="Free, auditable transformer LLM diagnostic. 5 recipes, 5 modes, 4 languages. Runs in your browser. $0 forever." />
22
 
23
  <!-- Theme color for browser UI -->
24
  <meta name="theme-color" content="#0a0e14" />
@@ -27,13 +27,14 @@
27
  <script src="https://cdn.jsdelivr.net/pyodide/v0.26.4/full/pyodide.js"></script>
28
  </head>
29
  <body>
 
30
  <header>
31
  <!-- Language switcher (top-right, round flags) -->
32
  <div class="lang-switcher">
33
- <button class="lang-btn" data-lang="en" data-label="English" title="English">🇬🇧</button>
34
- <button class="lang-btn" data-lang="es" data-label="Español" title="Español">🇪🇸</button>
35
- <button class="lang-btn" data-lang="fr" data-label="Français" title="Français">🇫🇷</button>
36
- <button class="lang-btn" data-lang="zh" data-label="中文" title="中文">🇨🇳</button>
37
  </div>
38
 
39
  <h1 data-i18n="hero.title">🔬 TAF Agent</h1>
@@ -61,10 +62,10 @@
61
  </header>
62
 
63
  <!-- Help modal -->
64
- <div id="help-modal">
65
  <div class="help-content">
66
- <button class="help-close" id="help-close">×</button>
67
- <h2 data-i18n="help.title">📘 TAF Agent — User Manual</h2>
68
 
69
  <h3 data-i18n="help.what.title">What does it do?</h3>
70
  <p data-i18n="help.what.body">Predicts <strong>practical viability</strong> of any transformer LLM
@@ -252,14 +253,14 @@
252
  <strong>📋 Recipe</strong>: manual selection with full form control.
253
  </span></span>
254
  </h2>
255
- <div class="mode-tabs">
256
- <button class="mode-btn active" data-mode="profile" data-i18n="modes.profile">📇 Profile a model</button>
257
- <button class="mode-btn" data-mode="compare" data-i18n="modes.compare">🆚 Compare models</button>
258
- <button class="mode-btn" data-mode="inspector" data-i18n="modes.inspector">🔍 Inspect config</button>
259
- <button class="mode-btn" data-mode="ask" data-i18n="modes.ask">💬 Ask plain English</button>
260
- <button class="mode-btn" data-mode="recipe" data-i18n="modes.recipe">📋 Pick recipe</button>
261
- <button class="mode-btn" data-mode="diagnose" data-i18n="modes.diagnose">🩺 Diagnose CLI</button>
262
- <button class="mode-btn" data-mode="phase" data-i18n="modes.phase">📊 Phase diagram</button>
263
  </div>
264
  <p id="mode-desc" class="recipe-desc" data-i18n="modes.desc">
265
  <strong>Quickest start</strong>: paste any HuggingFace model id (e.g. <code>meta-llama/Meta-Llama-3-8B</code>),
@@ -591,6 +592,8 @@
591
  <div class="share-bar">
592
  <button id="share-btn" class="secondary" type="button" data-i18n="share.btn">🔗 Copy share link</button>
593
  <button id="recipe-download-btn" class="secondary" type="button" data-i18n="share.download">💾 Download JSON</button>
 
 
594
  <button id="recipe-submit-btn" class="secondary" type="button" data-i18n="share.submit">📤 Submit to registry</button>
595
  <span id="share-status" class="subtle"></span>
596
  </div>
 
12
  <meta property="og:type" content="website" />
13
  <meta property="og:url" content="https://karlesmarin.github.io/tafagent/" />
14
  <meta property="og:title" content="TAF Agent — Test ANY Transformer LLM in Your Browser" />
15
+ <meta property="og:description" content="Free, auditable transformer LLM diagnostic. 8 recipes, 5 modes, 4 languages. Runs in your browser. No server, no auth, $0/month forever." />
16
  <meta property="og:site_name" content="TAF Agent" />
17
 
18
  <!-- Twitter Card -->
19
  <meta name="twitter:card" content="summary_large_image" />
20
  <meta name="twitter:title" content="TAF Agent — Test ANY Transformer LLM in Your Browser" />
21
+ <meta name="twitter:description" content="Free, auditable transformer LLM diagnostic. 8 recipes, 5 modes, 4 languages. Runs in your browser. $0 forever." />
22
 
23
  <!-- Theme color for browser UI -->
24
  <meta name="theme-color" content="#0a0e14" />
 
27
  <script src="https://cdn.jsdelivr.net/pyodide/v0.26.4/full/pyodide.js"></script>
28
  </head>
29
  <body>
30
+ <a href="#mode-section" class="skip-link" data-i18n="a11y.skip">Skip to main content</a>
31
  <header>
32
  <!-- Language switcher (top-right, round flags) -->
33
  <div class="lang-switcher">
34
+ <button class="lang-btn" data-lang="en" data-label="English" title="English" aria-label="Switch language to English">🇬🇧</button>
35
+ <button class="lang-btn" data-lang="es" data-label="Español" title="Español" aria-label="Cambiar idioma a Español">🇪🇸</button>
36
+ <button class="lang-btn" data-lang="fr" data-label="Français" title="Français" aria-label="Changer la langue en Français">🇫🇷</button>
37
+ <button class="lang-btn" data-lang="zh" data-label="中文" title="中文" aria-label="切换语言至中文">🇨🇳</button>
38
  </div>
39
 
40
  <h1 data-i18n="hero.title">🔬 TAF Agent</h1>
 
62
  </header>
63
 
64
  <!-- Help modal -->
65
+ <div id="help-modal" role="dialog" aria-modal="true" aria-labelledby="help-modal-title" aria-hidden="true">
66
  <div class="help-content">
67
+ <button class="help-close" id="help-close" aria-label="Close help">×</button>
68
+ <h2 id="help-modal-title" data-i18n="help.title">📘 TAF Agent — User Manual</h2>
69
 
70
  <h3 data-i18n="help.what.title">What does it do?</h3>
71
  <p data-i18n="help.what.body">Predicts <strong>practical viability</strong> of any transformer LLM
 
253
  <strong>📋 Recipe</strong>: manual selection with full form control.
254
  </span></span>
255
  </h2>
256
+ <div class="mode-tabs" role="tablist" aria-label="View modes">
257
+ <button class="mode-btn active" data-mode="profile" role="tab" aria-selected="true" data-i18n="modes.profile">📇 Profile a model</button>
258
+ <button class="mode-btn" data-mode="compare" role="tab" aria-selected="false" data-i18n="modes.compare">🆚 Compare models</button>
259
+ <button class="mode-btn" data-mode="inspector" role="tab" aria-selected="false" data-i18n="modes.inspector">🔍 Inspect config</button>
260
+ <button class="mode-btn" data-mode="ask" role="tab" aria-selected="false" data-i18n="modes.ask">💬 Ask plain English</button>
261
+ <button class="mode-btn" data-mode="recipe" role="tab" aria-selected="false" data-i18n="modes.recipe">📋 Pick recipe</button>
262
+ <button class="mode-btn" data-mode="diagnose" role="tab" aria-selected="false" data-i18n="modes.diagnose">🩺 Diagnose CLI</button>
263
+ <button class="mode-btn" data-mode="phase" role="tab" aria-selected="false" data-i18n="modes.phase">📊 Phase diagram</button>
264
  </div>
265
  <p id="mode-desc" class="recipe-desc" data-i18n="modes.desc">
266
  <strong>Quickest start</strong>: paste any HuggingFace model id (e.g. <code>meta-llama/Meta-Llama-3-8B</code>),
 
592
  <div class="share-bar">
593
  <button id="share-btn" class="secondary" type="button" data-i18n="share.btn">🔗 Copy share link</button>
594
  <button id="recipe-download-btn" class="secondary" type="button" data-i18n="share.download">💾 Download JSON</button>
595
+ <button id="recipe-download-md-btn" class="secondary" type="button" data-i18n="share.download_md">📝 Markdown</button>
596
+ <button id="recipe-download-tex-btn" class="secondary" type="button" data-i18n="share.download_tex">📜 LaTeX</button>
597
  <button id="recipe-submit-btn" class="secondary" type="button" data-i18n="share.submit">📤 Submit to registry</button>
598
  <span id="share-status" class="subtle"></span>
599
  </div>
js/i18n.js CHANGED
@@ -78,8 +78,13 @@ export const TRANSLATIONS = {
78
  "share.btn": "🔗 Copy share link",
79
  "share.copied": "✅ Copied to clipboard!",
80
  "share.download": "💾 Download JSON",
 
 
81
  "share.submit": "📤 Submit to registry",
 
 
82
  "share.import_title": "📂 Import a shared TAF result",
 
83
  "share.import_desc": "Got a JSON file from someone else's TAF analysis? Load it here to see the verdict + chain locally. Same view as if you'd run it yourself.",
84
  "share.import_btn": "📂 Load shared JSON",
85
  "synthesis.system": "You are a precise transformer LLM diagnostic assistant. Given pre-computed TAF formula results, write a clear plain-English summary in 4-6 sentences. Cite the section number (§X.Y) for each number you mention. Always give a concrete recommendation. Do NOT invent numbers.",
@@ -582,8 +587,13 @@ export const TRANSLATIONS = {
582
  "share.btn": "🔗 Copiar link",
583
  "share.copied": "✅ ¡Copiado al portapapeles!",
584
  "share.download": "💾 Descargar JSON",
 
 
585
  "share.submit": "📤 Enviar al registry",
 
 
586
  "share.import_title": "📂 Importar un resultado TAF compartido",
 
587
  "share.import_desc": "¿Tienes un fichero JSON del análisis TAF de alguien? Cárgalo aquí para ver el veredicto + cadena localmente. La misma vista que si lo hubieras ejecutado tú.",
588
  "share.import_btn": "📂 Cargar JSON compartido",
589
  "synthesis.system": "Eres un asistente de diagnóstico preciso para LLMs transformer. Dados resultados de fórmulas TAF pre-calculados, escribe un resumen claro en español de 4-6 frases. Cita el número de sección (§X.Y) para cada número que menciones. Da siempre una recomendación concreta. NO inventes números.",
@@ -950,8 +960,13 @@ export const TRANSLATIONS = {
950
  "share.btn": "🔗 Copier le lien",
951
  "share.copied": "✅ Copié dans le presse-papiers!",
952
  "share.download": "💾 Télécharger JSON",
 
 
953
  "share.submit": "📤 Soumettre au registry",
 
 
954
  "share.import_title": "📂 Importer un résultat TAF partagé",
 
955
  "share.import_desc": "Vous avez un fichier JSON de l'analyse TAF de quelqu'un ? Chargez-le ici pour voir le verdict + la chaîne localement. La même vue que si vous l'aviez exécuté vous-même.",
956
  "share.import_btn": "📂 Charger JSON partagé",
957
  "synthesis.system": "Vous êtes un assistant de diagnostic précis pour LLMs transformer. Étant donné des résultats de formules TAF pré-calculés, écrivez un résumé clair en français de 4-6 phrases. Citez le numéro de section (§X.Y) pour chaque nombre mentionné. Donnez toujours une recommandation concrète. N'INVENTEZ PAS de nombres.",
@@ -1318,8 +1333,13 @@ export const TRANSLATIONS = {
1318
  "share.btn": "🔗 复制分享链接",
1319
  "share.copied": "✅ 已复制到剪贴板!",
1320
  "share.download": "💾 下载 JSON",
 
 
1321
  "share.submit": "📤 提交到 registry",
 
 
1322
  "share.import_title": "📂 导入共享的 TAF 结果",
 
1323
  "share.import_desc": "有他人 TAF 分析的 JSON 文件? 在这里加载以本地查看判定 + 链。与您自己运行的视图相同。",
1324
  "share.import_btn": "📂 加载共享的 JSON",
1325
  "synthesis.system": "您是 transformer LLM 的精确诊断助手。给定预先计算的 TAF 公式结果,用 4-6 句中文写出清晰的摘要。为每个提到的数字引用章节号 (§X.Y)。始终给出具体建议。不要编造数字。",
 
78
  "share.btn": "🔗 Copy share link",
79
  "share.copied": "✅ Copied to clipboard!",
80
  "share.download": "💾 Download JSON",
81
+ "share.download_md": "📝 Markdown",
82
+ "share.download_tex": "📜 LaTeX",
83
  "share.submit": "📤 Submit to registry",
84
+ "share.submit_clip_ok": "↗ Opened GitHub. Body copied to clipboard — paste it into the issue body.",
85
+ "share.submit_clip_fail": "↗ Opened GitHub. Clipboard blocked — body logged in browser console (F12).",
86
  "share.import_title": "📂 Import a shared TAF result",
87
+ "a11y.skip": "Skip to main content",
88
  "share.import_desc": "Got a JSON file from someone else's TAF analysis? Load it here to see the verdict + chain locally. Same view as if you'd run it yourself.",
89
  "share.import_btn": "📂 Load shared JSON",
90
  "synthesis.system": "You are a precise transformer LLM diagnostic assistant. Given pre-computed TAF formula results, write a clear plain-English summary in 4-6 sentences. Cite the section number (§X.Y) for each number you mention. Always give a concrete recommendation. Do NOT invent numbers.",
 
587
  "share.btn": "🔗 Copiar link",
588
  "share.copied": "✅ ¡Copiado al portapapeles!",
589
  "share.download": "💾 Descargar JSON",
590
+ "share.download_md": "📝 Markdown",
591
+ "share.download_tex": "📜 LaTeX",
592
  "share.submit": "📤 Enviar al registry",
593
+ "share.submit_clip_ok": "↗ GitHub abierto. Cuerpo copiado al portapapeles — pégalo en el cuerpo del issue.",
594
+ "share.submit_clip_fail": "↗ GitHub abierto. Portapapeles bloqueado — cuerpo volcado en la consola del navegador (F12).",
595
  "share.import_title": "📂 Importar un resultado TAF compartido",
596
+ "a11y.skip": "Saltar al contenido principal",
597
  "share.import_desc": "¿Tienes un fichero JSON del análisis TAF de alguien? Cárgalo aquí para ver el veredicto + cadena localmente. La misma vista que si lo hubieras ejecutado tú.",
598
  "share.import_btn": "📂 Cargar JSON compartido",
599
  "synthesis.system": "Eres un asistente de diagnóstico preciso para LLMs transformer. Dados resultados de fórmulas TAF pre-calculados, escribe un resumen claro en español de 4-6 frases. Cita el número de sección (§X.Y) para cada número que menciones. Da siempre una recomendación concreta. NO inventes números.",
 
960
  "share.btn": "🔗 Copier le lien",
961
  "share.copied": "✅ Copié dans le presse-papiers!",
962
  "share.download": "💾 Télécharger JSON",
963
+ "share.download_md": "📝 Markdown",
964
+ "share.download_tex": "📜 LaTeX",
965
  "share.submit": "📤 Soumettre au registry",
966
+ "share.submit_clip_ok": "↗ GitHub ouvert. Corps copié dans le presse-papiers — collez-le dans le corps de l'issue.",
967
+ "share.submit_clip_fail": "↗ GitHub ouvert. Presse-papiers bloqué — corps dans la console du navigateur (F12).",
968
  "share.import_title": "📂 Importer un résultat TAF partagé",
969
+ "a11y.skip": "Aller au contenu principal",
970
  "share.import_desc": "Vous avez un fichier JSON de l'analyse TAF de quelqu'un ? Chargez-le ici pour voir le verdict + la chaîne localement. La même vue que si vous l'aviez exécuté vous-même.",
971
  "share.import_btn": "📂 Charger JSON partagé",
972
  "synthesis.system": "Vous êtes un assistant de diagnostic précis pour LLMs transformer. Étant donné des résultats de formules TAF pré-calculés, écrivez un résumé clair en français de 4-6 phrases. Citez le numéro de section (§X.Y) pour chaque nombre mentionné. Donnez toujours une recommandation concrète. N'INVENTEZ PAS de nombres.",
 
1333
  "share.btn": "🔗 复制分享链接",
1334
  "share.copied": "✅ 已复制到剪贴板!",
1335
  "share.download": "💾 下载 JSON",
1336
+ "share.download_md": "📝 Markdown",
1337
+ "share.download_tex": "📜 LaTeX",
1338
  "share.submit": "📤 提交到 registry",
1339
+ "share.submit_clip_ok": "↗ 已打开 GitHub。正文已复制到剪贴板——粘贴到 issue 正文。",
1340
+ "share.submit_clip_fail": "↗ 已打开 GitHub。剪贴板被阻止——正文已写入浏览器控制台 (F12)。",
1341
  "share.import_title": "📂 导入共享的 TAF 结果",
1342
+ "a11y.skip": "跳到主要内容",
1343
  "share.import_desc": "有他人 TAF 分析的 JSON 文件? 在这里加载以本地查看判定 + 链。与您自己运行的视图相同。",
1344
  "share.import_btn": "📂 加载共享的 JSON",
1345
  "synthesis.system": "您是 transformer LLM 的精确诊断助手。给定预先计算的 TAF 公式结果,用 4-6 句中文写出清晰的摘要。为每个提到的数字引用章节号 (§X.Y)。始终给出具体建议。不要编造数字。",
js/main.js CHANGED
@@ -142,8 +142,12 @@ function setStatus(msg) { $("status").textContent = msg; }
142
  // ════════════════════════════════════════════════════════════════════
143
  document.querySelectorAll(".mode-btn").forEach(btn => {
144
  btn.addEventListener("click", () => {
145
- document.querySelectorAll(".mode-btn").forEach(b => b.classList.remove("active"));
 
 
 
146
  btn.classList.add("active");
 
147
  const mode = btn.dataset.mode;
148
  state.currentMode = mode;
149
  // Hide all mode sections
@@ -1227,6 +1231,8 @@ function renderProfile(p, params) {
1227
  <div class="share-bar">
1228
  <button class="secondary" id="profile-share-btn" data-i18n="share.btn">🔗 Copy share link</button>
1229
  <button class="secondary" id="profile-download-btn" data-i18n="share.download">💾 Download JSON</button>
 
 
1230
  <button class="secondary" id="profile-submit-btn" data-i18n="share.submit">📤 Submit to registry</button>
1231
  <span id="profile-share-status" class="subtle"></span>
1232
  </div>
@@ -1268,11 +1274,23 @@ function renderProfile(p, params) {
1268
  $("profile-share-status").textContent = `✅ Downloaded ${filename}`;
1269
  setTimeout(() => $("profile-share-status").textContent = "", 5000);
1270
  });
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1271
  $("profile-submit-btn").addEventListener("click", async () => {
1272
- const url = await buildIssueUrl("profile", p);
1273
- window.open(url, "_blank");
1274
- $("profile-share-status").textContent = "↗ Opened GitHub registry (search hash before submitting to avoid duplicate)";
1275
- setTimeout(() => $("profile-share-status").textContent = "", 6000);
1276
  });
1277
 
1278
  // v0.6: γ predicted-vs-observed panel — interactive
@@ -1487,6 +1505,8 @@ function renderCompare(cmp) {
1487
  <div class="share-bar">
1488
  <button class="secondary" id="compare-share-btn" data-i18n="share.btn">🔗 Copy share link</button>
1489
  <button class="secondary" id="compare-download-btn" data-i18n="share.download">💾 Download JSON</button>
 
 
1490
  <button class="secondary" id="compare-submit-btn" data-i18n="share.submit">📤 Submit to registry</button>
1491
  <span id="compare-share-status" class="subtle"></span>
1492
  </div>
@@ -1505,11 +1525,23 @@ function renderCompare(cmp) {
1505
  $("compare-share-status").textContent = `✅ Downloaded ${filename}`;
1506
  setTimeout(() => $("compare-share-status").textContent = "", 5000);
1507
  });
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1508
  $("compare-submit-btn").addEventListener("click", async () => {
1509
- const url = await buildIssueUrl("compare", cmp);
1510
- window.open(url, "_blank");
1511
- $("compare-share-status").textContent = "↗ Opened GitHub registry";
1512
- setTimeout(() => $("compare-share-status").textContent = "", 6000);
1513
  });
1514
  }
1515
 
@@ -1576,21 +1608,71 @@ $("recipe-download-btn").addEventListener("click", async () => {
1576
  $("share-status").textContent = `✅ Downloaded ${filename}`;
1577
  setTimeout(() => $("share-status").textContent = "", 5000);
1578
  });
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1579
  $("recipe-submit-btn").addEventListener("click", async () => {
1580
  if (!state.lastFullResult) return;
1581
- const url = await buildIssueUrl("recipe", state.lastFullResult);
1582
- window.open(url, "_blank");
1583
- $("share-status").textContent = "↗ Opened GitHub registry (search hash before submitting to avoid duplicate)";
1584
- setTimeout(() => $("share-status").textContent = "", 6000);
1585
  });
1586
 
1587
  // ════════════════════════════════════════════════════════════════════
1588
  // Help modal
1589
  // ════════════════════════════════════════════════════════════════════
1590
- $("help-btn").addEventListener("click", () => $("help-modal").classList.add("open"));
1591
- $("help-close").addEventListener("click", () => $("help-modal").classList.remove("open"));
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1592
  $("help-modal").addEventListener("click", (e) => {
1593
- if (e.target.id === "help-modal") $("help-modal").classList.remove("open");
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1594
  });
1595
 
1596
  // ════════════════════════════════════════════════════════════════════
@@ -1609,6 +1691,75 @@ function downloadJSON(filename, data) {
1609
  setTimeout(() => { document.body.removeChild(a); URL.revokeObjectURL(url); }, 100);
1610
  }
1611
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1612
  // Sort object keys recursively for deterministic JSON
1613
  function sortKeys(o) {
1614
  if (Array.isArray(o)) return o.map(sortKeys);
@@ -1698,7 +1849,11 @@ async function makeFilename(type, data) {
1698
  return `taf-${type}-${name}-${suffix}-${hash}.json`;
1699
  }
1700
 
1701
- async function buildIssueUrl(type, data) {
 
 
 
 
1702
  const hash = await inputHash(type, data);
1703
  const modelName = modelShortName(data, "model");
1704
  let title, body;
@@ -1714,11 +1869,26 @@ async function buildIssueUrl(type, data) {
1714
  body = recipeToMarkdown(data, hash);
1715
  }
1716
  const dedupNote = `\n\n> **Input hash**: \`#${hash}\` — search this hash in registry issues to find independent verifications. Same inputs always produce the same hash.`;
1717
- const params = new URLSearchParams({
1718
- title: title,
1719
- body: body + dedupNote + "\n\n---\n*Submitted via [TAF Agent](https://karlesmarin.github.io/tafagent)*",
1720
- });
1721
- return `https://github.com/${REGISTRY_REPO}/issues/new?${params.toString()}`;
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1722
  }
1723
 
1724
  function profileToMarkdown(p, hash="") {
 
142
  // ════════════════════════════════════════════════════════════════════
143
  document.querySelectorAll(".mode-btn").forEach(btn => {
144
  btn.addEventListener("click", () => {
145
+ document.querySelectorAll(".mode-btn").forEach(b => {
146
+ b.classList.remove("active");
147
+ b.setAttribute("aria-selected", "false");
148
+ });
149
  btn.classList.add("active");
150
+ btn.setAttribute("aria-selected", "true");
151
  const mode = btn.dataset.mode;
152
  state.currentMode = mode;
153
  // Hide all mode sections
 
1231
  <div class="share-bar">
1232
  <button class="secondary" id="profile-share-btn" data-i18n="share.btn">🔗 Copy share link</button>
1233
  <button class="secondary" id="profile-download-btn" data-i18n="share.download">💾 Download JSON</button>
1234
+ <button class="secondary" id="profile-download-md-btn" data-i18n="share.download_md">📝 Markdown</button>
1235
+ <button class="secondary" id="profile-download-tex-btn" data-i18n="share.download_tex">📜 LaTeX</button>
1236
  <button class="secondary" id="profile-submit-btn" data-i18n="share.submit">📤 Submit to registry</button>
1237
  <span id="profile-share-status" class="subtle"></span>
1238
  </div>
 
1274
  $("profile-share-status").textContent = `✅ Downloaded ${filename}`;
1275
  setTimeout(() => $("profile-share-status").textContent = "", 5000);
1276
  });
1277
+ $("profile-download-md-btn").addEventListener("click", async () => {
1278
+ const hash = await inputHash("profile", p);
1279
+ const base = (await makeFilename("profile", p)).replace(/\.json$/, "");
1280
+ downloadText(`${base}.md`, profileToMarkdown(p, hash), "text/markdown;charset=utf-8");
1281
+ $("profile-share-status").textContent = `✅ Downloaded ${base}.md`;
1282
+ setTimeout(() => $("profile-share-status").textContent = "", 5000);
1283
+ });
1284
+ $("profile-download-tex-btn").addEventListener("click", async () => {
1285
+ const hash = await inputHash("profile", p);
1286
+ const base = (await makeFilename("profile", p)).replace(/\.json$/, "");
1287
+ downloadText(`${base}.tex`, profileToLatex(p, hash), "application/x-tex;charset=utf-8");
1288
+ $("profile-share-status").textContent = `✅ Downloaded ${base}.tex`;
1289
+ setTimeout(() => $("profile-share-status").textContent = "", 5000);
1290
+ });
1291
  $("profile-submit-btn").addEventListener("click", async () => {
1292
+ await submitToRegistry("profile", p, $("profile-share-status"));
1293
+ setTimeout(() => $("profile-share-status").textContent = "", 8000);
 
 
1294
  });
1295
 
1296
  // v0.6: γ predicted-vs-observed panel — interactive
 
1505
  <div class="share-bar">
1506
  <button class="secondary" id="compare-share-btn" data-i18n="share.btn">🔗 Copy share link</button>
1507
  <button class="secondary" id="compare-download-btn" data-i18n="share.download">💾 Download JSON</button>
1508
+ <button class="secondary" id="compare-download-md-btn" data-i18n="share.download_md">📝 Markdown</button>
1509
+ <button class="secondary" id="compare-download-tex-btn" data-i18n="share.download_tex">📜 LaTeX</button>
1510
  <button class="secondary" id="compare-submit-btn" data-i18n="share.submit">📤 Submit to registry</button>
1511
  <span id="compare-share-status" class="subtle"></span>
1512
  </div>
 
1525
  $("compare-share-status").textContent = `✅ Downloaded ${filename}`;
1526
  setTimeout(() => $("compare-share-status").textContent = "", 5000);
1527
  });
1528
+ $("compare-download-md-btn").addEventListener("click", async () => {
1529
+ const hash = await inputHash("compare", cmp);
1530
+ const base = (await makeFilename("compare", cmp)).replace(/\.json$/, "");
1531
+ downloadText(`${base}.md`, compareToMarkdown(cmp, hash), "text/markdown;charset=utf-8");
1532
+ $("compare-share-status").textContent = `✅ Downloaded ${base}.md`;
1533
+ setTimeout(() => $("compare-share-status").textContent = "", 5000);
1534
+ });
1535
+ $("compare-download-tex-btn").addEventListener("click", async () => {
1536
+ const hash = await inputHash("compare", cmp);
1537
+ const base = (await makeFilename("compare", cmp)).replace(/\.json$/, "");
1538
+ downloadText(`${base}.tex`, compareToLatex(cmp, hash), "application/x-tex;charset=utf-8");
1539
+ $("compare-share-status").textContent = `✅ Downloaded ${base}.tex`;
1540
+ setTimeout(() => $("compare-share-status").textContent = "", 5000);
1541
+ });
1542
  $("compare-submit-btn").addEventListener("click", async () => {
1543
+ await submitToRegistry("compare", cmp, $("compare-share-status"));
1544
+ setTimeout(() => $("compare-share-status").textContent = "", 8000);
 
 
1545
  });
1546
  }
1547
 
 
1608
  $("share-status").textContent = `✅ Downloaded ${filename}`;
1609
  setTimeout(() => $("share-status").textContent = "", 5000);
1610
  });
1611
+ $("recipe-download-md-btn").addEventListener("click", async () => {
1612
+ if (!state.lastFullResult) return;
1613
+ const r = state.lastFullResult;
1614
+ const hash = await inputHash("recipe", r);
1615
+ const base = (await makeFilename("recipe", r)).replace(/\.json$/, "");
1616
+ downloadText(`${base}.md`, recipeToMarkdown(r, hash), "text/markdown;charset=utf-8");
1617
+ $("share-status").textContent = `✅ Downloaded ${base}.md`;
1618
+ setTimeout(() => $("share-status").textContent = "", 5000);
1619
+ });
1620
+ $("recipe-download-tex-btn").addEventListener("click", async () => {
1621
+ if (!state.lastFullResult) return;
1622
+ const r = state.lastFullResult;
1623
+ const hash = await inputHash("recipe", r);
1624
+ const base = (await makeFilename("recipe", r)).replace(/\.json$/, "");
1625
+ downloadText(`${base}.tex`, recipeToLatex(r, hash), "application/x-tex;charset=utf-8");
1626
+ $("share-status").textContent = `✅ Downloaded ${base}.tex`;
1627
+ setTimeout(() => $("share-status").textContent = "", 5000);
1628
+ });
1629
  $("recipe-submit-btn").addEventListener("click", async () => {
1630
  if (!state.lastFullResult) return;
1631
+ await submitToRegistry("recipe", state.lastFullResult, $("share-status"));
1632
+ setTimeout(() => $("share-status").textContent = "", 8000);
 
 
1633
  });
1634
 
1635
  // ════════════════════════════════════════════════════════════════════
1636
  // Help modal
1637
  // ════════════════════════════════════════════════════════════════════
1638
+ // a11y: focus trap + restore + Esc handling for the help modal.
1639
+ let __helpModalReturnFocus = null;
1640
+ function openHelpModal() {
1641
+ const modal = $("help-modal");
1642
+ __helpModalReturnFocus = document.activeElement;
1643
+ modal.classList.add("open");
1644
+ modal.setAttribute("aria-hidden", "false");
1645
+ // Defer focus shift so the click that opened the modal isn't swallowed.
1646
+ setTimeout(() => $("help-close")?.focus(), 0);
1647
+ }
1648
+ function closeHelpModal() {
1649
+ const modal = $("help-modal");
1650
+ modal.classList.remove("open");
1651
+ modal.setAttribute("aria-hidden", "true");
1652
+ if (__helpModalReturnFocus && typeof __helpModalReturnFocus.focus === "function") {
1653
+ __helpModalReturnFocus.focus();
1654
+ }
1655
+ __helpModalReturnFocus = null;
1656
+ }
1657
+ $("help-btn").addEventListener("click", openHelpModal);
1658
+ $("help-close").addEventListener("click", closeHelpModal);
1659
  $("help-modal").addEventListener("click", (e) => {
1660
+ if (e.target.id === "help-modal") closeHelpModal();
1661
+ });
1662
+ // Esc closes; Tab cycles within modal when open.
1663
+ document.addEventListener("keydown", (e) => {
1664
+ const modal = $("help-modal");
1665
+ if (!modal.classList.contains("open")) return;
1666
+ if (e.key === "Escape") { e.preventDefault(); closeHelpModal(); return; }
1667
+ if (e.key !== "Tab") return;
1668
+ const focusables = modal.querySelectorAll(
1669
+ 'a[href], button:not([disabled]), input:not([disabled]), select:not([disabled]), textarea:not([disabled]), [tabindex]:not([tabindex="-1"])'
1670
+ );
1671
+ if (!focusables.length) return;
1672
+ const first = focusables[0];
1673
+ const last = focusables[focusables.length - 1];
1674
+ if (e.shiftKey && document.activeElement === first) { e.preventDefault(); last.focus(); }
1675
+ else if (!e.shiftKey && document.activeElement === last) { e.preventDefault(); first.focus(); }
1676
  });
1677
 
1678
  // ════════════════════════════════════════════════════════════════════
 
1691
  setTimeout(() => { document.body.removeChild(a); URL.revokeObjectURL(url); }, 100);
1692
  }
1693
 
1694
+ function downloadText(filename, text, mime = "text/plain;charset=utf-8") {
1695
+ const blob = new Blob([text], { type: mime });
1696
+ const url = URL.createObjectURL(blob);
1697
+ const a = document.createElement("a");
1698
+ a.href = url;
1699
+ a.download = filename;
1700
+ document.body.appendChild(a);
1701
+ a.click();
1702
+ setTimeout(() => { document.body.removeChild(a); URL.revokeObjectURL(url); }, 100);
1703
+ }
1704
+
1705
+ // LaTeX-escape a plain string for inclusion in a tabular cell.
1706
+ function latexEscape(s) {
1707
+ return String(s ?? "")
1708
+ .replace(/\\/g, "\\textbackslash{}")
1709
+ .replace(/[#$%&_{}]/g, m => "\\" + m)
1710
+ .replace(/~/g, "\\textasciitilde{}")
1711
+ .replace(/\^/g, "\\textasciicircum{}")
1712
+ .replace(/</g, "\\textless{}")
1713
+ .replace(/>/g, "\\textgreater{}");
1714
+ }
1715
+
1716
+ function profileToLatex(p, hash = "") {
1717
+ const ms = p.model_summary || {};
1718
+ const kn = p.key_numbers || {};
1719
+ let tex = `% TAF Profile — auto-generated by TAF Agent\n`;
1720
+ if (hash) tex += `% input hash: #${hash}\n`;
1721
+ tex += `\\begin{table}[ht]\n\\centering\n`;
1722
+ tex += `\\caption{TAF Profile — ${latexEscape(ms.architecture_class || "?")}${hash ? ` (\\#${latexEscape(hash)})` : ""}}\n`;
1723
+ tex += `\\begin{tabular}{lll}\n\\toprule\nRecipe & Verdict & Reason \\\\\n\\midrule\n`;
1724
+ Object.entries(p.recipes || {}).forEach(([rid, r]) => {
1725
+ tex += `${latexEscape(rid)} & ${latexEscape(r.verdict || "")} & ${latexEscape((r.reason || "").slice(0, 80))} \\\\\n`;
1726
+ });
1727
+ tex += `\\bottomrule\n\\end{tabular}\n\\end{table}\n\n`;
1728
+ tex += `% Key numbers (JSON):\n`;
1729
+ for (const [k, v] of Object.entries(kn)) {
1730
+ tex += `% ${k} = ${typeof v === "object" ? JSON.stringify(v) : v}\n`;
1731
+ }
1732
+ return tex;
1733
+ }
1734
+
1735
+ function compareToLatex(c, hash = "") {
1736
+ let tex = `% TAF Comparison — ${c.recipe_id} (${c.recipe_name})\n`;
1737
+ if (hash) tex += `% input hash: #${hash}\n`;
1738
+ tex += `\\begin{table}[ht]\n\\centering\n`;
1739
+ tex += `\\caption{TAF Comparison — ${latexEscape(c.recipe_id)} ${latexEscape(c.recipe_name || "")}${hash ? ` (\\#${latexEscape(hash)})` : ""}}\n`;
1740
+ tex += `\\begin{tabular}{lll}\n\\toprule\nModel & Verdict & Reason \\\\\n\\midrule\n`;
1741
+ c.rows.forEach(r => {
1742
+ tex += `${latexEscape(r.label)} & ${latexEscape(r.verdict)} & ${latexEscape((r.reason || "").slice(0, 80))} \\\\\n`;
1743
+ });
1744
+ tex += `\\bottomrule\n\\end{tabular}\n\\end{table}\n`;
1745
+ return tex;
1746
+ }
1747
+
1748
+ function recipeToLatex(r, hash = "") {
1749
+ let tex = `% TAF Recipe ${r.recipe_id} — ${r.recipe_name}\n`;
1750
+ if (hash) tex += `% input hash: #${hash}\n`;
1751
+ tex += `\\begin{table}[ht]\n\\centering\n`;
1752
+ tex += `\\caption{TAF Recipe \\texttt{${latexEscape(r.recipe_id)}} — verdict: ${latexEscape(r.verdict)}${hash ? ` (\\#${latexEscape(hash)})` : ""}}\n`;
1753
+ tex += `\\begin{tabular}{rll}\n\\toprule\nStep & Formula & Result \\\\\n\\midrule\n`;
1754
+ (r.chain || []).forEach(s => {
1755
+ tex += `${latexEscape(s.step)} & \\texttt{${latexEscape(s.formula || "")}} & ${latexEscape(formatResultPlain(s.result))} \\\\\n`;
1756
+ });
1757
+ tex += `\\bottomrule\n\\end{tabular}\n\\end{table}\n\n`;
1758
+ tex += `% Reason: ${latexEscape(r.reason || "")}\n`;
1759
+ if (r.mitigation) tex += `% Mitigation: ${latexEscape(r.mitigation)}\n`;
1760
+ return tex;
1761
+ }
1762
+
1763
  // Sort object keys recursively for deterministic JSON
1764
  function sortKeys(o) {
1765
  if (Array.isArray(o)) return o.map(sortKeys);
 
1849
  return `taf-${type}-${name}-${suffix}-${hash}.json`;
1850
  }
1851
 
1852
+ // v0.6 privacy fix: previously placed full JSON body in URL params → GH server logs +
1853
+ // referer headers captured user data. Now copy body to clipboard, open issue page
1854
+ // with title only, user pastes body manually. Title is non-sensitive (model name +
1855
+ // hash). On clipboard failure, fall back to console log so user can grab body.
1856
+ async function submitToRegistry(type, data, statusEl) {
1857
  const hash = await inputHash(type, data);
1858
  const modelName = modelShortName(data, "model");
1859
  let title, body;
 
1869
  body = recipeToMarkdown(data, hash);
1870
  }
1871
  const dedupNote = `\n\n> **Input hash**: \`#${hash}\` — search this hash in registry issues to find independent verifications. Same inputs always produce the same hash.`;
1872
+ const fullBody = body + dedupNote + "\n\n---\n*Submitted via [TAF Agent](https://karlesmarin.github.io/tafagent)*";
1873
+
1874
+ let clipboardOk = false;
1875
+ try {
1876
+ await navigator.clipboard.writeText(fullBody);
1877
+ clipboardOk = true;
1878
+ } catch (e) {
1879
+ console.warn("Clipboard write failed; body logged below:", e);
1880
+ console.log("[TAF Agent] Issue body to paste:\n\n" + fullBody);
1881
+ }
1882
+
1883
+ // Title-only URL — body intentionally omitted to avoid leaking via GH server logs / referer.
1884
+ const params = new URLSearchParams({ title });
1885
+ window.open(`https://github.com/${REGISTRY_REPO}/issues/new?${params.toString()}`, "_blank");
1886
+
1887
+ if (statusEl) {
1888
+ statusEl.textContent = clipboardOk
1889
+ ? (t("share.submit_clip_ok") || "↗ Opened GitHub. Body copied to clipboard — paste it into the issue body.")
1890
+ : (t("share.submit_clip_fail") || "↗ Opened GitHub. Clipboard blocked — body logged in browser console (F12).");
1891
+ }
1892
  }
1893
 
1894
  function profileToMarkdown(p, hash="") {
scripts/README.md ADDED
@@ -0,0 +1,38 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ # scripts/
2
+
3
+ ## `check_lean_manifest.py`
4
+
5
+ Cross-checks `data/lean_status.json` against the actual `lean-taf` Lean source repo. Run before pushing to catch:
6
+
7
+ - Theorems renamed / deleted in source but still in manifest.
8
+ - Line numbers in manifest no longer matching the source declaration (e.g. after a refactor moved theorems).
9
+ - New theorems in source not yet captured in manifest.
10
+ - Commit-hash drift between manifest and current `lean-taf` HEAD.
11
+
12
+ ### Usage
13
+
14
+ ```bash
15
+ # default — auto-detects ../lean-taf or ../NeurIPS/lean_taf/taf
16
+ python scripts/check_lean_manifest.py
17
+
18
+ # explicit path
19
+ python scripts/check_lean_manifest.py --lean-taf-path /path/to/lean-taf
20
+
21
+ # rewrite manifest in-place to match source (backs up to .bak first)
22
+ python scripts/check_lean_manifest.py --regenerate
23
+ ```
24
+
25
+ Exit 0 = clean, 1 = drift detected. Suitable as a pre-push hook or CI gate once `lean-taf` is checked out alongside.
26
+
27
+ ### Workflow
28
+
29
+ 1. After committing changes in `lean-taf` (renaming a theorem, adding a new one, etc.):
30
+ 2. In `tafagent/`, run `python scripts/check_lean_manifest.py` to see what drifted.
31
+ 3. If line numbers shifted but theorem set is unchanged: `python scripts/check_lean_manifest.py --regenerate` rewrites in-place.
32
+ 4. If new theorems appeared: regenerate captures them with `file`/`line` only — manually fill `claim`, `tactic`, `tags`, etc. before committing.
33
+ 5. Commit `data/lean_status.json` to `tafagent`.
34
+
35
+ ### What `--regenerate` preserves vs overwrites
36
+
37
+ - **Overwrites**: `file`, `line`, `lean_repo.commit`, `lean_repo.commit_short`.
38
+ - **Preserves**: `claim`, `tactic`, `preconditions`, `status`, `tags`, `source`, `ui_badge`, plus `findings`, `groups[].title/id`, `summary`, `ui_bindings`. The schema is rewritten with the same keys — anything not derivable from source is kept verbatim.
scripts/check_lean_manifest.py ADDED
@@ -0,0 +1,231 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ #!/usr/bin/env python3
2
+ """Cross-check tafagent's lean_status.json against the lean-taf source repo.
3
+
4
+ Detects three kinds of drift:
5
+ 1. Theorem named in manifest but missing from source file.
6
+ 2. Line number in manifest no longer matches the source declaration.
7
+ 3. Theorem present in source `theorem <name>` but absent from manifest.
8
+
9
+ Usage:
10
+ python scripts/check_lean_manifest.py
11
+ python scripts/check_lean_manifest.py --lean-taf-path /path/to/lean-taf
12
+ python scripts/check_lean_manifest.py --regenerate # rewrite line numbers in-place
13
+
14
+ By default looks for `../lean-taf` and `../NeurIPS/lean_taf/taf` (developer layout).
15
+ Set LEAN_TAF_PATH to override. Exit 0 = clean, 1 = drift detected (CI gate).
16
+ """
17
+ from __future__ import annotations
18
+ import argparse
19
+ import json
20
+ import os
21
+ import re
22
+ import sys
23
+ import subprocess
24
+ from pathlib import Path
25
+
26
+ THEOREM_RE = re.compile(r"^\s*theorem\s+([A-Za-z_][A-Za-z0-9_]*)\b")
27
+
28
+ REPO_ROOT = Path(__file__).resolve().parent.parent
29
+ MANIFEST = REPO_ROOT / "data" / "lean_status.json"
30
+ LEAN_TAF_CANDIDATES = [
31
+ REPO_ROOT.parent / "lean-taf",
32
+ REPO_ROOT.parent / "NeurIPS" / "lean_taf" / "taf",
33
+ ]
34
+
35
+
36
+ def find_lean_taf(arg_path: str | None) -> Path:
37
+ if arg_path:
38
+ p = Path(arg_path).expanduser().resolve()
39
+ if (p / "Taf.lean").exists():
40
+ return p
41
+ sys.exit(f"error: {p} does not contain Taf.lean — wrong path?")
42
+ env = os.environ.get("LEAN_TAF_PATH")
43
+ if env:
44
+ return find_lean_taf(env)
45
+ for c in LEAN_TAF_CANDIDATES:
46
+ if (c / "Taf.lean").exists():
47
+ return c.resolve()
48
+ sys.exit("error: lean-taf repo not found. Set LEAN_TAF_PATH or pass --lean-taf-path.")
49
+
50
+
51
+ def grep_theorems(lean_root: Path) -> dict[str, tuple[str, int]]:
52
+ """Return {theorem_name: (relative_file, line_number)} from Taf/*.lean."""
53
+ out: dict[str, tuple[str, int]] = {}
54
+ for lean_file in (lean_root / "Taf").glob("*.lean"):
55
+ rel = f"Taf/{lean_file.name}"
56
+ with lean_file.open(encoding="utf-8") as f:
57
+ for lineno, line in enumerate(f, start=1):
58
+ m = THEOREM_RE.match(line)
59
+ if m:
60
+ name = m.group(1)
61
+ if name in out:
62
+ # Duplicate theorem name across files (Lean would also reject) — flag.
63
+ print(f"warn: duplicate theorem name {name!r} at {rel}:{lineno} "
64
+ f"and {out[name][0]}:{out[name][1]}", file=sys.stderr)
65
+ out[name] = (rel, lineno)
66
+ return out
67
+
68
+
69
+ def get_lean_taf_head(lean_root: Path) -> str | None:
70
+ try:
71
+ return subprocess.check_output(
72
+ ["git", "-C", str(lean_root), "rev-parse", "--short", "HEAD"],
73
+ stderr=subprocess.DEVNULL,
74
+ ).decode().strip()
75
+ except (subprocess.CalledProcessError, FileNotFoundError):
76
+ return None
77
+
78
+
79
+ def manifest_theorems(manifest: dict) -> list[dict]:
80
+ out = []
81
+ for group in manifest.get("groups", []):
82
+ for t in group.get("theorems", []):
83
+ out.append(t)
84
+ return out
85
+
86
+
87
+ def check(manifest: dict, lean_root: Path) -> tuple[int, list[dict]]:
88
+ """Return (number_of_drifts, list_of_drift_records)."""
89
+ src = grep_theorems(lean_root)
90
+ drifts: list[dict] = []
91
+ seen_in_manifest: set[str] = set()
92
+
93
+ for t in manifest_theorems(manifest):
94
+ name = t["name"]
95
+ seen_in_manifest.add(name)
96
+ if name not in src:
97
+ drifts.append({"kind": "missing_in_source", "name": name,
98
+ "manifest_file": t.get("file"), "manifest_line": t.get("line")})
99
+ continue
100
+ src_file, src_line = src[name]
101
+ if t.get("file") != src_file:
102
+ drifts.append({"kind": "file_drift", "name": name,
103
+ "manifest_file": t.get("file"), "source_file": src_file})
104
+ if t.get("line") != src_line:
105
+ drifts.append({"kind": "line_drift", "name": name,
106
+ "manifest_line": t.get("line"), "source_line": src_line,
107
+ "file": src_file})
108
+
109
+ for name, (src_file, src_line) in src.items():
110
+ if name not in seen_in_manifest:
111
+ drifts.append({"kind": "missing_in_manifest", "name": name,
112
+ "source_file": src_file, "source_line": src_line})
113
+
114
+ # Commit-hash sanity check.
115
+ head = get_lean_taf_head(lean_root)
116
+ declared = manifest.get("lean_repo", {}).get("commit_short")
117
+ if head and declared and head != declared:
118
+ drifts.append({"kind": "commit_drift", "manifest_commit": declared, "head_commit": head})
119
+
120
+ return len(drifts), drifts
121
+
122
+
123
+ def regenerate(manifest: dict, lean_root: Path) -> int:
124
+ """Rewrite line numbers (and file paths) in-place. Preserves claims, tactics, etc.
125
+ Returns count of theorems updated."""
126
+ src = grep_theorems(lean_root)
127
+ updated = 0
128
+ for group in manifest.get("groups", []):
129
+ for t in group.get("theorems", []):
130
+ name = t["name"]
131
+ if name in src:
132
+ src_file, src_line = src[name]
133
+ if t.get("file") != src_file or t.get("line") != src_line:
134
+ t["file"] = src_file
135
+ t["line"] = src_line
136
+ updated += 1
137
+ head = get_lean_taf_head(lean_root)
138
+ if head:
139
+ manifest.setdefault("lean_repo", {})["commit_short"] = head
140
+ try:
141
+ full = subprocess.check_output(
142
+ ["git", "-C", str(lean_root), "rev-parse", "HEAD"],
143
+ stderr=subprocess.DEVNULL,
144
+ ).decode().strip()
145
+ manifest["lean_repo"]["commit"] = full
146
+ except (subprocess.CalledProcessError, FileNotFoundError):
147
+ pass
148
+ return updated
149
+
150
+
151
+ # Drift kinds split by severity. ERROR kinds break the badges (manifest references
152
+ # something the source doesn't have, or points at the wrong line). INFO kinds are
153
+ # advisory — new helpers in source, or the manifest predates a doc-only commit.
154
+ ERROR_KINDS = {"missing_in_source", "file_drift", "line_drift"}
155
+ INFO_KINDS = {"missing_in_manifest", "commit_drift"}
156
+
157
+
158
+ def format_drift(d: dict) -> str:
159
+ k = d["kind"]
160
+ if k == "missing_in_source":
161
+ return f" [ERR] MISSING in source: {d['name']} (manifest claims {d['manifest_file']}:{d['manifest_line']})"
162
+ if k == "file_drift":
163
+ return f" [ERR] FILE drift: {d['name']} -- manifest={d['manifest_file']} source={d['source_file']}"
164
+ if k == "line_drift":
165
+ return f" [ERR] LINE drift: {d['name']} in {d['file']} -- manifest={d['manifest_line']} source={d['source_line']}"
166
+ if k == "missing_in_manifest":
167
+ return f" [info] new in source: {d['name']} at {d['source_file']}:{d['source_line']} (not in manifest -- helper or unmapped)"
168
+ if k == "commit_drift":
169
+ return f" [info] commit drift: manifest={d['manifest_commit']} head={d['head_commit']} (regenerate to update)"
170
+ return f" [?] unknown drift kind: {d}"
171
+
172
+
173
+ def main() -> int:
174
+ # Force UTF-8 stdout so emoji / non-ASCII labels survive Windows cp1252 console.
175
+ try:
176
+ sys.stdout.reconfigure(encoding="utf-8")
177
+ except Exception:
178
+ pass
179
+
180
+ ap = argparse.ArgumentParser(description=__doc__.split("\n\n")[0])
181
+ ap.add_argument("--lean-taf-path", help="Path to lean-taf repo (default: env LEAN_TAF_PATH or ../lean-taf or ../NeurIPS/lean_taf/taf)")
182
+ ap.add_argument("--regenerate", action="store_true", help="Rewrite manifest line numbers + commit hash to match source. Backs up to lean_status.json.bak.")
183
+ ap.add_argument("--manifest", default=str(MANIFEST), help="Path to lean_status.json (default: data/lean_status.json)")
184
+ ap.add_argument("--strict", action="store_true", help="Treat info-level drifts (commit, new-in-source) as errors too.")
185
+ args = ap.parse_args()
186
+
187
+ lean_root = find_lean_taf(args.lean_taf_path)
188
+ manifest_path = Path(args.manifest)
189
+ with manifest_path.open(encoding="utf-8") as f:
190
+ manifest = json.load(f)
191
+
192
+ if args.regenerate:
193
+ backup = manifest_path.with_suffix(".json.bak")
194
+ backup.write_text(json.dumps(manifest, indent=2, ensure_ascii=False), encoding="utf-8")
195
+ n = regenerate(manifest, lean_root)
196
+ manifest_path.write_text(json.dumps(manifest, indent=2, ensure_ascii=False) + "\n", encoding="utf-8")
197
+ print(f"regenerated: {n} theorem(s) updated. backup → {backup.name}")
198
+ return 0
199
+
200
+ _, drifts = check(manifest, lean_root)
201
+ src_total = len(grep_theorems(lean_root))
202
+ manifest_total = len(manifest_theorems(manifest))
203
+ head = get_lean_taf_head(lean_root) or "?"
204
+ errors = [d for d in drifts if d["kind"] in ERROR_KINDS]
205
+ infos = [d for d in drifts if d["kind"] in INFO_KINDS]
206
+ print(f"manifest: {manifest_total} theorems source: {src_total} theorems")
207
+ print(f"manifest commit: {manifest.get('lean_repo', {}).get('commit_short', '?')} head: {head}")
208
+ print(f"lean_taf path: {lean_root}")
209
+ print()
210
+ if errors:
211
+ print(f"ERRORS ({len(errors)}):")
212
+ for d in errors:
213
+ print(format_drift(d))
214
+ print()
215
+ if infos:
216
+ print(f"INFO ({len(infos)}):")
217
+ for d in infos:
218
+ print(format_drift(d))
219
+ print()
220
+ if not errors and not infos:
221
+ print("OK -- no drift.")
222
+ return 0
223
+ if errors or (args.strict and infos):
224
+ print("Fix: re-run with --regenerate, then commit data/lean_status.json.")
225
+ return 1
226
+ print("OK -- only info-level drift; pass --strict to fail on these too.")
227
+ return 0
228
+
229
+
230
+ if __name__ == "__main__":
231
+ sys.exit(main())
style.css CHANGED
@@ -1,4 +1,19 @@
1
  /* TAF Agent — minimal clean styling */
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
2
  :root {
3
  --bg: #0a0e14;
4
  --bg-card: #12181f;
 
1
  /* TAF Agent — minimal clean styling */
2
+
3
+ /* a11y: skip-to-main link, visible only on keyboard focus */
4
+ .skip-link {
5
+ position: absolute;
6
+ left: 0; top: -40px;
7
+ background: #58a6ff;
8
+ color: #0a0e14;
9
+ padding: 0.5em 1em;
10
+ text-decoration: none;
11
+ font-weight: 600;
12
+ z-index: 9999;
13
+ transition: top 0.15s;
14
+ }
15
+ .skip-link:focus { top: 0; outline: 2px solid #fff; }
16
+
17
  :root {
18
  --bg: #0a0e14;
19
  --bg-card: #12181f;