load file relative to package home

Stream: lean4

[James Gallicchio]

I have a command elaborator genOpenAPI! <input> that needs the contents of a file during its elaboration.

I have a Lake library GitHub that I would like to distribute with a file (api.github.com.json), and I want GitHub.lean to call genOpenAPI! <something> and load the file in.

How do I accomplish this? Is there an IO function in the environment that correctly tracks the current file's package's directory?

[Mac Malone]

import Lean.Elab.ElabRules

open Lean in
elab "file%" : term => do
  return toExpr (← getFileName)

#eval file%  -- "path/to/module.lean"

[Mac Malone]

(adapted from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Source.20Location/near/387351837)

[James Gallicchio]

thanks :)