メニュー
Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance.
デフォルトでは、最初にソースを確認する Prompt が選択されています。直接コマンドに切り替えるか、ローカルコピーをダウンロードすることもできます。
インストールを決める前に、SKILL.md と SkillsMP に表示されている付属ファイルをお読みください。
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
直接コマンドでは確認用 Prompt が省略されます。実行前にソースを確認してください。
npx skills add https://github.com/leanprover/lean4 --skill profilingコマンドは1行のまま表示されます。コピー前に横へスクロールして全体を確認してください。
ローカルで確認しますか？SkillsMP が現在取得できるファイルをダウンロードできます。
Retrieve and investigate failing Lean CI job logs. Use when a CI job fails and you need to fetch its logs, or when monitoring a CI run for failures.
Build and run tests against the stage2 Lean compiler. Use when asked to build, rebuild, or test against stage2.
Diagnose a spurious stage1 test failure caused by olean-persisted compiler changes. Use when a stage1 test fails unexpectedly and the change adds or modifies an environment extension or other information persisted into .olean files.
SOC 職業分類に基づく
SKILL.md を表示中
| name | profiling |
| description | Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance. |
| allowed-tools | Bash, Read, Glob, Grep |
Full documentation: script/PROFILER_README.md.
script/lean_profile.sh ./build/release/stage1/bin/lean some_file.lean
Requires samply (cargo install samply) and python3.
samply record --save-only, symbolicate_profile.py, then serve_profile.py.lean_demangle.py works standalone as a stdin filter (like c++filt) for quick name lookups.--raw flag on lean_demangle.py gives exact demangled names without postprocessing (keeps ._redArg, ._lam_0 suffixes as-is).PROFILE_KEEP=1 to keep the temp directory for later inspection.threads[i].stringArray, indexed by threads[i].funcTable.name.