Zulip Chat Archive
Stream: general
Topic: warnings
Reid Barton (Dec 27 2018 at 17:40):
There isn't any way to suppress all warnings or specific warnings from lean, is there?
Johan Commelin (Dec 27 2018 at 17:53):
In the editor? Or in compiler output in the terminal?
Reid Barton (Dec 27 2018 at 17:54):
In the terminal
Reid Barton (Dec 27 2018 at 17:54):
preferably, from the command line
Johan Commelin (Dec 27 2018 at 17:54):
You could just pipe via grep...
Johan Commelin (Dec 27 2018 at 17:54):
Completely customisable, but maybe not exactly user friendly
Johan Commelin (Dec 27 2018 at 17:55):
What kind of filtering are you looking for?
Reid Barton (Dec 27 2018 at 17:58):
Often I want to suppress the many "warning: imported file uses sorry" messages, and sometimes I want to ignore the messages about using sorry as well
Johan Commelin (Dec 27 2018 at 18:03):
That seems like something that grep could do for you.
Last updated: Dec 20 2023 at 11:08 UTC