mmil.html not updated

[jkingdon]

The mmil.html file has not been updated as it should be during recent website updates.

For example, the pull request metamath/set.mm#2991 made edits to iset.mm and mmil.raw.html. One change it made was to add a theorem istopfin and also mention it in mmil.raw.html. Although https://us.metamath.org/ileuni/istopfin.html has been correctly updated, https://us.metamath.org/ileuni/mmil.html still has an older version which does not mention istopfin .

Notes:

• The regeneration is apparently supposed to happen here;

  metamath-website-scripts/install.sh

  Line 1286 in 8c9c043

  "markup mmil.raw.html mmil.html /alt_html /symbols /css /labels" \

  . Presumably there are also other steps involved in the whole process.
• This problem has been ongoing for at least two months; the mmil.html updates from In iset.mm, add seq3f1o and related theorems (converting df-iseq syntax to df-seq3 syntax) set.mm#2927 are not present for example.

[david-a-wheeler]

It's working now, correct?

[jkingdon]

It's working now, correct?

No.

If I generate mmil.html locally by running scripts/regen-from-raw without arguments, and look to the end of the page (right above the bibliography) I see a bunch of theorems about extensible structures and topology and so on, ending in dvfg . However, if I look at https://us.metamath.org/ileuni/mmil.html the last entry is phisum

[david-a-wheeler]

Thanks for letting me know. I'm not sure why that's happening, since set.mm is working. I don't have time to track it down now, but I will try when I can. The current script is over-complicated; if I can't debug another way, I may "simplify until I get it working".

If you have any hypotheses, let me know.

[jkingdon]

Thanks for letting me know. I'm not sure why that's happening, since set.mm is working. I don't have time to track it down now, but I will try when I can. The current script is over-complicated; if I can't debug another way, I may "simplify until I get it working".

Unless I'm missing something, set.mm isn't working either. I don't see any reference to Bauer in the bibliography at https://us.metamath.org/mpeuni/mmset.html even though it is mentioned in https://github.com/metamath/set.mm/blob/develop/mmset.raw.html

If you have any hypotheses, let me know.

Not especially. The closest thing I have to a suggestion is to figure out whether the script is logging somewhere or can be made to do so (especially error messages if any). Your idea of simplifying it also may be worth a try.

[david-a-wheeler]

Oy! No one's told me that set.mm isn't working!! Or at least I didn't see such a report.

Okay, I'll definitely work on this. Thanks for the report.

[jkingdon]

Oy! No one's told me that set.mm isn't working!! Or at least I didn't see such a report.

LOL, I don't mind being a second class citizen but you don't have to be so obvious about it.

More seriously, I think the difference is that mmil.raw.html changes a lot more often than mmset.raw.html.

Okay, I'll definitely work on this. Thanks for the report.

I appreciate all your efforts!

[david-a-wheeler]

You're no second class citizen - I just pointed specifically to the intuitionistic logic work on Hacker News.

I thought it'd been resolved, to be honest. But if it also affects set.mm that means it's potentially a broader (and different) problem. Some family matters are making it not possible for me to investigate right now, but I definitely intend to do that soon. If anyone else has suggestions I'd like to hear it.

[jkingdon]

Take care of your family matters first.

And do not take my light hearted ribbing too seriously.

[david-a-wheeler]

The disk filled, so the regeneration didn't completely succeed.

I've done some cleaning, hopefully it will now simply complete tonight and all will be well. At least, I hope so.

[jkingdon]

hopefully it will now simply complete tonight

🤞

[david-a-wheeler]

Ugh, it didn't work.

The simple solution is to upgrade from 25GB to 50GB storage, ($6/month to $12/month). That adds other things we don't need, but it's the quick fix. https://www.linode.com/products/shared/

If there's another easy fix I'm open to it, but I want the site to work properly soon :-).

[digama0]

A quick fix might be to disable mpegif generation until we can solve the underlying issue. Has something happened to cause space usage to go up?

[david-a-wheeler]

@digama0 - not that I know of.

[david-a-wheeler]

The last entry in iset.mm is alsc2d, and that's present in: https://us.metamath.org/ileuni/alsc2d.html

So I think it's working.

[david-a-wheeler]

Here's more evidence it's all working. Th ILE generated statement at https://us.metamath.org/ileuni/djur.html includes the text "Upgrade implication to biconditional and shorten proof.". That text was added July 15 this year.

I also suspect the generation is also faster. The new configuration has more memory as well (1GB to 2GB), enabling the OS to do more caching. That's not terribly important, but it's a nice bonus.

[jkingdon]

Perhaps there is more than one problem? The list of theorems at https://us.metamath.org/ileuni/mmil.html (just above the bibliography) still ends at phisum and it should end at dvfg

