Another update: mm-web-rs now supports mmtheoremN.html generation. This was not really a bottleneck but it is the next largest cost, taking around 10 seconds in metamath-exe, which is a small fraction of the overall build cost but is still much slower than mm-web-rs can do. It takes about 600ms now.
Besides speed improvements, the main other thing I am focusing on in this rewrite is updating the HTML to use modern standards and pass the validators (for some reason we have a link to the validator in the footer of every theorem page but it hasn't passed in years). So far I'm just using inline and <head> CSS but once metamath-exe is off the critical path for the website generation it will be easier to move more of the CSS into a separate file (which will result in big space savings since it won't have to be duplicated 40000 times). Both kinds of autogenerated file are also supported in mm-web-rs's server mode, so you can also have a live version of the website without filling your disk. It supports multiple databases now with the same URL layout as us.metamath.org, although it doesn't know how to serve static files yet, so this could in principle be called by the metamath.org web server for files that are not precompiled. On Mon, Oct 2, 2023 at 7:42 PM Benoit <[email protected]> wrote: > On Saturday, September 30, 2023 at 11:12:48 PM UTC+2 [email protected] > wrote: > > the other thing is that dealing with files hosted on set.mm repo is a bit > of a mess because it is so jumbled and flat. We have to cherry pick which > files go in mpegif, which are for ilegif and which are for nfegif. Putting > things in folders will make the script a lot simpler, and would make me > more supportive of just moving all the database-specific files into set.mm > repo if that's what we want to do. > > > I lean toward a rule like: > * files associated with a given database go the metamath/set.mm > repository (which could be renamed metamath/databases -- github manages > repository aliases); > * files which are more general and "website-wide" go to the > metamath/website repository (which is the merging of the > metamath/metamath-website-seed and metamath/metamath-website-scripts > repositories). > > As for organizing the metamath/databases repository, I'm of course all for > it, having opened https://github.com/metamath/set.mm/issues/1887 and > https://github.com/metamath/set.mm/pull/3515. > > Benoît > > > > On Sat, Sep 30, 2023 at 5:08 PM Mario Carneiro <[email protected]> wrote: > > There is very little code involved in keeping a file somewhere else, there > is just one cp line in the script. So I'm fine if we want to make an > exception for certain files. But currently it's not clear that this is what > is happening, and yet there is a lot of inconsistency, for example > mmbiblio.raw.html is hosted on set.mm repo but IL's mmbiblio.raw.html is > in the seed repo. Some kind of general rule for where to look for files > would be appreciated, the simpler the better. > > On Sat, Sep 30, 2023 at 1:04 PM Jim Kingdon <[email protected]> wrote: > > On 9/30/23 04:27, Mario Carneiro wrote: > > Moreover, I am of the opinion that we should also move all the .html and > .raw.html files from set.mm repo to the website repo, even though those > files are more heavily trafficked than most other pages. When you want to > add a new page, you need to modify the website repo anyway because > otherwise it won't get copied correctly, and if it's living next to the > scripts then it will be easy to maintain .raw.html and the necessary > processing along with it. By comparison, there is very little "tandem > update" work involved in an .html file versus the .mm file - they can > generally be updated in any order, with the main issue being possible > broken links if the mm file links to the html file or vice versa before the > other has landed. > > I see the big issue as being the links from the html files to specific > theorem names or math syntax. If the web pages now in the set.mm repo are > moved, there would appear to be some kind of catch-22 in terms of which > repository would have to be updated first and how we could build automated > checks that the websites refer to valid syntax/theorems. > > In particular, mmil.raw.html changes very frequently and it is very much > tied to updates to iset.mm and set.mm. > > Adding a new page is rarer, so I'm not sure that's a huge consideration > (especially if we make the scripts better organized so we better understand > where we need to add it). > > I'm not saying I'm implacably opposed to any change but I'd tread > cautiously. On the whole I think the current organization has served us > well (I mean, in terms of which web pages are maintained where, not all the > details of how the scripts are written which hopefully we are already on > the path to improving quite aside from moving web page files around). > > > -- > 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/c2fd9098-cd27-4557-f5f3-a5a4041c2461%40panix.com > <https://groups.google.com/d/msgid/metamath/c2fd9098-cd27-4557-f5f3-a5a4041c2461%40panix.com?utm_medium=email&utm_source=footer> > . > > -- > 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/8667c6f4-e57f-4be4-aa0d-89f5ab64088an%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/8667c6f4-e57f-4be4-aa0d-89f5ab64088an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuB8M%3Dk7KWxPg3b-JSkDbH%2BKQx6jf0SvYdN_gkaPu2LOA%40mail.gmail.com.
