detecting presence of main function without full elaboration

Stream: lean4

[Christian Pehle]

I'm looking for a way to detect the presence of a "main" function declaration without full elaboration. This would be useful for deciding whether a file should be compiled into an executable or library. My guess is that this is not really possible, but I might have overlooked something. A possible workaround would be to defer the decision whether to create a library or executable by writing a tool, which invokes the linker with appropriate flags after it is possible to elaborate the root file based on previously created .olean files.

[Mac]

@Christian Pehle what do you mean by "without full elaboration". Due to ability to interweave metaprogramming and declarative code in Lean to analyze any part of a Lean file, you need to elaborate up to that point.

[Christian Pehle]

@Mac I suspected that this was the case. Intuitively I thought it might be possible to get something like the names of all the declarations in a file without being able to elaborate the file without errors. But I guess this can't work if arbitrary macros and syntax extensions are involved.