cryptobiosis's picture
Publish static OProver results lab
e9eed22 verified
Raw
History Blame Contribute Delete
1.59 kB
const q=s=>document.querySelector(s),qa=s=>[...document.querySelectorAll(s)];fetch('./data/results.json').then(r=>r.json()).then(d=>{q('#hero').textContent=d.hero;q('#cost').textContent=d.cost;const sel=q('#stage');d.stages.forEach(s=>sel.add(new Option(`${s.label}${s.status}`,s.id)));function draw(){const s=d.stages.find(x=>x.id===sel.value);q('#stagecard').innerHTML=`<h3>${s.label}</h3><p class="status">${s.status}</p><p>Strict exact: ${s.exact??'not qualified'}/22 · holdout ${s.holdout??'—'}/18 · canary ${s.canary??'—'}/4</p><div class="bar" aria-label="Exact Lean rate"><i style="width:${s.exact?100*s.exact/22:0}%"></i></div><p><a href="${s.repo}">Open model repository</a></p>`}sel.onchange=draw;draw();q('#stats').innerHTML=`<li>${d.statistics.parser}</li><li>Unsafe generations: ${d.statistics.unsafe}</li><li>${d.statistics.stage4_vs_stage2}</li><li>${d.statistics.stage4_vs_stage3}</li>`;q('#prod').textContent=`Converted ${d.production.converted}; canary ${d.production.canary}; ${d.production.scope}.`;q('#jensen').textContent=`${d.jensen.status}; Lean-valid ${d.jensen.lean_valid}; RH PROVED: ${d.jensen.rh_proved}.`;q('#taxonomy').innerHTML=d.failure_taxonomy.map(x=>`<li>${x}</li>`).join('');q('#artifacts').innerHTML=d.stages.map(s=>`<li><a href="${s.repo}">${s.label}</a></li>`).join('')+`<li><a href="${d.dataset}">Training dataset</a></li>`});qa('.tabs button').forEach(b=>b.onclick=()=>{qa('.tabs button').forEach(x=>x.setAttribute('aria-selected','false'));b.setAttribute('aria-selected','true');qa('.panel').forEach(p=>p.hidden=p.id!==b.dataset.tab)})