Just to correct something (I am often mistaken, please correct me when I am) : Javascript/Webview may be bypassed with some a big amount of work, just not so herculean)...
Rendering math correctly and interacting with it is the main reason why I am stucking with a WebView/Javascript. After a bit more of thoughts, making that happen on something other than a WebView is possible but would require : 1) drawing on a canva/FrameBuffer 2) porting one input processor (the TeX input processor?) and the svg output processor/Jax of MathJax to another language (C ?) 3) writing a simple rectangular widget that is able to display the subset of svg that the output processor of MathJax use (mostly paths apparently) and to tally the bounding box of those paths/elements Doing that would be a HUGE benefit, resource and performance wise (the more demanding part would be 2) As well as allow everyone, everywhere to display/use maths Sounds like a very interesting project to me.... Sadly I do not have enough time to do that, now. :) Because that is the kind of fun and hard project that I just love indulging in ^^ Well, who knows, maybee in 3 years... :) Also. An authoring tool for maths that write proofs in metamaths/mm0 somewhat make it into an authoring tool for metamath/mm0 too... (but an imperfect one, as metamathiciens are concerned with the length of proofs and I do not yet see how Mephistolus could help with that. Mephistolus could complement with mmj2 though to allow metamathematicians to do what mmj2 cannot and the opposite) Best regards, Olivier Le dimanche 5 janvier 2020 11:23:57 UTC+1, Olivier Binda a écrit : > > > > Le samedi 4 janvier 2020 18:28:18 UTC+1, Mario Carneiro a écrit : >> >> Looking at this from a green-field perspective, what should a web >> interface for metamath look like? >> > > I am also really really interested by the answer to this question. > Because I am trying to build one. > My prototype will have to be refactored/improved because, I am 100% sure > that I won't get it right on my first try. > > But If I had, at least partial answers to this question, my first try > would be much much better/closer to what is needed > > > >> >> * The metamath web pages are completely non-interactive, although they >> set the standard for proof visualization. I think things could be improved >> here if the page was rendered by JS, rather than shipping a bunch of giant >> html tags. >> * The "structured version" looks great but the frequent mathjax causes >> some significant performance problems. I am doubtful that this can be kept >> up in an interactive setting, so we would have to use more ascii. >> * If I recall correctly, Stefan O'Rear made a prototype web app that >> could load and display theorems from set.mm, but I don't think this >> project made it very far and in particular it was not interactive (allowing >> to write proofs, check individually, run tactics, save the results, etc). >> >> MathJax renders math beautifully and it is possible to make it > interactive, as I will demonstrate soon. > > >> Modern web browsers are definitely up to the task of running a metamath >> verifier in JS, but I don't know a really successful user interface that we >> could apply here. Some observations: >> >> > MathJax is the only thing on earth NOW that enables interactive and > beautifully rendered maths on a computer. > So, javascript (or typescript, or whatever is used to make MathJax work) > is not an option. You have to somehow use javascript to build a decent math > ui. > > (even if you port MathJax to another language, you'll still need the dom > and javascript...or you would need to rewrite the dom in your target > language, good luck with that, > or painfully port MathJax to another subsystem that the dom) > > On a side note, having to work with javascript opens a lot of > opportunities : > antlr/lucene/elastic search do have javascript ports > > So you could write a complete standalone Methamath with UI application in > javascript, > or in a language that is able to speak with a WebView (like java, kotlin, > c++...) > > > > >> * Opening set.mm in a text area is not an option. It's just too big to >> be displayed. More likely, the information has to be condensed into a proof >> listing and a per-proof editor "worksheet" view similar to mmj2. Are people >> happy with this approach? >> * Downloading set.mm directly (with caching) on page load and saving to >> the browser cache is possible, so the user experience could be just as >> "live" as the lean web editor ( >> https://leanprover-community.github.io/lean-web-editor/). >> * WebAssembly is a pretty good option for doing metamath processing >> without the overhead of JS, and I expect you can do full set.mm >> verification on the same order as metamath.exe with the right setup. >> >> Ultimately, I usually don't go for web apps because they are almost never >> the best tool for the job, once you've got serious about the task at hand, >> but for the newbie experience they are a big plus, and metamath's fast >> check time would translate to a pretty solid user experience, at least in >> principle. >> >> > The UI requirement for a UI for metamath are somewhat low > performance-wise: we do not need 60 fps at resolution 4K ^^ > > Javascript will do beautifully > >> Mario >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d900212f-df1e-4ba4-bd11-582e47a639ec%40googlegroups.com.
