Is this the correct library for me to use?

[FruitfulApproach]

I first landed at multilspy thinking I could "hook into what the infoview sees". However, LSP is about generic document-level editing etc and not about Lean4 itself. I need to be able to decode Lean4 without having to fully parse it. If I had to parse it, then I would just make an extension to the lean4 C++ code itself.

My ultimate goal is to write a diagram editor in another language such as PyQt5 or Qt/C++ or Rust. I then take parts of Lean4 language and build nodes / arrows from it. Usually this would just apply to the category theory part of mathlib. I would also like to write lean4 code from a user drawing a diagram (roundtripping).

I am aware of Lean4/widgets - would that be more appropriate of a strategy to use rather than this library?

The final idea is that I would like to automate a diagram chase, and have the user see the searching happening visually on the screen, in the diagram editor tool. But it would be nice if it worked in both manual PA mode as well as automated mode.

It would be cool if the user specifies a diagram with some properties of certain of its paths ("exact rows" e.g.) and certain of its arrows ("f is an epimorphism"), and a goal to prove, "there exists a well-defined connecting hom" e.g. as in the Snake Lemma, and then see if the proof can be searched for, even if brute force, but I guess this library is about doing the search intelligently.

I'm just not sure where to start, but I am leaning towards starting at the widgets extension to Lean right now.

[yangky11]

Hi,

I don't think LeanDojo alone can achieve what you have described. It sounds like you need to process the repo interactively, whereas LeanDojo is designed mostly for offline data extraction. I'd suggest posting your question on Lean Zulip so that people might be able to help.