goals accomplished

Stream: new members

[Johan Commelin]

Kevin Buzzard said:

Because there is no more begin/end it's apparently now far too confusing to have party hats, because they sometimes appear when you're not done. The issue is with the end, which is no longer there. If you are happy to use a by/tada block like we used to use begin/end blocks then you can use this code written by Mario:

import Lean
open Lean Elab Tactic

elab "tada" : tactic => do
  let gs ← getUnsolvedGoals
  if gs.isEmpty then
    logInfo "Goals accomplished 🎉"
  else
    Term.reportUnsolvedGoals gs
    throwAbortTactic

I suggest that we add this to batteries or mathlib. Maybe as qed tactic.
I'm also fine if we lint against it appearing in mathlib.

But recently I've had several requests/complaints that the lack of "Your are done with your proof, all is good now" feedback is really confusing for beginners/students. It is also a clear step back from Lean 3 in UX.

At the moment, the snippet above is using logInfo.

• This creates a blue squiggly line, which might still be perceived as "I need to fix this noisy output".
• It als means that No goals is still visible in the infoview. Is it possible to have it use widgets to overwrite the No goals in instead?

[Niels Voss]

I can definitely see how this would improve UX. But arguably, teaching newcomers that they should always put tada at the end of their proof and then later telling them that it is banned in mathlib seems a bit strange. I think it might be best to avoid misleading newcomers by telling them that by and tada always come in pairs, when they actually might not. If we are to introduce this, I still suggest we be honest that tada is a tactic, and not lie by saying it is part of the language's syntax.

I'm not necessarily opposed to this, I just think we should decide carefully if we actually want tada. (Also, isn't tada functionally equivalent to done?)

[Niels Voss]

As an alternative suggestion, maybe we could put the message inline instead of the infoview. I use a VSCode plugin called Error Lens which displays info right next to the code.
image.png

I'm wondering if we could maybe do the same thing and put a 🎉 or something after a finished proof. It could look something like this (ignore the #eval s please):
image.png

To be clear, I'm not suggesting we hook onto Error Lens; I'm just using it as an example to show that such a thing is possible. Also, this would probably need to be configurable, since I would imagine some people wouldn't like this.

[Bjørn Kjos-Hanssen]

:tada: has the undesirable side effect of encouraging the user to take a break from using Lean. (Hey, I'm done!)

[Marc Masdeu]

I would really like that Mathlib (or Batteries) allowed the user to type something like open newbie and that allowed for all sorts of newcomer-friendlyness (like turning off auto-implicit, the tada (which I rather call qed as suggested above...). The open newbie line would remind the user that they are working in learning mode, and one could even have a open newbie-transition that would suggest the appropriate changes when these tactics or extra syntax are being used. Would that make sense?

[Niels Voss]

I have mixed feelings about this. On one hand, there's definitely some UX improvements that might not be appropriate for more experienced users. But on the other hand, I don't think telling new users that the first thing they should write is open newbie is a very good first look.

What are some of the issues that you think would bother beginners but not experienced users? If it's just two issues (autoImplicit and an unsatisfying by block end) then maybe those two issues should be resolved individually (I am of the opinion that autoImplicit should be off for everyone by default, or at least restricted to single letter terms in Sort _, but that's a topic for a different thread).

[Niels Voss]

The thing is, I've never seen any other language have something like a beginner only mode. Some languages do have special modes (like javascript's use strict), but these are specialized modes for the use case, not the type of user. If you imagine the open newbie as being something that primarily makes the language stricter, then it should be called open strict. If it primarily prints out more diagnostic information, it should be called open verbose. But in any case, adding language features usually has a cost, and this is true for Lean in spite of its metaprogramming capabilities.

[Marc Masdeu]

I see. Maybe an alternative would be that lake included a config file by default, with some editable options with comments on what their effect is. For instance, you would see the autoImplicit line turned on by default (as is now, but with a comment saying that if you change this then it will avoid some newcomer's errors). It could have additional verbosity turned off by default as well, and so on. The advantage I see in something like this is that one would be able to discover and experiment with all these features that are sometimes buried inside zulip conversations.

[Niels Voss]

I think that's a much better option. What are some of the options, besides autoImplicit, that would be included in such a config? (I also don't know if Lean should be moving in the direction of having a bunch of flags to control language behavior (this kind of thing has led other languages to fragment into dialects), but that's just my opinion.)

[Marc Masdeu]

I would leave it to experts to figure out what sort hackery can be accomplished with such flags. The moment you allow it, I am sure that people will come up with powerful ideas. I don't see how the problem of fragmentation into dialects could occur, as long as Mathlib imposes its own set of flags. Code submitted to Mathlib would have to adhere to that.

[Niels Voss]

Maybe not necessarily fragmentation (so long as we don't introduce any flags that require the same flag to be enabled downstream, like e.g. agda's --cubical flag), but in an extreme case it would mean a large portion of Zulip messages would need to start by posting a list of what options are enabled in the current context.

[Niels Voss]

As for the topic of this thread, I'm not sure having a flag to require qed at the bottom of every by block would be the best idea, but I can see its appeal (as long as it doesn't apply to one-liners like have : ... := by linarith)

[Kevin Buzzard]

Just my two cents: firstly, I think someone who doesn't have a programming background and doesn't have a clue what's doing on won't even understand the difference between "this is a tactic" and "this is part of the syntax". Secondly, I actively teach newbies that "by...done" is the syntax and have them code with the done at the end, when they're learning

[Niels Voss]

Do you think a specialized qed or tada tactic is needed, or is done good enough?

[Marc Masdeu]

Niels Voss said:

Do you think a specialized qed or tada tactic is needed, or is done good enough?

(Although the question was not probably directed to me) I would be happy with the done tactic as is, if the blue squiggly line could be removed.

[Kevin Buzzard]

I think that if we can repurpose done to put the emoji there, that would be excellent.

[Joachim Breitner]

We have ideas for a better visual indication of unsolved goals in the VSCode extension, but they require some more infrastructure under the hood to be really good (flicker-free etc.). It’s the dual of tada in that you’ll get a visible indication that there is work to be done, than an indication that all is done, but I expect i will improve UX here noticably. I am somewhat optimistic that we’ll see it within the next year, barring unexpected technical issues.

[Mario Carneiro]

It’s the dual of tada in that you’ll get a visible indication that there is work to be done, than an indication that all is done

Isn't that exactly the problem though? Lean is all about reporting success by just not saying anything, but if you are a newcomer you may not be used to this workflow and would prefer some positive indication that everything is done

[Mario Carneiro]

You have to have at least a bit of trust in the system that if errors exist they will be reported and e.g. your extension isn't simply unloaded

[Joachim Breitner]

That’s true, and I think we also considered some positive overall per-declaration indication, and it would be able to use the same infrastructure, I assume. We’ll see how pressing it is when at least the “open goals” indication is no longer easy to miss.

[Floris van Doorn]

This is lean#4190 (superseding lean#1970)
The difficulty is to figure out the difference between "you are done with this part, but the proof is not done" and "you are completely done with this proof".
If you're happy to show a :tada: in both cases, then that is trivial to implement.

[Johan Commelin]

I think we can still offer qed for people who like a visual clue in their source and infoview that the proof is over.
I think having this tactic is harmless, and people won't have much trouble understanding that the tactic is optional, and that mathlib style excludes it.

[Floris van Doorn]

I've been using by {and } as my begin/end blocks when teaching Lean, mostly so that the error is on the closing brace instead of the (more easily missable) by. I don't mind also having a qed like this, of course.

[Kevin Buzzard]

Oh that's also a nice idea!