View build logs without sorry?

Stream: Analysis I

[Li Xuanji]

Running lake build prints lots of logs like this

warning: /Users/xuanji/gits/analysis/analysis/Analysis/Section_4_3.lean:52:8: declaration uses 'sorry'

Is there an argument I can pass to suppress them and only see errors (not warnings)?

[Ruben Van de Velde]

Not quite, but you can add

[leanOptions]
warn.sorry = false

to lakefile.toml just for these warnings

[Li Xuanji]

Any idea how to set that in lakefile.lean (which this project uses)?

[Ruben Van de Velde]

Uh, maybe

lean_lib foo where
  leanOptions := #[⟨`warn.sorry, false⟩]

(untested)