Add other Recharts chart formats

[mars0i]

It appears that at present ProofWidgets4 only provides the LineChart chart format. Other charts--at least ScatterPlot--would be useful.

(I might try adding this myself, if that might be OK, but I thought I'd create an issue for it first.)

[Vtec234]

Hi, and thanks for your interest! Recharts was initially added to ProofWidgets as a proof of concept. Now that ProofWidgets is more stable, and is included in mathlib, we have to carefully consider which JS libraries it bundles (see #19). Having used the Recharts integration recently, I am not very impressed by this particular library. The documentation is not the best, and some common tasks are weirdly difficult. For example, to plot multiple functions in one component, it seems one has to compute the union of their graphs manually (see e.g. here). I would be happy to be proven wrong, but if that's the case we might want to consider switching to another plotting library rather than developing the Recharts API more. One popular option (which we already bundle for GraphDisplay) seems to be d3, with Observable Plot on top.

[mars0i]

to plot multiple functions in one component, it seems one has to compute the union of their graphs manually
I didn't realize that. Wow. That would be a pain for the kind of plot I was working toward. I agree the docs are not great. I had to do a lot of trial and error.

I wasn't familiar with Recharts or Observable Plot before now. I started from Plot.lean based on what I saw in the Demos directory because I was trying to plot simple functions rather than graphs. But I see now that the Observable Plot examples include a lot of data plotting, so that's good. (Raw D3 seems good to have as an option for something unusual, but my experience has been that using D3 directly to go beyond the canned examples on the D3 site is a nightmare. Unless they've completely changed the API, but I don't see how--the problem was the core conceptual model.)

I've done a lot of work in the past with Vega-lite. You've probably considered it, but it might be another option. Popular, does a lot, and the docs are OK. The problem with the library, and the docs, is that there are so many options and layers, that it's a lot to work through if you don't use it often. I used it with Clojure because it was what Clojure data science people were building on.

[mars0i]

Observable Plots looks good. Maybe this issue should be closed, and I can open another one for plotting with Observable Plots.

[mars0i]

If at some point plotting from Observable Plots is added, should Demos/Plot.lean be renamed--maybe to Demo/Recharts.lean or something like that?