Issues with Agda Mode symbols in VSCode

Learn
1

Apologies for the Agda focused question but many Agda devs hangout here and there doesn’t seem to be any movement on this issue in other Agda focused spaces.

Many Windows users of Agda via VSCode have issues with certain symbols turning into question marks when type checking a file. Here’s an example from before type checking and after:

screengrab of a piece of Agda code defining a type named "B" in blackboard font.
screengrab of a piece of Agda code defining a type named "B" in blackboard font.594×520 29 KB

screengrab of the same code after type checking, the file is correctly colored but all occurrences of the blackboard "B" have been replaced with pairs of question marks inside of diamonds.
screengrab of the same code after type checking, the file is correctly colored but all occurrences of the blackboard "B" have been replaced with pairs of question marks inside of diamonds.628×520 31 KB

Does anyone have any opinion on what’s going on here, if it’s most likely a VSCode issue, or something with Agda mode itself? I have no experience with the internals of VSCode, but I’ve finally gotten to the point in my work where I can no longer ignore the issue and so am willing to put effort into fixing it. The problem is I have no idea where to start.

Thanks for any help, it is deeply appreciated.

1 Like
2

Have you tried asking on their Zulip?

1 Like