Zulip Chat Archive

Stream: general

Topic: Catalogue of errors?


Stuart Presnell (Jan 29 2022 at 18:26):

Do we have a page where the common error messages are listed and explained, with hints for how to deal with them? For example, explaining what ambiguous overload means, or why two apparently identical expressions have failed to unify.

Bryan Gin-ge Chen (Jan 29 2022 at 18:27):

As far as I know such a thing doesn't exist, but it sounds like it'd be quite helpful.

Bryan Gin-ge Chen (Jan 29 2022 at 18:28):

I usually search this Zulip for error messages if I get confused by them.

Stuart Presnell (Jan 29 2022 at 18:38):

How would one create such a page and set things up so that people could PR entries and edits to it?

Eric Rodriguez (Jan 29 2022 at 18:39):

github.com/ericrbg/leanFAQ

Eric Rodriguez (Jan 29 2022 at 18:39):

feel free to add anything you want to the wiki :)

Eric Rodriguez (Jan 29 2022 at 18:39):

I'd recommend "technical issues" for this sort of thing

Johan Commelin (Jan 29 2022 at 18:39):

Yeah, I think it's good to follow the model of the FAQ

Johan Commelin (Jan 29 2022 at 18:40):

At first, it should be easy for people to just add a bunch of things. Once it reaches a somewhat stable state, we can easily make it available via the community website as part of the docs.

Bhavik Mehta (Jan 29 2022 at 18:54):

I think I was originally imagining the FAQ to contain this catalogue of errors, but I don't see why it shouldn't be a separate document!

Stuart Presnell (Jan 29 2022 at 19:14):

Yes, I think a separate document would be better


Last updated: Dec 20 2023 at 11:08 UTC