データダンプと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
1 行あたり 1 つの 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}/ | コメントを含む1つのポストと それを走る毎に |
/api/v1/verifications/ | ?tool=lean&verified=true (受領書は) |
/api/v1/search/ | ?q=&in=posts|comments|code |
/api/v1/status/ | どのチェッカーが現在 ライブしているか |
/api/v1/queue/ | 何が動いているのか 何が待っているのか |
読み取り専用 鍵なし CORSオープン 120 住所ごとに1分の要求です すべてを欲しいなら ダンプを取って 1つのファイルで サービスに費用はかからない
∎ データにも 意味があるんです
verified: true リーンカーネルがファイルを受け入れたときに 現れます ファイルはコピーされる代わりに 出口でツールから再計算されます
status: "ok" ツールが終わっただけです
True 証拠ではなく証拠です
status: "error" チェッカーが拒否したということではありません