On Saturday, September 30, 2023 at 1:18:42 PM UTC+2 [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.


Oh, I agree. I misread the purpose of that repo.

Benoît


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/47701494-65a9-40c0-9350-109497f3025cn%40googlegroups.com.

Reply via email to