building multiple binaries

Stream: lean4

[Arthur Paulino]

Has anyone else felt the need for Lake to be able to compile multiple binaries? If so, are there plans to make it possible?

#xy: I'm thinking about how to setup a proper testing infrastructure for a Lake project using something like https://hspec.github.io/. I would like to have the tests running in a way that an error can return 1 to the OS.

I have somewhat done it using a Lake script. However, the Lake script looks like a solution particular to a certain repository rather than something that can be extensively used by other libraries. Hence my idea about allowing Lake to build multiple binaries, such that one would be able to build the main binary and the testing binary.

Thanks in advance!

[Arthur Paulino]

I also tried running a Lean file with lean --run tests.lean, which has a main : List String → IO UInt32 function. But I'm getting a lot of errors like unknown constant sorryAx, even though I added the line Lean.initSearchPath $ ← Lean.findSysroot in my function. Maybe it's missing the definition of LEAN_PATH in my environment, but at this point I think it could be smoother with support from Lake :pray:

There's also the fact that I would prefer running the tests with the compiled binary instead of the interpreted code. Not only because of execution speed, but also because in production we would have compiled code running anyway

[Tomas Skrivan]

I will read the question more carefully later, but maybe you are missing lake env lean --run ...

[Arthur Paulino]

I think I can get away with a custom compilation command (similar to what lake build does).

If this is an welcome addition, I might try adding an extra attribute to the Lake package config on a fork:
moreBinTargets : List (String x String), that is, a list of pairs of Lean file names and binary file names

[Tomas Skrivan]

I would definitely like the ability to build multiple binaries. Exactly the same use case, for running tests. Currently I have a custom lake script executing lean --run ... command

Also the ability to build multiple shared libraries would be nice. That would be useful for my Lean as a scripting language project.

[Arthur Paulino]

I was able to make a setup that works (and is not too ugly). The idea is to build a binary for each Lean file in the Tests directory.

I simply tried to mimic the last steps of lake build. It's done in this Lake script.

@Tomas Skrivan you should be able to adapt this approach to your needs :+1:

[Henrik Böving]

as a more general thought: Maybe we could have Lake include scripts as dependencies? So not only have dependencies that provide Lean code but also ones that provide Lake scripts, this way one could e.g. host a general purpose lake-test repo and people could declare it as a script-dependency or w/e and just use it so we can avoid copying around such scripts from the beginning.

[Mac]

Fyi, building multiple binaries / libraries is on the TODO list and I will be back to working heavily on Lake starting tomorrow.

[Mac]

Good news! A new version of Lake (v3.1.1) landed in last night's nightly and the big new feature is support for multiple libraries and binaries! (I thought I had missed the deadline and it would be in tonight's nightly, hence why I am a little late with this announcement. ) The full changelog can be found in Lake's v3.1.0 release notes (v3.1.1 is a hotfix to solve an issue I discovered only after releasing v3.1.0). Detailed documentation on how to use the new Lake can be found in the README. However, I'll give a brief description of how to use the new multi-target feature here.

There are currently three target types: Lean libraries (a collection modules available to import that can be also be built into a static and/or shared library), Lean binary executables (a module with a main function), and external libraries (replacing moreLibTargets). Each comes with a new DSL command to define the target. Examples:

Lean Library

lean_lib foo {
  roots := - ...
  globs := - ...
  libName := - ...
  moreLinkArgs := - ...
}

Binary Executable

