Macros to get source location

Stream: lean4

[Chris Bailey]

Rust has a family of utility macros line!(), column!(), and file!() that expand to the line, column, and file where they're invoked. These are useful for things like error reporting, say you want to communicate what branch of a function failed in a way that's easily jumped to by someone debugging a problem. I couldn't find a direct analog so I took a stab at it, does anyone have any suggestions/improvements, particularly on the file! one? It seems like these can't just be macros because they need MonadLog and IO.

-- Seems to work; should print the source file path starting from the project root.
elab "file!" : term => do
  let curFile ← getFileName
  let xs := (← Lean.getSrcSearchPath).filterMap (curFile.dropPrefix? ·.toString)
  let truncdFileName :=
    match xs with
    | [] => curFile
    | hd :: tl =>
      let out := tl.foldl (init := hd) (fun sink next =>
        if Substring.bsize next < Substring.bsize sink then next else sink
      ) |>.toString
      if out.startsWith "/"
      then out.drop 1
      else out
  return toExpr truncdFileName

elab "line!" : term => do
  return toExpr (← Lean.getRefPosition).line

elab "column!" : term => do
  return toExpr (← Lean.getRefPosition).column

elab "position!" : term => do
  return toExpr (← Lean.getRefPosition)

[Aaron Liu]

The panic! macro expands to contain the file, line, and column it's written, as well as the name of the function it's in, maybe you can see how it works

[Chris Bailey]

That's a good thought. panic! uses Lean.Environment.mainModule which is probably a better bet.