Changes after user feedback

vs-code-extension/README.md

@@ -18,7 +18,7 @@ This extension provides the following commands:
 
 - `Nagini: Select Environment`: select a Python environment
 - `Nagini: Install Nagini`: install Nagini from source
-- `Nagini: Toggle Mode`: activate/deactivate server mode
+- `Nagini: Toggle Mode`: switch between Server mode (a persistent Nagini server) and Direct mode (a separate Nagini process per verification)
 - `Nagini: Select Backend`: select the backend verifier
 - `Nagini: Start Verification`: start a new verification process
 - `Nagini: Verify Function at Cursor`: verify only the function or method at the cursor position

vs-code-extension/package.json

@@ -54,7 +54,7 @@
       {
         "command": "nagini.startVerification",
         "title": "Nagini: Start Verification",
-        "icon": "$(unverified)"
+        "icon": "images/nagini_icon.png"
       },
       {
         "command": "nagini.verifyFunction",

vs-code-extension/src/commands.ts

@@ -11,7 +11,7 @@ import * as path from 'path';
 import { diagnosticCollection, logOutputChannel, stopVerificationButton } from './extensionState';
 import { updateToggleModeButton, updateSelectBackendButton, updateStatusItem } from './extensionState';
 import { VerificationState, VerificationSession, getNaginiCommandArgs, getNaginiClientCommandArgs } from './verificationState';
-import { checkNaginiInstallation, getNaginiPathFromEditor, getPythonPath, getPythonVersion, getSettings, parseDurationFromOutput, parseErrorsFromOutput } from './utils';
+import { checkNaginiInstallation, getNaginiPathFromEditor, getPythonPath, getPythonVersion, isGlobalPythonEnvironment, getSettings, parseDurationFromOutput, parseErrorsFromOutput } from './utils';
 
 let selectEnvironmentQueue: Promise<void> = Promise.resolve();
 export async function selectEnvironment(context: vscode.ExtensionContext, verificationState: VerificationState): Promise<void> {
@@ -72,8 +72,7 @@ export async function selectEnvironment(context: vscode.ExtensionContext, verifi
             try {
                 await verificationState.server.ensureRunning(verificationState, naginiPath);
             } catch (error: Error | unknown) {
-                logOutputChannel.error(`Server failed to start: ${(error as Error).message}`);
-                vscode.window.showErrorMessage(`Server failed to start: ${(error as Error).message}`);
+                await handleServerStartFailure(verificationState, error);
             }
         }
         logOutputChannel.info(`Environment selection finished. Current Python path: ${await getPythonPath(activeEditor.document.uri)}`);
@@ -110,6 +109,28 @@ export async function installNagini(context: vscode.ExtensionContext, verificati
         logOutputChannel.warn(`Could not determine the Python version before installing Nagini; proceeding. Nagini requires Python ${SUPPORTED_PYTHON_RANGE}.`);
     }
 
+    if (await isGlobalPythonEnvironment(activeEditor.document.uri) === true) {
+        logOutputChannel.info('Nagini installation: the selected interpreter is a global/system Python, not a virtual environment');
+        const select: string = 'Select Environment';
+        const installAnyway: string = 'Install Anyway';
+        const selection: string | undefined = await vscode.window.showWarningMessage(
+            'Nagini would be installed into a global/system Python interpreter rather than a virtual environment. ' +
+            'On many systems pip refuses this (externally managed environment), and it can interfere with system packages. ' +
+            'It is strongly recommended to select or create a virtual environment first.',
+            { modal: true },
+            select,
+            installAnyway
+        );
+        if (selection === select) {
+            vscode.commands.executeCommand('nagini.selectEnvironment');
+            return;
+        }
+        if (selection !== installAnyway) {
+            logOutputChannel.info('Nagini installation cancelled. Reason: user declined installing into a global interpreter');
+            return;
+        }
+    }
+
     const pythonPath: string = await getPythonPath(activeEditor.document.uri);
     const naginiPath: string = await getNaginiPathFromEditor(activeEditor);
 
@@ -136,6 +157,18 @@ export async function installNagini(context: vscode.ExtensionContext, verificati
                     if (failed) {
                         logOutputChannel.error(`Nagini installation process failed to spawn. Reason: ${stderr}`);
                         vscode.window.showErrorMessage(`Nagini installation process failed to spawn: ${stderr}`);
+                    } else if (/externally[- ]managed[- ]environment/i.test(`${stdout}\n${stderr}`)) {
+                        logOutputChannel.error(`Nagini installation failed: the selected Python installation is externally managed.\nstdout:\n${stdout}\nstderr:\n${stderr}`);
+                        const select: string = 'Select Environment';
+                        vscode.window.showErrorMessage(
+                            'Nagini installation failed: this Python installation is externally managed, so pip cannot install into it. ' +
+                            'Please select or create a virtual environment and try again.',
+                            select
+                        ).then((selection: string | undefined) => {
+                            if (selection === select) {
+                                vscode.commands.executeCommand('nagini.selectEnvironment');
+                            }
+                        });
                     } else if (code !== 0) {
                         logOutputChannel.error(`Nagini installation process exited with code ${code} and signal ${signal}\nstdout:\n${stdout}\nstderr:\n${stderr}`);
                         vscode.window.showErrorMessage(`Nagini installation process exited with code ${code} and signal ${signal}`);
@@ -147,8 +180,7 @@ export async function installNagini(context: vscode.ExtensionContext, verificati
                             try {
                                 await verificationState.server.ensureRunning(verificationState, naginiPath);
                             } catch (error: Error | unknown) {
-                                logOutputChannel.error(`Server failed to start: ${(error as Error).message}`);
-                                vscode.window.showErrorMessage(`Server failed to start: ${(error as Error).message}`);
+                                await handleServerStartFailure(verificationState, error);
                             }
                         }
                     }
@@ -189,11 +221,10 @@ export async function toggleMode(verificationState: VerificationState): Promise<
             try {
                 await verificationState.server.ensureRunning(verificationState, naginiPath);
             } catch (error: Error | unknown) {
-                logOutputChannel.error(`Server failed to start: ${(error as Error).message}`);
-                vscode.window.showErrorMessage(`Server failed to start: ${(error as Error).message}`);
+                await handleServerStartFailure(verificationState, error);
             }
         }
-        logOutputChannel.info(`Mode toggle finished. Current mode: ${verificationState.serverMode ? 'Server' : 'Local'}`);
+        logOutputChannel.info(`Mode toggle finished. Current mode: ${verificationState.serverMode ? 'Server' : 'Direct'}`);
     });
     await toggleModeQueue;
 }
