locating non-lean files from tactics

Stream: lean4

[Mario Carneiro]

For the polyrith tactic, there is a bit of code that locates a python file like this:

do
  path ← get_mathlib_dir,
  let args := [path ++ "../scripts/polyrith_sage.py"] ++ arg_list,
  s ← unsafe_run_io $ io.cmd { cmd := "python3", args := args},

where get_mathlib_dir locates the mathlib directory by hacks that I won't reproduce here. The question is: how do we do this robustly in lean 4? I would like a method that works in interactive mode (of mathlib or a downstream project), as well as in compiled code in downstream projects.

[James Gallicchio]

I wonder if the lakefile for mathlib could put something in scope for the current project and dependent projects