On November 27, 2020 12:14:09 AM EST, Mario Carneiro <[email protected]> wrote: >Hi All, > >I've just put the finishing touches on the mm0-rs HTML generator, which >makes pages such as >https://digama0.github.io/mm0/peano/thms/addass.html . >As should be pretty obvious, it's based on the metamath web page >display, >but I would like to make it a bit more interactive, possibly involving >doing more verification work directly in JS. What do people want to see >from a more "live" version of the web pages? Search seems like an >important >one, and step folding is also an option although I don't know how to make >that not annoying.
If it can be done easily without JavaScript, you should do it that way instead. It's generally faster do to it that way, and it'd be nice to have some functionality work when client-side JavaScript is disabled. There are obviously diminishing returns where that doesn't make sense. Basic text search is already built into browsers; I don't know if people need more than that for searching. Step expansion could be implemented using thr HTML details tag. > Another thing that is somewhat important for MM0 is >"expr-folding", where subexpressions that are used in many contiguous >steps >(like the proof context) are abbreviated. MM/MM0 like to work with such >expressions as they can be unified in constant time, but the standard >metamath proof display format makes this look very repetitive (and it >is >also expensive to print), suggesting that somehow the print isn't >capturing >"the essence of the proof" because it appears to be more repetitive >than is. A fair point. The metamath proof display has this problem also. In some texts you would show at the beginning some definitions to make notation simpler, followed by the text that uses it. Perhaps you could automatically detect sequences of symbols of a certain length that get reused more than a certain number of times, give them special symbols, and put them at the top as shorthand definitions. E.g., $1, $2, and so on. Each list would be local to a particular theorem. They could even other shorthand definitions. I don't know if that would actually help, but I'm throwing it out there as an idea. >Also, the web pages could benefit from some design work (I did my best >but >it's not my forte), and it also probably lacks some essential >components >like a nav bar or something like it. The current design is pleasantly >minimalistic but maybe some important elements are missing, so some >votes >on the most pressing issues would help. --- 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/FD80E50D-FDB9-40F6-9C59-D89AA163C7F4%40dwheeler.com.
