Zulip Chat Archive

Stream: general

Topic: VS code updating bug?


Patrick Massot (Jul 16 2020 at 14:49):

No, the Lean extension is not responsible for the Lean server. However there were also changes on the Lean side to accommodate the new fancy widgets.

Billy Price (Jul 16 2020 at 14:50):

Where should I submit this as an issue? It’s not clear to me where the source of the problem is

Patrick Massot (Jul 16 2020 at 14:55):

If you can't reproduce the issue without VSCode I would put it in the vscode-lean repo. In any case you expect Gabriel to handle it, and he is currently unavailable.

Patrick Massot (Jul 16 2020 at 14:56):

I also think this conversation has drifted and should not be in that stream. @Mario Carneiro could you move this to the general stream (since the first message of Billy mentioning this bug)?

Notification Bot (Jul 16 2020 at 15:16):

This topic was moved here from #Lean for the curious mathematician 2020 > Monday afternoon: metaprogramming session by Scott Morrison

Bryan Gin-ge Chen (Jul 16 2020 at 15:32):

I haven't tried to reproduce it yet, but I suspect this is an issue in Lean, since as far as I know, vscode-lean doesn't modify the cases of file imports and relies on the Lean server to resolve / manage imports.

@Billy Price Could you create an issue here: https://github.com/leanprover-community/lean

Billy Price (Jul 16 2020 at 15:48):

Done

Bryan Gin-ge Chen (Jul 16 2020 at 16:01):

Thanks! (link for future Zulip readers: lean#392)


Last updated: Dec 20 2023 at 11:08 UTC