lake indirect dependencies

Stream: lean4

[Jakob von Raumer]

I have a chain of depenencies of lake packages A, B, C and D where A directly only depends on B, while B lists both C and D in its dependencies, eventhough D is a dependency of C (in order to get the correct revisions). Now B builds perfectly with with this solution but as soon as I want to lake-build A, it fails with

error: stderr:
failed to write './lake-packages/YatimaStdLib/build/lib/YatimaStdLib/List.olean': 2 No such file or directory

The strange thing is: If I copy all the dependencies from B's lakefile to A's, it works again, but that a bit of a silly workaround...

(where YatimaStdLib is C fwiw) Any guesses what's going wrong? /cc @Mac

[James Gallicchio]

not sure how to help here, but
Jakob von Raumer said:

eventhough D is a dependency of C (in order to get the correct revisions).

could you explain this more? (is it a workaround for a different issue?)

[Jakob von Raumer]

There's that workaround that if you import two packages A and B that both depend on different versions of C, you import C directly and list it before A and B in the lakefile, then you can control what version of C they're using.

[Jakob von Raumer]

So yea, maybe that workaround somehow doesn't carry over to the new package.

[Mac Malone]

Jakob von Raumer said:

So yea, maybe that workaround somehow doesn't carry over to the new package.

Yeah, this is what I suspect is happening, though more investigation is necessary to be sure.

[Mac Malone]

What could be useful here is comparing the lake-manifest of A and B and seeing if there is a discrepancy in the version of D.

[Jakob von Raumer]

The hashes match up, but B shows up right in the middle of the dependency list in the lake-manifest for some reason, while I would have expected it to be listed at the end :thinking:

[Mac Malone]

@Jakob von Raumer If you have the time, constructing a MWE and posting an issue on the Lake GitHub would be helpful. This seems like something that may take some time and effort to debug.

[Jakob von Raumer]

Will try, not so easy to reproduce the situation with dummy repos either..