Publish @lean4/infoview to npm

[EdAyers]

A prerequisite for leanprover/lean4#1238 is to have the ./lean4-infoview folder to be published on npm, so that widget code can reference it. This is useful for allowing users to reuse infoview components such as the tagged expression renderer.

We can use external libraries so that the infoview doesn't have to dynamically load copies of itself, but having it in npm means that people can target it and not have typescript errors while they are building user-widget bundles.

Perhaps this could be automated so that each release of vscode-lean4 includes a release of @lean4/infoview on npm?

[lovettchris]

The infoview depends on the following:

"dependencies": {
"@lean4/infoview-api": "^0.1.0",
"@vscode/codicons": "0.0.28",
"react-fast-compare": "^3.2.0",
"tachyons": "^4.12.0",
"vscode-languageserver-protocol": "^3.17.0-next"
}

I wonder if widgets really want to depend on all these things, indirectly. Perhaps what we need instead is an "infoview-react" package that contains just fully reusable handy react components like InteractiveMessage to display MessageData opening up all of infoview to widgets for reuse will make it almost impossible to do anything significant in InfoView from here on out or perhaps we add some react component factories to lean4/infoview-api so that when you are running in VSCode the widgets get the vscode versions of these react components...? Does react have any "component interface" like concepts? There's a ton of exported functions that I'd want to pare down to a minimum for support reasons:

Also do we only support Typescript, or can it also be used by pure Javascript widget implementations? Do we need to support both React classes and React hooks? These seem to be the sorts of things react component developers talk about in their libraries...

Then there's testing, do we have the infoview running in other editors yet? How do things like dependencies on vscode provided CSS work out? Should the infoview be checked to create some abstraction layer there isolating those sorts of vscode only dependencies, then test that the infoview works standalone in a web browser or something...?

[EdAyers]

I think having a @lean4/infoview-components library is a good idea but I don't think we are ready to start abstracting things.
Currently the interface is "whatever is exported from lean4-infoview/src/components.tsx in the widgets-pr branch". This is release 0.1 and we aren't making any support commitments. In particular, we have a warning here, where we explicitly say breaking changes are to be expected. To begin thinking about stabilizing the API, we will need to have more examples of widgets that use it so that we can decide what to stabilize.

The lean4-infoview package and dependencies won't actually be bundled with the user-widgets, because it will be marked as an external dependency in the user-widget's bundler. So the dependencies are not duplicated or cluttering up the user-widget bundle. This will cause breaking changes if we change the code, but we can think about stabilising later.

I think all of the npm dependencies of @lean4/infoview are necessary for the functioning of the components that we wish to give to user-widget developers:
The list of unavoidable dependencies are:

• react-popper (which should be a dependency, not a dev dependency) is needed to make the tooltips appear. I think this should be replaced with floating-ui or perhaps dependency injection for tooltips.
• react-fast-compare is used for some non-standard event management that I don't understand, but it seems to be present in the tooltips so I don't think we can get around depending on it without a big refactor.
• @lean4/infoview-api is needed for RPC.
• vscode-languageserver-protocol  is not a VSCode-only dependency, it just has a bad name. Actually it's a standalone LSP implementation.

So the only deps that we would save from having an extracted lean4-infoview-components library are tachyons (that we are going to remove anyway) and the vscode icons. Maybe we could just set the vscode-icons and tachyons packages to be dev-dependencies.

Also do we only support Typescript, or can it also be used by pure Javascript widget implementations?

If it's packaged correctly it should support both typescript and javascript fine.

Do we need to support both React classes and React hooks?

I think everyone uses hooks these days. There are no breaking compatibility issues between hooks and classes as far as I can tell.

Then there's testing,

I guess tests would live in the root vscode-lean4/tests folder as they currently are.

How do things like dependencies on vscode provided CSS work out?

You just get whatever CSS is loaded in the infoview, there is no attempt to manage this. Maybe in the future, once tachyons is gone, we can start thinking about how to manage this properly.

Should the infoview be checked to create some abstraction layer there isolating those sorts of vscode only dependencies, then test that the infoview works standalone in a web browser or something...?

The only vscode-only dependencies are the codicons which are purely aesthetic, the infoview is usable from within other editors in theory.

[Vtec234]

We now have @leanprover/infoview on NPM. It is a very early version and breaking changes are to be expected. I am guessing it will take until after the official stable release of Lean 4 to stabilize.