github_repo: strip v prefix if revision is any version number

`github_repo` currently strips the `v` prefix from the file names in the
zip file downloaded from GitHub if `revision` is a semver, since GitHub
silently does the same if asked to archive the code for semver-like
tags. It looks like this logic extends to more than just semvers,
though - the same behaviour has been observed for strings that are
simple dotted version numbers with any number of components (e.g.
`1.1.10.1`). Account for this in the prefix-stripping logic.

Fixes #2829.

rules/subrepo_rules.build_defs

@@ -202,9 +202,19 @@ def github_repo(name:str, repo:str, revision:str, build_file:str=None, labels:li
     org, _, repo = repo.partition('/')
     assert repo, "Must pass a valid Github repo argument, e.g. thought-machine/please"
 
-    # If it looks like semver, we need to remove the v from it because github formats their zips differently for semver
-    # tags
-    if is_semver(revision):
+    # If revision looks like a version number, we need to strip any "v" prefix from it because
+    # GitHub also strips it from the top-level directory name for zips generated for tags that
+    # look like version numbers
+    def is_dotted_version_number(v):
+        v = v.removeprefix("v")
+        num = ["0", "1", "2", "3", "4", "5", "6", "7", "8", "9"]
+        for p in v.split("."):
+            for n in num:
+                p = p.replace(n, "")
+            if p != "":
+                return False
+        return True
+    if is_semver(revision) or is_dotted_version_number(revision):
         prefix = revision.removeprefix('v')
     else:
         prefix = revision