new: --deployer to use different space in dev mode

In dev mode, if deployer has his/her specified space config, it will deploy to which space instead of the default one.

.github/tools/config.py

@@ -21,7 +21,7 @@ PRODUCTION_SPACE_CONFIG: Dict[ProductionSpace, Config] = {
     }
 }
 
-UserName = Literal["default"]
+UserName = Literal["default", "jhihruei"]
 
 DEV_SPACE_CONFIG: Dict[UserName, Config] = {
     "default": {
@@ -38,4 +38,18 @@ DEV_SPACE_CONFIG: Dict[UserName, Config] = {
             "pinned": False,
         },
     },
+    "jhihruei": {
+        "space_name": "personal-dev",
+        "space_owner": "jy-raychen",
+        "space_readme": {
+            "title": "Personal Developing",
+            "emoji": "🏢",
+            "color_from": "yellow",
+            "color_to": "indigo",
+            "sdk": "gradio",
+            "sdk_version": "4.21.0",
+            "app_file": "app.py",
+            "pinned": False,
+        },
+    },
 }

.github/tools/deploy_to_space.py

@@ -33,12 +33,23 @@ if __name__ == "__main__":
     parser.add_argument("--username", required=True)
     parser.add_argument("--user_token", required=True)
     parser.add_argument("--mode", required=True, choices=["prod", "dev"])
+    parser.add_argument(
+        "--deployer",
+        help="The actor in Github Actions, it used to choose space config in dev mode.",
+    )
     args = parser.parse_args()
 
-    if args.mode == "prod":
-        space = Space(PRODUCTION_SPACE_CONFIG["production"])
-    elif args.mode == "dev":
-        space = Space(DEV_SPACE_CONFIG["default"])
+    try:
+        if args.mode == "prod":
+            space = Space(PRODUCTION_SPACE_CONFIG["production"])
+        elif args.mode == "dev":
+            space_config = DEV_SPACE_CONFIG.get(
+                args.deployer, DEV_SPACE_CONFIG["default"]
+            )
+            space = Space(space_config)
+    except Exception:
+        print("Error: The space is not set correctly!")
+        sys.exit(1)
 
     push_result = force_push_to_remote(
         space, args.username, args.user_token, args.branch_name

.github/tools/generate_readme.py

@@ -27,12 +27,23 @@ if __name__ == "__main__":
         description="Generate Hugging Face space config file (i.e. README.md)."
     )
     parser.add_argument("--mode", required=True, choices=["prod", "dev"])
+    parser.add_argument(
+        "--deployer",
+        help="The actor in Github Actions, it used to choose space config in dev mode.",
+    )
     args = parser.parse_args()
 
-    if args.mode == "prod":
-        space = Space(PRODUCTION_SPACE_CONFIG["production"])
-    elif args.mode == "dev":
-        space = Space(DEV_SPACE_CONFIG["default"])
+    try:
+        if args.mode == "prod":
+            space = Space(PRODUCTION_SPACE_CONFIG["production"])
+        elif args.mode == "dev":
+            space_config = DEV_SPACE_CONFIG.get(
+                args.deployer, DEV_SPACE_CONFIG["default"]
+            )
+            space = Space(space_config)
+    except Exception:
+        print("Error: The space is not set correctly!")
+        sys.exit(1)
 
     readme = readme_template(space.readme)
     print(readme)