Patrick Massot

I can confirm the issue on a new machine. Downgrading kalamine to 0.22 fixed it.

This was Étienne, I use none of these in my project because I hate dangling parentheses.

I fully agree, and this is an issue for teaching especially. My workaround is to use the [Error Lens](https://marketplace.visualstudio.com/items?itemName=usernamehw.errorlens) VSCode extension, but this shouldn't be required.

This description mixes Lean 3 and Lean 4 so it cannot work. You should decide which version you want to use. mathlibtools and leanproject are Lean 3 only, and you...

I really *really* don't think we should make the Lean extension harder to install only to please Agda users.

I think the warning should be more visible than using a light-grey color.

Let's wait until #3 stabilizes then. Also I don't think we should merge this without checking the Qt code. Hopefully commands.py should be very stable and that won't happen to...

@kevinsullivan it would be nice to follow up on this so that your course can be added to the webpage.

It would be nice if the Lean core development could document that kind of changes. Did you see anything there?

I meant that the Lean server mode is globally undocumented, and it would be nice if new cool features like this widget thing could change that undocumenting tradition.