Infoview-based demos

[0art0]

This PR adds a few more demos to the ProofWidgets/Demos folder, including:

• Commands #web and #browse for using the infoview as a browser
• A (shallow) interface with the Plotly JavaScript library for generating interactive plots in the infoview

[Vtec234]

Hi! Thanks for your contribution, and sorry to take so long to get to it. I see also that you have been doing cool things with it in 0art0/lean-slides :)

I can see two parts in this PR: Plotly integration and the #web command.

• For the #web command, we shouldn't have to write all that meta code. It should just be a macro! After trying it I realized it wasn't quite working, but I made it work now and PR'd a demo with you as coauthor at feat: macro demo #21. If you're happy with that, let's merge that one instead.
• As for Plotly, unfortunately I am not sure we should merge it. It is a worry for the distribution size. I just described the problem in issue Don't include demo widgets in release archive #19. Adding Plotly would bump the archive from 7M to 12M - still not much, but sizes add up. It would be awesome if you were interested in resolving that issue!

[0art0]

Thanks for taking the time to review this. I wasn't aware of the mkCanonical trick, I think it looks a lot neater as a macro! I'm happy merging #21 instead of this one. I have added a few minor helper functions to the demo in #22.

I agree about Plotly; I suppose it would be better to develop a separate Lean 4 plotting library which uses Components to expose the Plotly API from within Lean. Rendering plots using #html may become impractical for large datasets, so ideally this should include an option to write the plots to a file too.

I would be interested in contributing to improving archiving and adding lake conveniences. I probably won't be able to get to it right away, but I'd like to take a look at it in, say, a month's time and see if I can help!