behaviour of `exact` in lean4

Stream: new members

[Damiano Testa]

Dear All,

in the Lean4 code below, placing the cursor after exact gives Goals accomplished :tada: in the infoview (besides of course also giving an error):

example (p : Prop) : p := by
  exact--place cursor anywhere on this line after the first `e`

Is this expected?

The analogous Lean3 code

example (p : Prop) : p :=
begin
  exact
end

does not do this.

[Damiano Testa]

(apply, refine, refine' also show similar behaviour.)

[Kyle Miller]

I think it's due to the way Lean 4 inserts sorries at parse errors.

theorem foo (p : Prop) : p := by
  exact
  -- Goals accomplished!

-- error: expected term (at `#print`)
#print foo
/-
theorem foo : ∀ (p : Prop), p :=
fun p => sorryAx p true
-/

[Kyle Miller]

I find it a little concerning that it doesn't report declaration uses 'sorry', but on the other hand if a file has parse errors you shouldn't trust it at all.

[Damiano Testa]

Ok, thanks!

I am a little puzzled by the Goals accomplished response, but what you say clarifies the issue somewhat.

[Kyle Miller]

I wonder if it would be possible if instead of "Goals accomplished" it could say "No more goals, but contains sorry". This is a somewhat confusing Lean 4 behavior that makes "Goals accomplished" a bit less exciting.

[Damiano Testa]

I agree, not seeing Goals accomplished would be better. Even simply "declaration uses sorry", without mention to the non-existence of goals would be good!

[Matthew Ballard]

My students hate this.

[Kyle Miller]

@Matthew Ballard I actually had your message in mind, but I was too lazy to find a link to it.

[Kyle Miller]

Maybe, if one doesn't already exist, it would be worth making a Lean 4 issue with some examples with false "Goals accomplished" messages (false in that it's telling me I've accomplished my goals when I don't feel like I have).

[Patrick Massot]

I haven't try to teach using Lean 4 yet, but indeed I think this behavior would be really really confusing for students.

[Heather Macbeth]

The premature "Goals accomplished" issue was discussed at the mathlib porting meeting this week, cc @Mario Carneiro, @Scott Morrison, @Patrick Massot, ...

I had to leave before that discussion was finished, but I believe there was a proposal that we have different "no goals" and "goals accomplished" messages for the different situations. Did that proposal reach consensus from mathlib folks? If so, should we open a Lean 4 issue?

[Mario Carneiro]

I think so, this is all working as designed in some sense but I don't think it is arguable that this is confusing behavior so it just needs a specification for how to do better

[David Renshaw]

Could we report an error (or warning) on the exact line?

[David Renshaw]

It seems to me that the core problem is that the parsing error shows up far away from where it needs to be addressed.

[Heather Macbeth]

Mario and I just PM'd a bit about this, and I quote some of his comments with his permission. He clarifies the proposal from the meeting on Thursday and points out that it still doesn't make "goals accomplished" work as expected in some cases:

the proposal was basically to not use goals accomplished if there are any synthetic sorries in the goal, such as might be created by an erroring tactic

that's still a bit non-local though, for example here:

example : True := by
  have : True := by
    apply id
    exact trivial
    -- here
  apply id
  exact syntax error

in this example, we will get a "goals accomplished" message at the indicated location currently, do you find this to be a good thing or a bad thing? Under the proposal this will be shown as "no goals" because of the syntax error on a later line

[Heather Macbeth]

And regarding the example at hand in this thread, he concludes as @David Renshaw did that the premature "goals accomplished" is really a symptom, not a cause, the cause being Lean 4's "better" (i.e., more optimistic, and less dependent on separators like ,) parser than Lean 3.

that's because lean 3 completely falls over when there is a parse error

when there are parse errors you can't get anything useful from the goal view

so you have to be really good about putting commas and underscores when working with lean

count all the instances of don't forget the comma in NNG

[Heather Macbeth]

Personally, I have come to the conclusion that there is no possibility of having a sensible "goals accomplished" in Lean 4. It is a tradeoff, basically, and we lost it when we got rid of the commas. I propose that we rename "goals accomplished" to "no goals" so that it seems to imply no particular promise.

[Heather Macbeth]

For teaching I would combine that with @Adam Topaz's suggestion of inserting done at the end of each exercise so that at least the errors get localised to one exercise and don't drift into the next.

[Notification Bot]

8 messages were moved from this topic to #mathlib4 > premature "goals accomplished" by Heather Macbeth.