Retrieving `weak` options

Stream: lean4

[Damiano Testa]

With the option of setting weak options, there are now two "default" values:

• the actual defValue set when registering the option, and
• the weak value that may be set in the lakefile.

The defValue is myOption.defValue.

The currently set value can be found using e.g. myOption.get (← Lean.getOptions).

How can I retrieve the "default" weak option, if it is set?

It is hard to write a good #mwe, since this requires coordination of different files. For an example in Mathlib, linter.hashCommand has a defValue of false and a weak-value of true. How can I find out that the weak-value is true, if I do not know whether there is a set_option linter.hashCommand messing stuff around?

[Damiano Testa]

The reason for asking is that the longFile linter will have a default value of 0 (= inactive for downstream projects), but a weak value of 1500.

When linting, I would like to access 1500 without hard coding 1500 but doing a hypothetical ←getWeakOption linter.style.longFile to retrieve the value.

[Mario Carneiro]

I believe the way it is supposed to work is that the weak options will already be applied to the current options struct, overriding the default value. You shouldn't need to get them directly from some additional place for weak options

[Damiano Testa]

If I understand correctly, the weak version is available as the initial formvalue of the option. However, if the value is modified by a set_option before where I get it, then I cannot know if what I read is what the weak option was or what it was reset to be. Am I misunderstanding something?

[Damiano Testa]

In my use case (the long linefile linter), I want to know what is the "reference value" for the length of a file (1500 for mathlib), not what the option might have been set to by the time I am reading it.

[Kyle Miller]

What's the logic you're wanting here? I'm not sure I understand why you would want to know anything but the current value for the option.

[Michael Rothgang]

As I understand it, the aim is the following:

• mathlib wants the longFile syntax linter enabled
• projects depending on mathlib prefer it disabled, but should be able to enable it if they like
• syntax linters apply to any file importing the linter definition: thus, the solution mathlib contributors came up with was the following
  • the linter is disabled by default
  • mathlib's lakefile enables the linter (using a weak option)

So far, so good (and perhaps not surprising). The interesting bit is:

• the linter would like to know if its option is set to something larger or smaller than the default. (Basically, the linter complains on long files, and changing the linter option is the way to silence the linter. It would be good to keep such changes minimal, which is why the linter complains if a set_option is superfluous: but that change requires knowing the default configuration)
• the "default configuration" for the purposes of the previous point is not the default value (that's "disabled"), but the value set in mathlib's lakefile.

Does that make more sense? Is there anything still unclear?

[Kyle Miller]

I'm not sure why the linter needs to know this:

the linter would like to know if its option is set to something larger or smaller than the default

[Michael Rothgang]

This is required for the "auto-correction" feature the linter offers:
if you do set_option linter.style.longFile 3000, but that is not needed (say, as the file is now split, and has only 500 lines), it's nice to know this can be removed. mathlib's technical debt tracking looks at these options, so knowing when these can be removed is helpful.
The linter does so by comparing the current length with the option value: if the file is much shorter than its option, it suggests removing the option.

However, we don't want the linter to suggest adding a set_option ... <small_number> for small files: differentiating these two requires knowing the default value of the linter.

[Kyle Miller]

One solution here would be to have a linter.style.longFileOverride option that people could set within files, and make it a linter error to set linter.style.longFile.

[Damiano Testa]

I had also thought of adding an extra option that is the "official" limit and the linter reads both, but only one of the two is editable. I was just hoping to avoid the extra option, recycling what is already available as much as possible.

[Damiano Testa]

Anyway, hard-coding the limit in the linter is quick and easy! I also do not expect the limit to change often, so this is not really a major problem, mostly a curiosity!

[Kyle Miller]

Hard coding it means downstream users can't decide what the limit should be. It seems like having two options would be better for that reason, right?

I'd suggest the following (modulo name changes):

• Define option linter.style.longFile with default 0
• Define option linter.style.longFileOverride with default 0 (this default does not matter)

• The logic for "what is the current file length limit" would be

  • if linter.style.longFileOverride is set, use it.
  • otherwise, if linter.style.longFile is set, use it.
  • otherwise, use the default value for linter.style.longFile.

  (Recall that you can tell whether or not an option has been set, without needing to compare with the default value.)

  A result of 0 means "no limit".

• Make setting linter.style.longFile within files a linter error.

I think this would be better than trying to reason about weak. @Sebastian Ullrich can correct me if I'm wrong, but I think we should treat weak as only being part of the external interface to Lean, existing just to be able to set options from the command line.

[Damiano Testa]

Kyle, thanks, I did not think about the fact that downstream users might want the linter, but with a different default length than mathlib.

[Damiano Testa]

I know that there is a difference between a set or a non-set option, but I'm not sure that I know how to tell the difference...

[Kyle Miller]

If o is the current options, I think you could do o.get linter.style.longFileOverride.name (o.get linter.style.longFile.name linter.style.longFile.defValue). There's also o.get? to get the value if it's set and return none otherwise.

[Damiano Testa]

Thanks a lot!

[Kyle Miller]

(I'm not sure what would be good option names. Another option is longFile -> longFileDefault and longFileOverride -> longFile ?)

[Damiano Testa]

I had thought also of linter.style.maxLines for the "non-modifiable" one.

[Damiano Testa]

By the way, I do not know if you saw this message, but that seems also partially relevant for this thread: if there was a way to retrieve all weak options from a dependency, that would be a possible answer!

[Ruben Van de Velde]

Has anyone downstream actually requested that they be able to use the linter with a different limit? I feel like there may be some overengineering going on

[Kyle Miller]

It costs very little to have one more option @Ruben Van de Velde, both in implementation and maintenance, and potentially it is less expensive in maintenance overall. What are you worried about in particular?

[Ruben Van de Velde]

Time spent discussing, probably :)