Zulip Chat Archive

Stream: new members

Topic: natural number game comma

Andrea Bourque (Dec 24 2023 at 15:50):

in the natural number game you have to end lines with commas, whereas when I've used Lean (4) in VSCode, this is not required. Is this just a technicality with how the NNG is set up?

Julian Berman (Dec 24 2023 at 15:52):

You're referring to the Lean 3 Natural Number game.

Kevin Buzzard (Dec 24 2023 at 15:52):

I think you're playing the lean 3 version of the game?

Julian Berman (Dec 24 2023 at 15:52):

The Lean 4 natural number game uses Lean 4 syntax.

Julian Berman (Dec 24 2023 at 15:53):

It's Lean 3 vs Lean 4 where this syntax matters, it's not something that the natural number game is changing. For reference you can find the Lean 4 Natural Number game here: https://adam.math.hhu.de/#/g/leanprover-community/NNG4

Andrea Bourque (Dec 24 2023 at 15:54):

I kind of figured that was the case, but I couldn't find it on google (well, it is the third result, but it says "Lean Game Server" so I ignored it)

Julian Berman (Dec 24 2023 at 16:01):

You're right that that's a bit unfortunate. I'm not sure if there's intention (or a technical way) to fix it, I think it has to do with using hash routing with React -- though maybe still there's a way to properly have those be indexed as separate pages, clearly they're being looked at...

EDIT: Actually I think maybe it's that https://github.com/leanprover-community/lean4game needs a sitemap?

Julian Berman (Dec 24 2023 at 16:02):

But if you go to the Lean 3 NNG page aren't you automatically redirected to the Lean 4 one?

Andrea Bourque (Dec 24 2023 at 16:07):

Yes, if you go to https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/. But it has "Old" in the title, so I didn't click on it. The 4th result (for me) is https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/index2.html which doesn't redirect, and allows you to play the Lean 3 version fully.

Andrea Bourque (Dec 24 2023 at 16:09):

It's no big deal, I suppose. But I'm writing about Lean right now, so I wanted to make sure I had up-to-date info

Mauricio Collares (Dec 24 2023 at 16:15):

That's a good point, "Lean Game Server" is a confusing title. SEO for React single-page apps seems tricky.

Kevin Buzzard (Dec 24 2023 at 16:19):

Good point about "(old)"! I've just removed it, so google will notice at some point.

Kevin Buzzard (Dec 24 2023 at 16:29):

If someone can tell me how to put a warning on https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/index2.html saying "you're playing an old version" that would be great! I just tried adding two more lines to the html (the IMPORTANT NOTE) so it looks like this:

<!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>
  <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>
  <h1>IMPORTANT NOTE</h1>
  You are playing an old deprecated version of the Natural Number Game. Click here to play the new version.
  <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>

and now it looks like this:
Screenshot-from-2023-12-24-16-28-46.png

so I think I'd better remove it again...(I have absolutely no understanding of html beyond html1)

Andrea Bourque (Dec 24 2023 at 16:52):

Looks like one of those js files is putting the text on screen, so you have to edit them accordingly

Andrea Bourque (Dec 24 2023 at 16:53):

I don't think I or anyone else can say anything more specific than that, without access to the files

Mauricio Collares (Dec 24 2023 at 16:56):

Sources are at https://github.com/ImperialCollegeLondon/natural_number_game

Mauricio Collares (Dec 24 2023 at 16:57):

If you don't feel like re-deploying everything you can also do it the hacky way

Andrea Bourque (Dec 24 2023 at 17:00):

This does have the landing text in intro.lean, but I don't know if editing that would affect the webpage

Andrea Bourque (Dec 24 2023 at 17:23):

@Kevin Buzzard Try adding the following code anywhere in the body: 

