Forcing Lake to build lib

Stream: lean4

[Patrick Massot]

How do I tell Lake to build all lean files it can find in some directory in the project, even when it thinks those files are not used? The reason why Lake mistakenly thinks those files are useless is because they are imported dynamically using importModules.

[Henrik Böving]

You can remove the build directory which will force a full rebuild of the top.level

[Patrick Massot]

That won't do anything since Lake thinks those files are useless.

[Patrick Massot]

Those files are not statically imported by any other file in the project.

[Arthur Paulino]

We've done it here: https://github.com/yatima-inc/yatima-lang
The pieces of the puzzle are:

• A Yatima.lean file containing all Lean files inside the Yatima directory
• A Lake script that creates that file automatically
• A Yatima lib that allows you to call lake build Yatima

[Arthur Paulino]

If you want to go further, you can integrate it in a CI workflow:
https://github.com/yatima-inc/yatima-lang/blob/main/.github/workflows/ci.yml#L21-L24

The import_all? script checks if the Yatima.lean file indeed contains everything it should contain. If it fails, then it recommends the user to run lake run import_all

[Siddhartha Gadgil]

What I do is go into the correct subdirectory of lean_pkg and then build. But I believe e.g. lake build math3port works too with newer lakes (i.e., with the name used in require).

[Patrick Massot]

It looks like Arthur's trick could be used, but I was hoping for something much simpler. I don't understand Siddartha's suggestion.

[Arthur Paulino]

I'd love being able to say lake build-dir Yatima or something like that. It would also avoid the need for maintaining the Mathlib.lean file in the Mathlib4 repo

[Siddhartha Gadgil]

As an example if I am using mathlib in a meta way (as I do), in linux I do

cd lean_packages/mathlib
lake build
cd ../..

[Siddhartha Gadgil]

Have done this quite a bit and it works.

[Patrick Massot]

But mathlib itself does explicitly list its imports, so this isn't my situation at all.

[Siddhartha Gadgil]

More recent lakes also should allow simply:

lake build mathlib

[Siddhartha Gadgil]

In my example I have

importModules [{module := `Mathlib}

[Patrick Massot]

But mathlib itself is a Lean library which lists all its files.

[Siddhartha Gadgil]

I see. In my situation I had lean packages with their own lakefiles, which I used to build.

[Siddhartha Gadgil]

Do you mean that you have your own module? In that case one can import it in another build target and build that.

[Siddhartha Gadgil]

A cruder way, which I used in the past, was to temporarily import the file. I had to then remove import to avoid collisions. But that was before lake had multiple targets.

[Siddhartha Gadgil]

If I understand correctly, an option may be to have a file metaimports.lean which just imports stuff you would call with importModule and is a lake target. Then lake metaimports will build them all.

[Siddhartha Gadgil]

I see that I have converged to a manual version of Arthur's solution. So I have added no value (except to say I found no better way).

[Patrick Massot]

Maybe I'm not clear at all. Let's try with reproducible instructions. Do

lake +leanprover/lean4:nightly-2022-08-09 new exemple && cd exemple && mkdir Foo && echo "def x := 3" > Foo/foo.lean

Then run lake build. Then build/lib folder won't contain a compiled version of Foo/foo.lean. I want to know how to modify my lakefile to tell lake to compile every file contained in Foo and put the result in build/lib/Foo, and I don't ever want to write by hand the list of files contained in Foo since a computer should be smart enough to list files in a folder (I'm not even asking for a recursive listing).

[Arthur Paulino]

AFAIK it's not possible yet. Hence my wishlisted lake build-dir Foo command above.

Lake's current build capabilities are based on targets, not directories

[Patrick Massot]

I guess this is all consistent with the difference between imperative programming and functional programming: you can't give orders to lake.

[Mac]

Arthur Paulino said:

AFAIK it's not possible yet.

Lake's current build capabilities are based on targets, not directories

This has been possible for a long time and was a feature requested then by Mario. This is what the globs option of a Lean Library is for.

[Mac]

If you want to build a specifically module in the library's source directory (e.g., Foo) just add it to the globs. If you want to build the module and all submodules in the the source directory (e.g., Yatima) you can add .andSubmodules `Yatima to the list.

[Siddhartha Gadgil]

Mac said:

Arthur Paulino said:

AFAIK it's not possible yet.

Lake's current build capabilities are based on targets, not directories

This has been possible for a long time and was a feature requested then by Mario. This is what the globs option of a Lean Library is for.

Maybe the documentation could be tweaked. I read the README and did not find this feature as I did not understand what a glob was (and so decided something not applicable to me).