Html pages don't work

[GinoGiotto]

This problem seems to hold for all theorems in the database, below I show an example with bezout.

From https://us.metamath.org/mpeuni/bezout.html
I click structured version on the top right.

This links to http://metamath.tirix.org/bezout.html

Which shows a 404. Some days ago it worked fine, since I showed it as example in the mailing list. So maybe now it doesn't work because of the transition to https instead of http?

[tirix]

Oh, I'm sorry I should have mentioned it.

It's not because of the transition to https instead of http, but sadly because I had to make space on the server.

These html files were generated not with metamath-web, but with metamath-exe, with code from the PR metamath/metamath-exe#9.
[That PR was providing the capability to generate "structured typesetting" HTML files using metamath-exe, but a major refactoring of metamath-exe's code was started just before I was allowed to merge. I then unfortunately kind of gave up on trying to keep up with the changes done in the main branch.]

Unlike with metamath-web, the files were pre-rendered and stored on the server.
One problem with those files is that they are more than an order of magnitude larger than the normal unicode version, because every formula is expanded in SVG (it was a request at that time that there is no waiting time until the MathML is rendered, so I pre-rendered server-side all formulas).

The result is that the directory took up 12Gb of space on the server, and there was simply no space left for compiling and running metamath-web.

The simplest way to fix this would be to have the "structured version" links link to the new version (just adding mpeuni in the URL), rather than the previous version.
If the page layout is an issue, I could probably find a way to revert the templates in metamath-web to the original tables, fonts, and colors.
Otherwise I would need to upgrade the server behind metamath.tirix.org...
Of course ideally (in my point of view) the PR would be merged, that is, the functionality would be added to metamath-exe, and everything would be rendered on the official server - but that only shifts the space problem to someone else :-)

[GinoGiotto]

Now that the old STS pages have been replaced, and considering that metamath/metamath-exe#9 will probably not be merged, what's your direction for the future? These are the scenarios that came up in my mind:

1. Give up on the old pages and focus metamath-web.

2. Integrate some features of the old STS pages in metamath-web, such as the ability to collapse/expand proofs or display axiom dependencies and list of uses.

3. Reworking the old STS pages without metamath-exe and merging them in the official website. There would still be the problem of 12GB of space. Would the new 400x faster generation eliminate the need to pre-render pages?

[GinoGiotto]

If the page layout is an issue, I could probably find a way to revert the templates in metamath-web to the original tables, fonts, and colors.

I think the layouts of both metamath-web and the STS pages are aesthetically pleasing, so I personally don't have strong opinions on that.

[tirix]

Thanks to metamath/set.mm#3611, I could update the pages to the latest version of set.mm.
I've setup a cron to launch this update every day, I'll check that it works correctly tomorrow.

[GinoGiotto]

Thanks to metamath/set.mm#3611, I could update the pages to the latest version of set.mm.
I've setup a cron to launch this update every day, I'll check that it works correctly tomorrow.

Nice! I think once it's confirmed that it's working properly, this issue can be closed.

[tirix]

It looks good on my end, the script was run every day and the latest set.mm was pulled and is displayed.

There is a downtime of a few seconds for parsing the database, so I think I could even update a few times a day without this downtime being much noticeable.

[GinoGiotto]

There is a downtime of a few seconds for parsing the database, so I think I could even update a few times a day without this downtime being much noticeable.

Once a day or a few times a day are both fine for me, feel free to do what you think it's best.