Zulip Chat Archive

Stream: general

Topic: deprecating NNG3

Kevin Buzzard (Oct 23 2023 at 10:23):

There has been discussion about this before, but I think it's time to discourage any further play on NNG3. Google still takes me to NNG3 and there was a question about NNG3 on this Zulip over the weekend. I have no web experience and also I don't have a clear idea about how to do this (actually maybe the below is the first attempt at a clear idea).

I have access to the NNG3 server. All the code lives in a directory called xena/natural_number_game, which you can see in the URL https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ . I just did cp -r natural_number_game foobar in the xena directory and now https://www.ma.imperial.ac.uk/~buzzard/xena/foobar/ is also a copy of the natural number game, so I think that it's as simple as "everything is in that directory" (although I know this isn't a proof -- but I also have the memory that I got it onto the server by typing some mumbo-jumbo on my computer and then copying one directory over to the server and calling it natural_number_game).

If I look at index.html in the natural_number_game directory it looks like this:

buzzard@cathedral:~/public_html/xena/natural_number_game> more index.html
<!DOCTYPE html>
<html>
<head>
  <meta charset="utf-8">
  <meta name="viewport" content="width=device-width, initial-scale=1">
  <title>The Natural Number Game</title>
  <script type="text/javascript">
    var MathJax;
  </script>
  <script type="text/x-mathjax-config">
    MathJax.Hub.Config({
      tex2jax: {
        inlineMath: [['$','$'], ['\\(','\\)']],
        processEscapes: true,
        ignoreClass: "no-mathjax"
      }
    });
  </script>
  <script type="text/javascript" async src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS_CHTML" async>
  </script>
  <link rel='stylesheet' href='./interactive.css'/>
</head>
<body>
  <div id="root"></div>
  <script src='vs/loader.js'></script>
  <script src='vs/editor/editor.main.nls.js'></script>
  <script src='vs/editor/editor.main.js'></script>
<script type="text/javascript" src="./interactive.js"></script></body>
</html>
buzzard@cathedral:~/public_html/xena/natural_number_game>

What do we want to now be happening? I am thinking of moving that page to index2.html, and then having index.html being just a simple web page saying "this is the old NNG3 game, you should play the newer NNG4 game, to do that click here, and if you want to see the old NNG3 game then click here[index2.html], or just wait for 10 seconds and you'll go to the new NNG4 game anyway", and then leave most of NNG3 how it was (so no links break). Is this what I should do?

I'm hoping that someone can tell me how to write that new index.html page, we can drop it in foobar to check that things work as they should, and then copy everything back to the natural_number_game directory and, as @Sebastian Ullrich has been dreaming for years now, we can finally forget the comma :-)

I have <= world working on my laptop now and hopefully by the end of the day it will be live on the NNG4 server.

Chris Birkbeck (Oct 23 2023 at 10:31):

I still have the mirror for NNG3 we used at some point here. Do you want that to be removed as well? Or we can leave it up as backup in case someone really wanted to use it

Kevin Buzzard (Oct 23 2023 at 10:47):

Imperial want to remove the www.ma.imperial.ac.uk server completely (it is a constant battle between the department (ma stands for maths) and the university), so there's certainly a chance that in say 2 years that the server I'm using will just randomly disappear overnight.

Julian Berman (Oct 23 2023 at 12:40):

@Kevin Buzzard another option to consider is simply adding

<link rel="canonical" href="https://adam.math.hhu.de/#/g/hhu-adam/NNG4" />

to the <head> tag of the NNG3 page. This should essentially give all or a lot of its search engine mojo to NNG4 by telling Google "the real page is over there!" while not completely defacing its memory for someone who wants to really see that page.

Eric Wieser (Oct 23 2023 at 13:04):

That feels a bit too aggressive to me, as people searching for "lean 3 NNG" might still end up at the lean 4 page

Eric Wieser (Oct 23 2023 at 13:05):

Even just putting a 3 in the HTML title would probably go a long way to preventing SEO listing it for people looking for Lean 4

