Build instructions refer to website

Stream: lean4

[Heime]

Looked at the Lean source code. How is it that the information about installing Lean refers one to a website link. Rather there should be all the necessary instructions in the release itself one can look up to.

[Heime]

Can Lean be made to build with gcc rather than clang ?

[Kyle Miller]

The docs are in the repo, in the doc folder. I'm guessing you're talking about https://github.com/leanprover/lean4/blob/master/doc/setup.md, which is the source for https://lean-lang.org/lean4/doc/setup.html ?

[Kyle Miller]

There's also doc/make for https://lean-lang.org/lean4/doc/make/index.html

I'm pretty sure you select your choice of compiler by passing the appropriate option to cmake. I'm guessing cmake -D CMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ ... ? I just use the default myself.

[Heime]

Such instructions should be put in the top lean directory. There is no information on which files to read from the docs.

[Heime]

I am in the lean4 directory tree. How does one find the necessary information to build it. The information seems to be all split up in various files.

[Kyle Miller]

Building Lean from source is usually only done for the development of Lean itself, at least at the moment

[Heime]

Terribly frustrating

[Heime]

Standard ability to build from source should have been done from project start !!!

[Johan Commelin]

@Heime Please stop telling others what to do!

Also, see #butterfly

[Kyle Miller]

I saw in another thread you want to use Lean to prove theorems. Are you interested in using mathlib? If so, keep in mind that very very few mathlib users compile Lean (or mathlib for that matter!) from source themselves.

[Yaël Dillies]

This is an ongoing collaborative project.

1. (Almost) nobody is paid to work on it.
2. There are plenty of high priority issues that people are working on. Building from source Putting the source build instructions in plain sight is not currently one of them.

[Kim Morrison]

(But also, lots of us build from source every day, and the instructions are right there where Kyle has linked to them...)

[Kyle Miller]

@Yaël Dillies They're linked to right at the end of the readme, but the problem Heime seems to have is that this is a link to a web page with the rendered markdown rather than the markdown source file itself.

[Kyle Miller]

@Heime Just so you know, if you want to get started using Lean right away without trusting binaries, there's https://live.lean-lang.org/ . It's got all of mathlib available too.

[Kyle Miller]

For mathlib, a lot of the user experience is designed around getting a working VS Code, Lean VS Code extension, Lean binary, and mathlib cache ASAP. Mathematical users are almost never interested in building this from source, and the mathlib community here would rather that people not build from source because it's hard to help people debug their custom setups.

