mathlib4: autoImplicit false by default?

Stream: general

[Eric Wieser]

Various Zulip threads have complained that autoImplicit true (the status quo in mathlib4) is a repeated footgun for newcomers and experienced users alike.

[Eric Wieser]

I understand that this opinion is not universally held, so I am not proposing _banning_ autoImplicit true in mathlib. What I propose instead is having the footgun not be pointed at our feet by default, and that mathlib4 files announce that they are in footgun mode with set_option autoImplicit true.

[Eric Wieser]

I've created #6528 (which includes a slightly longer justification), which changes the default in mathlib4 to be autoImplicit false. To make this build, 317 files gained set_option autoImplicit true.

[Eric Wieser]

/poll What should mathlib4's stance on autoImplicit be, assuming we keep relaxedAutoImplicit false

• true by default, set_option autoImplicit false discouraged
• true by default, set_option autoImplicit false allowed
• false by default, set_option autoImplicit true allowed
• false by default, set_option autoImplicit true discouraged

[Eric Wieser]

(as a reminder, if we leave relaxedAutoImplicit the same, then autoImplicit true means "create single-letter variables automatically" and autoImplicit false means "give an error if I refer to a single-letter variable I forgot to declare")

[Matthew Ballard]

I think we need to know if there is a performance drag with auto implicits.

[Jireh Loreaux]

If there is a performance drag with them I will change my vote.

[Alex J. Best]

(deleted)

[Eric Wieser]

To give one performance data point: replacing Type _ with Type* was an overall wall time speedup of ~3%. If all of mathlib used autoimplicits (which generate Type _), then it would have not been possible to replace any of these.

[Mario Carneiro]

I would caution against using this performance argument against Type _ vs Type*, because I think there is an alternative solution (level metavars -> vars at the :=) which will get a similar speedup without needing Type* and which also applies to autoimplicits

[Eric Wieser]

About 10% of files currently use autoImplicit; so a reasonable estimate would be that purging it entirely (an extreme interpretation of option 4) would only gain us another 0.3% wall time, which I don't think justifies doing so.

[Eric Wieser]

I don't think performance improvements should be the main motivation here; switching to Type* from Type _ distances us from a particularly surprising class of foot gun, just as changing the default for autoImplicit would.

[Mario Carneiro]

the alternative solution also prevents the footgun issue

[Eric Wieser]

I don't agree, it just takes us back to the weaker version of it we had in lean 3

[Mario Carneiro]

remind me?

[Eric Wieser]

we would occasionally end up with declarations that unified to max u v everywhere instead of separate u and v universes. We had a linter that could catch the obvious cases, but it wasn't perfect.

[Eric Wieser]

And it could be triggered by things before the :=

[Mario Carneiro]

Type* will fix that, I'm just not convinced that it's a sufficiently big deal to make it mandatory even in basic files that don't have these universe issues

[Mario Carneiro]

(we still have the max u v linter BTW)

[Eric Wieser]

Yes, hopefully the structure of the poll above makes it clear that I am not proposing making anything mandatory

[Mario Carneiro]

I'm a bit against set_option autoImplicit in mathlib files, because it means that you don't know when opening a random file whether autoimplicits are legal or not and this makes interpreting statements harder

[Mario Carneiro]

I don't think we have precedent for that kind of "stylistic choice" on a per-file basis in mathlib

[Eric Wieser]

We already have that stylistic choice now, but without a marker to indicate that it's been made or CI to enforce it remain consistent. Files from mathport typically use the variables style, a handful of new files presumably use autoImplicits only

[Mario Carneiro]

If it is used, it should be because of some actual behavioral difference relevant to the content of the file (e.g. a pattern which frequently causes the max u v bug in that file), not because of the author's stylistic preference

[Eric Wieser]

I think "authors stylistic preference" is better than the status quo of "authors stylistic preference ∪ authors accident"

[Mario Carneiro]

I would exclude mathport-isms as just slightly shoddy style which will get cleaned up in time. But we should try to have a uniform style prescription, existing violations notwithstanding

[Mario Carneiro]

besides, any decision here isn't going to decrease the number of mathportisms in mathlib

[Mario Carneiro]

unless we take mathport style as gospel, and even then it wouldn't really work because mathport style changed over the course of the port

[Eric Wieser]

No, but a decision here makes a clear marker that labels a file that uses mathportisms from one that doesn't

[Mario Carneiro]

that sounds a little scary, like we would have a second wave of "style porting" mathlib

[Eric Wieser]

What are we considering a mathport-ism here?

[Eric Wieser]

We already have that second wave lined up with things like refine' vs refine, right?

[Mario Carneiro]

A mathport-ism is when mathport's output doesn't match idiomatic lean 4 style. This term is only as well-defined as the notion of lean 4 idiomatic style itself

[Mario Carneiro]

Yes, refine' is a mathport-ism

[Mario Carneiro]

also cases' and induction'

[Mario Carneiro]

I still anticipate we can eliminate all cases of refine' et al in one fell swoop once we fix the technical hurdles to doing mass AST rewrites

[Yaël Dillies]

I am very much in favour of keeping refine' around for the reason I already mentioned: When I'm writing a proof and apply lemma x, I don't want to try the $2^n$ combinations of _ and ?_ where $n$ is the number of explicit arguments to x. In short, refine is a good idea for proof-reading, but a terrible one for proof-writing (at least in the current situation where there's no automation for introducing the _ and ?_ in the right spots).

[Eric Wieser]

That sounds like an argument for refine' to have a try this action

[Eric Wieser]

A summary of the poll so far as it relates to #6528:

• 5 people prefer autoImplicit true as default (the status quo) (p2 \ p3)
• 5 people do not care what the default is as long as we're permissive (p2 \inter p3)
• 18 people prefer autoImplicit false as the default (p3 \union p4 / p2), of which 10 (p4 / p3) feel very strongly

[Anatole Dedecker]

Yaël Dillies said:

I am very much in favour of keeping refine' around for the reason I already mentioned: When I'm writing a proof and apply lemma x, I don't want to try the $2^n$ combinations of _ and ?_ where $n$ is the number of explicit arguments to x. In short, refine is a good idea for proof-reading, but a terrible one for proof-writing (at least in the current situation where there's no automation for introducing the _ and ?_ in the right spots).

Note that you can just write _ everywhere and see where Lean complains. But I'm not claiming it's a perfect solution

[Eric Wieser]

Given the vote and my aggregation above, I propose we merge/delegate #6528. It's likely to go stale fast, and every time it gets fixed it effectively starts with a fresh cache.

It's worth noting that it is very easy to revert #6528 if we change our minds later with a simple find and replace.

[Johan Commelin]

I kicked it on the queue

[Eric Wieser]

I wouldn't be surprised if the build fails in one or two place due to rot in the last 3 days, but I guess we'll find out!

[Eric Wieser]

It turns out this is picking up conflicts faster than I can fix them!

[Eric Wieser]

3 hours of babysitting (and distracting bors from interfering) from when it first hit the queue and it finally passes CI