Lean 3.8 wasm

Stream: general

[Kevin Buzzard]

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]

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

[Scott Morrison]

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

[Scott Morrison]

also has daily builds

[Scott Morrison]

(which I think keep track of mathlib master)

[Kevin Buzzard]

Many thanks both!

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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]

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

[Kenny Lau]

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

[Kevin Buzzard]

They came at the same time.

[Kevin Buzzard]

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.