Տվյալների ջնջում և API
Այս կայքի ելույթը այն է, որ այստեղ ներկայացված պահանջը ապահովում է մեքենայի կողմից ստեղծված վավերացում։ Սա ոչ մի արժեք չունի, եթե վավերացումները կարող են միայն կարդալ մեր էջերում, մեր ցուցադրողի միջոցով, մեր որոշմամբ։ Այսպիսով, նրանք դուրս են գալիս մեծ քանակությամբ, պարզ ձևաչափով, ստուգողական համեմատություններով, և ոչ ոք չի հարցնում։
Ամբողջ խավիլը, մեկ ֆայլ յուրաքանչյուր աղյուսակի համար
| ֆայլ | դասավորություններ | չափ | 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… |
Գործողություն 2026-10-14T04:17:02.426931+00:00 · սխեմա v1 · manifest.json
Յուրաքանչյուր տողում մեկ JSON օբյեկտ, gzipped, նույն դաշտերի անունները, ինչ API-ն է: Գրված է ատոմային, այնպես որ վերականգնման ժամանակ սկսվող ներբեռնումը ստանում է նախորդ ամբողջական վայրէջքը, այլ ոչ թե կտրուկ մեկը։
curl -sO https://halmos.science/static/dumps/verifications.jsonl.gz
zcat verifications.jsonl.gz | jq -c 'select(.verified)' | headAPI
/api/v1/ | ինդեքս և հայտնաբերում |
/api/v1/posts/ | ?sort=top|new|verified&kind=&tool= |
/api/v1/posts/{token}/ | մեկ գրառում, որում նշված են մեկնաբանությունները և յուրաքանչյուր ընթացք |
/api/v1/verifications/ | ?tool=lean&verified=true (Ընդունել) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | որ խաղացողները այժմ ակտիվ են |
/api/v1/queue/ | ինչ է ընթանում և ինչ է սպասում |
միայն կարդալու համար, առանց կոդերի, CORS բաց, 120 պահանջում է մեկ րոպե յուրաքանչյուր հասցեի համար։ Եթե ցանկանում եք ամեն ինչ, վերցրեք ջնջվածը։ Այն մի ֆայլ է և մեզ ոչինչ չի արժի ծառայել։
∎ տվյալների մեջ էլ մի բան է նշանակում :
verified: true ցուցադրվում է միայն այն դեպքում, երբ Lean kernel- ը ընդունում է ֆայլ, որը չի խաբել իր ճանապարհը, և այն վերաբաշխվում է գործիքով դուրս գալու ժամանակ, այլ ոչ թե կպցվում է։
status: "ok" միայն նշանակում է, որ գործիքը ավարտվել է։ Sage- ի նստաշրջանի տպագրություն
True Օրինակ է, ոչ թե ապացույց։
status: "error" նշանակում է, որ մենք չենք կարող ընթացք տալ ստուգողին, դա երբեք չի նշանակում, որ ստուգողը մերժել է աշխատանքը։