Access to the proof goal

Stream: lean4

[Éricles Aquiles Lima]

Hi! I'm new here, so I'm sorry if this question is misplaced.
I have an idea of a project here for which having access to the current proof goal or, more in general, to (what I think people call) the _context_ (eg. that which is shown on infoview on vscode) in a structured manner would be useful.
That is, I'd like to be able to extract the updated context for each line of a program for further processing. Would that, or something similar to that, be currently feasible (without having to open vscode, that is)? If so, I'd be very grateful for some pointers :)

[Trebor Huang]

Is that leanInk?

[Patrick Massot]

Indeed you can take inspiration from the code at https://github.com/leanprover/LeanInk. Entry points include https://github.com/leanprover/LeanInk/blob/main/LeanInk/Analysis/Analysis.lean which runs the Lean frontend on a given Lean file and https://github.com/leanprover/LeanInk/blob/main/LeanInk/Analysis/InfoTreeTraversal.lean which traverses the resulting data structures, the so-called InfoTree. If you are lucky then maybe you don't need to read that code at all, you can use the json output of LeanInk.