Building problem with not an object

Stream: lean4

[Heime]

I am building with

mkdir -p bld
cd bld
cmake -D CMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ ../lean4/
make

and ending up with

[ 81%] Linking CXX static library libleanrt_initial-exec.a
[ 81%] Built target leanrt_initial-exec
[ 81%] Built target Init_shared
[ ] Building /home/lean/lean4/bld/stage0/lib/lean/libleanshared.so
/usr/bin/ld: /home/lean/lean4/bld/stage0/lib/lean/libLean.a: member /home/lean/lean4/bld/stage0/lib/lean/libLean.a(FunInd.o) in archive is not an object
collect2: error: ldreturned 1 exit status
make[6]: *** [/home/lean/lean4/bld/stage0/stdlib.make:67: /home/lean/lean4/bld/stage0/lib/lean/libleanshared.so] Error 1
make[5]: *** [CMakeFiles/leanshared.dir/build.make:70: CMakeFiles/leanshared] Error 2
make[4]: *** [CMakeFiles/Makefile2:1079: CMakeFiles/leanshared.dir/all] Error 2
make[3]: *** [Makefile:146: all] Error 2
make[2]: *** [CMakeFiles/stage0.dir/build.make:86: stage0-prefix/src/stage0-stamp/stage0-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:91: CMakeFiles/stage0.dir/all] Error 2
make: *** [Makefile:136: all] Error 2

[Kim Morrison]

Have you tried with the recommended built steps?

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

Please do this first, and confirm you can successfully do this on your system, before asking questions about alternative ways to build.

[Kim Morrison]

The system requirements for these steps are described at https://lean-lang.org/lean4/doc/make/index.html.

[Heime]

It is strange for one to get the source code from github, and then having to do a git clone anyway. It completed stage1 and built the target stage1. Then what ?

[Utensil Song]

DA099CB6-EFDF-486A-9824-0521C6DA3764.jpg

https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan

[Heime]

I do not understand what the procedure is from the link provided.

[Utensil Song]

elan is for conveniently switching between lean versions. The procedure essentially installs elan, then link lean to your built lean. These Internet-depending Web-first binary-trusting steps are for the convenience of general users. They can also be easily converted to local-only plain-text self-build-as-much-as-possible steps by an experienced developer who had fought with building different building styles of software. Then for usage in a space station, everything can be packed, including all dependencies. But it's probably a different distribution to maintain.

[Heime]

I am trying to install and use the version currently on github. What would be the commands left to do?

[Utensil Song]

Those steps on the dev setup page in the screenshot and the link I posted. 3 commands.

[Heime]

Have followed the instructions on https://lean-lang.org/lean4/doc/make/index.html

Then I install elan. But what is this stage thing and what to do exactly. The wording is not clear.

[Utensil Song]

Explained here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Build.20instructions.20refer.20to.20website/near/43657078

[Heime]

After doing "make", what have I achieved ?

[Utensil Song]

Congratulations, you have built both stage0 lean and stage1 lean, the latter can be used as the working lean, by linking it to elan.

[Heime]

There is also stage2 and stage3. What are those ?

[Heime]

So first I get the source code from github, then again a new git clone. But then, instead of downloading those, one uses the Lean version manager elan instead. Did Tolkien work on this idea ???

[Kim Morrison]

I assumed it was sufficiently obvious that there is no need to make a second clone.

[Heime]

Perhaps, but not from reading the material. It is very confusing. It is not clear whether one needs the git version because of the --recurse-submodules option.

[Utensil Song]

For users who can't figure out how to handle git submodules themselves, it's safer to use just this one step to get the git repo and all submodules. Or there could be a million ways to go wrong with local setup and painful to debug remotely from Zulip.

[Heime]

Anyway, after the make command. it does not seem that elan should be used. Downloading directly the code from github, is that same as git clone with --recurse-submodules ?

[Utensil Song]

Not the same.

[Utensil Song]

The doc explained why it's not preferred to use make install as other projects, because usually one works with multiple Lean projects with multiple Lean versions.

[Utensil Song]

My humble suggestion is to learn things with an open mind like an empty cup. Follow things as they are, gradually figure why and how to improve. Admittedly the manual is not big-blue-button clear about everything, but what's stopping the learning in these chats is a priori knowledge about how things should be, but this is a diverse world.

