Zulip Chat Archive

Stream: lean4

Topic: dependencies


view this post on Zulip Reid Barton (Feb 03 2021 at 15:27):

I put together a minimal project to demonstrate dependency handling between packages in Lean 4. Basically, most things already work the same way as in Lean 3. The project is at https://github.com/rwbarton/lean4-test2.

Things that don't work (yet):

  • There's no leanpkg subcommand to add dependencies to a leanpkg.toml file. However, you can just manually add them, using the same syntax as in Lean 3 (and it's pretty clear that this isn't just working by accident).
  • Running lean directly (for example, lean --run) doesn't work by default, because there is no leanpkg.path. You can make it work by manually setting the LEAN_PATH environment variable: it should be a colon-separated list of the paths to the dependencies, each ending in /build.
  • :cross_mark: leanmake bin doesn't work because it doesn't link in the dependencies at the final step. @Sebastian Ullrich Is there a way to make it work? A partial workaround is to use lean --run instead; I'm not sure exactly which parts of the program will be interpreted vs compiled then. None of this matters for a library, of course.

Note that dependencies from git are now stored under build/deps rather than _target/deps, so don't be alarmed if you see no _target directory.

view this post on Zulip Reid Barton (Feb 03 2021 at 15:31):

The lean4-test2 project includes a dependency which is a separate Lean package which lives in a subdirectory, referred to in the main package by a path dep. This setup could be useful for mathlib if we want/need to put some early tactics in their own package so that we can run them as compiled code. There's currently no way that an external package can refer to just this subpackage as a dependency; but that's probably fine for the time being (it would mean if you want mathlib tactics then you also need all of mathlib).

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 15:34):

Reid Barton said:

  • Running lean directly (for example, lean --run) doesn't work by default, because there is no leanpkg.path. You can make it work by manually setting the LEAN_PATH environment variable: it should be a colon-separated list of the paths to the dependencies, each ending in /build.

I suppose we should have a leanpkg lean subcommand, like cargo rustc (or, in fact, nix run .#lean-dev...)

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 15:44):

Reid Barton said:

  • :cross_mark: leanmake bin doesn't work because it doesn't link in the dependencies at the final step. Sebastian Ullrich Is there a way to make it work? A partial workaround is to use lean --run instead; I'm not sure exactly which parts of the program will be interpreted vs compiled then. None of this matters for a library, of course.

See leanpkg help build:

NOTE: building and linking dependent libraries currently has to be done manually, e.g.

$ (cd a; leanpkg build lib)
$ (cd b; leanpkg build bin LINK_OPTS=../a/build/lib/libA.a)

If anyone wants to automate that, I'm open to leanpkg PRs

view this post on Zulip Reid Barton (Feb 03 2021 at 15:46):

I found that leanpkg build would already build all dependencies automatically, and the issue was only when linking the final executable.

view this post on Zulip Reid Barton (Feb 03 2021 at 15:46):

oh, I didn't realize leanpkg build bin exists. I see.

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 15:49):

Reid Barton said:

I found that leanpkg build would already build all dependencies automatically

Yes, but only the .oleans. leanpkg build ... is basically leanpkg configure; leanmake ...

view this post on Zulip Reid Barton (Feb 03 2021 at 15:52):

Right, I've just realized this as well. That explains why leanmake bin would do so much more work after leanpkg build.
I guess we have to take this into account if we really want compiled tactics in mathlib.

view this post on Zulip Reid Barton (Feb 03 2021 at 15:57):

Maybe we should cross that bridge later; for the moment it should be fine to use interpreted tactics

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 16:00):

You can probably tell, but this leanpkg+leanmake+make toolchain is pretty simplistic and held together by duct tape. I'm not really sure what the future of leanpkg should look like, if someone should write a proper build system for it, I only know that it won't be me for stated reasons... :)

view this post on Zulip Reid Barton (Feb 03 2021 at 16:01):

Yes, the duct tape became clear when I needed two levels of quoting in order to pass LINK_OPTS with two libraries, and a space in it :upside_down:

view this post on Zulip Reid Barton (Feb 03 2021 at 16:03):

How do compiled plugins work (at the lean level, putting aside the build system for now)? Do I just build a package which contains my tactics into a library, and then load it by invoking lean with --plugin?

view this post on Zulip Reid Barton (Feb 03 2021 at 16:05):

Does --plugin really want a static library?

view this post on Zulip Reid Barton (Feb 03 2021 at 16:05):

oh, the --help message indeed says shared library

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 16:09):

Yes, if you load a shared Lean library via --plugin, the interpreter will jump into the native code instead of interpreting the library functions (so they better be in sync, or it can get quite confusing)

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 16:13):

Ideally there should be something like

[dependencies.mathlib_tactics]
...
plugin = True

in leanpkg.toml to automate all this


Last updated: May 07 2021 at 12:15 UTC