RFC: Fun with LLVM

Stream: lean4

[Henrik Böving]

If a user decides to: import Lean.Compiler.IR.LLVMBindings or import any other file that imports this one right now they will get a linker error because leanc does not know about the fact that it can link against a lean built-in LLVM. However we probably do not want to teach leanc to link against LLVM per default because almost all Lean binaries do not actually want to do that (or might even want to link against other LLVMs instead). As I see it there are two solutions to this:

1. Just ignore it, who would want to import this file anyways
2. Add some option to lake that you can enable if you want. I guess this would have to be implemented as some leanc flag under the hood because leanc should be taught where the libraries are?

Does someone have an alternative approach or opinions on which one we should go for?