"This page was created from" message on the most recent proofs page is wrong

[CatsAreFluffy]

The commit hash referenced in the "This page was created from" message on https://us.metamath.org/mpeuni/mmrecent.html leads to a commit from December 2021.

[jkingdon]

Although the link is to the develop branch I too am seeing 212ee7d9 in the text which is a reference to metamath/set.mm@212ee7d . Perhaps Norm was updating this manually? If so, we should either drop it or make an automated way to generate it. Perhaps drop it as I'm not sure it is worth the complexity of maintaining that kind of script.

[digama0]

I think we should keep the commit SHA. It should not be hard to get the SHA from the update script, since it is working from an actual git checkout, although I will be very happy when we replace the scripts with something like a static site generator rather than all this homegrown stuff.

[jkingdon]

I think we should keep the commit SHA. It should not be hard to get the SHA from the update script, since it is working from an actual git checkout

Well, the nit-picky answer is that we download a tarball from github rather than a checkout ( https://github.com/metamath/metamath-website-scripts/blob/6e59a5da3dde1df34ccbd62373f572bac07819d3/regenerate-website.sh#L50 ). But that's only a small obstacle, if it would work to do a shallow clone instead or fetch the latest revision number at the same time we fetch the tarball.

My larger point is that if we want to do something about our over-complicated and fragile build scripts, we should look for places to.... uh, reduce complexity. I'm trying to save us from ourselves in terms of whether we are chasing something which is not much even noticed, much less would be missed if it were gone. But I'll only push so hard, especially if someone does indeed have the time to fix this revision number generation.

, although I will be very happy when we replace the scripts with something like a static site generator rather than all this homegrown stuff.

Conceptually, I probably like that idea (even if I can't fully visualize that future). But it does sound like a big project in terms of selecting one, figuring out where to stick in the metamath-specific parts, etc.