Zulip Chat Archive

Stream: lean4

Topic: building multiple binaries


Arthur Paulino (May 13 2022 at 19:14):

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 (May 13 2022 at 19:36):

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 (May 13 2022 at 19:56):

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

Arthur Paulino (May 14 2022 at 00:12):

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 (May 14 2022 at 12:55):

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 (May 14 2022 at 22:25):

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 (May 15 2022 at 12:51):

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 (May 15 2022 at 20:53):

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

Mac (Jun 11 2022 at 17:12):

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 (Jun 11 2022 at 17:22):

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 (Jun 11 2022 at 17:44):

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 (Jun 11 2022 at 17:47):

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 (Jun 11 2022 at 18:12):

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 (Jun 11 2022 at 18:25):

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 (Jun 12 2022 at 12:21):

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 (Jun 12 2022 at 14:48):

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

Siddhartha Gadgil (Jun 12 2022 at 14:52):

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 (Jun 12 2022 at 14:57):

@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 (Jun 12 2022 at 15:08):

Yes. I mean that.

Siddhartha Gadgil (Jun 12 2022 at 15:09):

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

Wojciech Nawrocki (Jun 12 2022 at 15:41):

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 (Jun 12 2022 at 15:42):

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 (Jun 12 2022 at 15:50):

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 (Jun 12 2022 at 17:46):

@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 (Jun 12 2022 at 18:14):

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 (Jun 13 2022 at 00:44):

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 (Jun 13 2022 at 16:01):

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

Wojciech Nawrocki (Jun 13 2022 at 16:15):

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 (Jun 13 2022 at 16:17):

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 (Jun 13 2022 at 17:25):

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 (Jun 13 2022 at 17:32):

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 (Jun 14 2022 at 02:43):

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 (Jun 14 2022 at 03:14):

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 (Jun 14 2022 at 03:40):

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 (Jun 14 2022 at 07:40):

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 (Jun 14 2022 at 07:57):

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 (Jun 14 2022 at 08:05):

Does workspace-global include remote dependencies?

Sebastian Ullrich (Jun 14 2022 at 08:09):

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 (Jun 14 2022 at 08:12):

Sebastian Ullrich said:

Does workspace-global include remote dependencies?

Yes it does.

Mac (Jun 14 2022 at 08:14):

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 (Jun 14 2022 at 08:16):

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

Tomas Skrivan (Aug 12 2022 at 12:06):

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 (Aug 12 2022 at 12:28):

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 (Aug 12 2022 at 12:33):

Yeah I do not want to edit lakefile manually.

Arthur Paulino (Aug 12 2022 at 12:39):

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 (Aug 12 2022 at 12:40):

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

Arthur Paulino (Aug 12 2022 at 12:46):

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 (Aug 12 2022 at 12:50):

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 (Aug 12 2022 at 12:54):

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

Arthur Paulino (Aug 12 2022 at 12:55):

Just gotta be careful not to add the same line twice

Tomas Skrivan (Aug 12 2022 at 12:59):

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 (Aug 12 2022 at 13:25):

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 (Aug 12 2022 at 13:38):

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

Tomas Skrivan (Aug 12 2022 at 13:51):

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 (Aug 12 2022 at 21:57):

Please let me know if you succeed :+1:

Mac (Aug 13 2022 at 00:10):

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 (Aug 13 2022 at 00:11):

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

Tomas Skrivan (Aug 16 2022 at 14:08):

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 (Aug 16 2022 at 14:22):

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 (Aug 16 2022 at 14:29):

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?


Last updated: Dec 20 2023 at 11:08 UTC