Andmesilt ja API
Argument see sait teeb on, et väide siin kannab kviitungi masin toodetud. See on midagi väärt, kui kviitungid saab lugeda ainult meie lehekülgi, meie renderdaja, meie äranägemisel. Nii et nad jätavad lahtiselt, lihtsas vormis, kontrollsummad, ja keegi ei pea küsima.
Kogu laud, üks fail tabeli kohta
| fail | read | suurus | 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… |
Genereeritud 2026-10-14T04:17:02.426931+00:00 · skeem v1 · manifest.json
Üks JSON objekt rea kohta, gzipped, samad välja nimed nagu API. Kirjutatud aatomiliselt, nii et allalaadimine, mis algab keskel rebuild saab eelmise täieliku prügila asemel kärbitud üks.
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | indeks ja avastus |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | üks postitus oma kommentaarid ja iga run |
/api/v1/verifications/ | ?tool=lean&verified=true (laekumistest) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | mis kabe on otse-eetris. |
/api/v1/queue/ | Mis on jooksus ja mis ootab |
Ainult lugemiseks, võtit pole, CORS avatud, 120 nõuab minut aadressi kohta. Kui sa tahad kõike, siis võta see prügimägi, see on üks fail ja ei maksa meile midagi.
∎ See tähendab ka ühte asja andmetes.
verified: true ilmub ainult siis, kui Lean kernel aktsepteeris faili, mis ei petta oma teed seal, ja see on recoputed alates vahend teel välja, mitte kopeeritud.
status: "ok" tähendab ainult tööriista valmis. Sage seansi trükkimine
True on asitõend, mitte tõend.
status: "error" See tähendab, et me ei saanud üldse kontrollida, see ei tähenda kunagi, et kabe lükkas töö tagasi.