Zulip Chat Archive

Stream: lean4

Topic: Getting Lake's srcPath directories


Julian Berman (Jul 14 2025 at 19:20):

In lean4#8699 the output from lake setup-file looks like it changed to remove .paths, and specifically .paths.srcPath. I see the reasoning for this (which of course makes sense) says:

These environment variables are already configured during sever setup by lake serve and do not change on a per-file basis.

But I don't really see another convenient to actually retrieve this information now -- specifically it looks like lake env's LEAN_SRC_PATH is the data I want, but unless I'm missing something it's only available there through that command (in shell format).

Am I missing another easier place which has this info? lean.nvim uses it to implement things like "I want to open any one of the .lean files that Lean has on its import path".


Last updated: Dec 20 2025 at 21:32 UTC