Remove files which live in set.mm repo

[jkingdon]

These files are copies of files in the set.mm repository. We would like to use the copies from the set.mm repository.

See metamath/metamath-website-scripts#2 (comment) and that whole issue for context.

As for why we have been (it would seem) using the copies from the metamath-website-seed repository rather than the set.mm repository, that's somewhat mysterious to me in light of https://github.com/metamath/metamath-website-scripts/blob/e59c4b52a5573df7385d6dd618a0adf0dade3ec8/regenerate-website.sh#L97 so I'm not sure I have a good idea of whether we are better off merging this pull request and seeing what happens, or trying to look at logs or better understand what is happening.

[david-a-wheeler]

We could just merge and see what happens (the YOLO approach) but I'd like to review the scripts first. In the end I suspect this is the right answer.

[jkingdon]

Please do review the scripts (and logs, if you have them).

[david-a-wheeler]

Sorry, it's just been a busy week. The file that controls website regeneration is named regenerate-website.sh; it is in the repo metamath-website-scripts not metamath-website-seed. I'll take a look.

[benjub]

LGTM. @jkingdon or @digama0 do you have merge permissions ?

[jkingdon]

LGTM. @jkingdon or @digama0 do you have merge permissions ?

I do, but I don't think the pull request is correct.

The process starts here: https://github.com/metamath/metamath-website-scripts/blob/main/regenerate-website.sh which pulls in the seed files here and then calls install.sh which turns the .raw.html files to .html but there is nothing which looks in repos/set.mm for the .raw.html files.

There is this: https://github.com/metamath/metamath-website-scripts/blob/6e59a5da3dde1df34ccbd62373f572bac07819d3/regenerate-website.sh#L97 but this just copies .raw files over. Here, let's check. Sure enough, there's a https://us.metamath.org/mpeuni/mmset.raw.html and a https://us.metamath.org/ileuni/mmil.raw.html on the live site. But they are the copies from metamath-website-seed not the ones from set.mm. Oh wait, L97 of the script does mpegif but not mpeuni, so let's check https://us.metamath.org/mpegif/mmset.raw.html and https://us.metamath.org/ilegif/mmil.raw.html - yes those are the ones from the set.mm repository rather than the seed one.

So the good news is that I now (think that I) understand what is going on. The bad news is that I'm not sure how to fix the script to use the copies from the set.mm repo. Maybe copy them from repos/set.mm to $METAMATHSITE/mpegif, $METAMATHSITE/ilegif, etc right after we do the same for .mm files. But that script fix would need to be made before the current pull request can be merged.