> On Nov 27, 2020, at 1:26 PM, Mario Carneiro <[email protected]> wrote: > > > > On Fri, Nov 27, 2020 at 1:17 AM David A. Wheeler <[email protected] > <mailto:[email protected]>> wrote: > On November 27, 2020 12:14:09 AM EST, Mario Carneiro <[email protected] > <mailto:[email protected]>> wrote: > 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. > > I'm not fussed about the technology used to achieve it, but my point is that > if you use step folding you will be clicking on unfold icons all day to get > through a 200 step proof. MM0 has a heavy linear sequence due to its use of @ > , so perhaps we can fold steps off that linear path; the parenthesis nesting > is usually only 3 or 4 (and often lower) except in some highly automated > proofs, while the actual step depth increases linearly with the proof size > (so it could be 20 or 30 for an average proof).
I doubt there’s a “perfect heuristic” for step folding, but I imagine there’s a point at which there’s “too much” step folding. You could impose a maximum depth of folding before you just “show the rest” instead of using more folding. You could also have a button that “shows all steps” that’s implemented with JavaScript. Users without JavaScript can still see the proof, and users with JavaScript (most of them) can easily see everything. > Basic text search is already built into browsers; I don't know if people need > more than that for searching. > > No? I use metamath's search function all the time when the web site can't > help, and I guess URLs pretty often when metamath is not on hand. I'm talking > about finding *theorems*, not steps. And anything with a fancy unification > search isn't going to be usable with just browser search. Granted, the index > page can probably be text-searched, but I doubt it will stay as one page > forever; I think there are over 200 mmtheorems*.html pages. Sorry, from the step folding I thought you were still talking about *one* proof. Yes, searching for theorems is of course useful. > My idea is that the user selects a target step and a "width" (a configurable > constant, say 10), and then all subexpressions that are not "destructured" in > the steps which are less than distance 10 from the chosen point along the > graph are abbreviated. (In other words, this is what you would get if you > wrote all those steps in mmj2 without the formulas and let it find them by > unification.) If you consider all the steps, you probably won't get any > abbreviations, but the more "local" you make it the more aggressively it will > shrink terms. This will require the pretty printer to be in JS, though. Interesting. I suspect both approaches have value. If you’re focusing on a *specific* step, then I can imaging that could be helpful, If you’re looking at the “proof as a whole” then I still think that defining certain common repeating constructs might be really helpful in making a proof easier to follow. It’s probably impossible to be sure without trying it out, since we’re talking about “what is easier for humans to process”? --- 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/EBC2AA5E-BEDF-49D0-9798-3858D22C3F4E%40dwheeler.com.
