Updating the website

[Scott Fenton]

Hi all,

With Norm's passing, does anyone have access to the webpage anymore? It's falling a little out of date with the current state of set.mm?

-Scott

[Jim Kingdon]

What part of the website? Some parts are definitely already open for pull request - for example https://github.com/metamath/set.mm/blob/develop/mmset.raw.html - but if you are thinking of something which isn't in git yet, I believe David Wheeler has access (and, I presume, a plan to get it into git although I want to be patient because I'm sure there is a lot to do just now).

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACKrHR8tnhVGYeuGnnOTZzNmn92nBBYn%3DEZsuVgQfUeegZPzJA%40mail.gmail.com.

[David A. Wheeler]

> On Dec 19, 2021, at 8:11 PM, Jim Kingdon <kin...@panix.com> wrote:
>
> What part of the website? Some parts are definitely already open for pull request - for example https://github.com/metamath/set.mm/blob/develop/mmset.raw.html - but if you are thinking of something which isn't in git yet, I believe David Wheeler has access (and, I presume, a plan to get it into git although I want to be patient because I'm sure there is a lot to do just now).

I have access to the underlying website, as does Mario.

Unfortunately, I won't be able to do much this month. There's the holidays, my father is having some very significant health issues, & my work has time-sensitive tasks right now. I expect that Mario & I will be working to get things moving, though, as soon as we can.

I have at least 3 items I want to see:
1. Properly-working "https:". Eventually "http:" should do only one thing: redirect to the corresponding "https:".
2. Automated regeneration of the website from the repo contents, with no human action.
3. Confidence that everything will keep working & be easily maintainable even after someone becomes incapacitated/dies.

--- David A. Wheeler

[Antony Bartlett]

I've just been on the site, and have noticed at least two seperate "Your comments are welcome: email Normal Megill" page footers, that you might also consider changing.

Terribly sad, rest in peace Norm!

    Best wishes,

        Antony

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2488B86D-EE2E-435D-96E4-58F28B9C89E0%40dwheeler.com.

[Antony Bartlett]

Oh... and additionally, I believe Mario is now the only active 'owner' of this mailing list, and as such might like to consider appointing some more 'owners'?

https://groups.google.com/g/metamath/about

(If I'm not mistaken about Jason Orendorff's last post here being 2018)

Sorry for double-posting, this only occurred to me when I went to check that my first message hadn't been eaten by Google Group's spam filter.

    Best wishes,

        Antony

[Glauco]

The main page of the site begins with "Over 23,000 proofs". It looks like it could be updated.

Glauco

[Alexander van der Vekens]

On Saturday, January 1, 2022 at 9:48:27 PM UTC+1 Glauco wrote:

The main page of the site begins with "Over 23,000 proofs". It looks like it could be updated.

What should be the number of proofs which should be provided here? Is it "over 27,000 proofs" (main body of set.mm, i.e., Parts 1-16), or the whole number of proofs including deprecated parts and mathboxes (this would be "over 41,000 proofs")?

[Glauco]

I guess a site visitor would be "comfortable" seeing coherence between that number and the largest number she sees in the Theorem List pages.

Is there a rough estimate of the number of theorems in the deprecated part?

What about dropping the second digit and go for a "ten thousand precision"?

Something like "over 40,000 proofs" that we will update when we will be above 50,000 ?

Glauco

[David A. Wheeler]

> On Dec 20, 2021, at 10:35 AM, Antony Bartlett <a...@akb.me.uk> wrote:
>
> Oh... and additionally, I believe Mario is now the only active 'owner' of this mailing list, and as such might like to consider appointing some more 'owners'?
>
> https://groups.google.com/g/metamath/about

I'm currently a manager of the Metamath mailing list, but only owners can make someone else an owner.

I agree that there should be at least 2 active owners of the mailing list, in case something happens. I'd be happy to serve, if others are fine with that. Only Mario can add currently another owner though.

Mario: Would you set me or someone else you trust as co-owner of the Metamath mailing list, so that we have a bus factor of more than 1?

--- David A. Wheeler

[Mario Carneiro]

David: I've added you as an owner.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/651EF2F8-25AC-42CA-9E27-4F611A237F5B%40dwheeler.com.

[Benoit]

I agree with David's proposed items:

> 1. Properly-working "https:". Eventually "http:" should do only one thing: redirect to the corresponding "https:".
> 2. Automated regeneration of the website from the repo contents, with no human action.
> 3. Confidence that everything will keep working & be easily maintainable even after someone becomes incapacitated/dies.

but for now, is it possible to regenerate the theorem pages (even if it is less frequent and manual, while waiting for automation) ?  Currently, the page http://us2.metamath.org:88/mpeuni/mmrecent.html indicates "Last updated on 8-Dec-2021 at 4:21 AM ET."  I don't remember how it was done, but generally, a change was on us2.metamath.org at most 24h after a PR was merged (and on us.metamath.org another 24h/48h after that).  It is getting a bit difficult to track the changes made in the past almost-one-month.

Benoît

[David A. Wheeler]

Yes, it's definitely possible. Norm sent me instructions on how to do it a long time ago. I first have to find them in my infinite email inbox. I haven't tried to do it, so of course something might not work, but I *think* I just have to find & follow the instructions (famous last words).

My problem is that I've been swamped at work (I worked through the holidays) & my father has some serious health problems, so I've been delayed. So I'll get to it (unless someone gets there first). So please be patient with me!!

--- David A. Wheeler

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f168b0a7-ac4d-4f7e-b88a-22cd569c4241n%40googlegroups.com.