parse error on 1-line calc

Stream: lean4

[Floris van Doorn]

example (n m : Nat) : n ≤ m ∧ True := by
  constructor
  calc
    n ≤ m := by sorry
    -- _ ≤ m := by sorry
  trivial -- error "unexpected end of input; expected ':='"
-- error disappears with line 5 uncommented

[Sabbir Rahman]

calc is a tactic that works with transitive relations, and in particular uses transitive laws to connect each line. If you only put one relation (e.g. n ≤ m := by sorry), calc has no way to use transitive laws. That's why it expects at least two lines.

[Floris van Doorn]

This error already exists on v4.18 (also on v4.19-rc3), but I think this used to work at some point.

[Floris van Doorn]

Sabbir Rahman said:

calc is a tactic that works with transitive relations, and in particular uses transitive laws to connect each line. If you only put one relation (e.g. n ≤ m := by sorry), calc has no way to use transitive laws. That's why it expects at least two lines.

Even if you think this is bad style, it certainly shouldn't give a parse error. Especially not one that can parse many subsequent tactics before raising an error.
Also, the following works, so I'd assume this falls "in the spec" of calc.

example (n m : Nat) : n ≤ m := by
  calc
    n ≤ m := by sorry

[Kevin Buzzard]

one-line calcs are very dangerous things because of these parse issues. I strongly encourage students away from them.

[Floris van Doorn]

Oh, this behavior already exists for longer? Was this introduced to make the indentation of calc more flexible? I'm in favor of that, but I put the line at "if you return to the same column as the calc tactic, then that ends the calc-tactic.

I guess I should make an RFC for this.

[Kevin Buzzard]

What I tell the students right now is "one-line calcs are never useful in practice so always avoid them"

[Edward van de Meent]

This issue with calc is definitely known for some time

[Aaron Liu]

I have thought of a way to fix this, but I have not tested it yet.