Zulip Chat Archive

Stream: general

Topic: Fields of Lake package defined in current working directory?


Mekeor Melire (Dec 10 2024 at 22:12):

Given a Lean4 Lake package source code in /my/great/program and a shell with current-working-directory being somewhere beneath that path, is it possible to easily and correctly access the fields (path to package root, path to lakefile in use, package name etc.) of the Lake package via Lean and Lake themselves? I'm imagining something along these lines:

lake env lean --stdin --run <<EOF
import Lake
def main : IO Unit := IO.println Lake.Some.Magic.currentPackage.dir
EOF

Last updated: May 02 2025 at 03:31 UTC