Skip to content

Commit 39b4b9f

Browse files
committed
U218-014 Add task provider for gnatprove
Update ada problem matcher regexp to accept more severities kinds.
1 parent 9d720be commit 39b4b9f

File tree

4 files changed

+136
-9
lines changed

4 files changed

+136
-9
lines changed

README.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,8 @@ The extension includes a task provider. It provides two "auto-detected" tasks
169169
(under `/Terminal/Run Task...` menu):
170170
* "ada: Build current project" - launch `gprbuild` to build the current GPR project
171171
* "ada: Check current file" - launch `gprbuild` to check errors in the current editor
172+
* "ada: Run gnatprove on the current project" - launch `gnatprove` for the current GPR project
173+
* "ada: Run gnatprove on the current file" - launch `gnatprove` to check errors in the current editor
172174

173175
You can bind keyboard shortcuts to them by adding to the `keybindings.json` file:
174176

integration/vscode/ada/package.json

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@
183183
],
184184
"pattern": [
185185
{
186-
"regexp": "^([^:]:?[^:]*):(\\d+):(\\d+):\\s+(warning|)(?:[:]\\s+)?(.*)$",
186+
"regexp": "^([^:]:?[^:]*):(\\d+):(\\d+):\\s+(?:([a-z]+):\\s+)?(.*)$",
187187
"file": 1,
188188
"line": 2,
189189
"column": 3,
@@ -209,6 +209,22 @@
209209
"description": "Just check the current file only"
210210
}
211211
}
212+
},
213+
{
214+
"type": "gnatprove",
215+
"required": [
216+
"projectFile"
217+
],
218+
"properties": {
219+
"projectFile": {
220+
"type": "string",
221+
"description": "The project file"
222+
},
223+
"taskKind": {
224+
"type": "integer",
225+
"description": "Check the current file only or whole project"
226+
}
227+
}
212228
}
213229
],
214230
"commands": [
@@ -256,4 +272,4 @@
256272
"vscode-languageclient": "^7.0.0",
257273
"ws": "^7.5.2"
258274
}
259-
}
275+
}

integration/vscode/ada/src/extension.ts

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,16 @@ import * as vscode_languageclient from 'vscode-languageclient/node';
2020
import * as process from 'process';
2121

2222
import GPRTaskProvider from './gprTaskProvider';
23+
import gnatproveTaskProvider from './gnatproveTaskProvider';
2324

24-
let alsTaskProvider: undefined | vscode.Disposable = vscode.tasks.registerTaskProvider(
25-
GPRTaskProvider.gprBuildType,
26-
new GPRTaskProvider()
27-
);
25+
let alsTaskProvider: vscode.Disposable[] = [
26+
vscode.tasks.registerTaskProvider(GPRTaskProvider.gprBuildType, new GPRTaskProvider()),
27+
28+
vscode.tasks.registerTaskProvider(
29+
gnatproveTaskProvider.gnatproveType,
30+
new gnatproveTaskProvider()
31+
),
32+
];
2833

