search

metamath / metamath-website-seed

Starting seed files for metamath public website. The website starts with these and then uses generation scripts to generate other files from the .mm files
Other
4 stars 9 forks source link

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

Open CatsAreFluffy opened 1 year ago

CatsAreFluffy commented 1 year ago

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 commented 1 year ago

Although the link is to the develop branch I too am seeing 212ee7d9 in the text which is a reference to https://github.com/metamath/set.mm/commit/212ee7d9d6c8104120a8553dba4a33318b44fa05 . 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 commented 1 year ago

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 commented 1 year ago

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.