Hi All, This is inspired by the George Hotz thread to some extent but also my own work on MM0 and such. What would be a good user experience for writing metamath theorems in a web application? For example, MM0 currently works via a language server (written in Haskell, with a new LSP server written in Rust on the way) connected to the VSCode editor, and this could be pretty easily ported to a web application using Monaco and emscripten, if I haven't misunderstood the state of the art here. But would that meet peoples' needs? I don't know whether there is a similar push-button way to get the mmj2 java application on the web, but again, it needs a UI rethink even assuming that works.
Looking at this from a green-field perspective, what should a web interface for metamath look like? Related work: * 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). 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: * 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. 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/CAFXXJSsA%2BA2QpokTwgYJRrta1hjZadaOG21mq0h7P1N4qKUEnA%40mail.gmail.com.
