Spaces:
Sleeping
Sleeping
| <html lang="en"> | |
| <head> | |
| <meta charset="UTF-8"> | |
| <meta name="viewport" content="width=device-width, initial-scale=1.0"> | |
| <title>Job {{ job.job_id }} — VeriDeepResearch</title> | |
| <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.16.9/dist/katex.min.css"> | |
| <script defer src="https://cdn.jsdelivr.net/npm/katex@0.16.9/dist/katex.min.js"></script> | |
| <script defer src="https://cdn.jsdelivr.net/npm/katex@0.16.9/dist/contrib/auto-render.min.js"></script> | |
| <style> | |
| * { box-sizing: border-box; margin: 0; padding: 0; } | |
| body { font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', sans-serif; background: #f5f5f5; color: #333; } | |
| .container { max-width: 800px; margin: 30px auto; padding: 0 20px; } | |
| h1 { font-size: 22px; margin-bottom: 4px; } | |
| .nav { font-size: 13px; margin-bottom: 16px; } | |
| .nav a { color: #4a90d9; } | |
| .question { background: #fff; padding: 16px; border-radius: 8px; margin-bottom: 16px; box-shadow: 0 1px 3px rgba(0,0,0,0.1); } | |
| .question p { font-size: 15px; line-height: 1.5; } | |
| .meta { display: flex; gap: 16px; flex-wrap: wrap; margin-top: 8px; font-size: 13px; color: #666; } | |
| .badge { display: inline-block; padding: 3px 10px; border-radius: 12px; font-size: 12px; font-weight: 600; text-transform: uppercase; } | |
| .badge-queued { background: #e8e8e8; color: #666; } | |
| .badge-researching, .badge-proving_fast { background: #e3f2fd; color: #1565c0; } | |
| .badge-aristotle, .badge-decomposing { background: #fff3e0; color: #e65100; } | |
| .badge-finalizing { background: #e8f5e9; color: #2e7d32; } | |
| .badge-completed { background: #c8e6c9; color: #1b5e20; } | |
| .badge-failed { background: #ffcdd2; color: #b71c1c; } | |
| .section { background: #fff; border-radius: 8px; padding: 16px; margin-bottom: 12px; box-shadow: 0 1px 3px rgba(0,0,0,0.1); } | |
| .section h2 { font-size: 15px; margin-bottom: 8px; color: #555; } | |
| #status-log { max-height: 300px; overflow-y: auto; font-size: 13px; line-height: 1.6; font-family: 'Menlo', monospace; white-space: pre-wrap; color: #444; } | |
| #lean-code { background: #1e1e1e; color: #d4d4d4; padding: 12px; border-radius: 6px; font-size: 13px; font-family: 'Menlo', monospace; overflow-x: auto; white-space: pre; max-height: 400px; overflow-y: auto; } | |
| .code-badge { font-size: 12px; font-weight: 600; margin-bottom: 6px; } | |
| .code-badge.verified { color: #2e7d32; } | |
| .code-badge.sorry { color: #e65100; } | |
| .code-badge.unverified { color: #888; } | |
| #answer { font-size: 14px; line-height: 1.7; } | |
| #answer p { margin-bottom: 8px; } | |
| #answer h1, #answer h2, #answer h3, #answer h4 { margin: 12px 0 6px; } | |
| #answer pre { background: #1e1e1e; color: #d4d4d4; padding: 12px; border-radius: 6px; overflow-x: auto; font-size: 13px; } | |
| #answer code { background: #f0f0f0; padding: 1px 4px; border-radius: 3px; font-size: 13px; } | |
| #answer pre code { background: none; padding: 0; } | |
| #answer ul, #answer ol { margin-left: 20px; margin-bottom: 8px; } | |
| #answer blockquote { border-left: 3px solid #ddd; padding-left: 12px; color: #666; } | |
| .stats { display: flex; gap: 24px; flex-wrap: wrap; font-size: 13px; color: #666; } | |
| .stats .stat { } | |
| .stats .stat-label { font-weight: 600; } | |
| .aristotle-table { width: 100%; font-size: 13px; border-collapse: collapse; } | |
| .aristotle-table th, .aristotle-table td { text-align: left; padding: 4px 8px; border-bottom: 1px solid #eee; } | |
| .download-link { display: inline-block; margin-top: 8px; font-size: 13px; } | |
| #done-banner { display: none; background: #c8e6c9; padding: 12px 16px; border-radius: 8px; margin-bottom: 12px; font-weight: 600; color: #1b5e20; } | |
| #done-banner.failed { background: #ffcdd2; color: #b71c1c; } | |
| </style> | |
| </head> | |
| <body> | |
| <div class="container"> | |
| <div class="nav"><a href="/">← New question</a> · <a href="/jobs">All jobs</a></div> | |
| <h1>Job <code>{{ job.job_id }}</code></h1> | |
| <div class="question"> | |
| <p>{{ job.question }}</p> | |
| <div class="meta"> | |
| <span>Phase: <span id="phase-badge" class="badge badge-{{ job.phase }}">{{ job.phase }}</span></span> | |
| <span>Elapsed: <span id="elapsed">{{ job.elapsed_str() }}</span></span> | |
| <span>Cost: $<span id="cost">{{ "%.4f"|format(job.total_cost) }}</span></span> | |
| <span>Iteration: <span id="iteration">{{ job.iteration }}</span></span> | |
| </div> | |
| </div> | |
| <div id="done-banner"></div> | |
| <div class="section"> | |
| <h2>Status Log</h2> | |
| <div id="status-log">{% for s in job.status_log %}- {{ s }} | |
| {% endfor %}</div> | |
| </div> | |
| <div class="section" id="lean-section" style="{% if not job.best_lean_code %}display:none{% endif %}"> | |
| <h2>Lean 4 Code</h2> | |
| <div id="code-badge" class="code-badge {% if job.best_code_verified and job.best_code_sorry_free %}verified{% elif job.best_code_verified %}sorry{% else %}unverified{% endif %}"> | |
| {% if job.best_code_verified and job.best_code_sorry_free %}✅ Verified{% elif job.best_code_verified %}🟡 Partial (contains sorry){% else %}⚠️ Unverified{% endif %} | |
| </div> | |
| <pre id="lean-code">{{ job.best_lean_code }}</pre> | |
| <a class="download-link" href="/job/{{ job.job_id }}/proof.lean">Download proof.lean</a> | |
| </div> | |
| <div class="section" id="answer-section" style="{% if not job.answer %}display:none{% endif %}"> | |
| <h2>Answer</h2> | |
| <div id="answer">{{ job.answer }}</div> | |
| </div> | |
| <div class="section" id="aristotle-section" style="{% if not job.aristotle_jobs %}display:none{% endif %}"> | |
| <h2>Aristotle Jobs</h2> | |
| <table class="aristotle-table"> | |
| <thead><tr><th>ID</th><th>Status</th><th>Prompt</th></tr></thead> | |
| <tbody id="aristotle-tbody"> | |
| {% for aj in job.aristotle_jobs %} | |
| <tr> | |
| <td><code>{{ aj.project_id[:8] }}</code></td> | |
| <td>{{ aj.status }}{% if aj.percent_complete %} ({{ aj.percent_complete }}%){% endif %}</td> | |
| <td>{{ aj.prompt_preview[:80] }}</td> | |
| </tr> | |
| {% endfor %} | |
| </tbody> | |
| </table> | |
| </div> | |
| <div class="section"> | |
| <h2>Stats</h2> | |
| <div class="stats"> | |
| <div class="stat"><span class="stat-label">Tokens:</span> <span id="tokens">{{ "{:,}".format(job.total_input_tokens) }} in / {{ "{:,}".format(job.total_output_tokens) }} out</span></div> | |
| <div class="stat"><span class="stat-label">Tool calls:</span> <span id="tool-counts">{% for k,v in job.tool_counts.items() %}{{ k }}:{{ v }} {% endfor %}</span></div> | |
| </div> | |
| </div> | |
| </div> | |
| <script> | |
| function renderMd(text) { | |
| // Simple markdown to HTML (no external deps) | |
| let html = text; | |
| // Escape HTML | |
| html = html.replace(/&/g, '&').replace(/</g, '<').replace(/>/g, '>'); | |
| // Code blocks: ```...``` | |
| html = html.replace(/```(\w*)\n([\s\S]*?)```/g, '<pre><code>$2</code></pre>'); | |
| // Inline code: `...` | |
| html = html.replace(/`([^`]+)`/g, '<code>$1</code>'); | |
| // Headers | |
| html = html.replace(/^#### (.+)$/gm, '<h4>$1</h4>'); | |
| html = html.replace(/^### (.+)$/gm, '<h3>$1</h3>'); | |
| html = html.replace(/^## (.+)$/gm, '<h2>$1</h2>'); | |
| html = html.replace(/^# (.+)$/gm, '<h1>$1</h1>'); | |
| // Bold: **...** | |
| html = html.replace(/\*\*(.+?)\*\*/g, '<strong>$1</strong>'); | |
| // Italic: *...* | |
| html = html.replace(/(?<!\*)\*(?!\*)(.+?)(?<!\*)\*(?!\*)/g, '<em>$1</em>'); | |
| // Unordered list | |
| html = html.replace(/^[\-\*] (.+)$/gm, '<li>$1</li>'); | |
| html = html.replace(/(<li>.*<\/li>\n?)+/g, '<ul>$&</ul>'); | |
| // Paragraphs: double newline | |
| html = html.replace(/\n\n+/g, '</p><p>'); | |
| html = '<p>' + html + '</p>'; | |
| // Clean up empty paragraphs | |
| html = html.replace(/<p>\s*<\/p>/g, ''); | |
| html = html.replace(/<p>(<h[1-4]>)/g, '$1'); | |
| html = html.replace(/(<\/h[1-4]>)<\/p>/g, '$1'); | |
| html = html.replace(/<p>(<pre>)/g, '$1'); | |
| html = html.replace(/(<\/pre>)<\/p>/g, '$1'); | |
| html = html.replace(/<p>(<ul>)/g, '$1'); | |
| html = html.replace(/(<\/ul>)<\/p>/g, '$1'); | |
| // Single newlines → <br> (but not inside pre) | |
| html = html.replace(/([^>])\n([^<])/g, '$1<br>$2'); | |
| return html; | |
| } | |
| const JOB_ID = "{{ job.job_id }}"; | |
| let polling = true; | |
| async function poll() { | |
| if (!polling) return; | |
| try { | |
| const resp = await fetch(`/api/job/${JOB_ID}`); | |
| const d = await resp.json(); | |
| // Phase badge | |
| const badge = document.getElementById('phase-badge'); | |
| badge.textContent = d.phase; | |
| badge.className = `badge badge-${d.phase}`; | |
| // Meta | |
| document.getElementById('elapsed').textContent = d.elapsed; | |
| document.getElementById('cost').textContent = d.total_cost.toFixed(4); | |
| document.getElementById('iteration').textContent = d.iteration; | |
| // Status log | |
| const logEl = document.getElementById('status-log'); | |
| logEl.textContent = d.status_log.map(s => `- ${s}`).join('\n'); | |
| logEl.scrollTop = logEl.scrollHeight; | |
| // Lean code | |
| if (d.best_lean_code) { | |
| document.getElementById('lean-section').style.display = ''; | |
| document.getElementById('lean-code').textContent = d.best_lean_code; | |
| const cb = document.getElementById('code-badge'); | |
| if (d.best_code_verified && d.best_code_sorry_free) { | |
| cb.textContent = '✅ Verified'; | |
| cb.className = 'code-badge verified'; | |
| } else if (d.best_code_verified) { | |
| cb.textContent = '🟡 Partial (contains sorry)'; | |
| cb.className = 'code-badge sorry'; | |
| } else { | |
| cb.textContent = '⚠️ Unverified'; | |
| cb.className = 'code-badge unverified'; | |
| } | |
| } | |
| // Answer (render markdown + LaTeX) | |
| if (d.answer) { | |
| document.getElementById('answer-section').style.display = ''; | |
| document.getElementById('answer').innerHTML = renderMd(d.answer); | |
| if (window.renderMathInElement) { | |
| renderMathInElement(document.getElementById('answer'), { | |
| delimiters: [ | |
| {left: '$$', right: '$$', display: true}, | |
| {left: '$', right: '$', display: false}, | |
| {left: '\\[', right: '\\]', display: true}, | |
| {left: '\\(', right: '\\)', display: false}, | |
| ], | |
| throwOnError: false, | |
| }); | |
| } | |
| } | |
| // Aristotle jobs | |
| if (d.aristotle_jobs && d.aristotle_jobs.length > 0) { | |
| document.getElementById('aristotle-section').style.display = ''; | |
| const tbody = document.getElementById('aristotle-tbody'); | |
| tbody.innerHTML = d.aristotle_jobs.map(aj => | |
| `<tr><td><code>${aj.project_id.substring(0,8)}</code></td>` + | |
| `<td>${aj.status}${aj.percent_complete ? ` (${aj.percent_complete}%)` : ''}</td>` + | |
| `<td>${(aj.prompt_preview || '').substring(0,80)}</td></tr>` | |
| ).join(''); | |
| } | |
| // Tokens/tools | |
| document.getElementById('tokens').textContent = | |
| `${d.total_input_tokens.toLocaleString()} in / ${d.total_output_tokens.toLocaleString()} out`; | |
| document.getElementById('tool-counts').textContent = | |
| Object.entries(d.tool_counts || {}).map(([k,v]) => `${k}:${v}`).join(' '); | |
| // Done? | |
| if (d.phase === 'completed' || d.phase === 'failed') { | |
| polling = false; | |
| const banner = document.getElementById('done-banner'); | |
| banner.style.display = ''; | |
| if (d.phase === 'completed') { | |
| banner.textContent = d.best_code_verified && d.best_code_sorry_free | |
| ? '✅ Proof verified!' : '⚠️ Completed (proof not fully verified)'; | |
| } else { | |
| banner.textContent = `❌ Failed: ${d.error || 'unknown error'}`; | |
| banner.className = 'failed'; | |
| } | |
| } | |
| } catch (e) { | |
| console.error('Poll error:', e); | |
| } | |
| } | |
| setInterval(poll, 3000); | |
| poll(); | |
| // Render LaTeX on initial load | |
| document.addEventListener('DOMContentLoaded', function() { | |
| if (window.renderMathInElement) { | |
| const answerEl = document.getElementById('answer'); | |
| if (answerEl && answerEl.textContent.trim()) { | |
| answerEl.innerHTML = renderMd(answerEl.textContent); | |
| renderMathInElement(answerEl, { | |
| delimiters: [ | |
| {left: '$$', right: '$$', display: true}, | |
| {left: '$', right: '$', display: false}, | |
| {left: '\\[', right: '\\]', display: true}, | |
| {left: '\\(', right: '\\)', display: false}, | |
| ], | |
| throwOnError: false, | |
| }); | |
| } | |
| } | |
| }); | |
| </script> | |
| </body> | |
| </html> | |