lean_exe foo {
  root := `Main
  supportInterpreter := true
  moreLinkArgs := #[]
}

External Library

extern_lib foo :=
  staticLibTarget fooFile #{mainOFile] -- i.e., any `FileTarget`

Defined targets can be built on the CLI using lake build foo or marked with the @[defaultTarget] attribute to build them on a bare lake build. Hopefully that all makes sense and the transition is to the new style is not too painful (and Ithere are no bugs in Lake). Good luck!

P.S. This new release of Lake has a number of other changes (including new syntax for specifying dependencies), so make sure you do take a look at the release notes. However, those changes are outside the scope of this thread, so I will not got into detail on them here now.

[Wojciech Nawrocki]

Can I ask why the transition from using Lean arrays to a custom DSL for specifying package dependencies? Does it enable new features? I must say I liked when the specification was "just" a Lean array, as opposed to a DSL whose semantics are not immediately clear. As you note, this might cause problems for linking dependencies in a particular order. (Overall the package manager seems to be moving in a good direction with lockfiles and such, so thank you for your work on it @Mac ! I only have the one DSL-complaint here.)

[Mac]

Wojciech Nawrocki said:

Can I ask why the transition from using Lean arrays to a custom DSL for specifying package dependencies?

I find DSLs appropriate for Lake for a few reasons: (1) it allows for more modularity (everything does not have declared before / within the package, things can be interleaved); (2) it hides Lake's internal representation of the configuration from the user, allowing it to be changed without breaking user code (which makes adding features and maintaining backwards compatibility easier); (3) it is consistent with Lean core's design (i.e., syntax, macro, elab, initalize, etc.).

Point (2) is especially important. With sufficiently expressive DSLs, the internal representation can be completely hidden (making a lot of refactors that would be otherwise breaking, capable of being made non-breaking). Furthermore, for breaking syntax changes (such as a language overhaul), a new DSL namespace could be created (e.g., DSLv2) allow users to opt into the new syntax. In contrast, direct interaction with the internal representation makes almost all changes breaking changes (as this update demonstrates with its many would-be breaking changes).

For the package dependency DSL, in particular, it can allow the eventually (possible) feature of resolving dependencies during lakefile elaboration and/or potentially enabling special syntax for referencing sub-targets of declared dependencies. It also is much terser, which I consider a major positive (I also think it is easier to read).

[Mac]

Wojciech Nawrocki said:

As you note, this might cause problems for linking dependencies in a particular order.

I do have plan to resolve this: new syntax (extern_lib foo requires bar, baz) and a topological sort of requirements. I just haven't included it here because I wanted to get this update out and I don't think that the current caveat is likely to effect many. Note the array solution still had ordering problems if some sorting need to be done with external libraries of downstream dependencies.

[Wojciech Nawrocki]

Hm, but the hiding of internal representation and custom syntax are orthogonal concerns, no? For example, there could be a stable structure PackageConfig that users declare which you then translate into a PackageConfigInternal. The Internal variant can be changed without affecting PackageConfig. So it seems like that all can be achieved without much DSL, and the real concern that is addressed by it is (1). Having separate commands for separate targets seems like a pretty good idea, e.g. Cargo does it. Anyway, I see you have your reasons so I am not really suggesting a change, just trying to untangle which features help where.

[Mac]

Wojciech Nawrocki said:

For example, there could be a stable structure PackageConfig that users declare which you then translate into a PackageConfigInternal. The Internal variant can be changed without affecting PackageConfig.

Yeah, maybe the word "internal" is misleading. What I meant by my concern was changes to the structure of the forward-facing PackageConfig. The structure of Lean object is very rigid, whereas syntax can be very flexible -- this makes it easier to avoid breaking changes. For example, just changing a field from type Foo to Option Foo can break compatibility in some cases. In contrast, with macros, both versions can be easily massaged into the same type.

Wojciech Nawrocki said:

Anyway, I see you have your reasons so I am not really suggesting a change, just trying to untangle which features help where.

Don't worry, I don't mind the questions. Thinking through these things is quite valuable. :smiley:

[Siddhartha Gadgil]

If there are multiple packages, can a compiled version of one be easily used in another, the way Main.lean uses compiled version of the other files?

[Mac]

@Siddhartha Gadgil I am not sure what you mean? Could you elaborate further on what you mean?

[Siddhartha Gadgil]

I mean that at present if I want to run something compiled instead of in the interpreter, I run it in the Main after lake build. In the case of multiple projects, is there some way that code from one project can similarly be used in compiled form in another project, even in the interpreter.

[Mac]

@Siddhartha Gadgil I am really sorry, but that still doesn't make sense to me. Why would running things inMain.lean have any impact on whether things are compiled or interpreted? Do you instead mean in the main function and then running the executable?

[Siddhartha Gadgil]

Yes. I mean that.

[Siddhartha Gadgil]

I mean is there a reasonably easy way to make one project use the executable form of another project.

[Wojciech Nawrocki]

Is the idea that you have a package A which could be compiled by leanc into libA.so, and then you have a package B importing A, and you would like the interpreter on B's files to use the compiled code in libA.so? That sounds a bit like leanprover/lake#47 which seems on hold, however.

[Wojciech Nawrocki]

Or do you mean that A is an executable with a def main that gets compiled to an A.exe (or whatever), and you would like to run that using IO.Process in B's main?

[Siddhartha Gadgil]

Wojciech Nawrocki said:

Is the idea that you have a package A which could be compiled by leanc into libA.so, and then you have a package B importing A, and you would like the interpreter on B's files to use the compiled code in libA.so? That sounds a bit like leanprover/lake#47 which seems on hold, however.

Yes indeed I mean this. For example one package may have a tactic which I want to use in the other.

[Mac]

@Siddhartha Gadgil In that case, you should be happy to know that my primary goal for this coming week is to support precompiling modules (i.e., leanprover/lake#47).

[z battleman]

This is kind of vaguely related so I thought I would ask here. Is it possible to point a lakefile to multiple c files? Basically, I want to Lean files each which points to its own c file that it interacts with over the FFI. Is such a thing possible?

[Siddhartha Gadgil]

Mac said:

Siddhartha Gadgil In that case, you should be happy to know that my primary goal for this coming week is to support precompiling modules (i.e., leanprover/lake#47).

Indeed that is wonderful news.

[Wojciech Nawrocki]

@Mac I have more questions :) Why the move away from functional package parameters like (args) to global variables?

[Wojciech Nawrocki]

And one more. Previously we specified explicitly which libraries to link in with moreLibTargets. In the new version, are the extern_libs linked into every lean_lib and lean_exe? Is it possible to specify which libraries to link per-target?

[Sebastian Ullrich]

In a similar vein, should require really be global (per workspace) instead of being scoped to libraries? For example, there might be a separate library containing all tests, which alone should depend on a test framework.

[Mac]

Wojciech Nawrocki said:

Mac Why the move away from functional package parameters like (args) to global variables?

As mentioned in the release notes, making it a global macro makes it easier to use across targets. I think adding parameters to every target would be annoying.

[Mac]

Wojciech Nawrocki said:

And one more. Previously we specified explicitly which libraries to link in with moreLibTargets. In the new version, are the extern_libs linked into every lean_lib and lean_exe? Is it possible to specify which libraries to link per-target?

Sebastian Ullrich said:

In a similar vein, should require really be global (per workspace) instead of being scoped to libraries? For example, there might be a separate library containing all tests, which alone should depend on a test framework.

Yes, as with the original moreLibTargets and dependencies, every extern_lib and require is applied globally. However, scoping them locally to a given target is a future planned feature.

[Wojciech Nawrocki]

Yes, as with the original moreLibTargets and dependencies, every extern_lib and require is applied globally. However, scoping them locally to a given target is a future planned feature.

This would be very useful. While on this topic, maybe it would make sense to commit to the separation entirely and make the compilation-related fields — moreLeancArgs/moreLinkArgs/supportInterpreter/etc — all per-target fields rather than parts of PackageConfig — it sounds like now the package has become more of a metadata statement about the source / build directory locations, and maybe in the future it will include author/website/version/etc, whereas the targets deal with compilation.

[Mac]

Wojciech Nawrocki said:

Yes, as with the original moreLibTargets and dependencies, every extern_lib and require is applied globally. However, scoping them locally to a given target is a future planned feature.

This would be very useful.

I can see how it could be eventually, but I am surprised you feel that strongly about it now. I don't really see many use cases for fine-grained dependency management at the moment. But maybe I am missing something obvious.

Wojciech Nawrocki said:

While on this topic, maybe it would make sense to commit to the separation entirely and make the compilation-related fields — moreLeancArgs/moreLinkArgs/supportInterpreter/etc — all per-target fields rather than parts of PackageConfig — it sounds like now the package has become more of a metadata statement about the source / build directory locations, and maybe in the future it will include author/website/version/etc, whereas the targets deal with compilation.

Part of this is already done: moreLinkArgs and supportInterpreter have already been moved to targets. I did not move moreLeancArgs and, most importantly, moreLeanArgs because I was not sure if compiling Lean modules with different options in same library was entirely safe (i.e., whether it could lead to potential incompatibilities between them). Also, if all (or multiple) targets share the same options it could be annoying to copy them to each one. One solution I am considering is to have both a package-wide field and a per target field and then combine the two when building.

[Wojciech Nawrocki]

I don't really see many use cases for fine-grained dependency management at the moment.

For example, you may want to compile with two different implementations of a numerical library. However, it doesn't seem like I need this feature for anything at the moment, so you are right, the "very useful" was exaggerated :)

[Sebastian Ullrich]

I was not sure if compiling Lean modules with different options in same library was entirely safe

No less than doing so in different libraries, I believe :laughing:

[Mac]

Sebastian Ullrich said:

No less than doing so in different libraries, I believe :laughing:

Yeah, I was also thinking about that. Is it a problem? I could move the options from being package-wide to workspace-wide and thus avoid any possibility of incompatibility. I just don't know enough about the risks to know which direction would be better to take. That is, should I move towards target-local scoping of options or move towards workspace-global scoping?

[Sebastian Ullrich]

Does workspace-global include remote dependencies?

[Sebastian Ullrich]

I can't think of any unsafe options other than some #defines that break the ABI, and in that case you're already in trouble with compatibility with the stdlib. So I don't think this is a big concern right now.

[Mac]

Sebastian Ullrich said:

Does workspace-global include remote dependencies?

Yes it does.

[Mac]

Sebastian Ullrich said:

I can't think of any unsafe options other than some #defines that break the ABI, and in that case you're already in trouble with compatibility with the stdlib. So I don't think this is a big concern right now.

So are you saying that target-local flags should likely be fine both for leanc and lean?

[Sebastian Ullrich]

Yes. Though there certainly are options that are desirable to be passed upstream, such as a debug compile profile.

[Tomas Skrivan]

What would be the best way to generate one binary per file in a certain directory? Should I write a command elaboration that would crawl that directory and generate bunch of lean_exe commands?

[Arthur Paulino]

We are kind of doing it in LSpec: https://github.com/yatima-inc/LSpec#setting-up-a-testing-infra
But it expects the user to edit the lakefile accordingly

[Tomas Skrivan]

Yeah I do not want to edit lakefile manually.

[Arthur Paulino]

I thought about empowering LSpec to be able to make editions on the lakefile for the user but turns out the editions may not be trivial, as shown in this example: https://github.com/yatima-inc/yatima-lang/blob/main/lakefile.lean#L36-L40

[Tomas Skrivan]

The non-trivial part is that you need to turn on interpreter?

[Arthur Paulino]

That's one example, but who knows what it might take to run some crazy tests some users may create. For example, one might want to test some FFI implementation with highly specific build parameters. And that's not even an unlikely scenario

[Tomas Skrivan]

My use case it for scripting in Houdini. Every script should create a new library so they should be all the same from the build perspective.

[Arthur Paulino]

Here's a crazy hack: make a Lake script that edits the lakefile itself, generating the lean_exe lines for you

[Arthur Paulino]

Just gotta be careful not to add the same line twice

[Tomas Skrivan]

Arthur Paulino said:

Here's a crazy hack: make a Lake script that edits the lakefile itself, generating the lean_exe lines for you

Before I attempt doing that I will keep on browsing through the meta-programming book and hopefully figure something else out :)

[Tomas Skrivan]

When I add this to my lakefile

elab "#lean_exe_generate" : command => do
  elabCommand (← `(lean_exe Main1))
  elabCommand (← `(lean_exe Main2))

#lean_exe_generate

and run lake build Main1 I get an error error: unknown target 'Main'

Why is that happening?

[Arthur Paulino]

Dunno, but ctrl-clicking on lean_exe and trying to mimic that (instead of calling lean_exe) might take you further

[Tomas Skrivan]

Interesting, changing to

elab "#lean_exe_generate" : command => do
  elabCommand (← `(@[leanExe]  def Main1 : Lake.LeanExeConfig :=  { name := `Main1} ))
  elabCommand (← `(@[leanExe]  def Main2 : Lake.LeanExeConfig :=  { name := `Main2} ))

now I get Building Main1 and oleans are created but I'm not getting Compling Main1 and Linking Main1

[Arthur Paulino]

Please let me know if you succeed :+1:

[Mac]

Tomas Skrivan said:

When I add this to my lakefile

elab "#lean_exe_generate" : command => do
  elabCommand (← `(lean_exe Main1))
  elabCommand (← `(lean_exe Main2))

#lean_exe_generate

and run lake build Main1 I get an error error: unknown target 'Main'

Why is that happening?

Hygiene. Lean will transform the Main1/Main2 into some cryptic hygienic identifier. If you want to use raw identifiers either use $(mkIdent `Main1) to create an unhygienic identifier manually or turn hygiene off with set_option hygiene false.

[Mac]

Note that you can also run CommandElabM directly now via #eval, so you may not even need to create the custom syntax.

[Tomas Skrivan]

Great! got it working. This code in lakefile creates one executable for each file Tests/*.lean

def lean_exe_generate : CommandElabM Unit := do
  let dirName := "Tests"
  let dir := (← IO.currentDir) / dirName
  for file in ← dir.readDir do
    if file.path.extension = "lean" then
      let name := mkIdent file.path.fileStem.get!
      let root := Syntax.mkStrLit (dirName ++ "/" ++ file.path.fileStem.get!)
      elabCommand (← `(lean_exe $name { root := $root }))

#eval lean_exe_generate

[Arthur Paulino]

This looks nice! I might incorporate this trick in the LSpec README someday. But it would also need a way to recursively search directories (not a big issue)

[Arthur Paulino]

It's easily doable with this function, which only God knows how many times I've copied throughout several repos

Offtopic: would it be worth PR'ing this function to the System API? I have replicated it too many times already. It can of course be generalized to accept a custom extension instead of being fixed on "lean".
Would any maintainer endorse it?