I don't think we should delete the symbols repo. Those GIFs are the result of Norm's hard work, and they stand alone as a project. See https://us.metamath.org/symbols/symbols.html for more context.
On Sat, Sep 30, 2023 at 7:12 AM Benoit <benoit.ju...@gmail.com> wrote: > 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 di....@gmail.com > 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 <kin...@panix.com> 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 metamath+u...@googlegroups.com. >>> 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/81baa742-493d-457a-9f5b-bb4d26498153n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/81baa742-493d-457a-9f5b-bb4d26498153n%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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvRkBqNtVJf8y%3DjjNZ6bkZ44YKk7pC7TTbfCNqfS6FRGQ%40mail.gmail.com.
