Lean 4 installation on Android

Stream: general

[Zhouhang Mᴀᴏ]

Hello, all. I wonder how to install Lean 4 without elan? I am trying to install it on Termux, where elan does not seem to work.

[Ruben Van de Velde]

I don't know, but I know that it'll be a lot more painful than trying to find a way to use elan

[Zhouhang Mᴀᴏ]

Termux is a CLI environment on Android. I would like to install Lean 4 on that.

[Eric Wieser]

What goes wrong when you try and install elan?

[Zhouhang Mᴀᴏ]

The error message does not seem to be informative. It says that resolving hostname github.com failed. I tried to cargo build elan, which fails as well. I see that elan is a fork of rustup, and rustup does not work on Termux either.

[Bulhwi Cha]

I'm trying to install Git on Termux first.

[Bulhwi Cha]

I can't download the elan-init.sh script file.

~ $ curl https://raw.githubusercontent.com/leanprover/elan-init.sh -sSf | sh
curl: (22) The requested URL returned error: 400

[Zhouhang Mᴀᴏ]

git is installed.

[Bulhwi Cha]

I'm trying to find a way to use curl or wget on Termux.

[Zhouhang Mᴀᴏ]

curl and wget work.

[Bulhwi Cha]

Bulhwi Cha said:

I can't download the elan-init.sh script file.

~ $ curl https://raw.githubusercontent.com/leanprover/elan-init.sh -sSf | sh
curl: (22) The requested URL returned error: 400

Do you get this error message?

[Zhouhang Mᴀᴏ]

Bulhwi Cha said:

I can't download the elan-init.sh script file.

~ $ curl https://raw.githubusercontent.com/leanprover/elan-init.sh -sSf | sh
curl: (22) The requested URL returned error: 400

The issue of this is that it is trying to download -aarch-android or something like this, which does not exist.

[Zhouhang Mᴀᴏ]

I download it manually instead.

[Bulhwi Cha]

I'll try it.

[Zhouhang Mᴀᴏ]

Namely, elan-aarch64-unknown-linux-gnu.tar.gz

[Bulhwi Cha]

I forgot to turn off Tor. :sweat_smile:

[Matthew Ballard]

It doesn’t address the question at hand but let me suggest using tailscale + Termux for a better experience. I do this on iPadOS (essentially) and am pretty happy with the ergonomics.

[Julian Berman]

It's been a few months since I tried, but I don't believe even if you get elan working that the published builds will work for you in Termux. I ended up compiling Lean manually within Termux, though note doing so requires manually editing a few of the CMake build files (because something is wrong with the -fPIC configuration on Android).

[Bulhwi Cha]

Bulhwi Cha said:

I forgot to turn off Tor. :sweat_smile:

Hmm, but I still can't get the script file when using curl.

[Zhouhang Mᴀᴏ]

Bulhwi Cha said:

Bulhwi Cha said:

I forgot to turn off Tor. :sweat_smile:

Hmm, but I still can't get the script file when using curl.

As I said, the real reason is that this script reads the architecture and the OS info, and produce a URL for elan which does not exist.

[Bulhwi Cha]

Julian Berman said:

It's been a few months since I tried, but I don't believe even if you get elan working that the published builds will work for you in Termux. I ended up compiling Lean manually within Termux, though note doing so requires manually editing a few of the CMake build files (because something is wrong with the -fPIC configuration on Android).

Well then, I guess I'll use Termux for other things!

[Bulhwi Cha]

Zhouhang Mᴀᴏ said:

As I said, the real reason is that this script reads the architecture and the OS info, and produce a URL for elan which does not exist.

I see. Thanks for the info.

[Zhouhang Mᴀᴏ]

Julian Berman said:

It's been a few months since I tried, but I don't believe even if you get elan working that the published builds will work for you in Termux. I ended up compiling Lean manually within Termux, though note doing so requires manually editing a few of the CMake build files (because something is wrong with the -fPIC configuration on Android).

Do you have a log for that? If this is the case, then it might be reasonable to request a package in Termux (with these files patched).

[Bulhwi Cha]

Do you want to request it from the Lean FRO?

[Zhouhang Mᴀᴏ]

It is about packaging. I would request on Termux-packages

[Bulhwi Cha]

But would they want to do it?

[Julian Berman]

Zhouhang Mᴀᴏ said:

Julian Berman said:

It's been a few months since I tried, but I don't believe even if you get elan working that the published builds will work for you in Termux. I ended up compiling Lean manually within Termux, though note doing so requires manually editing a few of the CMake build files (because something is wrong with the -fPIC configuration on Android).

Do you have a log for that? If this is the case, then it might be reasonable to request a package in Termux (with these files patched).

No, not at hand, but I'll try to keep it around next time I do so. If I knew more about CMake I'd know why/how the 2-layer build Lean uses "breaks" the usual way CMake has for doing this (which AFAIK is -DCMAKE_POSITION_INDEPENDENT_CODE=ON or the equivalent set()) but if you just pass that option, the compilation will succeed until it tries to link things and then it will complain that the .sos are not all PIC.

