Zulip Chat Archive
Stream: lean4
Topic: Running a lean script with custom library path
Siddharth Bhat (Mar 23 2022 at 18:19):
I'd like to run lean compile-this-file.lean --library-path=/path/to/my/library
.
I expected lean compile-this-file.lean --root=/path/to/my/library
to work, but it doesn't seem to (it complains that it's unable to find the import). Is this a use-case that's supported by the lean compiler?
Last updated: Dec 20 2023 at 11:08 UTC