Error messages for missing files don't say the culprit file

Stream: lean4

[Geoffrey Irving]

If I do some refactoring, resulting in file A.lean importing B.lean which doesn't exist, the error message doesn't mention A:

% lake build
error: 'B': no such file or directory (error code: 2)
  file: ./././B.lean

That's an artificial error message. Here is a real one:

% lake build
error: 'Ray.Dynamics.Multibrot.Effective': no such file or directory (error code: 2)
  file: ./././Ray/Dynamics/Multibrot/Effective.lean

Here the problematic files importing the now missing Effective.lean are

% sg -w Effective | grep import
./Ray.lean:import Ray.Dynamics.Multibrot.Effective
./Ray/Dynamics/Multibrot/Isomorphism.lean:import Ray.Dynamics.Multibrot.Effective

Should I file this as a bug? Would it go in the lean4 repo?

[Mario Carneiro]

I think this is already fixed

[Geoffrey Irving]

Ah, nice! Is the problem that I'm using lake from Homebrew and it's a bit old?

[Mario Carneiro]

no, it's not in an RC yet

[Mario Carneiro]

but on the development version of lean you get errors like this:

error: 'test.Test' ▸ 'Test.A' ▸ 'Test.foo': no such file or directory (error code: 2)
  file: ./././Test/foo.lean

[Mario Carneiro]

the sequence of modules seems to be the path from the root of the import hierarchy to the nonexistent file, generally you only care about the second to last entry

[Alex J. Best]

Mario Carneiro said:

no, it's not in an RC yet

I'm pretty sure this was out a while ago? lean4#2616 so it should be in recent lake versions. Do you have a reason to use homebrew's Geoffrey?

[Eric Wieser]

Is the error now attached the the import line with the problem?

[Mario Carneiro]

I just tested it on v4.5.0-rc1 and did not get the nice error message

[Mario Carneiro]

Lake version 5.0.0-b614ff1 (Lean version 4.5.0-rc1)

[Alex J. Best]

Hmm, I'm sure I saw this working fine in my leaff demo https://youtu.be/VkKfIWoM3Ms?t=135 which was also Lake version 5.0.0-b614ff1 (Lean version 4.5.0-rc1)

[Mario Carneiro]

I just checked and the code in question is definitely present on b614ff1d12bc

[Mario Carneiro]

but if I try to just mangle an import in mathlib and run lake build I don't get any call stack

[Mario Carneiro]

Eric Wieser said:

Is the error now attached the the import line with the problem?

Nope, that one is still future work, probably dependent on getting json output from lean

[Mario Carneiro]

actually maybe not, since lake is the one that is reporting the missing file and also parses the imports

[Mario Carneiro]

I guess the issue is in the other direction, the server doesn't understand what lake is saying

[Mauricio Collares]

This was refactored in lean4#2677, maybe the refactoring broke something? I don't know how to run lake tests

[Mario Carneiro]

I think you just run ./test.sh in each lake test

[Geoffrey Irving]

Alex J. Best said:

Mario Carneiro said:

no, it's not in an RC yet

I'm pretty sure this was out a while ago? lean4#2616 so it should be in recent lake versions. Do you have a reason to use homebrew's Geoffrey?

To amend: I’m using elan from Homebrew but leanprover/lean4:v4.5.0-rc1 (same as mathlib4).

[Mauricio Collares]

Ok, ignore my message, I ran the commands in the test and the breadcrumb showed up

[Mauricio Collares]

I think the thing here is that lake build does not show the breadcrumb on Mathlib, but lake setup-file File.lean Init Import1 Import2, which is what gets executed via LSP when editing a file interactively, does.