User tags conflicts

[MartinKolarik]

It seems we previously missed the fact that GitHub usernames may contain dashes, which leads to possible conflicts in user tags. u-xxx-yyy-zzz may mean:

• user xxx, tag yyy-zzz,
• user xxx-yyy, tag zzz,
• and now after feat: mark user owned probes in API responses #607 also user xxx-yyy-zzz

It's not just a theoretical problem, about 7.5% of our users have a dash in their username.

I see a number of solutions, but each creates some problems as well since many users have already set some tags. The best thing to do long-term is to use a different character to separate the username from the user's own tag while preserving the current tags until the users change them.

Specifically, the user tag should change to u-${username}:${tag}, which would change the above cases to u-xxx:yyy-zzz, u-xxx-yyy:zzz, and u-xxx-yyy-zzz.

We can set a flag for all the existing tags to use the old format and only apply the new format (for all tags of that probe) when the user edits the tags (a message must be shown in the editing UI in these cases).

[jimaek]

A tag with a : just doesn't feel right. What's wrong with keeping the same format?

user-dash -> u-user-dash-tag

The last dash is the tag, everything before is the username with a prefix

[MartinKolarik]

Everything before is not the username because the tag part contains dashes as well (very often). We need a different character and : is the prettiest one from those available.

[jimaek]

We don't plan on using them in URLs? Also won't it break the magic locations input?

[MartinKolarik]

The only special character for magic mode is + so far, so that's fine. I also don't see where we would need them in URLs, but even if we did it would be fine, : doesn't need any encoding.