I agree that the -scripts and -seed repos could be merged into one repo. 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.
On Sat, Sep 30, 2023 at 7:18 AM Mario Carneiro <[email protected]> wrote: > 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 <[email protected]> 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 [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 >> <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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsn1P-uZLnYhCzE%3DkGQErhcYvcAV%2BoAscSSiaq-%3D3u_sQ%40mail.gmail.com.