2934
export function activate(context: vscode.ExtensionContext): void {
3035
let serverModule = context.asAbsolutePath(process.platform + '/ada_language_server');
@@ -81,8 +86,8 @@ export function activate(context: vscode.ExtensionContext): void {
8186
}
8287

8388
export function deactivate(): void {
84-
if (alsTaskProvider) {
85-
alsTaskProvider.dispose();
86-
alsTaskProvider = undefined;
89+
for (const item of alsTaskProvider) {
90+
item.dispose();
8791
}
92+
alsTaskProvider = [];
8893
}
Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
/*----------------------------------------------------------------------------
2+
-- Language Server Protocol --
3+
-- --
4+
-- Copyright (C) 2018-2021, AdaCore --
5+
-- --
6+
-- This is free software; you can redistribute it and/or modify it under --
7+
-- terms of the GNU General Public License as published by the Free Soft- --
8+
-- ware Foundation; either version 3, or (at your option) any later ver- --
9+
-- sion. This software is distributed in the hope that it will be useful, --
10+
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
11+
-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
12+
-- License for more details. You should have received a copy of the GNU --
13+
-- General Public License distributed with this software; see file --
14+
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy --
15+
-- of the license. --
16+
----------------------------------------------------------------------------*/
17+
18+
import * as vscode from 'vscode';
19+
20+
enum taskKinds {
21+
proveProject, // Run gnatprove for the project
22+
proveFile, // Run gnatprove for the single file
23+
}
24+
25+
export default class gnatproveTaskProvider implements vscode.TaskProvider<vscode.Task> {
26+
public static gnatproveType = 'gnatprove';
27+
gnatproveTasks: vscode.Task[] | undefined;
28+
29+
constructor() {
30+
this.gnatproveTasks = undefined;
31+
}
32+
33+
// eslint-disable-next-line @typescript-eslint/no-unused-vars
34+
provideTasks(_token: vscode.CancellationToken): vscode.Task[] {
35+
if (!this.gnatproveTasks) {
36+
this.gnatproveTasks = getTasks();
37+
}
38+
return this.gnatproveTasks;
39+
}
40+
41+
resolveTask(
42+
task: vscode.Task,
43+
// eslint-disable-next-line @typescript-eslint/no-unused-vars
44+
_token: vscode.CancellationToken
45+
): vscode.ProviderResult<vscode.Task> {
46+
return task;
47+
}
48+
}
49+
50+
const getTasks = (): vscode.Task[] => {
51+
function makeTask(taskKind: taskKinds, args: string[], title: string) {
52+
const kind = {
53+
type: gnatproveTaskProvider.gnatproveType,
54+
projectFile: '${config:ada.projectFile}',
55+
taskKind: taskKind,
56+
};
57+
const shell = new vscode.ShellExecution('gnatprove', args);
58+
const task = new vscode.Task(kind, vscode.TaskScope.Workspace, title, 'ada', shell, '$ada');
59+
task.group = vscode.TaskGroup.Build;
60+
return task;
61+
}
62+
63+
const result: vscode.Task[] = [];
64+
65+
// Run gnatprove on current project
66+
const proveProject = makeTask(
67+
taskKinds.proveProject,
68+
getGnatproveArgs('${config:ada.projectFile}'),
69+
'Run gnatprove on the current project'
70+
);
71+
72+
// Run gnatprove on a file
73+
const proveFile = makeTask(
74+
taskKinds.proveFile,
75+
getGnatproveArgs('${config:ada.projectFile}', '${fileBasename}'),
76+
'Run gnatprove on the current file'
77+
);
78+
result.push(proveProject);
79+
result.push(proveFile);
80+
81+
return result;
82+
};
83+
84+
const getGnatproveArgs = (projectFile?: string, file?: string): string[] => {
85+
// Append file (if any) and `-gnatef` to generate full file names in errors/warnings
86+
const arg = file ? [file] : [];
87+
const p_gnatef = ['-cargs', '-gnatef'];
88+
return commonArgs(projectFile).concat(arg, p_gnatef);
89+
};
90+
91+
// return '-P project.gpr -XVAR=value` optiona
92+
const commonArgs = (projectFile?: string): string[] => {
93+
const vars: string[][] = Object.entries(
94+
vscode.workspace.getConfiguration('ada').get('scenarioVariables') ?? []
95+
);
96+
const fold = (args: string[], item: string[]): string[] => {
97+
const option = '-X' + item[0] + '=' + item[1];
98+
return args.concat([option]);
99+
};
100+
// Set projectFile is any
101+
const prj = projectFile ? ['-P', projectFile] : [];
102+
// for each scenarioVariables put `-Xname=value` option
103+
return vars.reduce(fold, prj);
104+
};

0 commit comments

Comments
 (0)