anandijain/Lean Inspect
Generate Lean goal traces and inject trace links into doc-gen output
View on GitHubTrust Signals
- Scorecard Score
- not yet scored
- Maintenance Recency
- Stale
- License
- None
Inputs
| name | description | required | default |
|---|---|---|---|
| project-root | Path to Lean project root (contains the .lean files) | no | . |
| doc-root | Path to doc-gen output root (e.g. docbuild/.lake/build/doc) | no | docbuild/.lake/build/doc |
| trace-dir | Where to write traces (JSON/HTML) | no | .lean-inspect-traces |
| trace-mode | Mode for trace generation (adaptive or dense) | no | dense |
| inject-debug | Enable debug logging when injecting docs (true/false) | no | true |
Outputs
no outputs