Merge branch 'topic/vscode-spark' into 'master'

Use GNATprove option picker with all SPARK tasks

See merge request eng/ide/ada_language_server!2105

Author: eliericha

integration/vscode/ada/package.json

@@ -1183,30 +1183,66 @@
                 "icon": "$(run)",
                 "when": "ADA_PROJECT_CONTEXT"
             },
+            {
+                "command": "ada.spark.tasks.cleanProject",
+                "title": "Clean project for proof",
+                "category": "SPARK",
+                "when": "ADA_PROJECT_CONTEXT"
+            },
+            {
+                "command": "ada.spark.tasks.examineProject",
+                "title": "Examine project",
+                "category": "SPARK",
+                "when": "ADA_PROJECT_CONTEXT"
+            },
+            {
+                "command": "ada.spark.tasks.examineFile",
+                "title": "Examine file",
+                "category": "SPARK",
+                "when": "editorLangId == ada && editorTextFocus"
+            },
+            {
+                "command": "ada.spark.tasks.examineSubprogram",
+                "title": "Examine subprogram",
+                "category": "SPARK",
+                "when": "editorLangId == ada && editorTextFocus"
+            },
+            {
+                "command": "ada.spark.tasks.proveProject",
+                "title": "Prove project",
+                "category": "SPARK",
+                "when": "ADA_PROJECT_CONTEXT"
+            },
             {
                 "command": "ada.spark.tasks.proveFile",
-                "title": "Prove file (task wrapper)",
+                "title": "Prove file",
                 "category": "SPARK",
                 "when": "editorLangId == ada && editorTextFocus"
             },
             {
                 "command": "ada.spark.tasks.proveSubprogram",
-                "title": "Prove subprogram (task wrapper)",
+                "title": "Prove subprogram",
                 "category": "SPARK",
                 "when": "editorLangId == ada && editorTextFocus"
             },
             {
                 "command": "ada.spark.tasks.proveSelectedRegion",
-                "title": "Prove selected region (task wrapper)",
+                "title": "Prove selected region",
                 "category": "SPARK",
                 "when": "editorLangId == ada && editorTextFocus"
             },
             {
                 "command": "ada.spark.tasks.proveLine",
-                "title": "Prove line (task wrapper)",
+                "title": "Prove line",
                 "category": "SPARK",
                 "when": "editorLangId == ada && editorTextFocus"
             },
+            {
+                "command": "ada.spark.askGNATproveOptions",
+                "title": "Select GNATprove options...",
+                "category": "SPARK",
+                "when": "ADA_PROJECT_CONTEXT"
+            },
             {
                 "command": "ada.loadGnatCovXMLReport",
                 "category": "Ada",
@@ -1529,7 +1565,7 @@
         "ws": "$ws"
     },
     "scripts": {
-        "check-licenses": "npx license-checker-rseidelsohn --summary --onlyAllow \"0BSD;Apache-2.0;BSD-2-Clause;BSD-3-Clause;BlueOak-1.0.0;CC0-1.0;GPL-3.0;GPL-3.0-or-later;ISC;MIT;Python-2.0;Zlib;EPL-2.0\" --excludePackages \"@vscode/vsce-sign-linux-x64;@vscode/vsce-sign-win32-x64;@vscode/vsce-sign\"",
+        "check-licenses": "npx license-checker-rseidelsohn --production --summary --onlyAllow \"MIT;ISC;CC-BY-4.0;GPL-3.0;BSD-3-Clause;EPL-2.0\"",
         "vscode:prepublish": "npm run compile && npm run esbuild-base -- --minify --sourcemap",
         "esbuild-base": "esbuild ./src/extension.ts --bundle --outfile=out/src/extension.js --external:vscode --format=cjs --platform=node",
         "compile": "node ./node_modules/typescript/bin/tsc && npm run compile-webview",

integration/vscode/ada/src/AdaCodeLensProvider.ts

@@ -17,7 +17,7 @@ import {
     CMD_BUILD_AND_RUN_GNATEMULATOR,
     CMD_BUILD_AND_RUN_MAIN,
     CMD_SPARK_PROVE_SUBP,
-} from './commands';
+} from './constants';
 import { envHasExec, getSymbols } from './helpers';
 import { adaExtState } from './extension';
 

