leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

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: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll