// Lean/Mathlib の機能、構文、タクティク、コード例、仕様、出典、背景理論を調査するときに使用する。Lean by Example の記事追加・編集前の下調べ、既存記事の根拠確認、外部資料からのコード例収集、Lean のバージョン差の確認で使う。
| name | research |
| description | Lean/Mathlib の機能、構文、タクティク、コード例、仕様、出典、背景理論を調査するときに使用する。Lean by Example の記事追加・編集前の下調べ、既存記事の根拠確認、外部資料からのコード例収集、Lean のバージョン差の確認で使う。 |
Lean by Example の記事追加・編集に必要な下調べを行う。調査結果は、記事本文で使える具体的な Lean コード例と、確認可能な出典に落とし込む。
lean-toolchain と lake-manifest.json の依存関係を前提にする。まず調査したい語をリポジトリ内で探す。
rg "keyword" LeanByExample
既存記事と似たテーマがある場合は、その .lean ファイルの構成、用語、検証方法を確認する。
依存パッケージが取得済みなら、Lean/Mathlib のソースも検索する。
rg "keyword" .lake\packages
以下の外部資料をすべて確認する。
候補となる説明・コード例・反例を短くメモする。最低限、次を残す。
#guard_msgs、#check_failure、#guard などで失敗も検証する。#check、#print、#reduce、#eval、#synth、#instances を使う。sorry を含む例は、未完成例として明示する場合を除き採用しない。既存記事を編集する場合は対象 .lean ファイルで検証する。
lake env lean LeanByExample\Path\To\File.lean
調査用の一時コードが必要な場合は、最終的に記事へ移すか削除する。不要な調査ファイルを残さない。
複数ファイルに影響する変更や import の追加がある場合は、必要に応じて lake build を実行する。
エラーや警告を記事で扱う場合は、実際のメッセージが現在の Lean で再現することを確認する。
調査結果を報告書 REPORT_TEMP.lean にまとめる。
Lean by Example で普段行っている形式で、解説はコメント部分に書いてコードはコメントアウトせずに動く形で書く。
報告書は 3000 行以内にまとめる。
報告や次工程への引き継ぎでは、次を簡潔に示す。
Lean 解説記事を編集・執筆するときに使う。
このリポジトリの実装のために環境構築を新規に行うときに使う。
Codex が git commit コマンドを実行するときに、専用の Git author/committer 名とメールアドレスを使うように指示する。