Zulip Chat Archive

Stream: general

Topic: Lean 3.8 wasm


Kevin Buzzard (Apr 11 2020 at 14:41):

In the Lean Game Maker I'm told that if I want to use Lean 3.8.0 I need to get my hands on three files called lean_js_js.js, lean_js_wasm.js and lean_js_wasm.wasm. Is there an easy way to get my hands on such files?

Bryan Gin-ge Chen (Apr 11 2020 at 14:43):

Try the lean-3.8.0--browser.zip file from the Lean3 .8 release page.

Scott Morrison (Apr 11 2020 at 14:43):

https://tqft.net/lean/web-editor/

Scott Morrison (Apr 11 2020 at 14:43):

also has daily builds

Scott Morrison (Apr 11 2020 at 14:44):

(which I think keep track of mathlib master)

Kevin Buzzard (Apr 11 2020 at 14:44):

Many thanks both!

Bryan Gin-ge Chen (Apr 11 2020 at 14:44):

Oh, cool. I didn't realize the cron job was running again!

Bryan Gin-ge Chen (Apr 11 2020 at 14:45):

It looks like the files at https://tqft.net/lean/web-editor/ are still at 3.7.2c. I guess 3.8.0 came out too late last night.

Bryan Gin-ge Chen (Apr 11 2020 at 14:48):

Oh wait, I forgot that I have to update my web editor repo. I should make the scripts there smarter.

Kenny Lau (Apr 11 2020 at 14:51):

did the Lean Game Maker come first, or did the Natural Number Game come first?

Kevin Buzzard (Apr 11 2020 at 15:05):

They came at the same time.

Kevin Buzzard (Apr 11 2020 at 15:06):

That's why the web page says it's by me and Mohammad -- I wrote the Lean repo and he wrote the game maker repo.


Last updated: Dec 20 2023 at 11:08 UTC