For those who aren't aware, I've been working on a rewrite of the website
generation code. The main PR is
https://github.com/metamath/metamath-website-scripts/pull/16 , with links
to other parts of the process. I wanted to share another milestone: I'm
also writing https://github.com/digama0/mm-web-rs/ as a rewrite-it-in-rust
alternative to the metamath.exe theorem generation code. The most expensive
part of the website generation is the theorem files (GIF and unicode) for
set.mm, 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, a phenomenal 452x improvement over the original. This
is multithreaded, but it is still only 18s + 17.3s single-threaded, so this
still makes a huge difference even if the machine is single-threaded (I
think it is).

-- 
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/CAFXXJSveh%3DEeqHKFBa6tFexeB-quA%3D3AaDo-DP1xxbBiripu_g%40mail.gmail.com.

Reply via email to