On Thu, Mar 2, 2023 at 5:37 PM David A. Wheeler <dwhee...@dwheeler.com> wrote:
> > > > 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. > > > > On Mar 2, 2023, at 4:33 PM, Mario Carneiro <di.g...@gmail.com> wrote: > > 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. > > That makes sense. I don't *object* to beautiful presentations, but if > that's unsolved, we could generally prefer pointing to the Unicode versions > (where long formulas are easily handled). > > MathJax is well aware of the need for automatic line breaking. They hope > to have s version 3 that resolves it: > https://docs.mathjax.org/en/latest/output/linebreaks.html > > https://stackoverflow.com/questions/40628064/mathjax-automatic-line-breaking-when-resizing > ... I'm fine with letting them solve the problem & we use their solution. > I don't know when they'll actually do that (if ever). > > > > > 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. > > Not *difficult*, but some are harder than others if we *dynamically* > generate. > In nginx you would typically specify a location pattern as a parameter, > and if it matches, > call a program (e.g., using fastcgi). Here's an example: > https://www.nginx.com/resources/wiki/start/topics/examples/fastcgiexample/ > > You'd *like* to have the web server directly serve static files (they're > good at that!), > but currently directories like "mpeuni" have a lot of files, some of which > might be dynamically generated > while others are probably statically generated. Typical websites put them > in separate directories, > to make it easy to tell them apart. > I'm fairly sure there is a way to set up an nginx config to do essentially the following: * On a request to /mpeuni/X.html: * If /var/www/mpeuni/X.html exists, serve that * Otherwise, call 'web-page-generator /mpeuni/X.html', save the result as /var/www/mpeuni/X.html (assuming it is not a 404) and serve it If they're all dynamically generated via the same program, or all > statically generated, then that's moot. > In this case 'web-page-generator' doesn't exactly have to be a single program, it can be a shell script or shim which calls out to multiple actual tools. It's basically another server behind the server, with nginx acting as a cache for it. It could handle a fairly wide range of different endpoints, including a mix of static and dynamic stuff. (Probably nginx can handle the static stuff though, assuming the relevant URLs can be easily described with globs.) > > 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. > > We could start with hard-coding, then move towards supporting a general > form. > I agree that in the long term we want to be general. > > I suspect type code coloring primarily useful to new users... but since we > *do* want to new users/readers, that's still relevant. We could even add it > later, but it also doesn't seem *that* hard to implement (at least > hard-coded). > Random coloring is another option to get an ok overall look (where the seed is something tied to the database itself or the typecode names so that it is stable enough for people to be able to use it as a consistent visual), or something based on the same rainbow spectrum used for the label numbers. It's definitely important for more than just new users, it is the only bit of color we use on metamath formulas which is an important aspect of visually breaking them up. It's the nearest thing we have to syntax highlighting. A $t command seems the most appropriate; there is already one that contains almost exactly this information: 'htmlvarcolor' shows the color *key* but does not actually contain the color mapping (so in theory they could diverge). htmlvarcolor '<SPAN CLASS=wff STYLE="color:blue;font-style:normal">wff</SPAN> ' + '<SPAN CLASS=setvar STYLE="color:red;font-style:normal">setvar</SPAN> ' + '<SPAN CLASS=class STYLE="color:#C3C;font-style:normal">class</SPAN>'; If this was instead htmlvarcolor "wff" as "blue"; htmlvarcolor "setvar" as "red"; htmlvarcolor "class" as "#C3C"; then we would be able to derive both the coloring on symbols and the color key from the same information (in addition to being able to validate that these are actually typecodes). Currently the coloring on symbols is baked into the 'althtmldef' for variable tokens. > 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. > > I can trivially create the name "experimental.metamath.org" (or whatever > you like), and point it somewhere. The real question is, where should it > point? > * It *could* point to the metamath.org site. It doesn't have a lot of > space for many more copies, and if you're not ready for it to get attacked > that'd be a bad thing. That requires no new money. > * You could set up a site literally anywhere else. A linode node costs > $6/month. Heroku has a low-cost plan (not free though). > I was thinking something more along the lines of metamath.org/experimental/foo.html. Wouldn't a new domain cost more? For experiments I don't think we need anything that has a huge space footprint. The main things would be pre-generated web pages and dynamic server tests (uncached). There is some potential for an experimental server to cause trouble or take down the site, but that's always going to be the case for any dynamic server option and anything we write for this purpose needs to be prepared for that from the start. The other reason to prefer doing this on metamath.org is to get practice for actually making these kinds of modifications. Most of the discussed changes would be rather similar to this. If you can create dev.metamath.org for free and point it to the same linode server, then I guess that's roughly isomorphic to metamath.org/experimental/ . Perhaps that's better for keeping things separate, although it still has be same "take down the server" risks. -- 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/CAFXXJStT0d_%3D0460xvu_nHXMEkfon0K%3D4-7yyV8x4uect85nQw%40mail.gmail.com.
