Zulip Chat Archive

Stream: lean4

Topic: detecting presence of main function without full elaboration


Christian Pehle (Sep 27 2021 at 13:30):

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 (Sep 27 2021 at 16:31):

@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 (Sep 28 2021 at 12:42):

@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.


Last updated: Dec 20 2023 at 11:08 UTC