search

metamath / metamath-website-scripts

Scripts to set up the metamath website(s) so they're under version control, can be reviewed, and can be rerun. The scripts download the seed files from metamath-website-seed, databases from set.mm, etc.
MIT License
2 stars 3 forks source link

Use .raw.html files from set.mm repository #13

Closed jkingdon closed 1 year ago

jkingdon commented 1 year ago

Those are the copies that we have been maintaining, but until now what has been used in the live site are the copies from metamath-website-seed Assuming this works, we can remove the copies in metamath-website-seed which are out of date anyway.

There's a more full diagnosis at https://github.com/metamath/metamath-website-seed/pull/14#issuecomment-1732751926

Steps:

  1. get review on this pull request (ideally from @digama0 or @david-a-wheeler )
  2. merge it
  3. wait a day for the nightly website rebuild to happen
  4. look at whether all 8 files are present in the generated site and whether they are the up to date copies from the set.mm repo
  5. if yes, celebrate a little and figure we are good on https://github.com/metamath/metamath-website-scripts/issues/2
  6. add nfegif/mmnf.raw.html to https://github.com/metamath/metamath-website-seed/pull/14 (the other seven files are already there)
  7. move https://github.com/metamath/metamath-website-seed/pull/14 out of draft and merge it
  8. wait a day for the nightly website rebuild to happen
  9. make sure nothing broke in step 7 (it shouldn't have, but with these scripts you never know) by looking at whether all 8 files are present in the generated site
jkingdon commented 1 year ago

Are we OK to merge this? I don't have write access to this repository so I can't do it myself.

It strikes me as the fastest path to getting the web site updated. Right now https://us.metamath.org/ileuni/mmil.html still ends on phisum (over a year out of date) and the other web pages affected by this pull request have the same issue.

digama0 commented 1 year ago

This PR is superseded by #16, which essentially rewrites the whole process and makes it much easier to review this kind of change. The current code in regenerate-website.sh is actually incorrect, it does the copying after running install.sh but this means that the copied files are not present in the mirrors or site zip.

jkingdon commented 1 year ago

This PR is superseded by #16, which essentially rewrites the whole process and makes it much easier to review this kind of change. The current code in regenerate-website.sh is actually incorrect, it does the copying after running install.sh but this means that the copied files are not present in the mirrors or site zip.

I don't have much of an opinion about how we fix it, so are we going to merge #16 ? I don't see any activity on that one in the last 3 weeks.

digama0 commented 1 year ago

I was hoping to give some time for @david-a-wheeler or others to review it, but alas this may just be something we need to test in production.

jkingdon commented 1 year ago

I was hoping to give some time for @david-a-wheeler or others to review it, but alas this may just be something we need to test in production.

If need be I can come up with a serious answer to this, but for the moment I'll just post http://www.quickmeme.com/meme/22sv

benjub commented 1 year ago

I see above that this PR is superseded by #16 which has been merged. So, should this be closed ?

jkingdon commented 1 year ago

I see above that this PR is superseded by #16 which has been merged. So, should this be closed ?

Yes