Metamath Proof Explorer web pages missing

[jkingdon]

For example, http://at.metamath.org/mpeuni/ax-5.html shows the correct page but https://us.metamath.org/mpeuni/ax-5.html shows a 404 error. As far as I noticed all the Intuitionistic Logic Explorer pages were unaffected (for example, https://us.metamath.org/ileuni/mmtheorems.html is fine).

Perhaps we ran out of disk space again or something?

[benjub]

Looks like the whole https://us.metamath.org/mpeuni/ and https://us.metamath.org/mpegif/ give 404 errors ? That looks pretty bad. If we need to make space fast, then we can remove all the GIF images (the webpages would still display the "ALT" attributes of the GIFs).

[digama0]

I took a look at the install log, the copy of set.mm that the server was using is cut off in the middle of a proof so metamath.exe failed to start or produce any web pages. I'm not sure yet what caused that.

[digama0]

I don't think the cause is a lack of disk space this time, we are at only 8GB / 26GB on the server. If I had to guess it was an internet interruption during the download, possibly related to the github outage reported in the other issue.

[digama0]

I'm currently running / monitoring the website generation script. So far it looks like everything is working, so it might just be a temporary issue which will be fixed when the script finishes now, or in the next nightly.

[digama0]

It looks like metamath.exe got killed in the middle of processing:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read '../metamath/set.mm'
Reading source file "../metamath/set.mm"... 42816545 bytes
42816545 bytes were read into the source buffer.
The source has 203383 statements; 2714 are $a and 40578 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> markup mmset.raw.html mmset.html /html /symbols /css /labels
Reading definitions from $t statement of ../metamath/set.mm...
1642 typesetting statements were read from "../metamath/set.mm".
Reading "mmset.raw.html"...
Creating "mmset.html"...
MM> markup mmcomplex.raw.html mmcomplex.html /html /symbols /css /labels
Reading "mmcomplex.raw.html"...
Creating "mmcomplex.html"...
MM> markup mmdeduction.raw.html mmdeduction.html /html /symbols /css /labels
Reading "mmdeduction.raw.html"...
Creating "mmdeduction.html"...
MM> markup mmnatded.raw.html mmnatded.html /html /symbols /css /labels
Reading "mmnatded.raw.html"...
Creating "mmnatded.html"...
MM> markup mmzfcnd.raw.html mmzfcnd.html /html /symbols /css /labels
Reading "mmzfcnd.raw.html"...
Creating "mmzfcnd.html"...
MM> markup mmfrege.raw.html mmfrege.html /html /symbols /css /labels
Reading "mmfrege.raw.html"...
Creating "mmfrege.html"...
MM> show statement */html/time
Creating HTML file "mmascii.html"...
Creating HTML file "mmtheoremsall.html"...
Creating HTML file "mmdefinitions.html"...
Creating HTML file "a1ii.html"...
SHOW STATEMENT run time =   0.03 sec for "a1ii.html"

[snip]

SHOW STATEMENT run time =   1.51 sec for "cnmptk1.html"
Creating HTML file "cnmpt1k.html"...
SHOW STATEMENT run time =   1.89 sec for "cnmpt1k.html"
Creating HTML file "cnmptkk.html"...
SHOW STATEMENT run time =   3.00 sec for "cnmptkk.html"
Creating HTML file "xkofvcn.html"...
SHOW STATEMENT run time =   2.75 sec for "xkofvcn.html"
Creating HTML file "cnmptk1p.html"...
SHOW STATEMENT run time =   1.17 sec for "cnmptk1p.html"
Creating HTML file "cnmptk2.html"...
Killed

This occurs again in the mpegif run:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read '../metamath/set.mm'
Reading source file "../metamath/set.mm"... 42816545 bytes
42816545 bytes were read into the source buffer.
The source has 203383 statements; 2714 are $a and 40578 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> markup mmset.raw.html mmset.html /alt_html /symbols /css /labels
Reading definitions from $t statement of ../metamath/set.mm...
1642 typesetting statements were read from "../metamath/set.mm".
Reading "mmset.raw.html"...
Creating "mmset.html"...
MM> markup mmcomplex.raw.html mmcomplex.html /alt_html /symbols /css /labels
Reading "mmcomplex.raw.html"...
Creating "mmcomplex.html"...
MM> markup mmdeduction.raw.html mmdeduction.html /alt_html /symbols /css /labels
Reading "mmdeduction.raw.html"...
Creating "mmdeduction.html"...
MM> markup mmnatded.raw.html mmnatded.html /alt_html /symbols /css /labels
Reading "mmnatded.raw.html"...
Creating "mmnatded.html"...
MM> markup mmzfcnd.raw.html mmzfcnd.html /alt_html /symbols /css /labels
Reading "mmzfcnd.raw.html"...
Creating "mmzfcnd.html"...
MM> markup mmfrege.raw.html mmfrege.html /alt_html /symbols /css /labels
Reading "mmfrege.raw.html"...
Creating "mmfrege.html"...
MM> show statement */alt_html/time
Creating HTML file "mmascii.html"...
Creating HTML file "mmtheoremsall.html"...
Creating HTML file "mmdefinitions.html"...
Creating HTML file "a1ii.html"...

[snip]

Creating HTML file "cmsss.html"...
SHOW STATEMENT run time =   1.90 sec for "cmsss.html"
Creating HTML file "lssbn.html"...
SHOW STATEMENT run time =   6.34 sec for "lssbn.html"
Creating HTML file "cmetcusp1.html"...
SHOW STATEMENT run time =   8.90 sec for "cmetcusp1.html"
Creating HTML file "cmetcusp.html"...
SHOW STATEMENT run time =   1.60 sec for "cmetcusp.html"
Creating HTML file "cncms.html"...
Killed

It looks like it's in the same general area in both cases as well. I don't suppose there have been some relevant changes there that might make metamath.exe use a lot of memory?

[digama0]

Found the log message:

[Mon Jan 16 14:11:37 2023] Out of memory: Killed process 515399 (metamath) total-vm:760236kB, anon-rss:562428kB, file-rss:0kB, shmem-rss:0kB, UID:1000 pgtables:1536kB oom_score_adj:0

so indeed it's a memory usage issue. I can't think of any recent changes to metamath-exe which could have caused this though.

[benjub]

Thanks @digama0 for https://github.com/metamath/metamath-exe/pull/125 Did you trigger a rebuild, or is there an automatic daily rebuild ?

And why did it use to work with the memory leaks you found ?

[digama0]

I am currently 170 minutes into a rebuild which seems to be going alright so far (EDIT: mpegif just finished :tada: so I think we will make it to the end). A few earlier attempts failed, including one after the memory leak PR, although I suspect this was due to the vscode SSH client taking up too much resources while I was monitoring the build.

The memory leaks were mostly minor, but there was one that was leaking chunks of set.mm between $( Begin $[ and $( End $[. As for why things changed or whether we will still be hitting the issue, I have no idea.

[digama0]

Either the build I did or the subsequent nightly build completed and all the pages seem to be up again, so I think it's safe to close this issue. (I really want to work on a replacement for metamath-exe for building the web pages, or even moving to a dynamic generation + caching model to avoid the cost of doing multi-hour recompiles on a regular basis, based on mm-web-rs, but alas time is finite.)