Build setup under elan proposal

Stream: lean4 dev

[Sebastian Ullrich]

Jannis Limperg said:

If you want to build Lean without Nix, you need overrides for the stage0/stage1 toolchains.

There's no reason we couldn't use lean-toolchain for that though

[Jannis Limperg]

Sure sure. This would even remove one manual step from the build process, which would be nice. Other than that, I don't think I've ever used overrides for anything.

[Sebastian Ullrich]

Note that strictly speaking it's not the build but the editor setup that needs this step

[Arthur Paulino]

+1 to disabling overrides then (I've never used it so I have nothing against this proposal)

[Sebastian Ullrich]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rethinking.20elan.20toolchain.20management

[Gabriel Ebner]

There's no reason we couldn't use lean-toolchain for that though

What is the concrete proposal here? Add lean-toolchain to .gitignore? Hard-code a "well-known" 🚲🏠 toolchain name for "the" local Lean 4 build? Support relative paths in lean-toolchain (and hardcode the build/release/stage1 path)?

[Gabriel Ebner]

And how would you switch between stage0 and stage1?

[Gabriel Ebner]

FWIW, I use env ELAN_TOOLCHAIN=4stage0 nvim for that.

[Sebastian Ullrich]

"Well-known toolchain name" sounds perfectly fine to me, I wouldn't be surprised if no-one ever deviated from the suggestions in the manual. The current instructions would be covered by one lean-toolchain in / and one in /src, are you thinking of a different workflow when talking about switching?

[Gabriel Ebner]

My workflow is from before the manual had this section. :smile: I usually use the stage1 build for src/ as well, but I don't mind changing that.

[Gabriel Ebner]

What's more painful though is that I usually have several lean checkouts (for long-running branches, upstream, etc.) and they obviously all have different toolchain names.

[Sebastian Ullrich]

I see. It shows that I haven't actually used the elan setup in a long time :) . But if you've already created separate toolchain names in this case, I'm assuming setting them in the lean-toolchain files would not be particularly more work than installing the overrides. Would having the changed files show up in git status be annoying?

[Sebastian Ullrich]

However I'm warming up to the idea of supporting relative paths and hard-coding build/release; it doesn't seem more controversial or harder to change locally than hard-coding the toolchain names.

[Gabriel Ebner]

Would having the changed files show up in git status be annoying?

Yes, very much because it breaks git commit -a. If we're going to remove elan override, then I'd prefer not to have lean-toolchain files checked into Lean core at all. (Or we support lean-toolchain.override files.)

[Arthur Paulino]

I think this discussion would be better placed in the thread Sebastian started in #general for more visibility and archiving organization

[Notification Bot]

15 messages were moved here from #mathlib4 > lake exe cache get by Sebastian Ullrich.

[Sebastian Ullrich]

Let's continue here in the dev channel

[Jannis Limperg]

I feel like relative paths in lean-toolchain are the obvious solution for Lean itself. Then you can have /lean-toolchain with ./build/release/stage1 and /src/lean-toolchain with ./build/release/stage0.

[Mac Malone]

Sebastian Ullrich said:

However I'm warming up to the idea of supporting relative paths and hard-coding build/release; it doesn't seem more controversial or harder to change locally than hard-coding the toolchain names.

I can personally attested to have used many different build directories including debug, gcc-release, clang-release, clang-debug at various points when I sometimes had to debug windows builds on my machine to see what was wrong with my build configuration and/or lean.

[Sebastian Ullrich]

You can still change the lean-toolchain file, it's not more work than changing the override

[Sebastian Ullrich]

And again, this does not affect building, only editing

[Mac Malone]

@Sebastian Ullrich True, but that has the same problem @Gabriel Ebner mentioned of annoyingly breaking git commit -a.

[Mac Malone]

I think his suggestion of lean-toolchain.override would be the best solution.

[Mac Malone]

It allows users to override the Git-sensitive lean-toolchain in a non Git-sensitive manner. which is pretty much the primary utility of elan override atm.

[Mac Malone]

It also has the advantage of being more visible than the current elan override.

[Sebastian Ullrich]

And people will remember to remove that untracked file when they finish their experiment?

[Sebastian Ullrich]

I'm a bit surprised about how many developers use git from the cmdline, but I don't mind giving people the choice between dirty file or untracked file