integration/vscode/ada/src/ExtensionState.ts

@@ -14,7 +14,7 @@ import {
     CMD_SHOW_ADA_LS_OUTPUT,
     CMD_SHOW_EXTENSION_LOGS,
     CMD_SHOW_GPR_LS_OUTPUT,
-} from './commands';
+} from './constants';
 import { AdaInitialDebugConfigProvider, initializeDebugging } from './debugConfigProvider';
 import { logger } from './extension';
 import { GnatTaskProvider } from './gnatTaskProvider';

integration/vscode/ada/src/alsExecuteCommand.ts

@@ -40,7 +40,7 @@ import {
     ReplaceTypeCommandArgs,
 } from './refactoring/alsReplaceTypeCommand';
 import { adaExtState } from './extension';
-import { CMD_RELOAD_PROJECT } from './commands';
+import { CMD_RELOAD_PROJECT } from './constants';
 
 /**
  * Type alias for a function that intercepts a command and executes it by return a promise that

integration/vscode/ada/src/commands.ts

@@ -7,17 +7,31 @@ import { Disposable } from 'vscode-jsonrpc';
 import { ExecuteCommandRequest } from 'vscode-languageclient';
 import { ALSSourceDirDescription, ExtensionState } from './ExtensionState';
 import { startVisualize } from './alsVisualizer';
+import {
+    CMD_BUILD_AND_DEBUG_GNATEMULATOR,
+    CMD_BUILD_AND_DEBUG_MAIN,
+    CMD_BUILD_AND_RUN_GNATEMULATOR,
+    CMD_BUILD_AND_RUN_MAIN,
+    CMD_GPR_PROJECT_ARGS,
+    CMD_RESTART_LANG_SERVERS,
+    CMD_SHOW_ADA_LS_OUTPUT,
+    CMD_SHOW_EXTENSION_LOGS,
+    CMD_SHOW_GPR_LS_OUTPUT,
+    CMD_SPARK_ASK_OPTIONS,
+    CMD_SPARK_CURRENT_GNATPROVE_OPTIONS,
+    CMD_SPARK_LIMIT_REGION_ARG,
+    CMD_SPARK_LIMIT_SUBP_ARG,
+    CMD_SPARK_PROVE_SUBP,
+} from './constants';
 import { AdaConfig, getOrAskForProgram, initializeConfig } from './debugConfigProvider';
 import { adaExtState, logger, mainOutputChannel } from './extension';
 import { loadGnatCoverageReport } from './gnattest';
 import { findAdaMain, getProjectFileRelPath, getSymbols } from './helpers';
-import { askSPARKOptions } from './sparkOptionsPicker';
+import { registerSPARKTaskWrappers } from './sparkCommands';
+import { askSPARKOptions, getLastSPARKOptions } from './sparkOptionsPicker';
 import {
     DEFAULT_PROBLEM_MATCHERS,
     SimpleTaskDef,
-    TASK_PROVE_FILE_PLAIN_NAME,
-    TASK_PROVE_LINE_PLAIN_NAME,
-    TASK_PROVE_REGION_PLAIN_NAME,
     TASK_PROVE_SUPB_PLAIN_NAME,
     TASK_TYPE_SPARK,
     findBuildAndRunTask,
@@ -33,89 +47,6 @@ import {
 import { Hierarchy } from './visualizerTypes';
 import { createHelloWorldProject, walkthroughStartDebugging } from './walkthrough';
 
-/**
- * Identifier for a hidden command used for building and running a project main.
- * The command accepts a parameter which is the URI of the main source file.
- * It is triggered by CodeLenses provided by the extension.
- *
- * @see {@link buildAndRunSpecifiedMain}
- */
-export const CMD_BUILD_AND_RUN_MAIN = 'ada.buildAndRunMain';
-
-/**
- * Identifier for a hidden command used for building and debugging a project main.
- * The command accepts a parameter which is the URI of the main source file.
- * It is triggered by CodeLenses provided by the extension.
- *
- * @see {@link buildAndDebugSpecifiedMain}
- */
-export const CMD_BUILD_AND_DEBUG_MAIN = 'ada.buildAndDebugMain';
-
-/**
- * Identifier for a hidden command used for building and running a project main,
- * using GNATemulator.
- * The command accepts a parameter which is the URI of the main source file.
- * It is triggered by CodeLenses provided by the extension.
- *
- * @see {@link buildAndRunMainWithGNATemulator}
- */
-export const CMD_BUILD_AND_RUN_GNATEMULATOR = 'ada.buildAndRunGNATemulator';
-
-/**
- * Identifier for a hidden command used for building and debugging a project main,
- * using GNATemulator.
- * The command accepts a parameter which is the URI of the main source file.
- * It is triggered by CodeLenses provided by the extension.
- *
- * @see {@link buildAndDebugSpecifiedMain}
- */
-export const CMD_BUILD_AND_DEBUG_GNATEMULATOR = 'ada.buildAndDebugGNATemulator';
-
-/**
- * Identifier for a hidden command that returns an array of strings constituting
- * the -P and -X project and scenario arguments.
- */
-export const CMD_GPR_PROJECT_ARGS = 'ada.gprProjectArgs';
-
-/**
- * Identifier for a hidden command that returns a string referencing the current
- * project.  That string is either `"$\{config:ada.projectFile\}"` if that
- * setting is configured, or otherwise the full path to the project file
- * returned from a query to the
- */
-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';
-const CMD_SPARK_ASK_OPTIONS = 'ada.spark.askSPARKOptions';
-
-/**
- * Identifier for the command that shows the extension's output in the Output panel.
- */
-export const CMD_SHOW_EXTENSION_LOGS = 'ada.showExtensionOutput';
-
-/**
- * Identifier for the command that shows the output of the ALS for Ada in the Output panel.
- */
-export const CMD_SHOW_ADA_LS_OUTPUT = 'ada.showAdaLSOutput';
-
-/**
- * Identifier for the command that shows the output of the ALS for GPR in the Output panel.
- */
-export const CMD_SHOW_GPR_LS_OUTPUT = 'ada.showGprLSOutput';
-
-/**
- * Identifier for the command that reloads the currently loaded project on server-side.
- */
-export const CMD_RELOAD_PROJECT = 'als-reload-project';
-
-/**
- * Identifier for the command that restarts all the language servers spawned by the extension
- * (Ada and GPR).
- */
-export const CMD_RESTART_LANG_SERVERS = 'ada.restartLanguageServers';
-
 export function registerCommands(context: vscode.ExtensionContext, clients: ExtensionState) {
     context.subscriptions.push(
         vscode.commands.registerCommand(CMD_RESTART_LANG_SERVERS, restartLanguageServers),
@@ -235,9 +166,6 @@ export function registerCommands(context: vscode.ExtensionContext, clients: Exte
     context.subscriptions.push(
         vscode.commands.registerCommand(CMD_GPR_PROJECT_ARGS, gprProjectArgs),
     );
-    context.subscriptions.push(
-        vscode.commands.registerCommand(CMD_GET_PROJECT_FILE, getProjectFromConfigOrALS),
-    );
     context.subscriptions.push(
         vscode.commands.registerCommand(CMD_SPARK_LIMIT_SUBP_ARG, sparkLimitSubpArg),
     );
@@ -249,6 +177,9 @@ export function registerCommands(context: vscode.ExtensionContext, clients: Exte
     );
 
     context.subscriptions.push(commands.registerCommand(CMD_SPARK_ASK_OPTIONS, askSPARKOptions));
+    context.subscriptions.push(
+        commands.registerCommand(CMD_SPARK_CURRENT_GNATPROVE_OPTIONS, getLastSPARKOptions),
+    );
 
     context.subscriptions.push(
         commands.registerCommand('ada.loadGnatCovXMLReport', loadGnatCovXMLReport),
@@ -258,36 +189,7 @@ export function registerCommands(context: vscode.ExtensionContext, clients: Exte
         vscode.commands.registerCommand('ada.issueReporter', openReportIssue),
     );
 
-    registerTaskWrappers(context);
-}
-
-/**
- * The following commands are wrappers around VS Code tasks that allow setting
- * key shortcuts to the wrapped tasks. Technically it is possible to set
- * shortcuts directly on the `workbench.action.tasks.runTask` command with the
- * target task as a command argument, however in several places the UI doesn't
- * take into consideration the command argument, and thus it becomes impossible
- * to distinguish the different tasks, and worse, our shortcut becomes
- * displayed for the vanilla `Run Task` command.
- *
- * To avoid all that, we provide these commands as wrappers.
- */
-function registerTaskWrappers(context: vscode.ExtensionContext) {
-    const sparkTaskWrappers: { [cmdId: string]: string } = {
-        'ada.spark.tasks.proveFile': `${TASK_TYPE_SPARK}: ${TASK_PROVE_FILE_PLAIN_NAME}`,
-        'ada.spark.tasks.proveSubprogram': `${TASK_TYPE_SPARK}: ${TASK_PROVE_SUPB_PLAIN_NAME}`,
-        // eslint-disable-next-line max-len
-        'ada.spark.tasks.proveSelectedRegion': `${TASK_TYPE_SPARK}: ${TASK_PROVE_REGION_PLAIN_NAME}`,
-        'ada.spark.tasks.proveLine': `${TASK_TYPE_SPARK}: ${TASK_PROVE_LINE_PLAIN_NAME}`,
-    };
-    for (const cmdId of Object.keys(sparkTaskWrappers)) {
-        const taskId = sparkTaskWrappers[cmdId];
-        context.subscriptions.push(
-            commands.registerCommand(cmdId, () =>
-                commands.executeCommand('workbench.action.tasks.runTask', taskId),
-            ),
-        );
-    }
+    registerSPARKTaskWrappers(context);
 }
 
 /**
@@ -890,7 +792,6 @@ async function buildAndDebugSpecifiedMainWithGNATemulator(main: vscode.Uri): Pro
  */
 export async function gprProjectArgs(): Promise<string[]> {
     const scenarioArgs = gprScenarioArgs();
-
     return ['-P', await getProjectFromConfigOrALS()].concat(scenarioArgs);
 }
 
@@ -959,7 +860,7 @@ export async function sparkLimitSubpArg(): Promise<string[]> {
  * zero-based while the `gnatprove` convention is one-based. This function does
  * the conversion.
  */
-function getLimitSubpArg(filename: string, range: vscode.Range) {
+function getLimitSubpArg(filename: string, range: vscode.Range): string {
     return `--limit-subp=${filename}:${range.start.line + 1}`;
 }
 
@@ -1088,8 +989,8 @@ async function sparkProveSubprogram(
     );
 
     /**
-     * Replace the subp-region argument based on the parameter given to the
-     * command.
+     * Replace the subp-region command argument with the --limit-subp argument
+     * pointing to the place where this command was triggered.
      */
     const taskDef = newTask.definition as SimpleTaskDef;
     assert(taskDef.args);
@@ -1103,17 +1004,6 @@ async function sparkProveSubprogram(
          * with the same name in the task history.
          */
         newTask.name = `${task.name} - ${fileBasename}:${range.start.line + 1}`;
-
-        /**
-         * Add a command to ask the User for options. We do this instead of
-         * pre-evaluating the options so that all invocations on the same
-         * subprogram have the same set of (unevaluated) arguments, which means
-         * that only one task shows up in the task history for each subprogram.
-         * If we pre-evaluated the options, then each different set of User
-         * choices would yield a different entry in the task history which is
-         * noisy.
-         */
-        taskDef.args.splice(regionArgIdx + 1, 0, `\${command:${CMD_SPARK_ASK_OPTIONS}}`);
     } else {
         throw Error(
             `Task '${getConventionalTaskLabel(task)}' is missing a '${regionArg}' argument`,
@@ -1126,6 +1016,11 @@ async function sparkProveSubprogram(
     const resolvedTask = await adaExtState.getSparkTaskProvider()?.resolveTask(newTask);
     assert(resolvedTask);
 
+    /**
+     * Ask for GNATprove options
+     */
+    await commands.executeCommand(CMD_SPARK_ASK_OPTIONS);
+
     /**
      * Execute the task.
      */