@@ -242,8 +273,7 @@ export async function selectBackend(verificationState: VerificationState): Promi
             try {
                 await verificationState.server.ensureRunning(verificationState, naginiPath);
             } catch (error: Error | unknown) {
-                logOutputChannel.error(`Server failed to start: ${(error as Error).message}`);
-                vscode.window.showErrorMessage(`Server failed to start: ${(error as Error).message}`);
+                await handleServerStartFailure(verificationState, error);
             }
         }
         logOutputChannel.info(`Backend selection finished. Current backend: ${verificationState.activeBackend}`);
@@ -309,9 +339,8 @@ export async function startVerification(verificationState: VerificationState, se
             try {
                 await verificationState.server.ensureRunning(verificationState, naginiPath);
             } catch (error: Error | unknown) {
-                logOutputChannel.error(`Server failed to start: ${(error as Error).message}`);
                 updateStatusItem(`$(x) Nagini failed to start the server`, 'error');
-                vscode.window.showErrorMessage(`Server failed to start: ${(error as Error).message}`);
+                await handleServerStartFailure(verificationState, error);
                 logOutputChannel.info(`Verification finished`);
                 return;
             }
@@ -422,6 +451,31 @@ function finalizeVerificationSession(verificationState: VerificationState, sessi
     session.resolveTermination();
 }
 
+// Reports a failure to start the Nagini server. When the failure is a port conflict (another
+// server is already bound to the socket), offers to disable server mode so verification can
+// still run with a separate Nagini process per file.
+export async function handleServerStartFailure(verificationState: VerificationState, error: Error | unknown): Promise<void> {
+    const message: string = (error as Error).message;
+    logOutputChannel.error(`Server failed to start: ${message}`);
+    if (/address already in use|EADDRINUSE/i.test(message)) {
+        const disable: string = 'Disable Server Mode';
+        const selection: string | undefined = await vscode.window.showErrorMessage(
+            'Nagini could not start its server because its port (127.0.0.1:5555) is already in use, ' +
+            'most likely because another Nagini server is already running on this machine. ' +
+            'You can disable server mode to verify each file with a separate Nagini process instead.',
+            disable
+        );
+        if (selection === disable && verificationState.serverMode) {
+            await verificationState.server.stop();
+            verificationState.serverMode = false;
+            updateToggleModeButton(verificationState);
+            logOutputChannel.info('Server mode disabled by user after a port conflict.');
+        }
+    } else {
+        vscode.window.showErrorMessage(`Server failed to start: ${message}`);
+    }
+}
+
 // Nagini supports Python 3.12 through 3.14 (inclusive).
 const MIN_SUPPORTED_PYTHON: { major: number; minor: number } = { major: 3, minor: 12 };
 const MAX_SUPPORTED_PYTHON: { major: number; minor: number } = { major: 3, minor: 14 };

vs-code-extension/src/extension.ts

@@ -35,8 +35,7 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
             try {
                 await _verificationState.server.ensureRunning(_verificationState, naginiPath);
             } catch (error: Error | unknown) {
-                logOutputChannel.error(`Server failed to start: ${(error as Error).message}`);
-                vscode.window.showErrorMessage(`Server failed to start: ${(error as Error).message}`);
+                await commands.handleServerStartFailure(_verificationState, error);
             }
         }
     }