[Zhouhang Mᴀᴏ]

They might not do this, but as long as our instruction of packaging are clearer, the probability that they would package this will increase. That is why I would ask for a log for some successful compilation.

[Bulhwi Cha]

I think we should first improve the documentation about how to make packages for Lean. It seems you're interested in doing so.

[Bulhwi Cha]

By the way, I failed to use cargo to build elan from its source.

[Zhouhang Mᴀᴏ]

Bulhwi Cha said:

By the way, I failed to use cargo to build elan from its source.

I succeeded. You might try cargo update first, and run this again?

[Bulhwi Cha]

Hmm, I still got an error. Please wait a moment. I'll show you the build process.

[Bulhwi Cha]

https://paste.sr.ht/~chabulhwi/51dd8e0c92f64d87c4b8742c7c777ac6af2eec17

[Bulhwi Cha]

Perhaps the version of Rust installed on my Termux is too old.

[Zhouhang Mᴀᴏ]

pkg update && apt upgrade?

[Bulhwi Cha]

I've already done it.

[Zhouhang Mᴀᴏ]

Julian Berman said:

It's been a few months since I tried, but I don't believe even if you get elan working that the published builds will work for you in Termux. I ended up compiling Lean manually within Termux, though note doing so requires manually editing a few of the CMake build files (because something is wrong with the -fPIC configuration on Android).

I requested at https://github.com/termux/termux-packages/issues/21923 and you could comment there.

[Kim Morrison]

Please please please do not ask package repositories to package Lean.

All this does is provides users with broken experiences. Lean is only intended for use via elan, otherwise you will never have the right version for a given project. If package repositories bundle a particular version of Lean, this doesn't happen. I have spent enough time in the past asking package repositories to deprecate or remove Lean, let's not do more of this.

[Zhouhang Mᴀᴏ]

elan does not work under Termux for unknown reasons.

[Kim Morrison]

I'd suggest working on that, then.

[Zhouhang Mᴀᴏ]

The minor issue that I encountered is issues on resolving github.com. I guess that it is because some libraries are not correctly linked. A major issue is that elan downloads pre-built binaries of Lean which is not linked against correct libraries (not the Termux ones).

[Bulhwi Cha]

From https://github.com/termux/termux-packages/issues/21923#issuecomment-2427841270:

You might still be able to use it on Termux through a Proot environment
(i.e. proot-distro https://github.com/termux/proot-distro)
But I have neither tested nor validated that option, and it would entail some overhead from Proot.

I've just installed elan and the current stable version of Lean on Arch Linux ARM provided by PRoot Distro.

[Bulhwi Cha]

Now, what can I do with Lean on Termux? :sweat_smile:

[Zhouhang Mᴀᴏ]

Bulhwi Cha said:

From https://github.com/termux/termux-packages/issues/21923#issuecomment-2427841270:

You might still be able to use it on Termux through a Proot environment
(i.e. proot-distro https://github.com/termux/proot-distro)
But I have neither tested nor validated that option, and it would entail some overhead from Proot.

I've just installed elan and the current stable version of Lean on Arch Linux ARM provided by PRoot Distro.

Thanks for the information. However, my device is not that performant, and I would not try that (I previously installed proot distro, and then found it too laggy and dropped).

[Bulhwi Cha]

I use Galaxy S10 5G, which was released in 2019.

[Zhouhang Mᴀᴏ]

Bulhwi Cha said:

Now, what can I do with Lean on Termux? :sweat_smile:

It is just like a computer. I am using a tablet, which is lighter than my laptop, and it is easier for me to carry it everywhere than to carry a laptop.

[Zhouhang Mᴀᴏ]

You can try to install VSCode on a proot distro, but I suspect that it would be too slow.

[Jon Eugster]

This thread sparked an idea in me, would people apprechiate a Lean-Android-App which could be downloaded through play store?

I might not have enouh time but most likely the knowledge to create one...

If so, what would be features which would make such an app useful? What are the potential use cases?

[Bulhwi Cha]

An Android app powered by Lean, which provides a user interface similar to Carnap? The video game I want to create first is kind of a Linux desktop version of it.

[Kevin Buzzard]

I was running lean 3 on (rooted) android in 2017 before I had a laptop :-)

[Kevin Buzzard]

Emacs in a terminal window and none of the Unicode characters showed up properly, so that's what you've got to beat :-)

[Julian Berman]

I've gone through parts of @Kevin Buzzard's formalizing mathematics repo in lean.nvim on Android on train rides. It was honestly quite fun.

A serious suggestion for such an app would perhaps be a learning app where one could play NNG and/or read #mil and interactively go through them, ideally even offline which is where running Lean on device would come in.

[Julian Berman]

Perhaps an even grander vision would be a general app for reading Verso texts comfortably, given it's the presumed future of all interactive Lean prose content.