Referencing package-local files

Stream: lean4

[Chase Norman]

Is there a best practice for how to get the path/contents of a file relative to the package, rather than to the user's package being built? Given that the shared libraries are precompiled, this information seems tricky to obtain.

[Chase Norman]

This question might be unfairly difficult; it seems uncommon for languages to have nice support for this. I will try another route.

[Alissa Tung]

That's common for other languages to have support for this, its very common in Rust, Golang, C, or something else.

In general there are two style: 1. Write an elaboration such that it can performs side-effects, read file and so on; 2. Write custom build scripts in Lakefile to generate Lean files that contents those infomation.

When writing elaboration for them, you might find Lean.MonadLog.getFileName useful.

[George Pîrlea]

I'm not sure I understand your question, but in Veil we've used this (Zulip thread):

syntax (name := currentDirectory) "currentDirectory!" : term

open Lean Elab Elab.Term in
@[term_elab currentDirectory] def elabCurrentFilePath : TermElab
  | `(currentDirectory!), _ => do
    let ctx ← readThe Lean.Core.Context
    let srcPath := System.FilePath.mk ctx.fileName
    let some srcDir := srcPath.parent
      | throwError "cannot compute parent directory of '{srcPath}'"
    return mkStrLit s!"{srcDir}"
  | _, _ => throwUnsupportedSyntax

If you depend on a file, you probably want to make lake aware of it as well, e.g. like this.

[Eric Wieser]

That looks like a bad idea to me, since you risk compiling the current path into the distributed olean files

[Eric Wieser]

Instead you should write a function in CoreM, and call that when you need it

[George Pîrlea]

Indeed, this isn't great, since it prevents you from distributing oleans. It only works if each user builds your package on their own machine and then doesn't move it. Bundling the needed file's contents into the Lean file (via include_str or similar) is likely better.

Instead you should write a function in CoreM, and call that when you need it

Maybe I misunderstood @Chase Norman's intention, but I think his use-case is: you define package A, and your user imports A in their own package X; the question is how to get paths relative to A rather than relative to X.

If you get core.Context.fileName or IO.currentDir or anything like that at runtime, you will only get paths relative to X.

[Eric Wieser]

Currently I think the preferred approach is to use include_str, to not only resolve the path but also inline its contents