interaction of +foo and (config := …)

Stream: lean4

[Joachim Breitner]

Tobias Grosser said:

Perfect. This resolved the issue (when applied strategically). It took me a moment to realize that -implicitDefEqProofs followed by a config option has no effect.

@Kyle Miller is that interaction between config and new style options know and intended (or at least tolerated)?

[Kyle Miller]

@Joachim Breitner Yes, this is known. Configuration options are processed-left-to-right, and if you have (config := ...) then that overrides everything.

I had considered special casing (config := { fields* }) to be like doing (config := { cfg_so_far with fields* }), but that seemed a bit hacky and potentially more surprising than the current behavior.

[Joachim Breitner]

Hmm, I think I'd have expected that latter behavior, or at least a warning if I mix the two syntaxes in ways that are likely not as intended. Or maybe we can simply change the syntax so that (config := … ) can only come first and once, to sidestep the issue?

Is that related to how config options work with simp variants like dsimp are defined right now as a macro? Does simp_arith (config := {contextual := true}) work as it looks, or does that override the config adjustments done by simp_arith?

It's not pressing, but maybe worth tracking as a UX issue, I'd say.

[Joachim Breitner]

Ah, declare_simp_like_tactic uses appendConfig which works syntactically. Maybe this mechanism could be unified with merging new style options and old style options, so that all three ways of setting flags (simp-like tactics, old style, new style) interact the same way. Maybe this would allow the simplification (heh) of simp-like tactics implementation or be a simple macro expansion of simp_arith to simp +arith, removing a bunch of code there.

[Kyle Miller]

For (config := { ... }) syntax, I would think we should leave it alone and discourage using it anymore. We still want to support (config := ...) however, since it's used for presets. Search mathlib for (config := . (with the dot) to see examples.

I think it could make sense to make any (config := ...) that appears after the first configuration item result in a warning. One oddity though is that if a tactic macro initializes the configuration list with a (config := ...) preset, then a side effect is that any additional user-specified (config := ...) would be a warning. Probably for the best, though; the "right" way to handle a tactic-specific default configuration is to extend the configuration structure and set new default values. There's a bit of boilerplate there, since currently there's no macro-accessible way to change which structure type to use for elaboration of the config — you need to make a tactic elaborator and make use of a programmatic interface for the tactic.

Re simp_arith and friends, the way they expand simp_arith $items* is simp $items +arith, so (config := ...) does the right thing. (Before new-style configurations, the way it used to work is that (config := $e) would expand to (config := $f $e) for some configuration-updating function $f$.) The appendConfig system is primarily there to make it convenient to concatenate the underlying arrays in an optConfig (I couldn't get simp $cfg* +arith to work in quotations), but it turned out to also be a convenient way to coerce config? to optConfig as well for backwards compatibility.

I'm not sure what code you see for declare_simp_like_tactic that would be simplified?

[Kyle Miller]

Re the macro limitation: one solution could be to have an additional special case (config.type := S) that overrides which structure to use for elaboration of the configuration items, for the purpose of adjusting the default values. The assumption is that S is compatible in the { e with } casting sense.