Re: [Metamath] Update: website generation rewrite

Another update: mm-web-rs now supports mmtheoremN.html generation. This was not really a bottleneck but it is the next largest cost, taking around 10 seconds in metamath-exe, which is a small fraction of the overall build cost but is still much slower than mm-web-rs can do. It takes about 600ms

Re: [Metamath] Update: website generation rewrite

On Saturday, September 30, 2023 at 11:12:48 PM UTC+2 di@gmail.com wrote: the other thing is that dealing with files hosted on set.mm repo is a bit of a mess because it is so jumbled and flat. We have to cherry pick which files go in mpegif, which are for ilegif and which are for nfegif.

Re: [Metamath] Update: website generation rewrite

the other thing is that dealing with files hosted on set.mm repo is a bit of a mess because it is so jumbled and flat. We have to cherry pick which files go in mpegif, which are for ilegif and which are for nfegif. Putting things in folders will make the script a lot simpler, and would make me

Re: [Metamath] Update: website generation rewrite

There is very little code involved in keeping a file somewhere else, there is just one cp line in the script. So I'm fine if we want to make an exception for certain files. But currently it's not clear that this is what is happening, and yet there is a lot of inconsistency, for example

Re: [Metamath] Update: website generation rewrite

On 9/30/23 04:27, Mario Carneiro wrote: 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,

Re: [Metamath] Update: website generation rewrite

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

Re: [Metamath] Update: website generation rewrite

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

Re: [Metamath] Update: website generation rewrite

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 wrote: > Thanks for the website generation work, and the

Re: [Metamath] Update: website generation rewrite

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

Re: [Metamath] Update: website generation rewrite

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

Re: [Metamath] Update: website generation rewrite

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

[Metamath] Update: website generation rewrite

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