Sebastian Ullrich

Thanks for the analysis. Since the original issue is about `readFile`, I believe the right course of action is to implement `readFile` independently of `getLine`, which it really should be...

We never use text mode: d85a4f5495a60a528befca9a2e77d461c2fbf918. We have two functions for reading raw binary data and for valid Unicode text.

Thank you for the detailed report. I can reproduce step 4 but not 1 in the sandbox. 

@digama0 We do believe that moving Mathlib's linters into a separate library (in the same repo) is achievable and independently valuable (for downstream users as well). This is likely true...

> Should this also adjust `LeanOptions`? @mhuisi We do not currently check the existence of options from `setup-file` at all, is that correct? Then making the server consistent with the...

That sounds like an okay compromise but at least it doesn't make additional support for weak options appear unreasonable. Added.

 Prototype developed with @nomeata at FRO retreat TODO: - [ ] test usefulness/annoyance factor - [ ] test reactivity, especially during editing in long files - [ ] support...

Err... you are totally correct, my mind simply assumed it had to be mirrored! Edit: edited

Closing for now, @datokrat will be working on this and related topics and is aware of this RFC but should not feel tied to it :)

> `if let x := then e1 else e2` Oops, now I remember what I thought was the tricky case! The problem with `notFollowedBy` is that it would yield a...