Conversation

You know what? I make an effort to always use plain language and try to come accross as matter of fact (playfulness might be accepted but is frowned upon) in diagnostics, but just removing the leading "error:" might actually be a small change ti reframe the interaction.

Jon Purdy

@evincarofautumn

Exactly! Doing that has led me in a direction I like, at least. Including a “warning” or “error” prefix does serve some purposes, like helping IDEs/editors format messages that follow (or vaguely imitate) the standardish GNU format, although those tags aren’t very informative.

Jon Purdy

@evincarofautumn

“Error” might be “I can’t”, or “You’ve asked me not to”, or “I will, but only if you super-promise that these shenanigans are what you meant to do”; “warning” might be about anything: style, performance, possible issues, or even *likely* issues too noisy to make errors.

Any idea what a better prefix would be? Or would it be better to just remove it? Or do we dial down the severity of this stuff in development, so you get 'info' and 'note' messages instead, leaving the errors for CI and release builds?

(this doesn't solve the issues you raised in the previous tweet, just wondering as somebody who makes a diagnostic reporting library, hehe 😳)

Esteban K�ber –

@ekuber

If you can break with convention, removing `error: ` is an easy win

Yeah, thinking maybe it would be good to demonstrate that in the examples and documentation. Try to nudge downstream tool-makers in the right direction I guess… ‘this is what your tool could be like’ – hehe :)

Rasmus Källqvist

@RasmusKallqvist

12:29 PM · Oct 9, 2021Twitter Web App

Maybe "reason:" could work as a prefix? As in "the reason compilation stopped". Otherwise "info" is probably good

Replying to

and

What about "fixme: "? Thinking about this:

Quote Tweet

Daniel Patterson

@dbp__

· Oct 9, 2021

This is most obvious with refactoring — experienced programmers will structure a refactoring so that the type checker tells them everywhere they need to fix (whenever possible…). Those “errors” are just a checklist from a very diligent partner.

Show this thread

Replying to

Also thinking about hole driven development, and about that gives you a bunch of 'todo's for missing parts of the code you still need to fill in… sometimes those are displayed as warnings, or in an interactive side-panel in your IDE/editor. 🤔

GitHub - leanprover/vscode-lean: An extension for VS Code which provides support for the Lean...

Thinking about Lean's info panel, which is a bit like a todo list (you can even add custom widgets for your own datatypes): github.com/leanprover/vsc – they still use red squigglies and text for ‘errors’ though. Other theorem provers have similar ways of listing your ‘goals’…

github.com

An extension for VS Code which provides support for the Lean language. - GitHub - leanprover/vscode-lean: An extension for VS Code which provides support for the Lean language.

Show replies

Replying to

and

I think that sounds good, but it will probably depend on what the overall context is. If it's always prefaced with "Compilation could not continue" or something? And then the fixme's is what must be solved