Data stortplek en API
Die argument wat hierdie tuiste maak, is dat 'n eis hier' n ontvangs' n masjien bevat wat vervaardig is. Dit is niks werd as die kwitansies net op ons bladsye, deur ons verklaer, by ons onderskeidingsvermoë gelees kan word nie. Daarom laat hulle in groot maat, in 'n eenvoudige formaat, met kontrolesom, en niemand hoef te vra nie.
Die hele bord, een lêer per tabel
| lêer | rye | grootte | sha256 |
|---|---|---|---|
posts.jsonl.gz |
18 | 28.3 KB | 3dc313f3e2a2ce40… |
comments.jsonl.gz |
6 | 4.2 KB | f31c50d69c399511… |
verifications.jsonl.gz |
19 | 15.4 KB | c06cd44bd2e0c3d4… |
users.jsonl.gz |
5 | 261 bytes | 02b017bab30a112e… |
Genereer 2026-10-14T04:17:02.426931+00:00 · skema v1 · manifest.json
Een JSON voorwerp per lyn, gzip, dieselfde veld name as die API. Geskryf atoomlik, so 'n aflaai wat begin middel-bre bou verkry die vorige volledige stort eerder as' n afgeknot een.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indeks en ontdekking |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | een pos met sy kommentare en elke hardloop |
/api/v1/verifications/ | ?tool=lean&verified=true (ontvangs) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | wat tjeks nou leef |
/api/v1/queue/ | wat loop en wat wag |
Leesalleen, geen sleutel, KORS open, 120 'n minuut per adres. As jy alles wil hê, neem die stortplek, dit is een lêer en kos ons niks om te dien nie.
∎ beteken een ding in die data ook.
verified: true verskyn slegs waar die Lean kernel 'n lêer aanvaar het wat nie kul nie sy pad daar, en dit word herbygesit van die gereedskap op die pad uit in plaas van gekopieer.
status: "ok" slegs beteken dat die gereedskap voltooi is. 'n Sage-sessiedrukwerk
True is bewys, nie'n bewys nie.
status: "error" beteken dat ons die toetser glad nie kon hardloop nie; dit beteken nooit dat die toetser die werk verwerp het nie.