lake doesn't find option

Stream: lean4

[Floris van Doorn]

When building fpvandoorn/carleson#234 locally by opening Carleson.ForestOperator.Forests, I get the error that lake failed when building Carleson.ToMathlib.Data.Set.Lattice with the error that the flag -Dlinter.flexible doesn't exists. However, this flag is defined in a very low-level Mathlib file, and when opening Carleson.ToMathlib.Data.Set.Lattice in VSCode it builds fine.

Any idea what is going on here?

[Floris van Doorn]

Github CI has the same error message:

✖ [2347/2409] Building Carleson.ToMathlib.Data.Set.Lattice
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/checkdecls/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/lean -DrelaxedAutoImplicit=false -Dpp.unicode.fun=true -DautoImplicit=false -Dlinter.style.longLine=false -Dlinter.style.multiGoal=true -Dlinter.oldObtain=true -Dlinter.refine=true -Dlinter.flexible=true -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Carleson/ToMathlib/Data/Set/Lattice.lean -R ./././. -o ././.lake/build/lib/Carleson/ToMathlib/Data/Set/Lattice.olean -i ././.lake/build/lib/Carleson/ToMathlib/Data/Set/Lattice.ilean -c ././.lake/build/ir/Carleson/ToMathlib/Data/Set/Lattice.c --json
error: <input>:1:0: invalid -D parameter, unknown configuration option 'linter.flexible'

If the option is defined in this library, use '-Dweak.linter.flexible' to set it conditionally
error: Lean exited with code 1

[Damiano Testa]

I wrote the linter, but I do not see any reason why this linter option should be any different than all the other linter options...

[Floris van Doorn]

Note that this configuration option is fine for any other file/import.

[Floris van Doorn]

This sounds like a lake issue, not anything related to this linter.

[Julian Berman]

