Support building dynamic libraries by default

[lecopivo]

I'm having trouble setting up a build for dynamic libraries. I can still do lake build Foo:shared but I'm unable to successfully set up the lakefile such that lake build Foo produces shared libraries.

mwe:

lake init Foo

change lakefile to:

import Lake
open Lake DSL

package foo {}

@[defaultTarget]
lean_lib Foo {}

Now I can do lake build Foo:shared and build/lib/libFoo.so gets created. I would like to lake build to do the same. I should set nativeFacets right?

However, I have tried:

  nativeFacets := #[`dynlib]
  nativeFacets := #[`shared]
  nativeFacets := #[`externLib.dynlib]

None of these work and they all give me application type mismatch error.

Tested on leanprover/lean4:nightly-2022-08-16

[tydeu]

This is not currently supported. It is on the TODO list though.

[lecopivo]

Ohh I see, I will move onto something else in the mean time then.

[lecopivo]

Thanks for getting this done, any chance getting this in master by the end of the month?

[tydeu]

@lecopivo Yes, I certainly hope to have v4.1 out by the end of the month.