On Sun, Jan 5, 2020 at 5:23 AM Olivier Binda <[email protected]> wrote:
> 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. > Actually, from what I understand, I think Mephistolus is attempting to address a slightly different problem than what I'm talking about. You are interested in a (visual?) front end for metamath that is geared to the teaching of mathematics itself (correct me if I am wrong), while I am talking about how to provide an interface for people writing metamath "code". Abstraction of the underlying representation helps a little bit in both cases, but hiding the textual representation away completely would not be a good idea if the point is to teach a newbie what metamath is, since then the skills don't transfer. * 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. > I'm sure it can. My main concern with use of mathjax is one of scale; mathjax rendering an average size metamath proof takes several seconds, which is over budget for an interactive editor. There are probably tricks you can play to improve this, but I see a difficult road here. 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. > This sentence makes no sense. MathJax is implemented in javascript, so of course you could do the same thing mathjax does with javascript. But again this shows our differing goals. For teaching math, sure, mathjax away, but for teaching metamath you probably want to introduce people to the ascii symbols that are used to represent expressions, because that's what appears in metamath files, and in all likelihood they will be typing these symbols when searching and writing proofs. (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) > WASM covers this. You can write the core program in any language that compiles to wasm and use JS hooks for interaction with the web browser. Of course the program needs to be aware that it is running in a browser to some extent so it throws up the right interface. > 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++...) > Right, that's the plan. 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 > Ha, you would be surprised how slow some frameworks can be. On Sun, Jan 5, 2020 at 7:24 AM vvs <[email protected]> wrote: > I am not sure that this is the right way to go, unless you want to convert >> the process of writing maths into the art of writing software, with >> features designed for software development but somehow adapted to maths. >> >> What about writing a standalone App DEDICATED to maths ? >> > If you think about it for a minute then you should realize that it's just > an old argument about GUI vs. CLI. Of course many people will prefer to > design some figure visually. And some powerful extensions can only be > written using programming languages. I think we need both. It is just > happens that creating a good visual UI is much harder than programming > languages. Also, I don't think that many CS students take an art lessons. > I don't think I have *ever* seen a practical visual programming language. They never graduate past the "toy" stage. (That said, an in-browser verifier will probably be a "toy", so perhaps it's not a bad match.) But for the purpose of acclimating newbies to the ecosystem, you want it to resemble the "real thing", so that skills transfer. So maybe it should be an mmj2 clone? 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/CAFXXJSuzjPVLeCGK03D5CQ3O10tUyu%2BLm%3DE3o4GiiqEV6ZsZrg%40mail.gmail.com.
