'Computing build jobs' for ever

Stream: lean4

[Marcus Rossel]

I'm trying to build mathlib based on a local version of batteries. That is, I've changed the lakefile.lean in the mathlib project to use:

require batteries from "../batteries/batteries"

Directory Structure

└── batteries
│   └── batteries
│   │   └── Batteries
│   │   │   └── ...
│   │   └──...
└── mathlib4
    └── ...

But when I run lake clean && lake update batteries && lake build in the mathlib4 directory, it just says ⣿ [?/?] Computing build jobs forever. I'm not sure how to debug this.

[Kim Morrison]

I think "Computing build jobs" forever is best debugged by pinging @Mac Malone, unfortunately. He's aware this sometimes happens, but I think doesn't have a repro that is sufficient for him to identify the cause.

[Kim Morrison]

My experience is that this usually means you are importing a file from the other library that doesn't exist, but that's only a necessary, not sufficient, condition.

[Marcus Rossel]

What does "importing a file from the other library that doesn't exist" mean?

[Mac Malone]

@Marcus Rossel For example, import Batteries.Foo where Batteries/Foo.lean does not exist (e.g., because it recently removed in a new version of batteries).

[Marcus Rossel]

So instead of necessarily causing a simple build error, a missing file might also contribute to the non-terminating Computing build jobs?

[Marcus Rossel]

(deleted)

[Mac Malone]

Marcus Rossel said:

So instead of necessarily causing a simple build error, a missing file might also contribute to the non-terminating Computing build jobs?

For some reason I have sadly yet to be able to figure out, yes, that appears to be the case for batteries/mathlib.