Possible lake `get_config?` regression

Stream: lean4

[Sky Wilshaw]

I have the following snippet in my lakefile:

meta if get_config? env = some "dev" then
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "main"

I execute this code locally with lake -Kenv=dev update. But since leanprover/lean4:v4.5.0-rc1 (I think?), the -Kenv=dev flag doesn't seem to do anything. For example,

post_update do
  IO.println (get_config? env)

prints none. I can't see anything in the update notes about this behaviour.

[Mario Carneiro]

cc: @Mac Malone

[Mac Malone]

@Sky Wilshaw I suspect you need to run lake -R -Kenv=dev update.

[Sky Wilshaw]

That does indeed fix the issue, thanks.

[Sky Wilshaw]

In future runs, will I need the -R flag?

[Mac Malone]

@Sky Wilshaw Without -R will used the cached configuration, instead of re-elaborating the configuration. -R forces a reconfiguration. To change -K options, you need to reconfigure. Some more details on the matter are mentioned in the v4.1.0 release notes.

[Mario Carneiro]

so this is not anything new to v4.5.0, right

[Sky Wilshaw]

That's interesting. I seem to have been able to use -K flags without reconfiguring until this update, which is weird.

[Mac Malone]

There has been some dicussion on improving this matter and making things work more intuitively.

[Mac Malone]

@Sky Wilshaw Lake will also reocnfigure automatically if detects it needs to (e.g., if the toolchain changes, there is no cached configuration, etc.). It may be that your previous times changing the -K options worked because they concided with an automatic reconfigure.

[Sky Wilshaw]

That would explain things - I use this script to bump mathlib, which (due to my frequency of updating) often coincides with a toolchain bump.

[Sky Wilshaw]

Thanks for clearing up the issue!

[Mac Malone]

You're welcome!

[Mac Malone]

Mario Carneiro said:

so this is not anything new to v4.5.0, right

One thing that did change in v4.3.0 is that the options are now persisted in the trace. Thus, automatic reconfigures no longer take the options from the command line, but rather those from the trace. This could explain why @Sky Wilshaw's script now stop working. For instance, on a v4.3.0 -> v4.4.0 bump it would use the cached options whereas on a v4.2.0 -> v4.3.0 bump it would use the CLI options.

[Yaël Dillies]

Sky Wilshaw said:

That's interesting. I seem to have been able to use -K flags without reconfiguring until this update, which is weird.

Me too, in fact. And I bumped my projects very regularly. So something really seems to have happened in v4.5.0.

[Sky Wilshaw]

What do you mean by the "trace"? Is there some documentation I can look at?

[Sky Wilshaw]

It's also possible that something in mathlib's lakefile changed recently and so these changes only mattered now.

[Mario Carneiro]

this is supposedly internal details, so I don't think there is much docs on it

[Mac Malone]

@Sky Wilshaw Sorry for the confusion. The trace in question is .lake/lakefile.olean.trace which is an internal file used to version the configuration cache. On the user end, the current rule (since v4.1.0) is that -K options should not be used without -R.

[Mario Carneiro]

but the existence of caching that sometimes ignores your settings is something that needs documentation

[Sky Wilshaw]

Is it ever correct behaviour to pass -K flags without -R? If not, should a warning or error be raised by lake?

[Mario Carneiro]

the name -R "reconfigure" certainly doesn't help, people universally have no idea when to use it

[Mac Malone]

Mario Carneiro said:

but the existence of caching that sometimes ignores your settings is something that needs documentation

That part is documented in the v4.1.0 release notes I mentioned.

[Mario Carneiro]

this is not a release notes thing, it needs to be a part of the permanent documentation

[Mac Malone]

Sky Wilshaw said:

Is it ever correct behaviour to pass -K flags without -R? If not, should a warning or error be raised by lake?

An error would have been a good idea, yes.

[Mario Carneiro]

at least until it is replaced by something saner :)

[Mac Malone]

Mario Carneiro said:

this is not a release notes thing, it needs to be a part of the permanent documentation

While I do agree, there is a question of where. In some part of the README? I doubt that would get much more visibility than the release notes.

[Sky Wilshaw]

Maybe in lake --help? I see no help option for -K flags at the moment.

[Mario Carneiro]

Sky Wilshaw said:

Is it ever correct behaviour to pass -K flags without -R? If not, should a warning or error be raised by lake?

The other pitfall is that after using -K and -R to set options, if you ever want to remove the -K option you have to use -R again, using lake without arguments will keep using the -K option

[Mac Malone]

Yeah, this is largely why -R is separate from the -K.

[Mario Carneiro]

and the other other pitfall is that if you don't pass -K options every time, after learning that they are persisted most of the time as long as you don't pass -R, then you are the mercy of lake's auto reconfigure logic whether that state will be lost and you start compiling with default settings again

[Mario Carneiro]

not sure if this is what changed in 4.3.0

[Mac Malone]

Mario Carneiro said:

not sure if this is what changed in 4.3.0

That is one thing that changed (automatic reconfigures preserve the options now).