Installing Lean4 on Ubuntu Machine

Stream: lean4

[Heime]

How can I install Lean4 from source on a ubuntu machine ?

[Henrik Böving]

Why do you want to install from source instead of as a binary distribution?

[Heime]

Because I build myself, not from binaries of others.

[Heime]

Do Lean4 developers provide source that people can build from source as with most decent developers do on unix-like machines ?

[Arthur Paulino]

The README section is written in big h1 formatting:
https://github.com/leanprover/lean4?tab=readme-ov-file#building-from-source

[Heime]

Are you roferring to this ?

git clone https://github.com/leanprover/lean4 --recurse-submodules
cd lean4
mkdir -p build/release
cd build/release
cmake ../..
make

[Arthur Paulino]

I'm referring to the whole section from the Lean 4 manual the README points to, not just that code block

[Heime]

I just follow the Linux (Ubuntu) part

[Eric Wieser]

Note that you will be fighting an uphill battle before you even write any Lean code; you will need to:

• Select the exact version of Lean that is compatible with the math library (based on your other thread which implies you need it)
• Either build elan from source too, then configure it to find your build-from-source version, or configure the editor extension of your choice to point to your build-from-source version
• Build all of mathlib yourself (as it sounds like you will not want to download the olean "binaries" using lake exe cache get), which is very slow
• Repeat all of the above steps every time you want to update mathlib

[Eric Wieser]

All of these steps are automatic if you let elan / lake exe cache get manage them for you

[Huỳnh Trần Khanh]

I wonder why a :butterfly: is warranted here. the message looks innocuous

[Bulhwi Cha]

I concur.

[Bulhwi Cha]

Heime said:

Do Lean4 developers provide source that people can build from source as with most decent developers do on unix-like machines ?

Oh, the word "decent" here might be unnecessary. The question seems to imply that you're a less decent developer if you don't build software yourself. I don't do it all the time.

[Arthur Paulino]

The tone of the interaction was pretty weird almost from the beginning :shrug:
Even without the "decent" business, comparing developers with an awkward nuanced expectation is not polite. Especially when you're not paying for the service being provided :upside_down:

[Ralf Stephan]

Of course, there is a reason for wanting to compile, i.e. security. But then, it's easier to create a virtual sandbox, and install there the recommended way.

[Notification Bot]

Huỳnh Trần Khanh has marked this topic as resolved.

[Notification Bot]

Huỳnh Trần Khanh has marked this topic as unresolved.