General Suggestion for Better Error Message

Stream: lean4 dev

[Xiyu Zhai]

theorem my_lemma2 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε h1 h2 h3 h4
  calc
    |x * y| = |x| * |y| := by sorry
  sorry

section

The above code give the error unexpected token 'section'; expected ':=' at the word section.

However it's confusing for first timers, because it's too sketchy to tell obviously what's causing the problem and shown at a location far away from the actual problem (the calc block).

I suggest that add more information into the error message about why ':=' is expected, such as unexpected token 'section'; expected ':=' for calc block. A calc block is expected to have more than one lines. And it should be shown under the whole calc block.

In general, an error message shall be detailed enough so that it's obvious what's causing the problem and how to fix it and shown in the right location.

People think parsing is easy. Actually it's quite the opposite. It takes great effort to implement a user-friendly error-reporting system. As Lean community is grow larger and larger, I believe this problem is increasingly important. Don't end up like Ocaml, end up like Rust with great focus on user experience.

[Kevin Buzzard]

If you're able, then I think the devs would welcome a PR.

[Xiyu Zhai]

I’m now familiar myself with Lean4. Probably starting from June, I could attempt to start working on some improvements.

[Shreyas Srinivas]

Lean cares a great deal about UX, so there is little danger of the ocaml vs rust scenario you have mentioned. This particular error reporting issue is a long standing one that has been resolved for some cases. The basic issue is how to accommodate the flexibility that lean allows in its syntax with good error reporting. There have already been discussions about solutions to this issue.

[Xiyu Zhai]

I'm reading through the source code.

One thing I find could possibly improve is that there could be more elaborate Error type.

Now it seems that Error is just abbreviated for String type.

If we make Error an inductive type and delay the actually printing, it could benefit many things, including:

1. Separation of concerns. No need to worry about pretty printing in the parsing stage.
2. Handy for code fix suggestions. Later one could pattern match these errors to give user possible fixes for their code. If errors are reduced to string early in the stage, it's not easy.
3. Decide for Error originality. Some errors can be a derivative from other errors and need not be displayed to the user.

[Xiyu Zhai]

I know this could mean a major overhaul. But one could first do

inductive Error
| TypeMismatch
| Other (s: String) -> Error

with other absorbing all the unhandled cases.

[Xiyu Zhai]

In Rust which I'm most familiar, it's common that one use a different Error type for each code unit, and there are rules specifying error conversions.

[Kim Morrison]

@Xiyu Zhai, if you're interested in contributing to Lean, suggesting major changes or new features is not the way to go. Bugfixes (see open issues!) (or documentation!) are the place to start.