talking to Lean from javascript?

Stream: general

[Scott Morrison]

Hi all (perhaps @Bryan Gin-ge Chen and/or @Edward Ayers specifically?)

What is the current state of calling Lean from javascript? Say I wanted to create a webpage that did not show a text editor at all, but some other interface, but I wanted to make calls to Lean under the hood. Is this possible? Is there some lean.js I can add in a script tag and do something with?

Is it possible to do this in a way that would work both in a standalone webpage, and in a widget in VSCode?

[Edward Ayers]

So the current model of widgets is that the logic and html are entirely done in lean and are connected to specific point in the lean source document. So I think what you are describing could be done with a modified version of widgets but probably not with what is there right now. idk if there is a way of directly getting values from the Lean VM using lean.js

[Scott Morrison]

So @Edward Ayers, does this mean that running javascript in a widget that then talks to the server API is currently out of scope?

[Edward Ayers]

yes that's right. Once you are in a widget all of the UI logic etc has to be written in Lean

[Edward Ayers]

I guess you could make the entire webapp as a widget

[Edward Ayers]

But then you wouldn't be able to use javascript libraries

[Edward Ayers]

I think for your use case it would be more useful to have an api where javascript communicates with lean and idk if that exists currently

[Edward Ayers]

When I made widgets the purpose was for inserting little bits of interactive UI without having to manage lean, C++, javascript every time you change something. It might be possible one day to build a full web app in lean but that's out of scope for me rn.

[Bryan Gin-ge Chen]

Yes, it's possible, but it's a bit more complicated at the moment than using just a <script> tag.

Here's a quick demo I just whipped together from a test file in my fork of lean-client-js-browser:

https://bl.ocks.org/bryangingechen/5dd3910365d477dc01fc5c3577d96278/f871317dc4d4468a3e28ecbc513cf5d98f3efb91

Basically, I've packaged lean-client-js-browser into a "UMD module" and then loading it asynchronously using d3-require. I'm using the same leanBrowser.js UMD module in my Observable notebooks. Happy to expand on anything above or to help out with any project you have in mind.

I don't think there's an easy way to do it in both a webpage and a widget in VS Code yet, but maybe @Edward Ayers has some ideas...

[Bryan Gin-ge Chen]

Ah, I didn't see Ed's message when I was responding since I was focused on the "Mentions" stream. My answer above addresses only "What is the current state of calling Lean from javascript? Say I wanted to create a webpage that did not show a text editor at all, but some other interface, but I wanted to make calls to Lean under the hood. Is this possible?"