General contribution question: adding basic utilities

Stream: lean4 dev

[Thomas Murrills]

Sometimes you wind up making small utilities that feel like they belong in a core lean 4 file as opposed to appearing "randomly" in e.g. a mathlib tactic. For example, I needed a merge and a toKVMap function for KVMaps. These seem basic and general enough (and not bespoke) that they might belong in the file where all the KVMap utilities are defined.

However, basic utilities like this are often relatively minor—only a couple lines of code, without any significant design choices—so I wasn't sure if the "RFC thread > detailed issue > get go-ahead" procedure detailed in the contribution guidelines still applied. (I'm a relative newcomer working on tactic porting, so that's all that I know about; apologies if there are unwritten rules about this or if I missed the written ones!)

So: are contributions of small but basic utilities like this welcome? If they are welcome, is the procedure the same as for other features? And if so, should they be talked about/PR'd file-by-file, utility-by-utility (assuming you're contributing a couple small utilities in the same file), or in one big thread/issue/PR spanning several files (if you're contributing utilities in different places)?

I know there's a lot going on and not many core devs, so I don't want to inundate the dev team with small issues and PR's! But just thought I'd ask in case contributions like these would be useful. :)

[Henrik Böving]

basic utilities generally speaking are a thing for std4, lean core is only what the compiler needs to bootstrap itself. You can talk to @Mario Carneiro about std4 contributions.

[Scott Morrison]

Sometimes it makes sense to put these things in mathlib4 as well. If it's useful for porting, but Mario doesn't have the bandwidth to put them in Std4, then mathlib4 will take them. :-)

[Mario Carneiro]

You can also make an issue on std4 if you think something from mathlib4 should be migrated, and I will get to it eventually

[Mario Carneiro]

Note that mathlib4 has an entire subdirectory Mathlib.Lean for "things that feel like they ought to be in lean core but aren't". For developing mathlib tactics that's where you should probably default to.

[Scott Morrison]

Mathlib/Lean/