> > 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? >
The most obvious advantage would be portability from a user's point of view. But does it really holds? As far as I know VSCode used native libraries and presently supports only 64-bit CPU. For that reason I was forced to use Emacs mode for Lean which I won't regret by the way. 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. > Again, there were attempts to use web sockets to interface with a local language server here: https://observablehq.com/@bryangingechen/lean-websocketd Certainly Lean is slow in JS, but how much better Metamath will look in browser remains yet to be seen. * 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. > That looks like an interesting idea if there is a good tools support. 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. > I will agree here. Besides, having a web editor available creates a more "mature" impression. Why Lean (with origin from just 2013) has it while Metamath has not? Though, I know that there are much more active community (and experienced developers) around Lean. Probably not least because having a parsed language is more appealing to programmers? And having a web UI enables someone to create a web tutorial at some point. Also, some people would say that JS itself is not a pretty language and is oriented towards web designers and not professional software developers. But I'm pretty sure that nobody would beat that click and forget experience when it comes to people who are curious about logic and proofs but not CS per se. -- 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/3c933ba7-1502-4747-8788-08e438a85d9b%40googlegroups.com.
