VS code updating bug?

Stream: general

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

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

[Bryan Gin-ge Chen]

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]

Done

[Bryan Gin-ge Chen]

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