Lean 4: generated .cpp depends on current working directory

Stream: general

[Uranus Testing]

Suppose I have ./a/b/c.lean.
I do:

segfault@cirno-6:~/src/lean/cwd-bug$ lean4 -c c.cpp a/b/c.lean

Then there is initialize_a_b_c in c.cpp:

segfault@cirno-6:~/src/lean/cwd-bug$ cat c.cpp | grep initialize_a_b_c
lean_object* initialize_a_b_c(lean_object* w) {

Then I go into a/ and generate new c.cpp inside of a/:

segfault@cirno-6:~/src/lean/cwd-bug/a$ lean4 -c c.cpp b/c.lean

And in new c.cpp there is initialize_b_c instead of initialize_a_b_c:

segfault@cirno-6:~/src/lean/cwd-bug/a$ cat c.cpp | grep initialize_b_c
lean_object* initialize_b_c(lean_object* w) {

Is this a bug or a feature?

[Uranus Testing]

Lean 4 version:

segfault@cirno-6:~/src/lean/cwd-bug$ lean4 -v
Lean (version 4.0.0, commit 9aa5a5c29838, Release)

[Sebastian Ullrich]

This is intentional. We expect multi-file projects with code generation not to be built by hand but with some build tool, e.g. the new leanmake, which should take care of this issue.

[Uranus Testing]

Another problem appears here: any other .lean-file will always refer to initialize_a_b_c regardless of cwd. Therefore the generation of .cpp-files outside «.» becomes impossible.

which should take care of this issue

So, should build-system fix this?

[Sebastian Ullrich]

There is nothing to fix. Just make sure to always call lean from the package root and everything will work out.

[Uranus Testing]

Thanks for the explanation.