feat: accept user-defined options on the cmdline

[Kha]

Initial options are now re-parsed and validated after importing. Cmdline option assignments prefixed with weak. are silently discarded if the option name without the prefix does not exist.

Fixes #3403

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4741 has successfully built against this PR. (2024-07-14 16:25:14) View Log
• ✅ Mathlib branch lean-pr-testing-4741 has successfully built against this PR. (2024-07-15 08:38:44) View Log
• ✅ Mathlib branch lean-pr-testing-4741 has successfully built against this PR. (2024-07-26 10:19:32) View Log
• ✅ Mathlib branch lean-pr-testing-4741 has successfully built against this PR. (2024-08-02 13:17:14) View Log

[mhuisi]

Should this also adjust LeanOptions?

[digama0]

I think it would be useful to be able to set options that are ignored if not declared in the imports. For example, suppose we want to set an option project-wide which is defined in the project itself (e.g. a mathlib linter which is supposed to only take effect in mathlib itself). In this case the file which defines the option and any files that don't import this file will have to be special cased by lake in order to avoid passing the option to these files and getting the unknown option error. This also mimics the behavior of -D flags in C or environment variables - just let the options pass if you don't recognize them.

Alternatively, this could be another type of "weak" option flag, which could be used when this is specifically the intent, and leave the default to check options eagerly.

[Kha]

@digama0 We do believe that moving Mathlib's linters into a separate library (in the same repo) is achievable and independently valuable (for downstream users as well). This is likely true for other projects as well, though I don't want to exclude the possibility of adding some weak option support further down the road if the benefit is clear.

[Kha]

Should this also adjust LeanOptions?

@mhuisi We do not currently check the existence of options from setup-file at all, is that correct? Then making the server consistent with the cmdline sounds like a good follow-up change to me. This PR as is at least should not be able to break anything, so I'd like to see it in the next RC.

[mhuisi]

Should this also adjust LeanOptions?

@mhuisi We do not currently check the existence of options from setup-file at all, is that correct? Then making the server consistent with the cmdline sounds like a good follow-up change to me. This PR as is at least should not be able to break anything, so I'd like to see it in the next RC.

Yes, I think you are correct.

[digama0]

@digama0 We do believe that moving Mathlib's linters into a separate library (in the same repo) is achievable and independently valuable (for downstream users as well). This is likely true for other projects as well, though I don't want to exclude the possibility of adding some weak option support further down the road if the benefit is clear.

Even if we did move all mathlib linters into a separate lean_lib (which I agree can be justified by other means than having to work around lean limitations), it wouldn't solve the problem unless we imported the entirety of this lib in every mathlib file, which is a technique we are trying to move away from because it leads to import bloat. This is especially true if some linter involves a reference to some nontrivial part of mathlib, so I think it would end up just limiting our ability to build and deploy these linters.

[nomeata]

Would it work to have a very small library mathlib_flags with possibly just a single file that just declares the options? Not the most elegant of setups, but maybe a good compromise – after being told that you misspelt an options is a worthwhile feature?

[Kha]

That sounds like an okay compromise but at least it doesn't make additional support for weak options appear unreasonable. Added.

[tydeu]

@Kha While I very much like the notion of "weak" options here, I am worried about having two different notions of weakness between Lake and Lean. "weak" in Lake means not included in the trace. Since since options are part of the trace, that notion of weakness could applied here. Therefore, could I bike-shed for perhaps using "try" instead of "weak" as the prefix for these options? (Alternatively we could come up with another word for Lake's notion, but it seems easier to change this than that.)

[nomeata]

local. maybe, as in “locally in this package defined option”?

[david-christiansen]

Or perhaps checked vs unchecked options?

[kmill]

Collecting possible prefixes as an alternative to weak:

• user
• local
• unchecked
• deferred
• flex
• lazy

Maybe in the end weak is the best of these, because validation is only done weakly. It's not user or local since it can be applied to builtin options, it's not completely unchecked since if the option exists its value does get checked, and it's not deferred or lazy since using weak turns off existence checking. The only remaining alternative is flex, as a synonym for "lenient" or "relaxed".

[tydeu]

@kmill A rather verbose alternatively would be an unrequired option (or, funnily, an optional option ).

[kmill]

Should we use this as an opportunity to teach about the feature?

Suggested change

	throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'"
	throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}', if this is a user-defined option use '-D{`weak ++ name}'"