[david-a-wheeler]

Perhaps there is more than one problem?

That is sadly possible :-(.

As you said, the displayed list just before https://us.metamath.org/ileuni/mmil.html#bib certainly ends with phisum, and the input file "mmil.raw.html" ends with dvfg.

However, in this repo metamath-website-seed the file ./ilegif/mmil.raw.html ends at phisum. I think this file is overriding things. The obvious thing to do is remove that file from this repo, and hopefully the equivalent file in the set.mm repo will be used instead. Sound like something we should try?

[jkingdon]

However, in this repo metamath-website-seed the file ./ilegif/mmil.raw.html ends at phisum. I think this file is overriding things. The obvious thing to do is remove that file from this repo, and hopefully the equivalent file in the set.mm repo will be used instead. Sound like something we should try?

I don't know whether to be sad that we apparently are reduced to trial and error to understand these scripts, or just say "sure, let's see what happens!" If you want to give a shot at the latter, I made metamath/metamath-website-seed#14

[david-a-wheeler]

We aren't really reduced to that, it's just that to look, someone (probably me) needs to take a little time to look. Let's take a look first, I don't think we're in that much of a hurry.

[jkingdon]

We aren't really reduced to that, it's just that to look, someone (probably me) needs to take a little time to look. Let's take a look first, I don't think we're in that much of a hurry.

OK, fair enough. Sounds like I came in dramatic when I should have aimed for more like.... amused I guess. Or something.

In any case, I agree, there's time to take a look.

[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.

[david-a-wheeler]

The script "regenerate-website.sh" downloads the site; it downloads various things, but it directly loads the seed directly into the $METAMATHSITE temporary holding area. The "regenerate-website.sh" script eventually calls "install.sh"; that was written by Norm and is rediculously complex (it needs a dramatic simplification).

Unfortunately, the current system presumes that these overview files are in the "seed" repo. In retrospect that's probably a mistake; I think all database-specific files like mmil.raw.html should go into their database repo (set.mm in this case), and remove them from the metamath-website-seed. But if you just remove the files from the set.mm repo, then currently it'll just cause a failure to generate mmil.html, so you won't have any index at all.

I think the best way forward is to rewrite the regeneration script. Most of what it does is unnecessary. E.g., it has mechanisms to counter problems when running on Windows XP (!!).

[david-a-wheeler]

Alright, I've started rewriting the regeneration script. It'll take a little time, but the result will be much cleaner I think.

[jkingdon]

I think I have a diagnosis for the problem about mmset.html and mmil.html not updating at (updated link) metamath/metamath-website-seed#14 (comment)

[GinoGiotto]

I think I have a diagnosis for the problem about mmset.html and mmil.html not updating at metamath/set.mm#3515 (comment) .

Your link redirects to my comment. I think you meant to link to metamath/metamath-website-seed#14 (comment) or #13 since my comment isn't a diagnosis.

[jkingdon]

I think I have a diagnosis for the problem about mmset.html and mmil.html not updating at metamath/set.mm#3515 (comment) .

Your link redirects to my comment. I think you meant to link to metamath/metamath-website-seed#14 (comment) or #13 since my comment isn't a diagnosis.

Thanks for pointing this out. I meant the former. Updated.

[digama0]

Alright, I've started rewriting the regeneration script. It'll take a little time, but the result will be much cleaner I think.

@david-a-wheeler Any progress on this? I'm thinking of looking into this myself, and it might help to see what you have so far.

[jkingdon]

Alright, I've started rewriting the regeneration script. It'll take a little time, but the result will be much cleaner I think.

@david-a-wheeler Any progress on this? I'm thinking of looking into this myself, and it might help to see what you have so far.

I was looking over what is at #12 (I don't know if there is anything which hasn't been pushed to that branch) and it seemed like a good start (and also the kind of thing which could potentially be merged incrementally if conceptualizing this as "rewrite" is leading us to bite off more than we can chew).

[david-a-wheeler]

The problem is that Norm's original script is so convoluted that it's hard to understand. I've decided that it'd be easier to rewrite than debug :-).

It's not really hard, I just need a block of time, and I had a big pair of work meetings in DC and Spain that have consumed much of my free time. I'm back, so hopefully I can make more progress now.

[jkingdon]

The problem is that Norm's original script is so convoluted that it's hard to understand. I've decided that it'd be easier to rewrite than debug :-).

Am I allowed to advocate for both rewrite and debug? That is, review and merge #13 now and also proceed on your efforts (which seem to be started in a good direction based on what I see at #12 ).

[jkingdon]

https://us.metamath.org/ileuni/mmil.html is now correct (goes up to dvcn) which was fixed by #16 and related pull requests.