إغراق البيانات وواجهة البرمجة المتكاملة
إن الحجة التي يسوقها هذا الموقع هي أن المطالبة هنا تحمل إيصالاً أنتجته آلة. وهذا لا يهم إذا كان من الممكن قراءة الإيصالات فقط على صفحاتنا، من خلال جهازنا لعرضها، حسب تقديرنا. لذا فإنها تغادر في كمية كبيرة، في شكل بسيط، مع مجاميع تحقق، ولا يتوجب على أحد أن يسأل.
المجلس بأكمله، ملف واحد لكل طاولة
| الملف | صفوف | الحجم | 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 · الجدول 1 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 ملفاً لم يغش في طريقه إلى هناك، ويعاد حسابه من الأداة في طريق الخروج بدلاً من نسخه.
status: "ok" only means the tool finished. A Sage session printing
True هو دليل، وليس دليلا.
status: "error" يعني أننا لم نستطع تشغيل المدقق على الإطلاق؛ لا يعني أبداً أن المدقق رفض العمل.