<script>
    document.addEventListener("DOMContentLoaded", function() {
        if (window.confirm('You are playing an old version of the Natural Number Game. Click ok to be redirected.'))
        {
            window.location.href='https://adam.math.hhu.de/#/g/leanprover-community/nng4';
        };
    };
</script>

Andrea Bourque (Dec 24 2023 at 17:28):

Also, on the topic of the NNG: is the Lean 4 NNG horrendously slow for anyone else? Almost every level I have to refresh the page because my input doesn't show up
For reference, I tried on both google chrome and firefox, both up-to-date, and on a good machine.

Kevin Buzzard (Dec 24 2023 at 20:33):

This is bad. There is some kind of bug here I think. @Alexander Bentkamp do you know what could be going on?

Alexander Bentkamp (Dec 24 2023 at 20:40):

I only caught the issue once, wasn't enough for me to debug. It does not seem slow, but rather stuck.

Alexander Bentkamp (Dec 24 2023 at 20:40):

Do you have a reliable way to reproduce it?

Andrea Bourque (Dec 24 2023 at 20:48):

@Alexander Bentkamp
I agree "stuck" is more accurate than "slow".
It doesn't do it for exactly every level, and once I reload a level once it doesn't get stuck again.
I can try on another machine. I don't really know how to "reliably reproduce" results though

Alexander Bentkamp (Dec 24 2023 at 21:00):

It just does not want to happen to me a second time...

Andrea Bourque (Dec 24 2023 at 21:01):

Works perfectly on my second machine. I used chrome on there to test it, and I have the same extensions and everything as on my first machine. Like I said, on my first machine, it fails on both firefox and chrome. So, it seems to be a hardware problem, which makes no sense to me.

Andrea Bourque (Dec 24 2023 at 21:02):

I can give more specifics about my computers if need be.

Alexander Bentkamp (Dec 24 2023 at 21:03):

I can't imagine that could be the issue and the info would not help me at all.

Alexander Bentkamp (Dec 24 2023 at 21:03):

@Jon Eugster

Andrea Bourque (Dec 24 2023 at 21:04):

It takes my input just fine, as in when I reload the page it shows that I have submitted input, it just seems to be failing to send me the output every so often.

Andrea Bourque (Dec 24 2023 at 21:06):

I filed an issue on the github

Alexander Bentkamp (Dec 24 2023 at 21:24):

That's a good idea, but we'll need more specific info to figure out what's going on, I am afraid. Here is an idea:

In Chrome, in a NNG level, press Ctrl+Shift+I. In the panel that opens, click on the Tab "Network". Reload the page. A list of items should appear in the panel. Click on the item nng4. A smaller panel opens on the right. Click on the tab "Messages". When your issue occurs, copy the recent messages listed there. That will give us a better idea what's going on. The output in the tab "Console" might also help. Thank you!

Andrea Bourque (Dec 24 2023 at 21:31):

okay, will do

Andrea Bourque (Dec 24 2023 at 21:35):

{"params":{"textDocument":{"version":2,"uri":"file:///Tutorial/5"},"processing":[{"range":{"start":{"line":0,"character":0},"end":{"line":1,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"} 215
15:34:51.432
{"params":{"version":2,"uri":"file:///Tutorial/5","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}},"message":"unsolved goals\na b c : ℕ\n⊢ a + b + (c + 0) = a + b + c","fullRange":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}    380
15:34:51.443
{"params":{"textDocument":{"version":2,"uri":"file:///Tutorial/5"},"processing":[{"range":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}},"kind":1}]},"method":"$/lean/fileProgress","jsonrpc":"2.0"} 215
15:34:51.444
{"params":{"version":2,"uri":"file:///Tutorial/5","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}},"message":"unsolved goals\na b c : ℕ\n⊢ a + b + (c + 0) = a + b + c","fullRange":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}    380
15:34:51.444
{"params":{"version":2,"uri":"file:///Tutorial/5","diagnostics":[{"source":"Lean 4","severity":1,"range":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}},"message":"unsolved goals\na b c : ℕ\n⊢ a + b + (c + 0) = a + b + c","fullRange":{"start":{"line":1,"character":0},"end":{"line":1,"character":0}}}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}    380
15:34:51.444
{"params":{"textDocument":{"version":2,"uri":"file:///Tutorial/5"},"processing":[]},"method":"$/lean/fileProgress","jsonrpc":"2.0"} 131
15:34:51.444
{"result":[],"jsonrpc":"2.0","id":216}  38
15:34:51.464
{"jsonrpc":"2.0","id":217,"method":"textDocument/foldingRange","params":{"textDocument":{"uri":"file:///Tutorial/5"}}}  118
15:34:52.978
{"jsonrpc":"2.0","id":218,"method":"textDocument/semanticTokens/full","params":{"textDocument":{"uri":"file:///Tutorial/5"}}}   125
15:34:53.046
{"result":[],"jsonrpc":"2.0","id":217}  38
15:34:53.145
{"result":{"data":[0,0,2,0,0]},"jsonrpc":"2.0","id":218}    56
15:34:53.211
{"jsonrpc":"2.0","method":"$/keepAlive","params":{}}    52
15:34:56.349
{"jsonrpc":"2.0","method":"$/lean/rpc/keepAlive","params":{"uri":"file:///Tutorial/5","sessionId":"15328810329659425578"}}  122
15:34:57.216
{"jsonrpc":"2.0","method":"$/keepAlive","params":{}}    52
15:35:01.372
{"jsonrpc":"2.0","method":"$/keepAlive","params":{}}    52
15:35:06.373
{"jsonrpc":"2.0","method":"$/lean/rpc/keepAlive","params":{"uri":"file:///Tutorial/5","sessionId":"15328810329659425578"}}  122
15:35:07.216
{"jsonrpc":"2.0","method":"$/keepAlive","params":{}}    52
15:35:11.368

Andrea Bourque (Dec 24 2023 at 21:35):

these appeared right after getting stuck

Andrea Bourque (Dec 24 2023 at 21:37):

Then it keeps cycling these three

{"jsonrpc":"2.0","method":"$/keepAlive","params":{}}    52
15:36:51.350
{"jsonrpc":"2.0","method":"$/keepAlive","params":{}}    52
15:36:56.350
{"jsonrpc":"2.0","method":"$/lean/rpc/keepAlive","params":{"uri":"file:///Tutorial/5","sessionId":"15328810329659425578"}}  122
15:36:57.216

Alexander Bentkamp (Dec 24 2023 at 21:42):

Thanks, it doesnt help me as much as I thought. We'll have to see.

Alexander Bentkamp (Dec 24 2023 at 21:43):

Maybe switching to editor mode and back will give you a faster way to get unstuck?

Andrea Bourque (Dec 24 2023 at 22:02):

Of course, now it isn't happening to me...

Andrea Bourque (Dec 24 2023 at 22:06):

Spoke too soon. Yep that works

Alexander Bentkamp said:

Maybe switching to editor mode and back will give you a faster way to get unstuck?

Jon Eugster (Dec 25 2023 at 13:51):

Julian Berman said:

You're right that that's a bit unfortunate. I'm not sure if there's intention (or a technical way) to fix it, I think it has to do with using hash routing with React -- though maybe still there's a way to properly have those be indexed as separate pages, clearly they're being looked at...

EDIT: Actually I think maybe it's that https://github.com/leanprover-community/lean4game needs a sitemap?

I created an issue lean4game#178. If anybody knows exactly what to do to get the content of the landing page https://adam.math.hhu.de better visibility on google, I'd be happy to hear. Otherwise I'll have to do a quick read in the new year

Alexander Bentkamp (Dec 25 2023 at 13:54):

Updating Wikipedia would help

Julian Berman (Dec 25 2023 at 14:49):

@Jon Eugster thanks! I meant do so myself after that message but it slipped my mind. A quick google yesterday I think found one or two vite plugins that looked like they'd generate one automatically.

If anybody knows exactly what to do to get the content of the landing page https://adam.math.hhu.de better visibility on google

If you haven't already I'd sign your domain up for Google Search console thingy (the technical term). Basically you need to verify domain ownership via a DNS record and then you'll get some stats from Google. The instructions are...

Julian Berman (Dec 25 2023 at 14:50):

https://support.google.com/webmasters/topic/9455938?hl=en&ref_topic=4558844&sjid=10061958421070178963-NA and more specifically go to https://search.google.com/search-console

Last updated: May 02 2025 at 03:31 UTC