Zulip Chat Archive

I am playing the natural number game to try and learn about lean, but for some reason, the screen always says "lean is busy... " for all my proofs, even the ones I have previously completed and which ran fine before. I have deleted the code on the level where this problem started, and I have restarted my browser and computer. I was wondering if anyone had any guidance.

Kevin Buzzard (Dec 20 2021 at 14:13):

It might be a cookie issue? Try a different browser?

Kevin Buzzard (Dec 20 2021 at 14:13):

I should be clear here -- I have no idea what cookies are but I know that they're relevant in order to make things work. I'm listed as an author but I only wrote the Lean code; I don't know anything about the web interface.

Bryan Gin-ge Chen (Dec 20 2021 at 14:16):

If you open your browser's dev tools console, do you see any suspicious messages?

Josh Fleckner (Dec 20 2021 at 14:22):

Bryan Gin-ge Chen said:

If you open your browser's dev tools console, do you see any suspicious messages?

I see this "Failed to load resource: the server responded with a status of 404 (Not Found)"

Josh Fleckner (Dec 20 2021 at 14:23):

Kevin Buzzard said:

It might be a cookie issue? Try a different browser?

I tried it on safari and chrome to the same result. It is weird because the game itself is loading, just not when I type in anything myself. Maybe I just have poor connection.

Bryan Gin-ge Chen (Dec 20 2021 at 14:28):

Does the console message say which file was not found? If it's something like favicon.ico then that's normal.

Bryan Gin-ge Chen (Dec 20 2021 at 14:30):

I just visited https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ now and after clicking to world 2 I see something like the following in my console. Everything seems to work as expected, so this is the "normal" output:

 GET https://www.ma.imperial.ac.uk/favicon.ico [HTTP/1.1 404 Not Found 106ms]

force-graph loading 10 nodes 10 links

 downloading lean...

error: Object { error: "unrelated", message: "{\"response\":\"webworker-error\",\"error\":{\"error\":\"stderr\",\"chunk\":\"wasm streaming compile failed: TypeError: WebAssembly: Response has unsupported MIME type '' expected 'application/wasm'\"}}" }

error: Object { error: "unrelated", message: "{\"response\":\"webworker-error\",\"error\":{\"error\":\"stderr\",\"chunk\":\"falling back to ArrayBuffer instantiation\"}}" }

starting lean...

lean server initialized.