I reproduced locally, and then confirmed the command lake outputted also reproduced without lake (which I guess on its own doesn't mean anything, in theory the bug could be lake building something out of order I guess?) but now I rm -r .lake'd and can't reproduce a second time quite yet, even after deleting the Mathlib cache entirely... EDIT: oh, never mind, I'm a dum dum, the reason I couldn't reproduce a second time is because I added import Mathlib.Tactic.Linter.FlexibleLinter to the file to confirm that fixes it, and didn't save the file to remove it :/

[Floris van Doorn]

Oh, so is the issue is that the file I import, Mathlib.Data.Set.Lattice doesn't import Mathlib.Tactic.Linter.FlexibleLinter?

[Floris van Doorn]

I guess this is a Mathlib issue in the import structure.
Why does Mathlib.Init not import Mathlib.Tactic.Linter (or all linters)?
It still seems undesirable that when setting a configuration option in the lakefile, you cannot have files in your project that do not import the file declaring that option.

[Michael Rothgang]

I can confirm the mismatch: Mathlib.Tactic.Linter.FlexibleLinter is imported in Mathlib.Tactic (or Mathlib.Tactic.Linter or Mathlib.lean) --- but unlike the other syntax linters mathlib enables by default, it is not imported in Mathlib.Init. (I was wrong a moment ago, Floris. Sorry.)

This means it is possible to have a mathlib file which does not import this linter.

[Michael Rothgang]

@Damiano Testa What do you think of importing it in Mathlib.Init as well? If downstream projects want to use it (and I tried so in carleson, on the grounds that it wasn't too onerous once you fixed all initial violations), we should remove such footguns.

[Michael Rothgang]

I believe that would be the right fix: created #21794

[Michael Rothgang]

@Floris van Doorn If you want to make sure: does bumping mathlib to branch#MR-import-flexible fix the CI errors in carleson#234?

[Damiano Testa]

I'm not at a computer, but I'm trying to understand the issue. Is this a problem that pertains to any option? And the problem is when a downstream project imports a file that, due to its import structure, does not import the option?

[Damiano Testa]

If so, should we enforce that all options are imported in Marhlib.Init?

[Julian Berman]

That sounds slightly odd to me personally as a general solution (with the usual caveat that I don't know how this works in detail). But why should every downstream user importing an early file in Mathlib's hierarchy pay the cost of importing extra stuff (if they aren't trying to use the linters). It would seem more like something the downstream project should have to enable (i.e. import all the linters if they want them). Concretely, I think I'd personally expect import Mathlib.Some.Early.File to not say what linters it promises to import (and leave this be an implementation detail of Mathlib on which linters it wants to run on its own files), and then any downstream project which really does want to use all of the linters should have to explicitly import Mathlib.Linters somewhere early in its own import hierarchy to enable all of Mathlib's linters at its own build time.

[Julian Berman]

(The caveat on not knowing how this currently works is doing a lot in that sentence, because my expectation I think applies equally well to any other thing which isn't a linter, say some random module in Mathlib that isn't needed always, I'd have the same expectation that importing something I need from Mathlib.Somewhere doesn't automatically give me lots of extra stuff if its not needed for the import I did -- and maybe this already isn't the case for things other than linters)

[Edward van de Meent]

maybe having an undefined option set in some file should be a (silenceable) warning instead?

[Michael Rothgang]

Damiano Testa said:

I'm not at a computer, but I'm trying to understand the issue. Is this a problem that pertains to any option? And the problem is when a downstream project imports a file that, due to its import structure, does not import the option?

Yes, in principle this applies to any option. More precisely, AIUI the issue is

• the Carleson project sets linter.flexible true in its lakefile
• some file Carleson.FooBar does not transitively import the flexible linter
• compiling this file errors, with an error about that option being unknown

[Damiano Testa]

I'm still trying to form an opinion on what I think is a good setup for this.

It seems that right now, if project A defines an option, then any project depending on A can either

• align with the default choice of A on the option and everything is fine;
• decide that it wants a different default value for the option, in which case it must take care of importing the option in all its files.

[Damiano Testa]

I think that projects setting their own default values for options in projects on which they depend should not be required to import the option everywhere. At the same time, it seems also like a convenient diagnostic tool to have the ability to find out if this is the case.

[Damiano Testa]

This example is a good use-case: Carleson wants to use the linter. It is reasonable that some Mathlib file does not import the linter and that Carleson could import that file and nothing else.

[Damiano Testa]

It is also reasonable that Carleson would like to know that the option that Carleson wants to be true is actually false in that file.

[Damiano Testa]

Saying this another way, if Carleson wanted to turn on the linter only on files that import it, but be content with mathlib's choice for the other files, this would require doing more than setting the option in the lakefile, which seems a little counterintuitive to me.

[Sebastian Ullrich]

Doesn't weak do exactly what you're asking for?

[Michael Rothgang]

Damiano Testa said:

Saying this another way, if Carleson wanted to turn on the linter only on files that import it, but be content with mathlib's choice for the other files, this would require doing more than setting the option in the lakefile, which seems a little counterintuitive to me.

I must admit that I find this a strange choice. To me, enabling a linter in a lakefile says "I want this linter enabled everywhere". Getting an error "I don't know this option" or silently disabling this linter in some files is surprising.

I would call this a bug in mathlib: if a linter can reasonably be enabled downstream, it should be available there (i.e. imported in Mathlib.Init).

[Edward van de Meent]

i guess a middle ground might be: if you want to enable a linter in your lakefile, make a project-wide Init.lean file which imports said linter (or at least linter option) and make sure your project always has that file imported.

[Edward van de Meent]

still, i think throwing an error over setting an unknown option is a bit overkill

[Edward van de Meent]

Sebastian Ullrich said:

Doesn't weak do exactly what you're asking for?

(spoiler: my understanding was wrong)

As i understand it, weak means set this option, but not in downstream projects. that doesn't mean that it won't complain when the option is set but is not imported

[Damiano Testa]

I thought that Sebastian's suggestion was to set the weak option in the downstream project.

[Edward van de Meent]

yes, but as i understand it, if an option is weak or not only matters for projects downstream of the one that sets it?

[Edward van de Meent]

so changing how Carleson sets the option won't have an effect on Carleson

[Edward van de Meent]

(if my understanding is correct)

[Damiano Testa]

I think that weak means "if you find the option, set it, otherwise do nothing".

[Edward van de Meent]

ah...

[Edward van de Meent]

looking into it, lean4#4741 seems to be the adding of weak options, and indeed it does what you describe

[Damiano Testa]

I tested locally and fpvandoorn/carleson#235 seems to work as intended.

[Damiano Testa]

Just to be explicit:

• if you import transitively the flexible linter, the PR above should not change anything;
• if you do not import the flexible linter, then neither CI nor VSCode raise an error.

[Damiano Testa]

At least, this is what I observed on my computer.

[Floris van Doorn]

Thanks!

[Floris van Doorn]

@Sebastian Ullrich the error message currently states "If the option is defined in this library, use '-Dweak.linter.flexible' to set it conditionally". Can this be changed to something like "If the option is defined in a file that is not always imported (e.g. it is defined in this library), use '-Dweak.linter.flexible' to set it conditionally"?

[Sebastian Ullrich]

I'd accept that PR :)

[Julian Berman]

Can this be changed to something like "If the option is defined in a file that is not always imported (e.g. it is defined in this library), use '-Dweak.linter.flexible' to set it conditionally"?

I realize this is quite minor of a scenario so feel free to ignore, but I still don't really understand why that's behavior someone should want. Taking this specific example -- If you want the flexible linter turned on on your project it's because you're trying to make sure you don't have files that use overpowered tactics, right? Why would you want to silently not run that linter in some cases? Either you want that check on your project's files or not? And it doesn't seem sufficient to rely on where in Mathlib's import hierarchy it gets imported -- for a general case option, it seems like a possible scenario is that Mathlib imports it at stage X in its hierarchy because its implementation requires something from stage X, but that that option makes perfect sense to run on files at stage X-1 or before, so if you're downstream of Mathlib, using weak seems suspect to me (-- so making the error message nudge people towards it also seems a bit weird).