olean files to source

Stream: lean4

[Aurélien Saue]

Hello,
In an effort to convert the olean files created by mathport into source files, I am trying to make a tool that is able to read olean files.
I have found the readModuleData function from Environment.lean which is able to read an olean file into a ModuleData object.
Using toString on the contents gives a basic first result but could be improved a lot.
Do you know which better functions could be used to display the expressions?

[Daniel Selsam]

The delaborator (as in "de-elaborator") maps Expr to Syntax, and can be customized e.g. by various pp.<flag> options. It is here: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Basic.lean#L382. ppTerm goes from Syntax to Format: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter.lean#L22-L25

[Aurélien Saue]

Hi!
Using the delaborator as proposed I get fine results except that the implicit arguments of functions are displayed.
I guess I could solve that using the pp.explicit option but I don't manage to pass the options because I don't understand how the OptionsPerPos argument works or how to create it.
Could anyone help me a little?

[Sebastian Ullrich]

The implicit arguments are displayed? That should not be the default.

[Aurélien Saue]

Yes... Maybe the expressions I get with readModuleData have nonly explicit arguments?

[Aurélien Saue]

I mean maybe the implicit arguments are stored as explicit in the olean file so when I try to extract them back I cannot know if they were implicit or not

[Aurélien Saue]

What is weird is that in the function definitions all the implicit arguments are printed as implicit but in function applications the implicit arguments are displayed and there is no @ before the function name