dependencies

Stream: lean4

[Reid Barton]

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.

[Reid Barton]

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).

[Sebastian Ullrich]

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...)

[Sebastian Ullrich]

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

[Reid Barton]

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

[Reid Barton]

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

[Sebastian Ullrich]

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 ...

[Reid Barton]

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.

[Reid Barton]

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

[Sebastian Ullrich]

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... :)

[Reid Barton]

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:

[Reid Barton]

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?

[Reid Barton]

Does --plugin really want a static library?

[Reid Barton]

oh, the --help message indeed says shared library

[Sebastian Ullrich]

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)

[Sebastian Ullrich]

Ideally there should be something like

[dependencies.mathlib_tactics]
...
plugin = True

in leanpkg.toml to automate all this