Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

Limit the amount of error messages #1912

Open
Kha opened this issue Jan 24, 2018 · 0 comments
Open

Limit the amount of error messages #1912

Kha opened this issue Jan 24, 2018 · 0 comments

Comments

@Kha
Copy link
Member

Kha commented Jan 24, 2018

It is not too hard to make Lean produce thousands of error messages, at least when working on the core lib. This can noticeably slow down editors (flycheck outright disables checkers that produces > 400 messages) and is not exactly any more helpful on the command line. Should we add a flag to limit the amount of error messages? With some reasonable default (50?)?

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant