stage0 lean uses oleans from stage1

Stream: lean4 dev

[Mario Carneiro]

When I try running lean +lean4-stage0 tests/lean/run/28.lean (on linux) it works, and does not complain about missing olean files or missing package 'Init', but the stage0/ directory contains no olean files in it. Running strace, I can see that it is very sneakily loading stage1 oleans:

openat(AT_FDCWD, "/home/mario/Documents/lean/lean4/build/release/stage0/../stage1/lib/lean/Init/Data/Stream.olean", O_RDONLY) = 3

This is being called with an empty LEAN_PATH, so who is responsible for this redirection? (I would normally be fine leaving this as is, but I'm trying to do a windows test right now and the magic trick doesn't seem to work there.)

EDIT: the trick is implemented here

[Mario Carneiro]

I think I see the issue: on windows this is resolving to C:\Users\Mario\.elan\toolchains\lean4-stage0\..\stage1\lib\lean where .elan\toolchains\lean4-stage0 is a symbolic link of some kind generated by elan, and I guess this does not resolve as intended

[Mario Carneiro]

@Mac Malone How does this behave on your machine?

[Mac Malone]

@Mario Carneiro I'm confused. What is the problem here? You mentioned that it works on Linux, but you did say not what is the error on Windows.

[Mario Carneiro]

lean +lean4-stage0 test.lean fails on windows and works on linux

[Mario Carneiro]

specifically, it isn't able to find Init

[Mac Malone]

Yep, same problem.

[Mario Carneiro]

amd my diagnosis is that elan will create a "junction" at .elan\toolchains\lean4-stage0 on windows, and for this kind of link using .. takes you to .elan\toolchains, rather than realpath-ing .elan\toolchains\lean4-stage0 to lean4\build\release\stage0 first so that .. gets to build\release and ..\stage1 is the desired location

[Mac Malone]

That trick definitely wouldn't work on Windows because .. just backs up the executable path (i.e., the one in the Elan toolchain folder), it doesn't follow work up symlinked path like it does on Linux.

[Mario Carneiro]

Is realpath available on windows? We could apply it manually there

[Mac Malone]

The problem is that realpath is the source not the destination for symbolic link on Windows (whereas it is vice versa on Linux).

[Mario Carneiro]

hack solution: elan toolchain link stage1 build/release/stage1 :upside_down:

[Mac Malone]

Yeah, that would work

[Mario Carneiro]

realpath indeed doesn't seem to do anything. Does it ever differ from the identity function?

[Mac Malone]

It gives an absolute path if you give it a relative one?

[Mac Malone]

The underlying Windows API function name is called GetFullPathName/_fullpath

[Mac Malone]

There is no Linux-style realpath notion in Windows.

[Mario Carneiro]

I see that readlink exists though

[Mario Carneiro]

nevermind, you can implement readlink with a pile of windows code but it's not built in

[Mac Malone]

For example, Python's os.path.realpath apparently uses GetFinalPathNameByHandleW.

[Mario Carneiro]

the docs seem to suggest that it will follow symbolic links

[Mac Malone]

Oh, true.

[Mac Malone]

There are two other problems:

• IO.FS.realpath uses GetFullPathName instead of GetFinalPathNameByHandle
• Lean never calls realpath on the IO.appPath which just uses GetModuleHandle

[Mario Carneiro]

I think it's fine not to do (2), as long as we explicitly use realPath in the ../stage1 trick (which is only used in the very rare circumstance of a stage0 build)

[Mac Malone]

Investigating a bit more, you are right that FinalPath follows symlinks, but it does not appear to follow backlinks.

[Mac Malone]

That is ../stage1 would still resolve into the toolchains directory rather than the destination directory.

[Mario Carneiro]

That is, we would change that line to

  if Internal.isStage0 () then
    buildDir := (<- followSymlink buildDir) / ".." / "stage1"

where followSymlink may or may not be spelled as realPath

[Mario Carneiro]

here followSymlink can even be implemented as "read the specified symbolic link and return the target"

[Mario Carneiro]

because we know that we only care about the target itself being a symbolic link (being set up by elan)

[Sebastian Ullrich]

This is missing a description of the use case. Don't use stage 0 for anything but building stage 1.

[Mario Carneiro]

In this case I was using it to test how stage0 and stage1 differ on a test case

[Mario Carneiro]

Until stumbling on this issue I had no idea that stage0 was not a "real" lean compiler, I've used it for compiling things with elan before (indeed, there's almost no point in the lean4-stage0 toolchain link if it never works)

[Mario Carneiro]

maybe a less hackish way to make this work would be to symlink the stage1 lib/lean into stage0

[Mario Carneiro]

Actually I take it back, there is an even more important reason to make this work: you can't browse the lean sources using the stage0 compiler without this

[Mario Carneiro]

that is, on linux I have elan toolchain override lean4-stage0 in the project root, and this fails on windows

[Mario Carneiro]

(note, the documentation says to set lean4 in / and lean4-stage0 in src/, but this is known to not work with vscode and I do lean4 in tests/ and lean4-stage0 in /)

[Sebastian Ullrich]

I think that's the wrong workaround, you'll want to put lean4-stage0 into src/lean-toolchain

[Mario Carneiro]

sure, that's isomorphic I guess?

[Mario Carneiro]

in any case it won't solve the issue of stage0 not finding oleans

[Sebastian Ullrich]

I believe elan is the only part of our infrastructure brave enough to attempt something like symlinks on Windows. I cannot put into words what a mess that platform is.

[Mario Carneiro]

(IMO this infrastructure is the one that is a mess, this stage0 -> stage1 thing is such a hack)

[Mario Carneiro]

I've been thinking about doing a boostrap build outside the context of the lean4 repo repository structure but it seems completely impossible

[Sebastian Ullrich]

I think that workaround exists solely for editor integration. During the build we can set LEAN_PATH properly.

[Mario Carneiro]

why can't lean root just have some information regarding the LEAN_PATH? Or dare I say, a lakefile