Preventing a library from depending on another

Stream: lean4

[Geoffrey Irving]

Currently there is one Render library declared in https://github.com/girving/ray-render/blob/main/lakefile.lean, which depends on two upstream libraries, Interval and Ray. In order to minimize dependencies, I’d like to split Render into two libraries, one of which depends on Interval only (not Ray). Is there a good way to enforce this in the lakefile?

[Geoffrey Irving]

(The motivation is making the computational executables not depend on a bunch of mathematics, reducing the number of .o files built by several thousand.)

[Eric Wieser]

assert_not_exists in your Lean files might be enough

[Geoffrey Irving]

Thank you, that works!