On Sat, 4 Jan 2020 14:58:41 -0500, Mario Carneiro <[email protected]> wrote: > 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.
Metamath format is extremely easy to parse, I suspect it would be simplest just to use it as-is. > 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. That said, I think it *would* be awesome to have a useful "zero install" tool for creating Metamath proofs. It can be a pain to install tools; if users can skip that step entirely that's one less barrier to entry. There are now many ways to store nontrivial amounts of data from client-side JavaScript. Please allow me to make a few comments about UI. The big draw of *me* to mmj2 is that mmj2 lets people do proofs going backwards, proofs going forwards, and even speculative "in the middle" proofs of fragments or facts that might be useful later. Some tools force you to go backwards, and I find that to be a straightjacket. The big negative of mmj2 is that it doesn't support much in the way of tactics. Yes, it has a little automation built in, but it doesn't have a system where users can easily define tactics that build on other tactics that can then be invoked from the UI. I'm not sure how to integrate that into a text editor like interface, but it seems to be it'd be possible. E.g., some sort of escape like a leading "!" that switches modes. --- David A. Wheeler -- 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/E1ioJeV-0007xe-1K%40rmmprod07.runbox.