Julian Berman (Oct 23 2023 at 13:27):

(I think the 10 second redirect may cause that behavior anyhow, unsure)

Julian Berman (Oct 23 2023 at 13:28):

But I hope the point is to catch people searching for lean rather than specifically lean 4, or maybe "natural number game" since I assume people will start to use that unqualified to mean NNG4.

Eric Rodriguez (Oct 23 2023 at 13:29):

Eric Wieser said:

That feels a bit too aggressive to me, as people searching for "lean 3 NNG" might still end up at the lean 4 page

I think this is probably what the community wants, the best way to deal with this imo is just to put a link to the 'old version' on the lean4 one

Eric Wieser (Oct 23 2023 at 13:33):

I think the best answer here is what Kevin suggests, namely

  • Replaces the current NNG3 page with something that says " :paperclip: It looks like you were looking for the Lean 3 natural number game; are you sure you don't want the Lean 4 one?"
  • Keep the lean3 one around at a new URL. Make sure to use "lean 3" as much as possible in any text that SEO might use.

Jon Eugster (Oct 23 2023 at 14:40):

Kevin Buzzard said:

I'm hoping that someone can tell me how to write that new index.html page, we can drop it in foobar to check that things work as they should, and then copy everything back to the natural_number_game directory [...]

Here's a very simple redirect page, which redirects the user after 15 seconds. You could still style it up a bit to your liking.

<!DOCTYPE html>
<html>
<head>
  <meta charset="utf-8">
  <meta name="viewport" content="width=device-width, initial-scale=1">
  <title>The (old) Natural Number Game</title>
  <link rel='stylesheet' href='./interactive.css'/>
</head>
<body>
  <p>This is a deprecated version of the Natural Number game.</p>
  <p>You will be redirected to the <a href="https://adam.math.hhu.de">current Lean 4 version of the NNG</a> in <span id="time_left">15</span> seconds.</p>
  <p><i>(To play the deprecated Lean 3 version of the NNG, click <a href="https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/">here</a>.)</i></p>
  <script>
      /* seconds until redirect */
      var time_out = 15;

      var start = new Date().getTime();
      var countdown = setInterval(function() {
        var now = new Date().getTime()
        document.getElementById("time_left").innerHTML =  time_out - Math.floor((now - start) / 1000) ;
      }, 1000)

      var timer = setTimeout(function() {
          window.location='https://adam.math.hhu.de'
      }, 1000 * time_out);
  </script>
</body>
</html>

Martin Dvořák (Oct 25 2023 at 22:46):

FYI, a friend of mine was searching for NNG today and started playing the Lean 3 version because it was still at the top of Google results.

Chris Wong (Oct 26 2023 at 05:05):

And in this Reddit thread, someone linked NNG3. (Though, to their credit, someone else linked NNG4 immediately afterward.)

Kevin Buzzard (Oct 26 2023 at 06:20):

@Jon Eugster do you know why we don't yet have <= world on the live version of NNG4? I hope to get to deprecating NNG3 today (although teaching hell continues until Friday)

Jon Eugster (Oct 26 2023 at 09:14):

probably just the auto-update script that's broken for some reason. I'll check that tonight, but Im off this morning.

Actually, it's clearly just the broken script, it's building now.

Luigi Massacci (Nov 13 2023 at 07:47):

I assume that NNG3 is still live? I told a classmate about NNG and I saw this morning he ended up finding NNG3.

Kevin Buzzard (Nov 13 2023 at 08:23):

It's on my job list for today to try and understand enough about how web pages work to do something about this.

Mauricio Collares (Nov 13 2023 at 08:35):

I assume there are less hacky ways if you do have access to the source repository, but if all you want to do is to include a message telling people to go to NNG4, you should be able to directly edit game_data.json's introData attribute (the "Getting your home page content onto the webserver" section at https://sysnews.ma.ic.ac.uk/web-homepages/ might help too).

