Uthutho lwedata kunye ne-API
Umbuzo olu luhlu luyenza kukuba umbuzo apha uthatha iposi eyenziwe ngumqhubi. Oku akusebenzi ukuba iposi ingafundwa kuphela kwiphepha lethu, ngendlela yethu yokubonisa, kwindlela yethu yokukhetha. Ngoko ke bashiya ngokuthe nkqo, kwifomati ecacileyo, nge checksums, kwaye akukho mntu kufuneka abuze.
Ibhodi yonke, ifayili enye ngetheyibhile
| Ifayile | umqolo | Ubungakanani | 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… |
Iveliswe 2026-10-14T04:17:02.426931+00:00 · i-schema v1 · manifest.json
I-JSON enye yomgca ngamnye, i-gzipped, igama lendawo elifanayo njenge-API. Ibhalwe ngokuzenzekelayo, ngoko kukhuphelo oluqala phakathi kokwakha kwakhona lufumana i-dump epheleleyo edlulileyo kunokuba i-cut-off.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | Iinkqubo ze-IoT |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | one post with its comments and every run |
/api/v1/verifications/ | ?tool=lean&verified=true (i-invoyisi) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | i-checkers ephilayo ngoku |
/api/v1/queue/ | i-Agenda 2000 |
Funda- kuphela, akukho qhosha, CORS ivuliwe, 120 ifuna umzuzu ngamnye kwidilesi nganye. Ukuba ufuna konke, thatha umonakalo. Ifayile enye kwaye ayikothuthi nto ukuncedisa.
∎ I-
verified: true ivela kuphela apho i Lean kernel ithathe ifayile engakhange ikhokelele indlela yayo apho, kwaye iphinda ibalo ukusuka kwisixhobo kwindlela yokuphuma kunokuba ikopiwe.
status: "ok" only means the tool finished. A Sage session printing
True ibonisa, ayibonisi.
status: "error" ithetha ukuba asikwazi ukuqhuba umvavanyi naphi na; ayithethi ukuba umvavanyi uthathelwe ingqalelo umsebenzi.