Provide a better error message if the required dev-tool cannot be found []

Author: wchilders-nvidia

.git-hooks/pre-push.py

@@ -107,6 +107,19 @@ def _is_excluded_file_path(path_str: str) -> bool:
 
 TOOL_PATH_GIT = shutil.which('git')
 
+def find_dev_tool(name):
+  '''Return the path of the dev tool called name on PATH, or exit with an
+  error if the environment lacks it (e.g., direnv isn't applied).'''
+  tool_path = shutil.which(name)
+  if tool_path is None:
+    print(
+      f"error: the environment is missing the required tool '{name}'; "
+      'put dev_tools/bin on PATH (e.g., via direnv) and push again.',
+      file = sys.stderr
+    )
+    sys.exit(1)
+  return tool_path
+
 def run_git(args, *, check = True, text = True):
   '''Run a git command and return the completed process.'''
   return subprocess.run(
@@ -287,7 +300,7 @@ def check_changed_files(self, first_new_commit):
       if use_docker:
         file_change_check_proc = subprocess.run(
           [
-            shutil.which('edg-exec'),
+            find_dev_tool('edg-exec'),
             '--',
             'edg-check-file-changes',
             str(input_file.relative_to(mono_repo_dir).as_posix()),
@@ -299,7 +312,7 @@ def check_changed_files(self, first_new_commit):
       else:
         file_change_check_proc = subprocess.run(
           [
-            shutil.which('edg-check-file-changes'),
+            find_dev_tool('edg-check-file-changes'),
             str(input_file),
             str(output_file)
           ],