Mathlib on Raspberry Pi (i.e. arm architecture)

Stream: new members

[Daniel Jentsch]

Hello all,

I hope this is the right place to ask this. I would really appreciate if someone could help me with that.

I am trying to install the mathlib on my Raspberry Pi 3B with Raspbian. Unfortunately, the recommended installation method involves a script which tries to download another script specifically for the required architecture (which is specified via a substring of the file name it requests) which does unfortunately not exist. So I wonder, if it is possible to install the mathlib manually and if somebody could explain me how to do this.

I can give you more specific information on request, of course.

Any help is appreciated!

[Johan Commelin]

@Daniel Jentsch Interesting! But my first worry is about hardware specs. How much RAM does the RPi 3B have? Because mathlib with <= 4GB is quite terrible usually.

[Johan Commelin]

Also, does this help: https://leanprover-community.github.io/toolchain.html

[Johan Commelin]

It is a more detailed version, explaining what the 1-line-install script does

[Yaël Dillies]

Johan Commelin said:

Because mathlib with <= 4GB is quite terrible usually.

What an euphemism :upside_down:

[Daniel Jentsch]

Hi Johan! Well this might be a bottleneck indeed: It has one GB of RAM. So do you think this would be a waste of time?

[Yaël Dillies]

mathlib with 8GB is also hell sometimes.

[Johan Commelin]

@Daniel Jentsch I'm afraid 1GB cannot give you a usable setup. You might be able to play with some very basic things. But since Raspbian will probably eat at least 200 MB, there is very "little" left for lean.

[Johan Commelin]

Are you interested in programming with Lean, or in maths? And if it's maths, what kind of maths?

[Daniel Jentsch]

I want to formalize a mathematical proof for a course at university. The computer I usually use is currently not usable. So I am using this Raspberry as a substitute. I would normally wait until I will have a decent computer again, but due to the course I thought I should really get it running this month.

[Johan Commelin]

@Daniel Jentsch You might try using Lean in the sagecloud, or something like that.

[Johan Commelin]

Then you can off-load everything to a server

[Daniel Jentsch]

Can you elaborate on that?

[Kevin Buzzard]

https://cocalc.com/ (which is run by the Sage people) is a way of running Lean in the cloud. It's something like 3.10 though, if this is an issue (we're on about 3.30 now)

[Daniel Jentsch]

@Kevin Buzzard I will try that, thanks a lot! I don't think that the version is an issue. A propos the version: Does mathlib now even work with lean 4?

[Johan Commelin]

Nope, porting mathlib to Lean 4 is actively being worked on. But it will take several months (6~8?) before it is done.

[Daniel Jentsch]

Ok, thanks a lot to all of you for your help. I will try working with this sagecloud. Maybe I'll come back if I have further questions. Thanks again!

[Eric Wieser]

gitpod is also possibly a viable option, which has the advantage of working on bleeding-edge lean (or any version you like)

[Bryan Gin-ge Chen]

For gitpod, all you need to do is click on the gitpod badge in the mathlib repo readme which points to: https://gitpod.io/#https://github.com/leanprover-community/mathlib

[Eric Wieser]

It's fairly straightforward to set up on your own repo too

[Eric Wieser]

Although it has usage caps that might get in your way

[Daniel Jentsch]

@Eric Wieser @Bryan Gin-ge Chen thanks for your suggestions, I am trying to make this work right now.

[Eric Taucher]

Side question.
Since a Pi has limited ram, can LEAN run on a cluster?

[Bryan Gin-ge Chen]

I'm not sure exactly what you mean by running Lean on a cluster, but I think people have successfully used VS Code's remote-ssh functionality with the Lean 3 extension.

[Eric Taucher]

@Bryan Gin-ge Chen
By clustering I mean running LEAN on multiple RaspberryPis connected together to form a cluster. (ref).

I suspect that one processor will do most of the work (user GUI) but for the searching or compute intensive calls, I am thinking search, the call could be partitioned up and done concurrently. Here is an example I did using Prolog. The part that does the distribution of the work is done with the concurrent_forall predicate.

[Bryan Gin-ge Chen]

I don't think Lean has any built in support for something like that. But maybe it's still possible!