feat: improve activation error when forked extension is installed (#613)

Every so often, users decide that they want to get (what they believe to
be) the "full" Lean experience in VS Code and install every single
Lean-related extension from the VS Code marketplace. While
well-intentioned, since the marketplace also contains forks of our
extension, this then leads to an internal activation error when VS
Code's `commands.registerCommand` API throws an exception for trying to
register duplicate commands.
This PR improves the error message that is displayed in this case to
hint at the cause so that users are more likely to be able to fix it
themselves without requiring assistance.

Author: mhuisi

vscode-lean4/src/utils/internalErrors.ts

@@ -1,5 +1,5 @@
 import { env } from 'vscode'
-import { displayNotificationWithInput } from './notifs'
+import { displayModalNotification, displayNotificationWithInput } from './notifs'
 
 export async function displayInternalError(scope: string, e: any) {
     let msg: string = `Internal error (while ${scope}): ${e}`
@@ -17,10 +17,21 @@ export async function displayInternalError(scope: string, e: any) {
     }
 }
 
+const duplicateCommandError = (scope: string) =>
+    `Error (while ${scope}): Two separate Lean 4 VS Code extensions that register the same VS Code functionality are installed.
+Please uninstall or disable one of them and restart VS Code.
+
+The 'Lean 4' extension by the 'leanprover' organization is the only official Lean 4 VS Code extension.`
+
 export async function displayInternalErrorsIn<T>(scope: string, f: () => Promise<T>): Promise<T> {
     try {
         return await f()
     } catch (e) {
+        const msg = e.message
+        if (msg !== undefined && typeof msg === 'string' && msg.match(/command '.*' already exists/)) {
+            await displayModalNotification('Error', duplicateCommandError(scope))
+            throw e
+        }
         await displayInternalError(scope, e)
         throw e
     }