A simple widget for Lean4
which displays a graph in the infoview and allows the user to get information about the nodes.
import GraphWidget
def nodes : Array GraphWidget.Node := #[
{
id := "0"
info := "Info A"
},
{
id := "1"
info := "Info B"
}
]
def dot : String := "\
digraph {
\"A\" [label=\"Node A\", id=\"0\", color=red];
\"B\" [label=\"Node B\", id=\"1\", color=blue];
\"A\" -> \"B\";
}"
open GraphWidget ProofWidgets ProofWidgets.Jsx in
#html <Graph nodes = {nodes} dot = {dot} />
This will display a graphviz graph in the infoview with two nodes with labels Node A
and Node B
connected by a directed edge from Node A
to Node B
.
Clicking on Node A
will display Info A
and clicking on Node B
will display Info B
.
Markdown (with math) can be used in the info
field of the nodes.
Assuming you have a standard lean4 project with a lakefile, adding the following to lakefile.lean
should work:
require graph_widget from git "https://github.com/adamtopaz/graph_widget.git"