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 enable 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, kotloin, 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/55412a92-a612-43be-8f41-635a94f6d537%40googlegroups.com.
