Thanks for the website generation work, and the much needed simplification. I think further simplification, on many levels, would be achieved by dropping GIF support (as for the HTML generation, we could have the default be the current HTML/unicode, and the backup being HTML/plaintext, which simply displays the text in the source, with possibly some coloring as in the unicode case).
As for the repos, this would allow to delete https://github.com/metamath/symbols. I also think that the two repos metamath-website-script and metamath-website-seed be a single repo "website" (which I already proposed when I was informed of their creation). I don't see the need for this extra complexity. (Also, why prepend repositories in the project "metamath" with the prefix "metamath-" ?) Benoît On Saturday, September 30, 2023 at 11:02:40 AM UTC+2 [email protected] wrote: > Note that mm-web-rs also supports a "server" mode, where you can give it a > file and it will serve a live site without much precomputation. All it > needs is a live reload feature (i.e. it detects when you save the .mm file > and reloads) and you will get instant feedback (loading individual pages > takes milliseconds). I've also been contemplating just running this on the > server directly, so that we don't need to spend gigabytes of space on all > the precomputed HTML files if it is comparably fast to just compute them on > the spot. > > On Sat, Sep 30, 2023 at 3:04 AM Jim Kingdon <[email protected]> wrote: > >> On 9/29/23 21:52, Mario Carneiro wrote: >> >> > in my test these are 4893.94 s and 5020.87 s respectively (that is, >> > 2h45m total). I just got the new version working, and it takes 10.8 s >> > and 11.1 s respectively >> >> Exciting stuff! >> >> This has me pondering various possibilities, such as generating the >> whole site on my machine (because I'm often proving where I don't have >> good internet) rather than just one page at a time as I have been doing. >> >> >> -- >> 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/a1613087-36e4-a936-0641-e935315cedda%40panix.com >> . >> > -- 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/81baa742-493d-457a-9f5b-bb4d26498153n%40googlegroups.com.
