JS version

Stream: new members

[Gunnar Mein]

Pardon the noob question, and I realize the JS version might really be no more than a gimmick for the community here, but I am trying to use it to verify student high school algebra work. Both https://leanprover-community.github.io/lean-web-editor and https://leanprover.github.io/live/latest/ are driven by some complicated webasm loader mechanism - and then some, I mean 60KLOC of JavaScript for an editor page without the editor? - , is there a "how-to" for that anywhere?

I also had hopes for https://github.com/leanprover/lean.js, and can indeed get that to work, but it hasn't been updated in 5 years and doesn't recognize things like linarith (and possibly all things mathlib). Any pointers would be appreciated! Thanks!

[Bryan Gin-ge Chen]

The github repo for the community web editor is here: https://github.com/leanprover-community/lean-web-editor

The README has some info on getting set up, but if you have any questions, feel free to ask here.

[Gunnar Mein]

I took the liberty of following the tracks and came across this on your repo: https://github.com/bryangingechen/lean-client-js/blob/cache/lean-client-js-browser/demo.ts. Worth following as a template?

[Bryan Gin-ge Chen]

Sure, depending on what you want to do. Note that the main repo is here (I don't think there are any differences with my fork atm): https://github.com/leanprover/lean-client-js

Some projects that use lean-client-js outside of the community web editor are the natural number game (powered by the lean-game-maker) and some old Observable notebooks I made (I should check if they still work...).

[Gunnar Mein]

Ah thanks! I got to your repo because that is where fetch_lean_js.sh (exact name?) gets its files.

[Bryan Gin-ge Chen]

Yeah, for historical reasons we've been using my GitHub pages storage as a webhost. I was figuring out how JS + the web worked as I was hacking on it, so you may notice lots of other weird quirks. Suggestions / PRs welcome!

[Gunnar Mein]

Got that to work. Thanks for your help!