Best practice for using Lean on Android devices

Stream: general

[Yijun Yuan]

Now I'm on an academic travelling, and what I have on hand is an android tablet. As far as I know, there are 3 ways to use lean on this tablet:

1. Lean 4 Web Extremely easy to use, but unstable, unable to do version controlling.
2. Cloud-based solution, like Github Workspace. Seems to be easy to use, but need to install the lean toolchain (I never tried it).
3. Local installation. It seems that Lean (elan, lake, ...) is not directly available for Termux environment , and I have to install it in the Ubuntu environment by proot. However, the performance of proot container is really bad. Lean is very laggy. It seems that there is a native Linux Terminal in Android 15 by Google, but unfortunately, my Xiaomi pad does not have that.

So, what's your opinion? I believe this will also benifit others.

[Julian Berman]

Yeah the native terminal from #general > Lean on Android is what I use. Are you sure you don't have it -- note it does require being enabled in the developer options for you to see it

[Julian Berman]

Otherwise I'd recommend just using any remote solution. Codespaces if you like it, SSHing or connecting to some computer you have elsewhere, etc.

[Yijun Yuan]

Julian Berman said:

Yeah the native terminal from #general > Lean on Android is what I use. Are you sure you don't have it -- note it does require being enabled in the developer options for you to see it

Well... I'm pretty sure. Xiaomi have modified a lot to the system