On Sat, Jan 4, 2020 at 1:36 PM vvs <[email protected]> wrote: > 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. >
I haven't heard of any issue like this, although admittedly I haven't touched a 32-bit machine in a long time. VSCode is an electron application, which means that it is pretty portable, and it runs on all major platforms. But the web isn't one of those, and Monaco ( https://github.com/microsoft/monaco-editor) is the "web version" of VSCode (it uses the same back end code IIRC but the actual interface is a bit different and not nearly as feature-rich). Really, anything that is LSP compatible would work just as well, but I have learned my lesson from mmj2 never to attempt to write a text editor because it will eat your life. (And now I'm curious if Raph Levien concurs :) ) 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. > The main reason lean is slow in JS is because it was not really designed to run like that. It's a giant C++ app that was just run through emscripten, and I have doubts about the number of layers involved to make things happen. I am confident that a text editor + metamath web app would be bottlenecked on the text editor, not the metamath (which is pure compute and so translates well to wasm). 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? > Microsoft funding... > 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. > I agree, although JS has improved a lot in recent years it's not really a language I would choose to program in. But wasm has opened the field a lot here for writing programs in your language of choice, as well as the bevy of JS-transpilable languages, so JS isn't your only option on the web anymore, practically speaking. On Sat, Jan 4, 2020 at 1:36 PM Thierry Arnoux <[email protected]> wrote: > On 04/01/2020 18:28, Mario Carneiro wrote: > > * 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). > > Here is a link to Stefan's Web test. It would be interesting if someone > tried it out. I assume it would be a very good starting point for a > possible JS assistant. > > https://github.com/sorear/smm/tree/master/webtest > Ah, thanks I couldn't find the link. > From the README, it seems it provides commands available to the javascript > console, so it certainly provides a good back-end. What would need to be > filled-in is a front-end (displaying formulas, etc.) > > In order to load an assistant, it should not be required to load the full > set.mm, including comments and proofs. Definitions and statements would > be enough, and whatever that input file is, it shall be cached so that next > time the user loads it, a local copy is used. > I thought about serving pre-parsed metamath files in e.g. JSON, but metamath is already pretty easy to parse, so there might not even be that much to gain through transforming the data. I know that SMM3 was able to verify faster than download time (although I don't think it was designed to work on streaming input), so conceivably this can be done with close to zero overhead. (Also, I think 30 MB or whatever we're up to now is something like the size of the average web page by now so I think we won't be noticed. :P ) On Sat, Jan 4, 2020 at 1:50 PM Jim Kingdon <[email protected]> wrote: > On 1/4/20 9:28 AM, Mario Carneiro wrote: > > > 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 think your instinct is sound in terms of being skeptical about the > value of building a whole IDE inside a web browser. Not impossible, just > not clearly a win over making sure that Visual Studio Code (and anything > else using a language server, like NeoVIM) works well. And a lot of work > to even get to the point of "is this something I or others would want to > use?" > Right, this is the main draw of "try it online" web apps: they lower the barrier to entry. Probably set.mm isn't even necessary for this purpose, since here you are mostly doing toy examples and a reduced or axioms-only set.mm would be an easy way to provide a decent standard library without much else. There is a potential integration with editors/IDEs in terms of "I hit > save, and my web browser reloads a proof view - generally similar to > SHOW STATEMENT/ALT_HTML - with my changes. That's inspired by how tools > like webpack work for writing web apps (for example, those using React). > Perhaps the biggest obstacle which springs to mind is how well the tools > handle partly written proofs or proofs with errors. > I still don't really understand what the GMFF option in mmj2 does (or what GMFF stands for), but I recall it doing something similar to this; it would render your current worksheet in a web browser with the gif images and you could write and they would live-update. On Sat, Jan 4, 2020 at 2:31 PM Jon P <[email protected]> wrote: > I've thought a bit about a web editor and I really like the idea. It makes > distribution of the tool effortless. Here's a few things. > > Firstly for me I think the most enduring challenge of metamath is finding > theorems in the database to use them in proofs. I had a go at making a > search engine but that didn't go so well. I like how Milpgame is laid out > with all the theorems down the left hand side. I think in my imaginary > ideal tool that would be something which was central, easy ways to search > the database with common theorems in a palette maybe and even suggested > theorems to use next if that is possible. > Common theorems in a palette is an interesting idea. In particular, I wonder if theorems sorted by number of uses (say, the top 20 theorems) would make a useful "propositional logic toolbox" for doing all the in between work. Of course that's only half of the work, the other half is finding relevant theorems for your goal, and I have always used metamath.exe's "search" command for this. It's a very simple mechanism, essentially text search with a tiny bit of regex, but it's enough to find all theorems about a particular constant or an algebraic manipulation theorem. Secondly I had a look at making a frontend and came across Quill > <https://quilljs.com/>, you can see how in maybe 10 lines > <https://quilljs.com/playground/> you can add a text editor to a webpage > so I think the frontend would be relatively easy. > I think that text editors is one area that is very well trodden by the larger programming community, so I have little doubt that there is something suitable (and likely many things), so I'm not giving it that much thought. The main question is if you can get the desired interaction mode to work with the library. Thirdly I recently came across literate programming > <https://en.wikipedia.org/wiki/Literate_programming> for the first time. > I think it's a really interesting idea and immediately made me think of > metamath. If it were possible to write proofs in natural language and then > have macros replace the natural language with mm steps I think that could > be a really powerful way of bridging the gap between beginners and > experienced users. It's also interesting how it only uses substitutions > which is very in line with how metamath works. It might also really help > with constructing a proof, that's generally how I try to do things, to > write down the ideas first and then fill in the details after. > Patrick Massot has done something similar with lean: https://www.math.u-psud.fr/~pmassot/lean/ . (Click on the lines of proof to see the tactic line that corresponds to it, with buttons on each side to show how the state changes.) > I even had some crazy thought about trying to auto generate natural > language explanations of proofs from existing proofs, however that was > probably just a flight of fancy. > It's not completely crazy: I am reminded of the Ganesalingam / Gowers prover (https://arxiv.org/abs/1309.4501), which produces plausible natural language proofs for statements about metric spaces. However, this prover is finding its own proofs, so it's not quite the same as processing existing proofs, which can use a much broader range of theorems, each having a complex "gloss" in terms of a deduction style argument. 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/CAFXXJSueH0T6MOS5XFa4aPQ5gpFMntSHgVgqo13V_nJn%2B%3D%2BKFg%40mail.gmail.com.
