When I open Proposition world[0] in chromium chromium-88.0.4324.150 I get the errors below in javascript console and a permanent "Lean is busy..." in the upper right corner of the page. The same page works in firefox on OpenBSD.
Do we disable something in the port that Lean requires? [0] http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=1 DevTools failed to load SourceMap: Could not load content for http://wwwf.imperial.ac.uk/~buzzard/xena/min-maps/vs/loader.js.map: HTTP error: status code 404, net::ERR_HTTP_RESPONSE_CODE_FAILURE DevTools failed to load SourceMap: Could not load content for http://wwwf.imperial.ac.uk/~buzzard/xena/min-maps/vs/editor/editor.main.nls.js.map: HTTP error: status code 404, net::ERR_HTTP_RESPONSE_CODE_FAILURE DevTools failed to load SourceMap: Could not load content for http://wwwf.imperial.ac.uk/~buzzard/xena/min-maps/vs/editor/editor.main.js.map: HTTP error: status code 404, net::ERR_HTTP_RESPONSE_CODE_FAILURE 2cb95188232511bdb78a.worker.js:8 downloading lean... interactive.js:45 error: {error: "unrelated", message: "{"response":"webworker-error","error":{"error":"co…an: ReferenceError: WebAssembly is not defined"}}"}error: "unrelated"message: "{"response":"webworker-error","error":{"error":"connect","message":"could not start emscripten version of lean: ReferenceError: WebAssembly is not defined"}}"__proto__: constructor: ƒ Object()hasOwnProperty: ƒ hasOwnProperty()isPrototypeOf: ƒ isPrototypeOf()propertyIsEnumerable: ƒ propertyIsEnumerable()toLocaleString: ƒ toLocaleString()toString: ƒ toString()valueOf: ƒ valueOf()__defineGetter__: ƒ __defineGetter__()__defineSetter__: ƒ __defineSetter__()__lookupGetter__: ƒ __lookupGetter__()__lookupSetter__: ƒ __lookupSetter__()get __proto__: ƒ __proto__()arguments: (...)caller: (...)length: 0name: "get __proto__"__proto__: ƒ ()[[Scopes]]: Scopes[0]set __proto__: ƒ __proto__() lean_js_js.js:1 Uncaught (in promise) ReferenceError: WebAssembly is not defined at Object.Module.asm (lean_js_js.js:1) at lean_js_js.js:1 at 2cb95188232511bdb78a.worker.js:8 at new Promise (<anonymous>) at r (2cb95188232511bdb78a.worker.js:8) at Object.e.loadJsOrWasm (2cb95188232511bdb78a.worker.js:8) at e.InProcessTransport.loadJs (2cb95188232511bdb78a.worker.js:8) at e.InProcessTransport.<anonymous> (2cb95188232511bdb78a.worker.js:8) at Generator.next (<anonymous>) at 2cb95188232511bdb78a.worker.js:8 Module.asm @ lean_js_js.js:1 (anonymous) @ lean_js_js.js:1 (anonymous) @ 2cb95188232511bdb78a.worker.js:8 r @ 2cb95188232511bdb78a.worker.js:8 e.loadJsOrWasm @ 2cb95188232511bdb78a.worker.js:8 (anonymous) @ 2cb95188232511bdb78a.worker.js:8 (anonymous) @ 2cb95188232511bdb78a.worker.js:8 (anonymous) @ 2cb95188232511bdb78a.worker.js:8 n @ 2cb95188232511bdb78a.worker.js:8 init @ 2cb95188232511bdb78a.worker.js:8 connect @ 2cb95188232511bdb78a.worker.js:8 onmessage @ 2cb95188232511bdb78a.worker.js:8 Promise.then (async) send @ 2cb95188232511bdb78a.worker.js:8 onmessage @ 2cb95188232511bdb78a.worker.js:8 DevTools failed to load SourceMap: Could not load content for http://wwwf.imperial.ac.uk/~buzzard/xena/min-maps/vs/base/worker/workerMain.js.map: Fetch through target failed: Target not supported; Fallback: HTTP error: status code 404, net::ERR_HTTP_RESPONSE_CODE_FAILURE