lake build complains

Stream: lean4

[Michael Stoll]

I have set up a project (with Mathlib as a dependency) via lake (...) new Legendre_QF math etc. This generated a directory Legendre_QF with a bunch of files in it, one of which was LegendreQF.lean. Since this project needs more than one file, I replaced this file with a subdirectory LegendreQF containing the lean files. Now lake build and lake build LegendreQF complain

error: no such file or directory (error code: 2)
  file: ./././LegendreQF.lean

and lake build LegendreQF/Legendre.lean (this is the main file) gives

error: unknown package `LegendreQF`

I suspect that I should make some edits to lakefile.lean, which currently reads

import Lake
open Lake DSL

package «legendre_QF» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «LegendreQF» {
  -- add any library configuration options here
}

but I don't know what precisely needs to be changed. Any hints?

( I was trying this because I had problems getting the leaf file to "see" the new name of a definition in a transitively imported file. In which order do I have to re-process the files to make it work?)

[Ruben Van de Velde]

Next to lakefile.lean, add a new file LegendreQF.lean with import LegendreQF.Legendre in it

[Michael Stoll]

OK; this works regarding lake build. (Maybe it can be documented somewhere that one needs to set up the subfolder in addition to the file?)

[Michael Stoll]

But it ddidn't solve my original problem... I'll try to minimize and open a new thread for that.

[Alex J. Best]

I would add globs := #[.andSubmodules `LegendreQF] in the lean_lib options

[Michael Stoll]

What does that do?

[Alex J. Best]

It tells lake that the library LegendreQF should contain all the submodules (files approximately) inside the LegendeQF folder

[Alex J. Best]

Which means you don't need a big file importing everything which needs updating when you move / rename a file

[Mac Malone]

@Alex J. Best If one does not want the root LegendreQF file, then on can use just .submodules, which just includes the files in the directory (.andSubmodules adds the root to the mix).

[Ruben Van de Velde]

(I would have thought .addSubmodules to be the to_additive version)

[Michael Stoll]

Is this documented at a place where people like me can find it easily?

[Michael Stoll]

Turns out my original problem was caused by forgetting to hit ctrl-S on the modified file... :shrug:

[Mac Malone]

@Michael Stoll The options for a lean_lib are documented in the README. There are also the online docs for the types (e.g., docs4#Lake.Glob docs4#Lake.LeanLibConfig).

[Michael Stoll]

OK; thanks for the pointer.
But this is not necessarily the place I would look at first. I think it would help if this specific option were mentioned in the instructions for setting up projects.

[Mac Malone]

@Michael Stoll Which instructions would those be?

[Mac Malone]

(i.e., which ones were you using?)

[Michael Stoll]

Something along the lines of "if your project contains more than one file, then create a subfolder (with the correct name) to put your stuff in and add globs := #[.submodules <project name>] in the lean_lib options in lakefile.lean`"?

[Siddhartha Gadgil]

Seems like an occassion to ask: what is a glob? The Readme assumes that readers know this (maybe readers who don't know this can safely assume they will never need to use it).

[Mac Malone]

@Michael Stoll Sorry, I meant where were the instructions you were looking at? Where you using the Lake README, some mathlib tutotirals, etc.?

[Mac Malone]

In Lake, that is not mentioned because that is not the recommended design. The standard Lean 4 style is to have a root file for every folder which imports (some public subset of) the modules in the folder.

[Michael Stoll]

I was using these instructions. (And then I asked here...)

[Michael Stoll]

Mac Malone said:

In Lake, that is not mentioned because that is not the recommended design. The standard Lean 4 style is to have a root file for every folder which imports (some public subset of) the modules in the folder.

Where is this documented?

[Michael Stoll]

It would make sense to add a description of this (or a suitable link) to the instructions I linked to above.

[Mac Malone]

I do not believe that is actually documented anywhere. As to the mathlib instructions, I agree have a piece there would be useful. However, those are mathlib-specific docs, so the mathlib would need to decide what is appropriate there.

[Michael Stoll]

How can something be "standard Lean 4 style" if it is not documented anywhere? :smile:

[Mac Malone]

@Siddhartha Gadgil The term "glob" comes from unix (see Wikipedia). I would be happy to use a more descriptive option name if you have a suggestion!

[Michael Stoll]

I would actually prefer not to have to know about "glob" if I just want to set up a lean/mathlib project with several files in it...

[Mac Malone]

@Michael Stoll Fair point (about the docs on the style)! However, it is the style used by core and much of the ecosystem (e.g., Std) -- and before Lake, it was even was required by the build system.

[Michael Stoll]

So to know what the standard style is, I'd have to read the code in Core and Std? That is a tough ask...

[Michael Stoll]

(Or rather, I guess, have a look at the structure of the directory tree.)

[Mac Malone]

True, there should definitely be some documentation in Lake about how to setup a multi-file project (with directories).

[Michael Stoll]

And a prominent link to it from the mathlib side!

[Siddhartha Gadgil]

Mac Malone said:

Siddhartha Gadgil The term "glob" comes from unix (see Wikipedia). I would be happy to use a more descriptive option name if you have a suggestion!

Thanks. Now it's clear and indeed I have used globs without knowing that is what they are called. For readers like me I would suggest adding the same Wikipedia hyperlink to the word glob, and perhaps an example.

[Mac Malone]

Initially, how most of Lean 4 worked could only be gleaned by reading the code in core. :laughing: We are working on moving away from that into better documentation. :grinning_face_with_smiling_eyes:

[Mario Carneiro]

@Mac Malone By the way, you really should copy a large fraction of the readme into the docs on lean_lib, lean_exe and package. Right now they just describe the basic syntax using where and so on but say nothing about the actual fields that can be used, you have to go to definition through several layers of lake to get to the actual struct definition because of the macros, which makes it hard to access or discover new options

[Mac Malone]

@Mario Carneiro imo what we really needs is constant hyper-linking in the hover markdown. Then you could just click on the LeanLibConfig mentioned in the docstring to go to it.

[Mac Malone]

Also, it is unfortunate that even in the online docs (i.e., docs4#Lake.DSL.leanLibDecl), it is not linkified. (I guess this probably due to the namespaces tripping up the heuristic?)

[Mac Malone]

@Henrik Böving Isdoc-gen4 not able to use the namespace of the declaration for reference when searching for constants to linkify in the docstring?

[Henrik Böving]

It should be able to do that. In general I would appreciate if someone came up with concrete rules / expectations as to how documentation gets linkified instead of this weird heuristic approach that we've been going with so far.

[Mac Malone]

Michael Stoll said:

Mac Malone said:

In Lake, that is not mentioned because that is not the recommended design. The standard Lean 4 style is to have a root file for every folder which imports (some public subset of) the modules in the folder.

Where is this documented?

I rediscovered today that this actually already documented in the Lean repository here as part of the Lean 4 manual (available online here). I had forgotten about that. :sweat_smile: Nonetheless, a similar blurb should still be in the Lake docs and in the mathlib ones as well.