search

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
292 stars 73 forks source link

Lean server fails to initialize correctly in Safari 13.0.3 on macOS Catalina 10.15.1 #36

Closed DonaldKellett closed 4 years ago

DonaldKellett commented 4 years ago

When attempting to play the Natural Number Game in Safari 13.0.3 on macOS Catalina 10.15.1, the top-right window keeps displaying "Lean is busy ..." indefinitely (i.e. after a substantial period of time, e.g. 15 seconds):

螢幕截圖 2019-12-05 13 13 27

Performing "Inspect Element" on the webpage reveals that the Lean server is not correctly initialized - even though the console message states that the Lean server is initialized:

螢幕截圖 2019-12-05 13 13 14

... the error messages reveal that a number of Promise-related errors/exceptions are thrown:

螢幕截圖 2019-12-05 13 13 18

bryangingechen commented 4 years ago

This is a known issue. Safari 13 unfortunately has a regression that prevents the WebAssembly from running. I agree it would be good to warn users about this somewhere.

bryangingechen commented 4 years ago

It looks like Safari 13.1 has fixed the issue that caused the browser version of Lean not to work. (At least it's working for me ..)

DonaldKellett commented 4 years ago

I currently have Safari version 13.0.5. Once I update to Safari 13.1, I'll remember to check out NNG again to confirm the fix.

kbuzzard commented 4 years ago

Thanks for this -- I've put some comments on the intro page.