[Heime]

That is what I am saying - not the same. One can still produce the target in some local tree though.

[Heime]

Some considered my comments harsh, but they may have some validity. Would it not be easier if this a-priori knowledge is written down though ?

[Heime]

Or is it only me who is asking these questions ?

[Utensil Song]

By a priori knowledge I'm refering to what's already in one's mind before learning a new thing. And it's stopping the learning in my metaphor, not the other way around.

[Heime]

After invoking "make", how can one test an example proof ?

[Utensil Song]

After finishing elan steps, you may go back to README and find related information about how to use Lean for proofs. Or maybe you prefer to read the next chapter testing: https://lean-lang.org/lean4/doc/dev/testing.html but that's for verifying that you haven't broken Lean after modifying its source. These are different levels of the game.

[Heime]

After invoking make, one should have the target. How can a version manager be important at this stage ? The way I see things, one makes a target and runs a test on it. Absolutely no need for any version manager.

[Utensil Song]

It's not mandatory. make install , make test work as expected. It's just more productive to use elan. Lake, lean's make, will communicate with elan, the version manager, to handle the hassles for users. These building blocks of lean is part of lean, they are an ecosystem to work together to support small to large-scale lean projects. I'm sure the space station has many components, it's also not a monolithic architecture.

[Mario Carneiro]

There is no need to ever use make install and I recommend against it

[Mario Carneiro]

Believe it or not elan is useful even for development inside the lean repo because there are several versions of lean inside the repo if you follow the instructions: the most relevant versions are lean4/build/release/stage0 and lean4/build/release/stage1. You should use the former to compile the sources in src/ and the latter to compile the tests

[Mario Carneiro]

make test will automatically use the appropriate version of lean for the tests, but you will want to use the stage1 build when compiling tests manually or when using your development build on projects elsewhere on your file system

[Utensil Song]

Yes, the above is merely explaining the way Heime expects does exist, but not optimal for using Lean.

[Mario Carneiro]

You should use the elan commands

elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

described in https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan to set up links to the stage0 and stage1 compilers, and then you can use lean +lean4 ... to use the stage1 compiler anywhere

[Mario Carneiro]

Just for completeness: most of the time stage1 will compile src/ to identical C sources as stage0 would, so stage2 will end up binary-identical with stage1 and so the process converges. Rarely, there are some changes that require multiple stage0-update's to get to a fixpoint, but the master branch will normally not have such sources.

[Heime]

The approach constitutes total madness.

[Heime]

This project is failing miserably.

[Utensil Song]

It's clear now that Heime expects a traditional self-contained tar ball+plain text README/INSTALL+"make;make test;make install" experience for new users of a software, without the need of technical sophistication, not that worrying about binary security or bootstraping. But Lean uses other mechanisms to make new users feel at home, leaving building from source to people interested in Lean internals or Lean developers, assuming some technical sophistication. That's where the frustration comes from, expressed in inappropriate language.

[Arthur Paulino]

@Heime this is my last message to you.

You seem to be failing miserably at understanding the goals of the developers and users of Lean 4. That is something most decent developers wouldn't get wrong.

How can this project be failing at all if it has drawn the attention of so many mathematicians, including one of the greatest mathematicians alive today?

What you seek here is not that important for the vast majority of the users, by a large margin. And when something is not important, it won't be prioritized. People building space stations know this better than anyone.

If you're willing to help improve the experience of hundred/thousands of users by doing Lean 4 development, then you will need to do the steps you're trying to follow. And even then, following those steps is not rocket science (to your disappointment).

I've been in the software engineering industry for about 20 years. And to this day, when I have to build anything before I am able to use it, it's rather frustrating. Even when things go smoothly, I feel like I waste computer cycles and, more importantly, my own cycles - because someday I will die and I am pretty sure I won't be thinking "ah, I should have built more software on my own" in my deathbed.

People have different parameters. Yours are yours and unless you are paying for a service I don't think you have the right to demand anything. You can ask questions and, if people want to answer you, they will. But you can't demand answers either.

