Linker error when no main

Stream: lean4

[James Gallicchio]

Hey all, on latest stable, in a clean project, if you declare the exe root to be a certain module and that module doesn't have a top level main function, you get an inscrutable error from the linker rather than any error from Lake. Could we get a better error message?

I am working on a complicated program downstream of Mathlib and got the linker error, assumed it was something way more difficult to debug, and then happened by chance to notice my main function wasn't in the root namespace and that was the issue.

[James Gallicchio]

I think this is a question for @Mac Malone? Let me know if I should make a GH issue!

[Mac Malone]

A GH issue for this would be great! Solving this will probably require some new coordination between Lean and Lake.

[Mac Malone]

(Since either Lake needs to figure out that the module has a main in it or it needs a way to tell Lean that is expecting it to have one.)

[James Gallicchio]

https://github.com/leanprover/lean4/issues/4752 :saluting_face:

[James Gallicchio]

I'm hoping this is an easy fix -- even with some familiarity with how C programs are compiled, it's a scary (and huge) error message to get from such a small/careless mistake

[Kim Morrison]

If you wanted to move "linter errors should come with an explanation that something has gone horribly wrong and it's not your fault" to a separate issue, that would be helpful. I agree we should be nicer to the user here.

[James Gallicchio]

Sure. I wasn’t entirely sure what scope I wanted the error message improved for, though — I get linker errors often when doing FFI work, and on one hand the errors definitely could be improved (eg reporting an error on an implemented_by) but on the other it is a much more difficult problem to solve

[James Gallicchio]

Like, I think you could get a linker error if a project you depend on is missing some C library dependency, and it’s not the compiler or library author’s fault. Which is a hairy edge case to explain in an error message :/