Merge remote branch 'origin/master' into edge

integration/vscode/ada/src/AdaCodeLensProvider.ts

@@ -11,12 +11,10 @@ import {
     commands,
     Uri,
 } from 'vscode';
-import { CMD_BUILD_AND_DEBUG_MAIN, CMD_BUILD_AND_RUN_MAIN } from './commands';
-import { getMains, getSymbols } from './helpers';
+import { CMD_BUILD_AND_DEBUG_MAIN, CMD_BUILD_AND_RUN_MAIN, CMD_SPARK_PROVE_SUBP } from './commands';
+import { envHasExec, getMains, getSymbols } from './helpers';
 
 export class AdaCodeLensProvider implements CodeLensProvider {
-    static readonly ENABLE_SPARK_CODELENS = false;
-
     onDidChangeCodeLenses?: Event<void> | undefined;
     provideCodeLenses(
         document: TextDocument,
@@ -73,7 +71,7 @@ export class AdaCodeLensProvider implements CodeLensProvider {
         });
 
         let res2;
-        if (AdaCodeLensProvider.ENABLE_SPARK_CODELENS) {
+        if (envHasExec('gnatprove')) {
             /**
              * This is tentative deactivated code in preparation of SPARK support.
              */
@@ -88,10 +86,11 @@ export class AdaCodeLensProvider implements CodeLensProvider {
                     if (token?.isCancellationRequested) {
                         throw new CancellationError();
                     }
-                    // TODO make SPARK codelenses conditional to the availability of SPARK on PATH
-                    return new CodeLens(f.range, {
-                        title: '$(play-circle) Prove',
-                        command: 'TODO',
+
+                    return new CodeLens(f.selectionRange, {
+                        title: '$(check) Prove',
+                        command: CMD_SPARK_PROVE_SUBP,
+                        arguments: [document.uri, f.selectionRange],
                     });
                 });
             });

integration/vscode/ada/src/ExtensionState.ts

@@ -3,12 +3,18 @@ import { Disposable, ExecuteCommandRequest, LanguageClient } from 'vscode-langua
 import { AdaCodeLensProvider } from './AdaCodeLensProvider';
 import { createClient } from './clients';
 import { AdaInitialDebugConfigProvider, initializeDebugging } from './debugConfigProvider';
+import { logger } from './extension';
 import { GnatTaskProvider } from './gnatTaskProvider';
 import { initializeTesting } from './gnattest';
 import { GprTaskProvider } from './gprTaskProvider';
 import { TERMINAL_ENV_SETTING_NAME } from './helpers';
-import { registerTaskProviders } from './taskProviders';
-import { logger } from './extension';
+import {
+    SimpleTaskProvider,
+    TASK_TYPE_ADA,
+    TASK_TYPE_SPARK,
+    createAdaTaskProvider,
+    createSparkTaskProvider,
+} from './taskProviders';
 
 /**
  * This class encapsulates all state that should be maintained throughout the
@@ -45,6 +51,9 @@ export class ExtensionState {
     cachedExecutables: string[] | undefined;
     cachedAlireTomls: vscode.Uri[] | undefined;
 
+    private adaTaskProvider?: SimpleTaskProvider;
+    private sparkTaskProvider?: SimpleTaskProvider;
+
     public clearALSCache() {
         this.cachedProjectFile = undefined;
         this.cachedObjectDir = undefined;
@@ -89,13 +98,18 @@ export class ExtensionState {
     };
 
     public registerTaskProviders = (): void => {
+        this.adaTaskProvider = createAdaTaskProvider();
+        this.sparkTaskProvider = createSparkTaskProvider();
+
         this.registeredTaskProviders = [
             vscode.tasks.registerTaskProvider(GnatTaskProvider.gnatType, new GnatTaskProvider()),
             vscode.tasks.registerTaskProvider(
                 GprTaskProvider.gprTaskType,
                 new GprTaskProvider(this.adaClient)
             ),
-        ].concat(registerTaskProviders());
+            vscode.tasks.registerTaskProvider(TASK_TYPE_ADA, this.adaTaskProvider),
+            vscode.tasks.registerTaskProvider(TASK_TYPE_SPARK, this.sparkTaskProvider),
+        ];
     };
 
     public unregisterTaskProviders = (): void => {
@@ -215,4 +229,13 @@ export class ExtensionState {
 
         return this.cachedAlireTomls;
     }
+
+    /**
+     *
+     * @returns the SPARK task provider which can be useful for resolving tasks
+     * created on the fly, e.g. when running SPARK CodeLenses.
+     */
+    public getSparkTaskProvider() {
+        return this.sparkTaskProvider;
+    }
 }

integration/vscode/ada/src/commands.ts

@@ -1,5 +1,6 @@
 import assert from 'assert';
 import { existsSync } from 'fs';
+import { basename } from 'path';
 import * as vscode from 'vscode';
 import { SymbolKind } from 'vscode';
 import { Disposable } from 'vscode-jsonrpc';
@@ -10,10 +11,13 @@ import { adaExtState, logger, mainOutputChannel } from './extension';
 import { findAdaMain, getProjectFileRelPath, getSymbols } from './helpers';
 import {
     SimpleTaskDef,
+    TASK_PROVE_SUPB_PLAIN_NAME,
+    TASK_TYPE_SPARK,
     findBuildAndRunTask,
     getBuildAndRunTasks,
     getConventionalTaskLabel,
     isFromWorkspace,
+    workspaceTasksFirst,
 } from './taskProviders';
 
 /**
@@ -50,6 +54,7 @@ export const CMD_GET_PROJECT_FILE = 'ada.getProjectFile';
 
 export const CMD_SPARK_LIMIT_SUBP_ARG = 'ada.spark.limitSubpArg';
 export const CMD_SPARK_LIMIT_REGION_ARG = 'ada.spark.limitRegionArg';
+export const CMD_SPARK_PROVE_SUBP = 'ada.spark.proveSubprogram';
 
 export function registerCommands(context: vscode.ExtensionContext, clients: ExtensionState) {
     context.subscriptions.push(vscode.commands.registerCommand('ada.otherFile', otherFileHandler));
@@ -125,6 +130,9 @@ export function registerCommands(context: vscode.ExtensionContext, clients: Exte
     context.subscriptions.push(
         vscode.commands.registerCommand(CMD_SPARK_LIMIT_REGION_ARG, sparkLimitRegionArg)
     );
+    context.subscriptions.push(
+        vscode.commands.registerCommand(CMD_SPARK_PROVE_SUBP, sparkProveSubprogram)
+    );
 }
 /**
  * Add a subprogram box above the subprogram enclosing the cursor's position, if any.
@@ -640,8 +648,8 @@ export async function sparkLimitSubpArg(): Promise<string[]> {
     return getEnclosingSymbol(vscode.window.activeTextEditor, [vscode.SymbolKind.Function]).then(
         (Symbol) => {
             if (Symbol) {
-                const subprogram_line: string = (Symbol.range.start.line + 1).toString();
-                return [`--limit-subp=\${fileBasename}:${subprogram_line}`];
+                const range = Symbol.range;
+                return [getLimitSubpArg('${fileBasename}', range)];
             } else {
                 /**
                  * If we can't find a subprogram, we use the VS Code predefined
@@ -658,6 +666,19 @@ export async function sparkLimitSubpArg(): Promise<string[]> {
     );
 }
 
+/**
+ *
+ * @param filename - a filename
+ * @param range - a {@link vscode.Range}
+ * @returns the --limit-subp `gnatprove` CLI argument corresponding to the given
+ * arguments. Note that lines and columns in {@link vscode.Range}es are
+ * zero-based while the `gnatprove` convention is one-based. This function does
+ * the conversion.
+ */
+function getLimitSubpArg(filename: string, range: vscode.Range) {
+    return `--limit-subp=${filename}:${range.start.line + 1}`;
+}
+
 /**
  * @returns the gnatprove `--limit-region=file:from:to` argument corresponding
  * to the current editor's selection.
@@ -731,3 +752,71 @@ export async function getEnclosingSymbol(
 
     return null;
 }
+
+/**
+ * Command corresponding to the 'Prove' CodeLens provided on subprograms.
+ *
+ * It is implemented by fetching the 'Prove subbprogram' task and using it as a
+ * template such that the User can customize the task to impact the CodeLens.
+ */
+async function sparkProveSubprogram(
+    uri: vscode.Uri,
+    range: vscode.Range
+): Promise<vscode.TaskExecution> {
+    /**
+     * Get the 'Prove subprogram' task. Prioritize workspace tasks so that User
+     * customization of the task takes precedence.
+     */
+    const task = (await vscode.tasks.fetchTasks({ type: TASK_TYPE_SPARK }))
+        .sort(workspaceTasksFirst)
+        .find(
+            (t) =>
+                getConventionalTaskLabel(t) == `${TASK_TYPE_SPARK}: ${TASK_PROVE_SUPB_PLAIN_NAME}`
+        );
+    assert(task);
+
+    /**
+     * Create a copy of the task.
+     */
+    const newTask = new vscode.Task(
+        { ...task.definition },
+        task.scope ?? vscode.TaskScope.Workspace,
+        task.name,
+        task.source,
+        undefined,
+        task.problemMatchers
+    );
+
+    /**
+     * Replace the subp-region argument based on the parameter given to the
+     * command.
+     */
+    const taskDef = newTask.definition as SimpleTaskDef;
+    assert(taskDef.args);
+    const regionArg = '${command:ada.spark.limitSubpArg}';
+    const regionArgIdx = taskDef.args.findIndex((arg) => arg == regionArg);
+    if (regionArgIdx >= 0) {
+        const fileBasename = basename(uri.fsPath);
+        taskDef.args[regionArgIdx] = getLimitSubpArg(fileBasename, range);
+        /**
+         * Change the task name accordingly, otherwise all invocations appear
+         * with the same name in the task history.
+         */
+        newTask.name = `${task.name} - ${fileBasename}:${range.start.line + 1}`;
+    } else {
+        throw Error(
+            `Task '${getConventionalTaskLabel(task)}' is missing a '${regionArg}' argument`
+        );
+    }
+
+    /**
+     * Resolve the task.
+     */
+    const resolvedTask = await adaExtState.getSparkTaskProvider()?.resolveTask(newTask);
+    assert(resolvedTask);
+
+    /**
+     * Execute the task.
+     */
+    return await vscode.tasks.executeTask(resolvedTask);
+}

integration/vscode/ada/src/helpers.ts

@@ -24,6 +24,7 @@ import winston from 'winston';
 // eslint-disable-next-line @typescript-eslint/no-unused-vars
 import { ExtensionState } from './ExtensionState';
 import { adaExtState, logger } from './extension';
+import { existsSync } from 'fs';
 
 /**
  * Substitue any variable reference present in the given string. VS Code
@@ -436,3 +437,46 @@ export function getSymbols(
 export function escapeRegExp(text: string) {
     return text.replace(/[-[\]{}()*+?.,\\^$|#\s]/g, '\\$&');
 }
+
+/**
+ *
+ * @param execName - the name of an executable (without the extension) to find
+ * using the PATH environment variable.
+ * @returns `true` if the executable is found, `false` otherwise.
+ */
+export function envHasExec(execName: string): boolean {
+    const exePath: string | undefined = which(execName);
+
+    return exePath != undefined;
+}
+
+/**
+ * Finds the path to an executable using the PATH environment variable.
+ *
+ * On Windows, the extension of the executable does not need to be provided. The
+ * env variable PATHEXT is used to consider all applicable extensions (e.g.
+ * .exe, .cmd).
+ *
+ * @param execName - name of executable to find using PATH environment variable.
+ * @returns the full path to the executable if found, otherwise `undefined`
+ */
+export function which(execName: string) {
+    const env = { ...process.env };
+    setTerminalEnvironment(env);
+    const pathVal = env.PATH;
+    const paths = pathVal?.split(path.delimiter);
+    const exeExtensions =
+        process.platform == 'win32'
+            ? /**
+               * On Windows use a default list of extensions in case PATHEXT is
+               * not set.
+               */
+              env.PATHEXT?.split(path.delimiter) ?? ['.exe', '.cmd', '.bat']
+            : [''];
+
+    const exePath: string | undefined = paths
+        ?.flatMap((p) => exeExtensions.map((ext) => path.join(p, execName + ext)))
+        .find(existsSync);
+
+    return exePath;
+}