Components & presentations

[Vtec234]

• Introduce a type Component Props which gives a Lean type to the props of a React component.

• Add capability to store RpcEncodable widget props in the InfoTree (via ofCustomInfo but we could add it to core Lean later). See Compat.lean for implementation details.

• Support using widget components inline in JSX syntax so we can partly describe GUIs in pure Lean, kind of like ProofWidgets4. JS still needs to be written for any kind of event handling or RPC call.

• Add a component to display Penrose diagrams.

• Introduce a framework for displaying Exprs as interactive widgets from Lean code. An Expr presenter registered with @[expr_presenter] is similar to a delaborator but outputs HTML trees instead of syntax, and the output HTML can contain elements which interact with the original Expr in some way. We call interactive outputs with a reference to the original input presentations following [Ciccarelli].

  An example presenter looks like

@[expr_presenter]
def presenter : ExprPresenter where
  userName := "With octopodes"
  isApplicable _ := return true
  present e :=
    return EncodableHtml.ofHtml
      <span>
        -- Note the use of a widget component with RpcEncodable props in JSX. This is typechecked
        {.text "🐙 "}<InteractiveCode fmt={← Lean.Widget.ppExprTagged e} />{.text " 🐙"}
      </span>

Depends on leanprover/lean4#1969 and the associated vscode-lean4 PR.

[EdAyers]

This looks awesome