ProofWidgets.Html to JSX.Element

Stream: lean4

[Adam Topaz]

I am working on a widget/component which takes a prop of type docs#ProofWidgets.Html on the Lean4 side. On the typescript side, I would like to be able to interpret this prop as a JSX.Element instead of Html from https://github.com/leanprover-community/ProofWidgets4/blob/3b2633db0d7848a35acafd20fef918bc6081cb9b/widget/src/htmlDisplay.tsx#L14 . Is this possible to accomplish @Wojciech Nawrocki ?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hi @Adam Topaz! The thing to do is just wrap your html : Html in a <HtmlDisplay html={html} /> in the Typescript code. This is a JSX.Element that renders the given HTML.

[Adam Topaz]

That’s what I’ve been doing, but I don’t know how to import HtmlDisplay into typescript while working outside proofwidgets itself

[Adam Topaz]

It would be great if you could extract that out as an npm package

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Adam Topaz said:

It would be great if you could extract that out as an npm package

Just did this! It's @leanprover-community/proofwidgets4. For now it only exports the HtmlDisplay component at the top-level. Feel free to PR more exports (I think you may still import other components by referring to the relevant file directly), but see discussion below.

Note that importing the package from NPM is not ideal. This is because the default setup for building widgets (with Rollup, if you copied that script) is to "bundle", which means to include the source code for every imported package except a few builtin ones (notably react and @leanprover/infoview) verbatim in the output file. @leanprover-community/proofwidgets4 is not builtin, so every widget that imports it would result in another copy stored in memory. This is not a big deal in practice as this particular package is small, but it obviously does not scale, and importantly may break packages that rely on any kind of global state. My intended solution to this is to let the Lean server work as a kind of tiny CDN, where widget modules can import other widget modules. Something like

@[widget_module]
def ProofWidgets4 : Lean.Widget.Module := ...

@[widget_module]
def otherWidget : Lean.Widget.Module where
  javascript := "
    import * as pw4 from 'ProofWidgets4'
  "

I started an experimental implementation in vscode-lean4#557. It allows importing widget modules by hash only which is unambiguous but pretty awkward. A more ergonomic scheme would support more readable names for modules, as discussed in the docstring there.

Any feedback or testing is welcome.