Honestly, I am humbled by seeing this community willing to help you even after so much insulting. It's evidence that this project is succeeding gracefully.

[Bulhwi Cha]

I don't know the inner workings of Lean or GCC, but I've built GCC myself a few times. The default configuration for a native build of GCC is to perform a 3-stage bootstrap of the compiler when make is invoked. This includes building three times the target tools for use by the compiler. See https://gcc.gnu.org/install/build.html.

Heime said:

The approach constitutes total madness.

So, I'm okay with having multiple stages of a compiler.

[Heime]

Yes, I am fine with having multiple stages of a compiler.

[Heime]

@Arthur Paulino What I am asking is not that complicated. I should be able to get clear answers, rather than more sophistication. The current intention is to provide an additional way. Perhaps not a sophisticated way as you say. I do not trust anybody's word, whether that is the greatest mathematician alive today or 3000 years ago. You have made something convenient to use. But can one trust it. In its current state, the answer is no. That is all. But then, as is customary, I see the peer pressure cropping out of the woodwork. Perelman was correct all along. for his disagreement with the organized mathematical community.

[Arthur Paulino]

Breaking my own word because I think this is important to get through and because I have my reasons to believe you're not just a troll: distrust does not justify the choice of words you often make.

One can strive for a trustless (and yet robust) setup while also being respectful. If that's really important for you and you want to help, you will have to get involved in the project and develop a good relationship with the maintainers. You will need to make sure that your plans won't interfere negatively with their daily activities (they build Lean very often... it's part of their job).

And when you get frustrated, you will need the maturity to channel your energy towards constructive actions. It will likely involve dialogue. And if you're friendly, it is likely to speed up the whole process.

Lastly, if you literally don't trust anyone's word, that's an issue of yours. You can't assume it's the case for others, especially in the context of being in a community.

[Heime]

I am in agreement on your points. Because I want to get to the point of recommending this proving system to others. These people want to do their computing in a very precise way. Convenience is secondary to them. Please see https://www.gnu.org/philosophy/when-free-software-isnt-practically-superior.html

[Heime]

Am smiling now because I am quite sure we are not much different actually. I can bet that there are people in this community that do not trust some paper proofs and have to apply their prover system for the task. Much of what we do is not about looking up or down to somebody, but convincing ourselves that what we see is actually correct. In this sense I agree with this community completely. I won't be here otherwise.

[Heime]

I used to be an honorary member of a department who did not view my use of computers favourably. For me, it was a good enough reason to leave. Has anyone had experiences like this before ?

[Heime]

Is lean good in terms of classical analysis ?

[Yaël Dillies]

Not as much as Isabelle, but people are working on it

[Heime]

I have done

make install DESTDIR=/home/enterprise/bin/ PREFIX=startrek

Which produces lake, lean, leanc and leanmake.

Is this a good thing ?

[Julian Berman]

Not particularly -- as previously covered, Lean isn't really ready for space voyage. Those are the correct binaries though.

[Heime]

Can I use them to prove an example, or to follow a tutorial ?

[Kyle Miller]

Not really -- Lean is not yet stable software, and you globally installed the bleeding-edge version. Tutorials and other projects usually assume that you have a very particular version of the Lean toolchain. If you are lucky, the tutorials will work, but for example Mathlib does not compile on the bleeding-edge version.

[Kyle Miller]

Well, actually, at least you now have a global lake, and if you have elan installed, it will automatically download the appropriate version of lean when you do lake build for a given Lean project.

[Heime]

Should having a stable version where mathlib compiles without have to do another lean build that one cannot control be a priority for the lean project ?

[Kyle Miller]

Yes, having more stability is a priority, but it's a very long project. You can consult the 5-year project roadmap: https://lean-fro.org/about/roadmap/

[Bulhwi Cha]

For now, you can compile a stable release of Lean 4 (e.g. v4.7.0) and build Std and Mathlib for it.

[Heime]

But with elan, right?

[Heime]

I could compile and make a target of it, with Std and Mathlib. For what things would such a setup be good for ? How far can one go with it as a prover system ?

[Mario Carneiro]

If you want to use mathlib, you will need a lean version which can compile mathlib. It's better to stick to stable versions in that case

[Mario Carneiro]

Note that Std/Mathlib are libraries and do not actually go in the make target or get installed anywhere global

[Mario Carneiro]

they are generally used as dependencies of your local project and built using lake

[Heime]

I am pleased with this level of discussion. A direct honest status I was got getting previously.

[Mario Carneiro]

You should use elan toolchain override in your project if you want it to ignore the lean-toolchain and use your local build. Otherwise it will attempt to download the right version (in this case, also v4.7.0) and put it in ~/.elan/toolchains

[Mario Carneiro]

FLASHING WARNING LIGHTS this is not the way most users use lean, and issues may occur for you which do not occur for others which use elan directly and make no attempt to override it

[Heime]

Does the lean version with "make install DESTDIR=something" be good enough to compile mathlib?

[Mario Carneiro]

Good enough, yes, but getting the configuration into all the right places may be tricky

[Arthur Paulino]

Heime said:

Can I use them to prove an example, or to follow a tutorial ?

If you just want to see Lean alive on your machine with the binaries you have, try the following

-- foo.lean
theorem foo : A = A := rfl

#check foo

And then

$ path-to-your-binaries/lean foo.lean
foo.{u_1} {α✝ : Sort u_1} {A : α✝} : A = A

[Mario Carneiro]

most things will, in the absence of indications to the contrary, get elan to download the stable from the internet in spite of your make install

[Heime]

Could elan be made to download whatever is necessary so that a user could build the whole thing from source ?

[Mario Carneiro]

Again, that's a feature request and elan does not currently support it to my knowledge

[Mario Carneiro]

PRs welcome

[Mario Carneiro]

You can use elan override to make it use sources and build outputs you have prepared separately, but it's far from a fully automatic process

[Mario Carneiro]

Honestly I think it would be great if elan could just do builds automatically in place of the download step, that would allow it to work even on git repos without releases

[Mario Carneiro]

But it does put an extra 30 minutes or so on the process which is not great for most users

[Mario Carneiro]

Doing a full bootstrap chain is IMO out of scope for elan though. I would expect that to be the domain of a specialized project (which I've idly considered writing a few times FYI, but never really broke ground on)

[Jannis Limperg]

Mario Carneiro said:

FLASHING WARNING LIGHTS this is not the way most users use lean, and issues may occur for you which do not occur for others which use elan directly and make no attempt to override it

I've done this a few times to test local Lean changes and it works perfectly fine in my experience.

[Matthew Ballard]

The main issue for me is forgetting I've overidden the toolchain and wondering why cache is downloading nothing

[Julian Berman]

The cache doesn't work anyhow when you compile Lean

[Julian Berman]

(Unless something's changed and I'm out of date? I haven't used it in ages)

[Mario Carneiro]

Yes, I'm referring to living with an overridden toolchain long term, not just testing local changes. The cache might work if you do things just right, but I'm not sure anyone has taken the time to figure it all out

[Jannis Limperg]

I suspect that @Heime would not want to use the cache anyway, preferring to build Mathlib locally.

[Mario Carneiro]

...fair

[Heime]

If one could build a minimally stable version, that would not be bad. Then have the ability to add other tools, libraries, to it.

[Heime]

Seems that a minimally useful version should build lean with mathlib included.

[Heime]

Free Software Licenses generally allow you to utilize caching mechanisms when building projects like Mathlib for Lean.

[Heime]

@Jannis Limperg What procedure would you suggest, as you have done it before ?

[Arthur Paulino]

@Heime have you tried this?
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Building.20problem.20with.20not.20an.20object/near/436615532

[Arthur Paulino]

elan override --help outputs helpful information

[Johan Commelin]

Heime said:

I am pleased with this level of discussion. A direct honest status I was got getting previously.

Nonsense. In earlier discussions you were being disrespectful, demanding, and you had a bad attitude.
Don't act as if we suddenly started to behave the way you always wanted. If anybody changed, it is you.

[Heime]

Fine. Congratulation on the great work that still has not got a stable version with workable functionality after 11 years. With a further 5 year plan to this project.

[Anne Baanen]

Speaking for the CoC team here: The discussion on this topic has turned non-constructive and the situation does not seem to be improving. We ask all members to take a pause from engaging here for a bit.