On Thu, Mar 2, 2023 at 12:53 PM David A. Wheeler <dwhee...@dwheeler.com> wrote:
> 2. The text just runs off to the right, instead of going over multiple > lines, making long ones unreadable. That's important but easy for the > non-MathML case (just a little CSS), though I don't know how hard that is > for MathML/MathJax. > This is a pretty fundamental problem with MathJax style displays, and I don't have a good solution. LaTeX generally isn't great about automatic line breaking inside mathematics, but metamath routinely involves very large formulas, so although this looks good for the mid-sized examples the large ones really suffer. A related issue is that mathjax isn't really able to cope with having thousands of large and complex formulas on a page and the CPU time / draw time really spikes on some of the examples. For MM0 I'm planning to mostly just sidestep this issue by using ASCII-first displays, perhaps using unicode or programming fonts with ligatures but not much more. That way line breaking is limited to just pretty printing which can feasibly be written with a handcrafted JS library. > 3. I think it's important we support existing URLs. That's easy with > pregeneration, just rename to taste. If this is dynamically generated, that > would require some changes to support the .html endings *and* support > returning static pages. > I don't think this will be difficult no matter what we do, since we can set up all the necessary routing in nginx. I am not above potentially making mpegif redirect to mpeuni though (or a future URL scheme), or serving only dynamic pages for deprecated formats. I think we should try to make https://us.metamath.org/mpeuni/areacirc.html link to a theorem about the area of a circle in perpetuity but not necessarily serving exactly the same HTML as it does today. > 4. This one omits many of the capabilities of the metamath-exe generator, > e.g., compare with <https://us.metamath.org/mpeuni/areacirc.html>. That > includes: > Distinct variable group: 𝑥,𝑦,𝑅 > Allowed substitution hints: 𝑆(𝑥,𝑦) > Colors of variables (off, setvar, class) ... this one isn't as important > to me & would be a lot of work, so I'm not fussy there. > Syntax hints (with links to them) > List of axioms used (with links) > List of definitions used (with links) > List of theorems that reference it (with links) > By the way (and I realize this wasn't directed at both tools), mm-web-rs was designed explicitly as a carbon copy replacement for metamath-exe generation, and supports all of these things. (Thierry's generator as I understand it is more of an exploration of what we could have if we break with the traditional format.) IIRC if you open them in a browser side by side the result is identical except for distinct variable groups, which use a different (arguably better) heuristic for collecting $d pairs into cliques. (Exact clique cover is an NP hard problem, though, so some amount of approximation is required.) I think the variable coloring heuristic uses some hard-coded typecode names so it is not suitable for general databases; there are actually quite a few aspects of the web site generator that are tailored for set.mm which should probably use $t commands instead. I would link an example here, but I'm not sure where to host it. On that note, we might consider a place on the main website for experimental stuff now that us2 is down. Do you know if there is a spot which already works for this? I'm thinking of some place where it is safe to just drop files and have them persisted across website builds, with a URL that implies that they may go offline at any time. -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuQVq2bW3G8uqoAXcpZhE8_jrdGi0meL_zgPKsH%3DCUcKw%40mail.gmail.com.
