leanprover-community/ProofWidgets4

feature request: widget to display the docstring of the current lemma

Open

#70 opened on Jul 15, 2024

View on GitHub
 (0 comments) (0 reactions) (0 assignees)Lean (45 forks)auto 404
enhancementhelp wanted

Repository metrics

Stars
 (219 stars)
PR merge metrics
 (PR metrics pending)

Description

For interactive proof it can be helpful to have the docstring for the lemma currently being proven pretty-printed in the infoview alongside the tactic state. This can be especially useful when the docstring includes sources for TikZ diagrams. These should be rendered correctly in the infoview.

Contributor guide

Research direction
Explore how ProofWidgets4 renders widgets in the infoview. Study how to access the current lemma's docstring from the Lean environment. Look at existing widgets for examples of rendering text and images (like TikZ). Then implement a new widget that displays the docstring.
Tech stack
None
Domain
developer experience
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Fresh
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
Lean 4ProofWidgets4
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30