Local mobile app

Stream: lean4

[Geoffrey Irving]

It’s probably a lot of work for minimal advantage, but it would be cool to have a local iPhone app with a Lean 4 repl.

[Eric Wieser]

The web editor works fairly well on mobile, but I guess not without internet access

[Geoffrey Irving]

Yeah, it’s nice to have offline capabilities, though probably not nice enough to be worth it in this case.

[Eric Wieser]

Depending on your use-case, you could host your own web editor from a laptop in your backpack, and connect to a local wifi network with your mobile...

[Ruben Van de Velde]

My main issue on mobile is copying code out of it

[James Gallicchio]

Geoffrey Irving said:

Yeah, it’s nice to have offline capabilities, though probably not nice enough to be worth it in this case.

even once we have a wasm backend and can run stuff in browser, there's issues running any wasm executable that needs more than like 100MB of memory on mobile :melt:

[Geoffrey Irving]

Hmm, I thought the iOS wasm memory limit is closer to 1/2 GB. They did decrease it a while ago: I had to optimize https://perfect-pentago.net to fit under 1/2 GB, since before it used almost 1 G and started erroring out recently.

[Geoffrey Irving]

But maybe that’s different as it only uses the memory for brief spikes.

[James Gallicchio]

https://github.com/WebAssembly/design/issues/1397 I think that's just an issue with wasm memory specification ;-) you're probably not doing anything wrong

[Geoffrey Irving]

That isn’t a problem for the pentago website: I make a fresh wasm instance for each position solve, then tear it all down.

[Geoffrey Irving]

But basically: it used to work using almost 1 GB at peak, then stopped working when they tightened the limit, and now it works optimized to use slightly less than 1/2 GB. But that’s still way more than 100 MB.