Website is down

[Rohan Ridenour]

https://us.metamath.org/ 403s, other pages 404.

[Mario Carneiro]

Sorry about that, I chose the wrong time to test the new website build process and the cron job started running in the middle of it, and unfortunately killing the cron job just made it copy an empty website to the live site. Things should be back up now.

On that note, what is now up is the new website build, so everyone please try clicking around and make sure everything seems to be working (not just theorem pages but also links to the downloads and other stuff on the homepage, the GIF and UNI directories for all five supported databases, and the symbols and mmsolitaire pages).

On Wed, Oct 25, 2023 at 3:28 AM Rohan Ridenour <catis...@gmail.com> wrote:

https://us.metamath.org/ 403s, other pages 404.

--
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/bddc8891-7fae-467b-b794-ca84f2681fc8n%40googlegroups.com.

[Thierry Arnoux]

https://us.metamath.org/mpeuni/mmrecent.html

Still throws a 404.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvt7E89qnTKXTppUv1Awsy5SCB-YiBbDBHYfn-hGr%2B7HQ%40mail.gmail.com.

[Mario Carneiro]

should be fixed now

[Thierry Arnoux]

Thanks! That page now loads Ok, even though "most recent" shows theorems from 24-Sep-2023.

The link on the home page https://us.metamath.org/ still points to http://us2.metamath.org:88/mpeuni/mmrecent.html but that's a different issue.

[Mario Carneiro]

Oh, this is probably because the site build was done using the set.mm branch from https://github.com/metamath/set.mm/pull/3524. I'll have to rerun the whole thing to update the website with the latest stuff from the develop branch, which is probably a good test just to make sure that the last minute issues are fixed this time now that all the branches have landed, but it apparently takes about 3 hours to run. (I can't wait for the 400x speedup from https://groups.google.com/g/metamath/c/eqsqv7WjQPs...)

[Mario Carneiro]

Crap, I deleted the site again. Sorry folks, it will be back in 3 hours.

[Jim Kingdon]

Clicking around now......

* https://us.metamath.org/ileuni/mmil.html is up to date (missing theorems list goes to dvcn) for the first time in over a year. https://us.metamath.org/ilegif/mmil.html too.

* https://us.metamath.org/mpeuni/mmset.html and https://us.metamath.org/mpegif/mmset.html include the [Bauer] reference (another litmus test for up to dateness).

* https://us.metamath.org/ileuni/mmrecent.html is up to date (shows a revision from 22-Oct-2023)

So looks good!

Thanks for all the hard work on this.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvt7E89qnTKXTppUv1Awsy5SCB-YiBbDBHYfn-hGr%2B7HQ%40mail.gmail.com.

[Gino Giotto]

It seems there are problems with pictures. For example in https://us.metamath.org/mpeuni/mmset.html scrolling down a little there is the "Breakdown of a proof step. Credit: N. Megill 2003. Public Domain." that doesn't show.

[BTernary Tau]

I am able to see the breakdown of a proof step image, as well as the circled orange number icons.

[Discher, Samiro]

I also do not see the breakdown image. Maybe you didn't clear browser cache?

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von BTernary Tau <btern...@gmail.com>
Gesendet: Mittwoch, 25. Oktober 2023 17:58:02
An: Metamath
Betreff: Re: [Metamath] Website is down

 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7eaff53f-cf22-4a6e-bdac-e98b9390b27cn%40googlegroups.com.

[Mario Carneiro]