(I don't know your opinion of VS Code. I held out using emacs for awhile, but eventually VS Code was just too convenient... I still use magit frequently to prepare PRs however.)

[Heime]

Johan, That's for me to decide.

[Heime]

Not putting the source build instructions in plain sight just proves how terrible the development has been progressing.

[Heime]

Since 2013, the Gnu Project runs the computational needs of the International Space Station. WE know about building software more than anyone.

[Heime]

Good Day Kyle, Correct the problem is that one only finds a link to an online repository instead.

[Heime]

Kim. Assuming as you say that lots of you build from source every day, it should be easy to add that information. There are people who always build from source as its developers do. There should be clear instructions for that included. And the process being made easy to accomplish. If you cannot even build it, how can one expect the rest to be any good.

[Ruben Van de Velde]

Heime, I suggest you take a step back and consider whether this community and its goals align with yours

[Kim Morrison]

You keep saying that you can't build it, after having been pointed to the instructions. Are you stuck at some particular step? Please tell us where you are up to, and if you want concrete help.

[Shreyas Srinivas]

Heime said:

WE know about building software more than anyone

Who is included in "we"? As Kim says, it really helps us to help you if we know where you are stuck at when following these instructions : https://lean-lang.org/lean4/doc/make/index.html

[Arthur Paulino]

Heime, I don't know if you're understanding how your participation here comes across. If this is how you portray yourself in every open-source community, I kinda feel bad for you. You would be able to achieve much more with just the minimal level of friendliness, politeness and respect towards the work of others.

We have repeatedly tried to help you achieve what you want, even with warnings for the extra work you're signing up for. And still, you keep on bashing this project.

While we're interested in enabling you to do what you need, your standards for how software should be built and maintained are not absolute.

This community has its guidelines (which have already been presented to you: #butterfly is a clickable link!). Lean 4 is currently maintained by the Lean FRO, which has its vision and goals. If those don't sparkle your interest, again, I am sorry

[Heime]

Ruben. It is not about alignment. It is mainly people getting upset because of some criticism. Since when is building from source not important. Tell that to the actual developers and they will tell you.

[Heime]

Arthur. this is not about what I can achieve but what the lean project can achieve if it rejects the nonsense and starts looking at things the way they are.

[Johan Commelin]

@Heime Are you able to build Lean 4 from source? If not, please tell us where you are stuck.

[Shreyas Srinivas]

Heime, lean can be built from source, that is how it gets built after every PR merge. There are docs on how to build it and yes they are on a webpage. If you encounter errors there is this forum. There are exactly 0 things wrong with this.

[Eric Wieser]

I'm not sure what your yardstick is for "actual developers", but by all reasonable definitions the some of the "actual developers of lean" are amongst the people you are talking to in this thread.

[Shreyas Srinivas]

Also, if what you want are raw markdown files you can find them in the docs folder: https://github.com/leanprover/lean4/blob/master/doc%2Fsetup.md

They are not a major improvement over the webpage (quite the opposite)

[Heime]

Then I shall discuss with the Lean FRO then. It is disconcerting to say the least when the group pressures other to say only good things. I wonder what has been the experience of people wanting to build from source using the lean4 release . Was the experience fantastic ???

[Johan Commelin]

You are talking with Lean FRO employees in this thread.

[Shreyas Srinivas]

You are talking to the FRO already as Eric says. Yes I was able to build from source if that's your question. Many times.

[Johan Commelin]

@Heime Are you able to build Lean 4 from source? If not, please tell us where you are stuck.

[Kyle Miller]

Criticism is fine, and "build directions should be more obvious" is noted.

Statements about "how terrible the development has been progressing" isn't criticism though, that's just an opinion, and (in my opinion) one that is not too useful to share. This Zulip community values a more collaborative spirit than that.

[Heime]

Eric, the yardstick is to find the information that guides one on how to complete a lean build. Currently, the information does not naturally provide links that can be used effectively.

[Kyle Miller]

We're happy to help, but help us help you. What have you tried? Where are you in the process?

This is what I do when I build Lean from scratch, these six commands: https://lean-lang.org/lean4/doc/make/index.html#generic-build-instructions

[Kyle Miller]

There are also some details elsewhere for setting up elan, the toolchain manager, if you want to build mathlib too. But again, I strongly suggest that you don't go in this direction. You mentioned in another thread that you like moving fast, and this is one of the slowest ways to get started.

[Heime]

The statement mentioned was in response to the idea that instructions for users to build from source is not a priority. It is not good doing so much work but then not have clear enough guide to build from source. Any developer worth his salt knows that building from source is paramount.

[Heime]

I can work on it if the work ends up in the lean4 release. Such a guide to build from source should be in the release. I cannot see what is controversial about it.

[Shreyas Srinivas]

But it is in the release

[Kyle Miller]

There's only so much energy I'll put into trying to get you a working Lean setup: should I take it that you did figure it out and you have a working Lean setup? You haven't answered any of our questions about it yet.

[Shreyas Srinivas]

If you clone the source, open docs/setup.md you have the setup instructions right there

[Shreyas Srinivas]

If you want to build there are instructions for that as well

[Shreyas Srinivas]

https://github.com/leanprover/lean4/blob/master/doc%2Fmake%2Findex.md

[Heime]

Let me go through the process of building it. Then I can send details of how to organise the documentation better for anyone to be able to do it without need of outside help..

[Heime]

Have not managed to get a working version yet.

[Jon Eugster]

hot take, but it might be desirable if non-computer-affine beginners don't see the manual building instructions in plain side but instead are guided towards the intended installation.

And the experts (who even know that compilers exist) can probably also figure out which document a link points at if they try to work offline ;)

But yes, documentation is always a work-in-progress thing and generally PRs improving documentation are quite well-received!

[Bulhwi Cha]

Jon Eugster said:

But yes, documentation is always a work-in-progress thing and generally PRs improving documentation are quite well-received!

How about this change?

 - [FAQ](https://lean-lang.org/lean4/doc/faq.html)

+There are various Markdown documents in the `doc` subdirectory. If you prefer
+them to the formatted web pages, please see [`doc/SUMMARY.md`](doc/SUMMARY.md)
+first.

 # Installation

See https://github.com/chabulhwi/lean4/commit/de0569ad2acfe9262a6c4b1e2426b5b19f48dbaa. I haven't opened a pull request yet.

[Bulhwi Cha]

Heime said:

Kim. Assuming as you say that lots of you build from source every day, it should be easy to add that information.

Well, at least this is true. The information about building Lean is already in the doc subdirectory. We just need to let users know.

[Bulhwi Cha]

Shall I open a PR?

[Johan Commelin]

Bulhwi Cha I personally think that you should not open a PR. For 99.99% of the world, the rendered md is preferable, and the existing link sufficient.
So this extra sentence will just add clutter.
Again, personal opinion. Ultimately up to the FRO.

[Bulhwi Cha]

Johan Commelin said:

For 99.99% of the world,

Um, there's no need to exaggerate. Otherwise, I get your point.

[Bulhwi Cha]

From https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/README?h=v6.9-rc6:

README

Linux kernel
============

There are several guides for kernel developers and users. These guides can
be rendered in a number of formats, like HTML and PDF. Please read
Documentation/admin-guide/README.rst first.

In order to build the documentation, use make htmldocs or
make pdfdocs. The formatted documentation can also be read online at:

https://www.kernel.org/doc/html/latest/

There are various text files in the Documentation/ subdirectory,
several of them using the reStructuredText markup notation.

Please read the Documentation/process/changes.rst file, as it contains the
requirements for building and running the kernel, and information about
the problems which may result by upgrading your kernel.

In my opinion, it's a good idea to add information about the files in the doc subdirectory. The Linux kernel project did inform kernel developers and users about it.

You can navigate the documentation conveniently in VS Code if you open and preview the doc/SUMMARY.md file. I haven't noticed this until now.

20240501_14h48m20s_grim.png

[Kim Morrison]

I agree that this paragraph is not an improvement, sorry.

[Bulhwi Cha]

Fair enough. Although I'm having more disagreements with the Lean FRO and the Mathlib maintainers day by day, I agree that you have the final say.

[Heime]

One should really provide outputs in various formats far the taste of various users.

[Julian Berman]

It's fairly trivial to convert markdown into whatever else one likes, or to ignore it and make believe it's a text file which is likely what someone who wants "I have the source code now what" is going to do. As a user and not an FRO member I have to respectfully say out of all the things underdocumented in Lean (and in general all the work to do) that to me this seems incredibly low on the list personally. I have been in this situation of "how do I compile this again" and I really can't say it took me longer than a few minutes to find the relevant file -- Lean is definitely (conservatively) in the upper quartile for me of software I've had to compile in terms of "how easy is this to figure out". You'll again note above though that others have mentioned that concrete suggested improvements are likely welcome, though you seem not to be taking the hint there.

[Heime]

The standard procedure is to have the information explained in the readme. But somehow people do not want to follow that. Actually, I feel silly telling you all this. I'm sure tho FRO would have investigated the matter. I will do it only because if I do not do this, it will never get done.

[Julian Berman]

There are many standard procedures in open source for this. You come from only one of them, though one indeed common where your intended audience is likely to compile your software by hand.

[Heime]

That's right, for those who compile directly and only from source.

[Joachim Breitner]

If your goal is to only use software that can be built entirely from source (defined as “preferred form of modification”) then I fear you'll have to stay away from lean, as it is a bootstrapping compiler, and you cannot build lean without a pre-built form of the lean compiler. The repository contains a pre-built copy of the lean compiler (compiled to C) to get started, but it won't ever satisfy a strict requirement “must be built directly and only from source”. Sorry for having to break that to you, if that means that lean cannot be of interest to you.

[Heime]

If that is how the bright people in the FRO build the software, we at the GNU Project are not impressed. Quite dishonest to then make the users believe the software abides by the Gnu General Public License.

[Joachim Breitner]

I fully agree that it would be very dishonest to make anyone believe that the software abides by the GPL!
It would be a bit less dishonest to make the software believe that the user abide by the GPL…
(I rarely saw software abiding or not abiding a license. Although, who knows, these days with LLMS…)
But even that would be a bit off the truth, given that we expect our users to abide the Apache 2.0 licence.

[Damiano Testa]

This discussion is fascinating: what does it mean to "build from source"?

[Joachim Breitner]

https://bootstrappable.org/ gives an answer which sets a high bar that we will have trouble to reach, unfortunately. My stage0-audit project (https://lean-stage0.nomeata.de/) tries to help a bit in that direction, with little hope to closing the loop.

[Arthur Paulino]

Heime, with all due respect, I don't think impressing "you at the GNU Project" is a top priority item in the Lean FRO list. Maybe 3rd or 4th is you're lucky though

[Heime]

Felicitations Damiano. Building from source means building from Source Code - the preferred form for modifying it by ids developers; the compacted code is not source code.

[Eric Wieser]

How exactly do you assemble your source code into a binary though using only more source code? Sounds quite hard if you don't allow yourself to use "compacted code" of any kind.

[Joachim Breitner]

The guix project can bootstrap from a very small (357 bytes) binary. It’s fascinating! (much more than this thread in a way)
https://guix.gnu.org/en/blog/2023/the-full-source-bootstrap-building-from-source-all-the-way-down/ is a possible entrypoint if you want to learn more about this.

[Damiano Testa]

So, without wanting to appear sarcastic, "building from source code" still means bootstrapping, but with a "small" initial compiler?

[Joachim Breitner]

Depends on who you ask, I think. The lean developers, or the bootstrappable builds project?
For lean building from source uses a non-small pre-existing compiler that's (partially) compiled.
For the bootstrappable builds project it starts with a very small initial assembler of sorts.

[Arthur Paulino]

Building from source means that you're God, The Source Itself, and can manifest a big bang to compile the entire existence everytime you need to run a program.

I'm signing off. Good luck Heime :wave:

[Damiano Testa]

Thank you for the explanations! To be honest, I am not actually sure that I know what "compiled" even means, so I have quite a bit of reading to do to fully appreciate this discussion, but it has been very interesting! :smile:

[Arthur Paulino]

My 2c to Damiano: building from source usually means using machine code to generate more machine code from human readable code

[Julian Berman]

(Damiano if you want an overly-opinionated suggestion what you've asked is a software philosophy rabbithole, and I'd opine further one very much not worth your time to chase too far)

[Heime]

The Gnu Project demonstrated its respected position in the world as the choice for the International Space Station. As Joachim indicated, we function at a very high bar. One can use compacted code provided you have control over the source code that produces it. Fundamentally, the work should rest upon the Lean Developers.

[Joachim Breitner]

Ah, sorry for probably assuming too much background knowledge. Maybe the answer you are looking for here is this:
To get a a piece of software (like lean) you can either download a _binary_. This is a file that that you can run, but you cannot read it e.g. to see what it is doing, or change what it is doing.

It is also not how software is created. Software is typically written in some programming language (here, confusingly, also Lean, but also a piece of C++), which is then translated into the binary, machine-intelligble from by a program called the compiler.

So instead of downloading the binary you can download the source (if it is Open Source – hence the name), and compile it yourself. This way you can (at least in theory) read what the program is doing, maybe even change what it is doing.

Developers build the program from source all the time, of course. And some users do, too, out of curiosity, or because they firmly believe in the benefits of Free Software.

[Joachim Breitner]

The ISS is indeed a very high bar!

[Henrik Böving]

Damiano Testa said:

Thank you for the explanations! To be honest, I am not actually sure that I know what "compiled" even means, so I have quite a bit of reading to do to fully appreciate this discussion, but it has been very interesting! :smile:

Compilation in the most general sense means that you translate from a source into a (usually different) target language. We often say that Lean is compiled into C and from there further compiled into a binary. If you take a bigger picture you might just say that Lean is compiled into a binary. If you take a closer look you might say that Lean is compiled into some IR that is then compiled to C and so on. You could also say that the Lean elaborator is a compiler from the Lean source language to the docs#Lean.Expr kernel language.

So as you can see compilation is usually in the eye of the beholder and the context.

The current way to compile Lean from source is as follows:

• The lean4 repo contains a stage0 directory that is the C output of some previous binary Lean compiler on the Lean compiler itself (back when Lean didn't compile itself yet this contained whatever version of the Lean 3 C++ impleemtnation was first used to compile a Lean 4)
• This stage0 is then compiled using a C compiler into a binary
• This stage0 compiler is then run on the actual source code in src/ to again produce C and then ultimately a stage1 binary.

You can repeat this process ad infinitum with stage2 stage3 etc. Sometimes this is interesting to do for a developer but that is getting out of scope.

Now why are some people scared of bootstrapping: You basically put trust in the fact that stage0 (or whatever other contraption people use, we will get into that) is an implementation that does not backdoor you the binaries it produces. If you are interested in this kind of attack look up "Reflection on Trusting Trust" by Ken Thompson.

I personally think our bootstrapping process is pretty acceptable. If you bootstrap rust (https://github.com/rust-lang/rust/blob/master/INSTALL.md) you are made to download a binary Rust compiler that will fulfill essentially the role of stage0. For compiling LLVM/clang you are expected to have a fully functioning C compiler on board and even the glorious GNU gcc performs a multi stage bootstrap that expects the existence of some C compiler binary on your system to begin the procedure (https://gcc.gnu.org/install/build.html).

[Damiano Testa]

Ok, thank you all for the information! I had no idea of all these subtleties and further and further amazed at how the first computer started to work in the first place!

[Heime]

One can disable bootstrapping for GCC.

[Heime]

The first computers were women. Everything starts with a woman.

[Anne Baanen]

Speaking here for the code of conduct team. @Heime, this is a warning. We have had several reports about your behaviour in this chatroom. We want to make clear that the code of conduct forbids "Trolling, insulting or derogatory comments, and personal or political attacks". You are making a lot of demands of Lean and the community, stating from a claimed position of authority that your preferences are the only acceptable way. Your current behaviour makes useful discussion impossible. Please ensure that your contributions are constructive. Continuing in the current way will lead to a ban.

[Heime]

Commenting that the build instructions are not sufficiently usable or that the build system is defective are not attacks. Furthermore, it is the Lean Project who has claimed that one can actually build from source. I was even going to help out with the process. If you want to ban me, go right ahead. I will then certainly not recommend others to use it and will make an official statement about it.

[Bulhwi Cha]

Your phrasing wasn't appropriate.

[Bulhwi Cha]

Bulhwi Cha said:

You can navigate the documentation conveniently in VS Code if you open and preview the doc/SUMMARY.md file. I haven't noticed this until now.

When you're sharing or capturing a window, not a screen, it can be more convenient to navigate the documentation in a text editor. Otherwise, you'll have to change the window. Of course, you can just load a web page in the text editor.

Sometimes, it's better to let users choose what they want to use. But as I've said before, the maintainers have the final say.

[Mario Carneiro]

Heime said:

Building from source means building from Source Code - the preferred form for modifying it by ids developers; the compacted code is not source code.

Lean is a bootstrapping compiler, and it does not have a boostrappable path which is of reasonable length. (My understanding is that there are approximately 1000 lean compilers on the full bootstrap chain.) This is recognized as an issue, but it is very low priority, and there is no particular reason for the lean developers to be working on this to the detriment of much more important issues, as long as users are able to use lean effectively to solve their problems. I think it is important to recognize that it's possible to work on a bootstrap chain for lean independently of the lean4 repo, and I advise you to do so if you consider this issue of sufficient importance to devote your time to it. If you don't have the time for it, please understand that most other people also don't and do not have unrealistic expectations (or demands) for anything to happen here.

[Mario Carneiro]

(Speaking for myself, I think the draw of a from-source bootstrap chain is much reduced if you aren't actually reading all the sources. It's much easier to hide a bug in the actual code than some complex trusting-trust attack, and the lean compiler is huge enough that it's easy to hide a bug or two in the plain text itself. And if you can't even read one lean compiler, you can forget about reading the 1000 lean compilers that the from-source bootstrap chain gives you. You'd be better off just reading the stage0 C code directly at that point.)

[Bulhwi Cha]

I didn't know that lean4#4045 by Kyle Miller was already merged.