vs-code-extension/src/extensionState.ts

@@ -37,7 +37,7 @@ export function initializeState(context: vscode.ExtensionContext): void {
         syntaxHighlighter
     );
 
-    toggleModeButton.tooltip = 'Nagini: Toggle Server Mode';
+    toggleModeButton.tooltip = 'Nagini: Toggle Server/Direct Mode';
     toggleModeButton.command = 'nagini.toggleMode';
     selectBackendButton.tooltip = 'Nagini: Select the Backend Verifier';
     selectBackendButton.command = 'nagini.selectBackend';
@@ -49,7 +49,7 @@ export function initializeState(context: vscode.ExtensionContext): void {
 }
 
 export function updateToggleModeButton(verificationState: VerificationState): void {
-    toggleModeButton.text = verificationState.serverMode ? 'Server' : "Local";
+    toggleModeButton.text = verificationState.serverMode ? 'Server' : 'Direct';
 }
 
 export function updateSelectBackendButton(verificationState: VerificationState): void {

vs-code-extension/src/server.ts

@@ -81,12 +81,16 @@ export class Server {
             session.stderr = session.stderr.trim();
             if (session.failed) {
                 logOutputChannel.error(`Server process failed to spawn. Reason: ${session.stderr}`);
-                vscode.window.showErrorMessage(`Server process failed to spawn: ${session.stderr}`);
             } else if (session.killed) {
                 logOutputChannel.info(`Server process ${session.process.pid} finished. Result: Interruption`);
             } else if (code !== 0) {
                 logOutputChannel.error(`Server process failed. Reason: process exited with code ${code} and signal ${signal}\nstdout:\n${session.stdout}\nstderr:\n${session.stderr}`);
-                vscode.window.showErrorMessage(`Server process failed: process exited with code ${code} and signal ${signal}`);
+                // A pre-startup failure is reported to whoever awaited startup via the rejected
+                // ready promise; only surface a popup here for a crash after a successful start,
+                // when there is no longer anyone awaiting it.
+                if (session.serverStartedSuccessfully) {
+                    vscode.window.showErrorMessage(`Nagini server stopped unexpectedly: process exited with code ${code} and signal ${signal}`);
+                }
             } else {
                 logOutputChannel.info('Server process finished');
             }
@@ -128,7 +132,7 @@ function finalizeServerSession(session: ServerSession): void {
             ? session.stderr
             : session.killed
                 ? 'Server was stopped before it finished starting'
-                : 'Server process exited before it finished starting';
+                : (session.stderr || 'Server process exited before it finished starting');
         session.rejectReady(new Error(reason));
     }
     session.resolveTermination();

vs-code-extension/src/utils/verificationHelpers.ts

@@ -22,17 +22,30 @@ export async function getNaginiPathFromEditor(editor: vscode.TextEditor, serverM
 }
 
 async function getNaginiPath(pythonPath: string, serverMode: boolean = false): Promise<string> {
-    const scriptsDirectory: string = await getPythonScriptsDirectory(pythonPath);
-    if (process.platform === 'win32') {
-        return path.join(scriptsDirectory, serverMode ? 'nagini_client.exe' : 'nagini.exe');
-    } else {
-        return path.join(scriptsDirectory, serverMode ? 'nagini_client' : 'nagini');
-    }
+    const executable: string = process.platform === 'win32'
+        ? (serverMode ? 'nagini_client.exe' : 'nagini.exe')
+        : (serverMode ? 'nagini_client' : 'nagini');
+    const scriptsDirectories: string[] = await getPythonScriptsDirectories(pythonPath);
+    const candidates: string[] = scriptsDirectories.map((directory: string) => path.join(directory, executable));
+    // Prefer a location that actually contains the executable; pip may install into the user
+    // scripts directory (a --user install) when the interpreter's site-packages is not writeable.
+    return candidates.find((candidate: string) => fs.existsSync(candidate)) ?? candidates[0];
 }
 
-async function getPythonScriptsDirectory(pythonPath: string): Promise<string> {
-    return new Promise((resolve: (value: string) => void, reject: (reason: Error) => void) => {
-        const process: cp.ChildProcess = cp.spawn(pythonPath, ['-c', 'import sysconfig; print(sysconfig.get_path(\'scripts\'))']);
+// Returns the interpreter's default scripts directory and, when available, the per-user scripts
+// directory, so that both regular and --user installs of Nagini can be located.
+async function getPythonScriptsDirectories(pythonPath: string): Promise<string[]> {
+    const script: string = [
+        'import sysconfig, json',
+        'dirs = [sysconfig.get_path("scripts")]',
+        'try:',
+        '    dirs.append(sysconfig.get_path("scripts", sysconfig.get_preferred_scheme("user")))',
+        'except Exception:',
+        '    pass',
+        'print(json.dumps(dirs))'
+    ].join('\n');
+    return new Promise((resolve: (value: string[]) => void, reject: (reason: Error) => void) => {
+        const process: cp.ChildProcess = cp.spawn(pythonPath, ['-c', script]);
         let stdout: string = '';
         let stderr: string = '';
         process.stdout?.on('data', (data: Buffer) => stdout += data.toString());
@@ -43,11 +56,18 @@ async function getPythonScriptsDirectory(pythonPath: string): Promise<string> {
         process.on('close', (code: number | null, signal: string | null) => {
             stdout = stdout.trim();
             stderr = stderr.trim();
-            if (code === 0) {
-                resolve(stdout);
-            } else {
+            if (code !== 0) {
                 reject(new Error(`Python process \'${pythonPath} ${process.spawnargs.join(' ')}\' failed with code ${code} and signal ${signal}: ${stderr}`));
+                return;
             }
+            let directories: string[];
+            try {
+                directories = (JSON.parse(stdout) as string[]).filter((directory: string) => typeof directory === 'string' && directory.length > 0);
+            } catch {
+                directories = stdout ? [stdout] : [];
+            }
+            // De-duplicate while preserving order (default scripts directory first).
+            resolve(directories.filter((directory: string, index: number) => directories.indexOf(directory) === index));
         });
     });
 }
@@ -61,6 +81,16 @@ export async function getPythonPath(uri: vscode.Uri): Promise<string> {
     return pythonPath;
 }
 
+export async function isGlobalPythonEnvironment(uri: vscode.Uri): Promise<boolean | undefined> {
+    const api: PythonExtension = await PythonExtension.api();
+    const envPath: EnvironmentPath = api.environments.getActiveEnvironmentPath(uri);
+    const resolvedEnv: ResolvedEnvironment | undefined = await api.environments.resolveEnvironment(envPath);
+    if (resolvedEnv === undefined) { return undefined; }
+    // `environment` is populated for virtual/conda/etc. environments and is undefined for
+    // global or system interpreters.
+    return resolvedEnv.environment === undefined;
+}
+
 export async function getPythonVersion(uri: vscode.Uri): Promise<{ major: number; minor: number } | undefined> {
     // Query the interpreter directly rather than trusting the Python extension's reported
     // version metadata, which can be stale or wrong for some environments.