Exportable Data?

Stream: lean4

[Pietro Monticone]

Does anyone know of a reference that offers an overview of the different types of "exportable" data from a given Lean file?

[Henrik Böving]

What kind of exportable data are you looking for here? Just what's in Environment? Or something more semantically rich?

[Pietro Monticone]

The point is precisely that I’m not knowledgeable enough to look for a specific kind of exportable data just yet.

My question is more general: I’m trying to understand what types of data I could potentially export from a Lean file.

Is there any resource or reference that could help me get an overview of what kind of data is available?

Essentially, I’m interested in understanding both the breadth and depth of data I can access or export from a Lean project.

[Henrik Böving]

Right, most generally speaking as a raw data source you can somewhat easily access:

• the parsed docs#Lean.Syntax by well, runnign parsing on the file
• the docs#Lean.Elab.InfoTree, this contains a ton of information. The majority of features that the LSP provides to you are constructed based on InfoTrees
• if you want to elaborate the file or load its olean you get an docs#Lean.Environment. Besides all declarations from the file this also contains the data of persistent extensions. A ton of stuff is stored in these environment extensions. What things are instances, what things are linked to external code, simp lemmas etc. etc. Given that people can also add environment extensions on their own it's not really possible to pinpoint the exact kind of data that you can get from them. An interesting starting point might be tools like doc-gen or verso as they operate a lot on data provided by the Environment. doc-gen in particular is a very heavy user of built-in environment extensiosn.

[Pietro Monticone]

Thanks a lot for the clarification!