The proof step picture is indeed misplaced (@BTernaryTau try clearing your cache), it seems it was placed in the symbols repo by mistake (https://github.com/metamath/symbols/blob/main/symbols/_proofstep.gif). Same for _orange1circ.gif and _orange2circ.gif . These will probably have to be fixed individually so if you spot any others mention them here.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7eaff53f-cf22-4a6e-bdac-e98b9390b27cn%40googlegroups.com.

[Mario Carneiro]

The images have been restored on the live site, and the corresponding changes to the repos are metamath-website-seed@39991733 and symbols@85edf428.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/48d84c2f3b32419ab514a92cf22bdb07%40rwth-aachen.de.

[Gino Giotto]

It seems there is supposed to be an image in  https://us.metamath.org/mpeuni/mmset.html , where it says       Read this section carefully to learn how to follow a Metamath proof 

[Gino Giotto]

Also, I don't know if it's just me, but if I click Recent proofs which is in the first box titled
Metamath Proof Explorer from https://us.metamath.org/ then it says:

This site can’t be reached

us2.metamath.org 

took too long to respond.

But if I click (this mirror) then it works.

[Mario Carneiro]

On Wed, Oct 25, 2023 at 1:14 PM Gino Giotto <ginogiott...@gmail.com> wrote:

Also, I don't know if it's just me, but if I click Recent proofs which is in the first box titled
Metamath Proof Explorer from https://us.metamath.org/ then it says:

This site can’t be reached

us2.metamath.org 

took too long to respond.

That one was fixed by @tirix in https://github.com/metamath/metamath-website-seed/pull/19 , it will show up tomorrow.

The floating head of wisdom just happens to be symbol-sized and styled so I missed it in the other commit.

[Gino Giotto]

From https://us.metamath.org/mpeuni/bezout.html

I click  Structured version on the top right.

That brings me to Tirix website.

But from Tirix website clicking Unicode version or Nearby theorems gives a "Not Found" page.

(Btw Tirix website is actually very pretty, I like it a lot)

[Mario Carneiro]

I'm afraid tirix will have to fix that himself, I don't know where the source or hosting for that site is. (Although, I think it would be quite possible to integrate those pages into the main site 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/0899e5e9-5535-458f-b84e-afbb9824a860n%40googlegroups.com.

[Gino Giotto]

From my perspective Tirix website feels a bit "hidden" and "hard to reach", which I think it's a bit of a shame since how much potential it has. I would be happy to see it advertised more around.

[Mario Carneiro]

We have one more test to go, tonight I will let it run on its own. Hopefully all the hotfixes for issues reported here will also be reflected in the updated script.

There is also a bit of remaining cleanup to do re: images in set.mm repo. All the _frege_*.svg files are duplicated in seed/mpegif/, and I think something similar is true for the other images as well. I want to move most of these files (including mmfrege.html, mmcomplex.html, mmzfcnd.html) to the seed repo because they are just static files.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8c574141-5856-475c-baf9-ceaded20bb72n%40googlegroups.com.

[Gino Giotto]

I've been clicking stuff randomly for a while now, this is what I found:

From https://us.metamath.org/ the mmsolitaire.tar.gz , mpeuni.tar.gz , qleuni.tar.gz and symbols.tar.gz links give a 404.

From https://us.metamath.org/copyright.html#pd the GNU General Public License link gives a 404.

From https://us.metamath.org/mm.html the chinese mirror doesn't work cn.metamath.org (is it because I'm not in china?).

[Mario Carneiro]

On Wed, Oct 25, 2023 at 3:46 PM Gino Giotto <ginogiott...@gmail.com> wrote:

From https://us.metamath.org/ the mmsolitaire.tar.gz , mpeuni.tar.gz , qleuni.tar.gz and symbols.tar.gz links give a 404.

These links have been discontinued for space concerns:
https://github.com/metamath/metamath-website-scripts/blob/8d81a0c1ab3e433b335b4e6a3bdc364d277b4946/old/install.sh#L1580-L1581

although the new code
https://github.com/metamath/metamath-website-scripts/blob/8d81a0c1ab3e433b335b4e6a3bdc364d277b4946/build-website.sh#L188-L189

extends this to all subfolders rather than just mpeuni for consistency.

A PR to remove / comment out the links from the website are welcome.

[Mario Carneiro]

On Wed, Oct 25, 2023 at 3:46 PM Gino Giotto <ginogiott...@gmail.com> wrote:

From https://us.metamath.org/copyright.html#pd the GNU General Public License link gives a 404.

The top level LICENSE.TXT has been removed, as the web site is PD not GPLv2 (except for some enumerated exceptions) and this positioning of the license was misleading. The script used to copy this LICENSE.TXT into mmsolitaire/ and metamath/, but metamath/ is now being handled separately (the metamath-exe repo) and mmsolitaire already has this file, so the copies are no longer necessary. I think it would make the most sense to just point to https://www.gnu.org/licenses/old-licenses/gpl-2.0.en.html#SEC1 in that link rather than use a local copy.

[Gino Giotto]

On the https://us.metamath.org/mmsolitaire/mms.html webpage, when it says  "  (double arrow): logically equivalent to" there seems to be a missing picture.

[Mario Carneiro]

Looks like this is because the source was line-broken there, it says

<IMG
SRC='leftrightarrow.gif' WIDTH=15 HEIGHT=19 ALT='&lt;-&gt;'>

in the source and this is enough to fool the simple image usage heuristic here:

https://github.com/metamath/metamath-website-scripts/blob/8d81a0c1ab3e433b335b4e6a3bdc364d277b4946/build-website.sh#L133

I'm not sure what the best alternative is. Perhaps the easiest thing would be to just make those non-breaking points and make sure that there are no such breaks in any of the other files...

--

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/ee5cb20c-ab52-4d2b-9b4b-ab67bf0c27fdn%40googlegroups.com.

[Mario Carneiro]

Fixed in https://github.com/metamath/metamath-website-seed/pull/20.