Mauricio Collares (Nov 13 2023 at 08:53):

Ah, the source is at https://github.com/ImperialCollegeLondon/natural_number_game and there are even convenient compile.sh and ship.sh scripts, so I guess the main concern would be scp not working.

Kevin Buzzard (Nov 13 2023 at 09:52):

The main problem is that I don't have a clue about computers and whenever I turn to this job I just feel miserable. I'll see if I can do it now.

Kevin Buzzard (Nov 13 2023 at 10:07):

OK I have manually mucked about with some index.html file and it looks like NNG3 is finally deprecated!

I didn't do what Julian suggested here because I don't know how to add something to a <head> tag or more generally what that means. And I didn't do the last bit of what Eric suggested here about writing "lean 3" but I hopefully did the rest.

Mauricio Collares (Nov 13 2023 at 10:23):

Nitpick: If I wait 15 seconds it redirects to adam.math.hhu.de here (where I can choose NNG4 or Formaloversum), not directly to NNG4

Kevin Buzzard (Nov 13 2023 at 10:29):

Feel free to tell me how to fix this. I have no idea why that's happening.

Kevin Buzzard (Nov 13 2023 at 10:30):

buzzard@server:xena/natural_number_game> more index.html
<!DOCTYPE html>
<html>
<head>
  <meta charset="utf-8">
  <meta name="viewport" content="width=device-width, initial-scale=1">
  <title>The (old) Natural Number Game</title>
  <link rel='stylesheet' href='./interactive.css'/>
</head>
<body>
  <p>You have attempted to access the old Lean 3 version of the Natural Number game.</p>
  <p>You will be redirected to the <a href="https://adam.math.hhu.de/#/g/hhu-adam/NNG4">current Lea
n 4 version of the game</a> in <span id="time_left">15</span> seconds.</p>
  <p><i>(To play the deprecated Lean 3 version of the NNG, click <a href="https://www.ma.imperial.a
c.uk/~buzzard/xena/natural_number_game/index2.html">here</a>.)</i></p>
  <script>
      /* seconds until redirect */
      var time_out = 15;

      var start = new Date().getTime();
      var countdown = setInterval(function() {
        var now = new Date().getTime()
        document.getElementById("time_left").innerHTML =  time_out - Math.floor((now - start) / 100
0) ;
      }, 1000)

      var timer = setTimeout(function() {
          window.location='https://adam.math.hhu.de'
      }, 1000 * time_out);
  </script>
</body>
</html>

Damiano Testa (Nov 13 2023 at 10:49):

You can probably change the window.location URL to https://adam.math.hhu.de/#/g/hhu-adam/NNG4.

Kevin Buzzard (Nov 13 2023 at 11:01):

Aah, I hadn't realised that the NNG4 URL was in that page twice. Thanks! Should be fixed now?

Damiano Testa (Nov 13 2023 at 11:05):

Works for me on Android, both waiting and clicking on the link.

Luigi Massacci (Nov 13 2023 at 13:06):

Also works on Firefox (both ways) on iPad and Ubuntu desktop, and usually if it works on the iPad with firefox it works for everyone…

Kevin Buzzard (Nov 13 2023 at 13:39):

Thanks for the tests everyone!

Jon Eugster (Nov 16 2023 at 09:16):

Damiano Testa said:

You can probably change the window.location URL to https://adam.math.hhu.de/#/g/hhu-adam/NNG4.

@Kevin Buzzard btw the tail of this URL (i.e. after #) is not guaranteed to be persistent, depending on future development. For example, I will likely change it to https://adam.math.hhu.de/#/g/leanprover-community/NNG4 within the next few weeks, in order to reflect the recent relocation of the github repo.

I generally encourage linking to the landing page https://adam.math.hhu.de in more permanent documents/places, as this one is guaranteed to be persistent.

Kevin Buzzard (Nov 16 2023 at 09:17):

Ok I can try and remember to change it back :-)

Last updated: Dec 20 2023 at 11:08 UTC