lemma notation

Stream: batteries

[Eric Wieser]

Both docs#lemma and docs#Batteries.Tactic.Lemma.lemmaCmd exist; should the second one have lower priority to avoid ambiguous parsing?

[Mario Carneiro]

the second first one should not exist, it should have been removed when lemmaCmd was merged

[Mario Carneiro]

actually, it looks like the implementation is not ideal for the mathlib use case - turning an option on would affect only mathlib and not its dependents, and the docstring on lemma is also not very good if lang.lemmaCmd option is enabled

[Eric Wieser]

Mario Carneiro said:

when lemmaCmd was merged

Are you talking about a different lemmaCmd to docs#Batteries.Tactic.Lemma.lemmaCmd, which you say should be removed ?

[Mario Carneiro]

the easiest way to get desired behavior in mathlib is indeed to just make the priority of lemma slightly higher than default

[Mario Carneiro]

I think we need to rethink this implementation in batteries, it's not that easy to just flip a switch and turn on the command

[Eric Wieser]

What's the default notation priority?

[Mario Carneiro]

default

[Mario Carneiro]

you can write default+1

[Mario Carneiro]

maybe it would be better to just have batteries provide a function which does the equivalent of the present mathlib definition line called enableLemmaGlobally, and then mathlib can call it. That way we can centralize the metaprogramming machinery involved in one place

[François G. Dorais]

I don't understand why this needs to be a transitive option.

[Mario Carneiro]

batteries can provide both options

[Damiano Testa]

What happens if a downstream project opens a mathlib file with a lemma: would that parse?

[Mario Carneiro]

it's a mathlib choice whether it wants to do it globally or only within mathlib

[Mario Carneiro]

@Damiano Testa yes, lake respects project-local options

[Mario Carneiro]

I suspect that mathlib will either want to enable it globally, or add lang.lemmaCmd to the math template in lake (but there will still be a backwards incompatibility in this case for all projects downstream of mathlib using lemma today)

[Mario Carneiro]

For the project-local option, there is still the issue of the bad docstring though, I don't know any way to script around this issue

[Mario Carneiro]

I think we just need to make the docstring more ambiguous so that it reads okay for either possible setting of lang.lemmaCmd

[François G. Dorais]

The docstring in Batteries could be the same as in Mathlib. The error message is enough if the lemma option is not on. No?

[Damiano Testa]

If the option is not turned on, lemma is still a parse error, so maybe the doc-string in Batteries could be the one in mathlib. After all, lemma is still a "small" theorem...

[Mario Carneiro]

actually no, it's an elaboration time error now rather than a parse error. That's actually the reason for adding it to batteries in the first place: when it's a parse error you get much worse errors talking about applications and stuff

[François G. Dorais]

I don't see a definite plan after this discussion. Would someone volunteer to make an issue on Batteries?

PS: With more maintainers on Batteries, we can make better use of issues. This is still a TODO for now but we will get to it!

[Eric Wieser]

Mario Carneiro said:

the easiest way to get desired behavior in mathlib is indeed to just make the priority of lemma slightly higher than default

Is this a sensible immediate plan?

[Mario Carneiro]

yes, if it's causing issues please do that

[Eric Wieser]

#17533