Skip to content

Commit f62d9d2

Browse files
godunkogodunko
committed
Merge branch 'topic/edge_merge' into 'edge'
Merge master into edge See merge request eng/ide/ada_language_server!1201
2 parents b6b4ee7 + 974bb0a commit f62d9d2

File tree

3 files changed

+116
-56
lines changed

3 files changed

+116
-56
lines changed

‎.gitlab-ci.yml‎

Lines changed: 102 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,69 @@ variables:
55
stages:
66
- build_and_test
77

8+
.detect-branches:
9+
# Version 1.
10+
# Detects source and target branches. Checkout necessary branch for
11+
# repository when run downstream pipeline is detected.
12+
# ACI_SOURCE_BRANCH is set to source branch (merge request, pull)
13+
# ACI_TARGET_BRANCH is set to target branch of merge request, or 'master'/'edge' for pull
14+
# ACI_REPOSITORY_NAME_EDGE_SUFFIX is set to '-edge' when target repository is 'edge'
15+
# ACI_ANOD_QUALIFIER is set to 'edge' when target repository is 'edge'
16+
# ACI_SUBPROJECTS_ROOT is set to '/tmp' and may be overritten by script
17+
- |
18+
if [[ -n "$ACI_UPSTREAM_SOURCE_BRANCH" ]]; then
19+
ACI_SOURCE_BRANCH="$ACI_UPSTREAM_SOURCE_BRANCH";
20+
elif [[ -n "$CI_MERGE_REQUEST_SOURCE_BRANCH_NAME" ]]; then
21+
ACI_SOURCE_BRANCH="$CI_MERGE_REQUEST_SOURCE_BRANCH_NAME";
22+
else
23+
ACI_SOURCE_BRANCH="$CI_COMMIT_BRANCH";
24+
fi;
25+
if [[ -n "$ACI_UPSTREAM_TARGET_BRANCH" ]]; then
26+
ACI_TARGET_BRANCH=$ACI_UPSTREAM_TARGET_BRANCH;
27+
elif [[ -n "$CI_MERGE_REQUEST_TARGET_BRANCH_NAME" ]]; then
28+
ACI_TARGET_BRANCH="$CI_MERGE_REQUEST_TARGET_BRANCH_NAME";
29+
elif [[ "x$CI_COMMIT_BRANCH" == "xedge" ]]; then
30+
ACI_TARGET_BRANCH="edge";
31+
else
32+
ACI_TARGET_BRANCH="master";
33+
fi;
34+
if [[ "$ACI_TARGET_BRANCH" == "edge" ]]; then
35+
ACI_REPOSITORY_NAME_EDGE_SUFFIX="-edge";
36+
ACI_ANOD_QUALIFIER="edge"
37+
else
38+
ACI_REPOSITORY_NAME_EDGE_SUFFIX="";
39+
ACI_ANOD_QUALIFIER=""
40+
fi
41+
ACI_SUBPROJECTS_ROOT=/tmp
42+
echo "Source branch: $ACI_SOURCE_BRANCH"
43+
echo "Target branch: $ACI_TARGET_BRANCH"
44+
echo "Name suffix: $ACI_REPOSITORY_NAME_EDGE_SUFFIX"
45+
echo "Qualifier: $ACI_ANOD_QUALIFIER"
46+
echo "Subprojects: $ACI_SUBPROJECTS_ROOT"
47+
48+
# On downstream pipeline checkout the necessary branch
49+
- if [[ "$CI_PIPELINE_SOURCE" == 'pipeline' ]]; then
50+
if `git -C $CI_PROJECT_DIR show-ref $ACI_SOURCE_BRANCH > /dev/null`; then
51+
git -C $CI_PROJECT_DIR checkout $ACI_SOURCE_BRANCH;
52+
elif `git -C $CI_PROJECT_DIR show-ref $ACI_TARGET_BRANCH > /dev/null`; then
53+
git -C $CI_PROJECT_DIR checkout $ACI_TARGET_BRANCH;
54+
fi
55+
fi
56+
57+
.checkout-subproject:
58+
# Version 1.
59+
# Input variables:
60+
# ACI_SUBPROJECTS_ROOT - root directory to checkout repositories.
61+
# ACI_SUBPROJECT_REPOSITORY_URL_PATH - path component of the repository's URL.
62+
# ACI_SUBPROJECT_NAME - name of the directory for subproject.
63+
- |
64+
git -C $ACI_SUBPROJECTS_ROOT clone $GIT_CLONE_BASE/$ACI_SUBPROJECT_REPOSITORY_URL_PATH $ACI_SUBPROJECT_NAME
65+
if `git -C $ACI_SUBPROJECTS_ROOT -C $ACI_SUBPROJECT_NAME show-ref $ACI_SOURCE_BRANCH > /dev/null`; then
66+
git -C $ACI_SUBPROJECTS_ROOT -C $ACI_SUBPROJECT_NAME checkout $ACI_SOURCE_BRANCH;
67+
elif `git -C $ACI_SUBPROJECTS_ROOT -C $ACI_SUBPROJECT_NAME show-ref $ACI_TARGET_BRANCH > /dev/null`; then
68+
git -C $ACI_SUBPROJECTS_ROOT -C $ACI_SUBPROJECT_NAME checkout $ACI_TARGET_BRANCH;
69+
fi
70+
anod vcs --sandbox-dir /it/wave --add-repo $ACI_SUBPROJECT_NAME $ACI_SUBPROJECTS_ROOT/$ACI_SUBPROJECT_NAME
871
972
# Build and test with ANOD
1073
# TODO: add a build and test based on Alire in parallel to this.
@@ -15,59 +78,49 @@ build_and_test:
1578
- mem:16
1679
stage: build_and_test
1780
interruptible: true
81+
rules:
82+
- if: $CI_PIPELINE_SOURCE == 'merge_request_event'
83+
- if: $CI_PIPELINE_SOURCE == 'pipeline'
84+
- if: $CI_COMMIT_BRANCH == 'master' && $CI_COMMIT_TITLE =~ /Merge branch.*/
85+
- if: $CI_COMMIT_BRANCH == 'edge' && $CI_COMMIT_TITLE =~ /Merge branch.*/
1886
script:
19-
- . ~/.aws_container_credentials
20-
- export PATH=/it/e3/bin:$PATH
21-
22-
# Check whether we're in an MR targeting 'edge' or commiting to
23-
# `something/edge` branch then setup some variables.
24-
- TARGET_BRANCH="master"
25-
- if [[ "x$CI_MERGE_REQUEST_TARGET_BRANCH_NAME" = "xedge" ||
26-
"$CI_COMMIT_BRANCH" =~ .*/edge ]];
27-
then
28-
echo "Targeting the edge branch." ;
29-
REPO_SUFFIX="-edge" ;
30-
BUILD_SPACE_SUFFIX="_edge" ;
31-
QUALIFIER="edge" ;
32-
TARGET_BRANCH="edge" ;
33-
fi
87+
- !reference [.detect-branches]
3488

35-
# Setup the 'anod vcs' for this repo
36-
- cd /it/wave
37-
- anod vcs --add-repo ada_language_server${REPO_SUFFIX} $CI_PROJECT_DIR
89+
- |
90+
ACI_SUBPROJECT_REPOSITORY_URL_PATH=/eng/ide/spawn.git
91+
ACI_SUBPROJECT_NAME=spawn
92+
- !reference [.checkout-subproject]
3893

39-
# Figure out if we're on a sync branch
40-
- BRANCH=master
41-
- if [[ $CI_COMMIT_BRANCH =~ ^sync/ ]]; then
42-
BRANCH=$CI_COMMIT_BRANCH;
43-
elif [[ $CI_MERGE_REQUEST_SOURCE_BRANCH_NAME =~ ^sync/ ]]; then
44-
BRANCH=$CI_MERGE_REQUEST_SOURCE_BRANCH_NAME;
94+
- |
95+
ACI_SUBPROJECT_REPOSITORY_URL_PATH=/eng/ide/vss.git
96+
ACI_SUBPROJECT_NAME=vss
97+
- !reference [.checkout-subproject]
98+
99+
- |
100+
ACI_SUBPROJECT_REPOSITORY_URL_PATH=/eng/ide/markdown.git
101+
ACI_SUBPROJECT_NAME=markdown
102+
- !reference [.checkout-subproject]
103+
104+
- |
105+
ACI_SUBPROJECT_REPOSITORY_URL_PATH=/eng/ide/gnatdoc.git
106+
ACI_SUBPROJECT_NAME=gnatdoc$ACI_REPOSITORY_NAME_EDGE_SUFFIX
107+
- !reference [.checkout-subproject]
108+
109+
- if [[ "$ACI_TARGET_BRANCH" == "edge" ]]; then
110+
BUILD_SPACE_SUFFIX="_edge";
45111
fi
46112

47-
# Setup the 'anod vcs' for the other repos, if we're on
48-
# a "sync" branch.
49-
- for subproject in vss spawn gnatdoc ; do
50-
echo "for subproject $subproject ..." ;
51-
cd /tmp ;
52-
git clone $GIT_CLONE_BASE/eng/ide/$subproject ;
53-
cd $subproject ;
54-
if `git show-ref $BRANCH > /dev/null` ; then
55-
echo "... checking out $BRANCH"
56-
git checkout $BRANCH ;
57-
cd /it/wave ;
58-
anod vcs --add-repo $subproject /tmp/$subproject ;
59-
else
60-
echo "... checking out $TARGET_BRANCH"
61-
git checkout $TARGET_BRANCH ;
62-
fi ;
63-
done ;
64-
65-
# Build & test using anod
66-
- cd /it/wave
67-
- anod build als --qualifier=$QUALIFIER --minimal
68-
- anod test als --qualifier=$QUALIFIER --minimal
69-
70-
# Process the report
113+
- |
114+
# Setup the 'anod vcs' for this repo
115+
cd /it/wave
116+
anod vcs --add-repo ada_language_server$ACI_REPOSITORY_NAME_EDGE_SUFFIX $CI_PROJECT_DIR
117+
118+
# Build & test using anod
119+
cd /it/wave
120+
- anod build als --qualifier=$ACI_ANOD_QUALIFIER --minimal
121+
- anod test als --qualifier=$ACI_ANOD_QUALIFIER --minimal
122+
123+
# Process the report
71124
- e3-testsuite-report
72125
--failure-exit-code 1
73126
--xunit-output $CI_PROJECT_DIR/xunit_output.xml
@@ -85,7 +138,7 @@ build_and_test:
85138
export GPR_PROJECT_PATH=/it/wave/x86_64-linux/als/src/subprojects/gnatdoc/gnat:$GPR_PROJECT_PATH;
86139
export GPR_PROJECT_PATH=/it/wave/x86_64-linux/als/src/subprojects/VSS/gnat:$GPR_PROJECT_PATH;
87140
cd /it/wave/x86_64-linux/als/src;
88-
lsif-ada gnat/lsp_server.gpr > $CI_PROJECT_DIR/dump.lsif ||
141+
lsif-ada gnat/lsp_server.gpr > $CI_PROJECT_DIR/dump.lsif 2>/dev/null ||
89142
touch $CI_PROJECT_DIR/dump.lsif )
90143

91144
- if [ ! -z ${FAILED+x} ]; then echo "There was at least one testcase failure" && exit 1; fi

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,7 @@ The extension includes a task provider. It provides the following "auto-detected
161161
* "ada: Prove subprogram" - launch `gnatprove` on the current subprogram in the current editor
162162
* "ada: Prove selected region" - launch `gnatprove` on the selected region in the current editor
163163
* "ada: Prove line" - launch `gnatprove` on the cursor line in the current editor
164+
* "ada: Clean project for proof" - launch `gnatprove` on the current GPR project to clean proof artefacts
164165

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

‎integration/vscode/ada/src/gnatTaskProvider.ts‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -94,44 +94,50 @@ const getGnatArgs = (args: string[]): string[] => {
9494
* Map of known tasks/tools indexed by a string/taskKind
9595
*/
9696
const knownTaskKinds: { [id: string]: TaskProperties } = {
97+
cleanProjectForProof: {
98+
command: getGnatArgs(['gnatprove', '--clean']),
99+
extra: undefined,
100+
title: 'Clean project for proof',
101+
},
97102
examineProject: {
98-
command: getGnatArgs(['gnatprove', '--mode=flow']),
103+
command: getGnatArgs(['gnatprove', '-j0', '--mode=flow']),
99104
extra: undefined,
100105
title: 'Examine project',
101106
},
102107
examineFile: {
103-
command: getGnatArgs(['gnatprove', '--mode=flow', '-u', '${fileBasename}']),
108+
command: getGnatArgs(['gnatprove', '-j0', '--mode=flow', '-u', '${fileBasename}']),
104109
extra: undefined,
105110
title: 'Examine file',
106111
},
107112
examineSubprogram: {
108-
command: ['gnatprove', '--mode=flow'],
113+
command: ['gnatprove', '-j0', '--mode=flow'],
109114
extra: limitSubp,
110115
title: 'Examine subprogram',
111116
},
112117
proveProject: {
113-
command: getGnatArgs(['gnatprove']),
118+
command: getGnatArgs(['gnatprove', '-j0']),
114119
extra: undefined,
115120
title: 'Prove project',
116121
},
117122
proveFile: {
118-
command: getGnatArgs(['gnatprove', '-u', '${fileBasename}']),
123+
command: getGnatArgs(['gnatprove', '-j0', '-u', '${fileBasename}']),
119124
extra: undefined,
120125
title: 'Prove file',
121126
},
122127
proveSubprogram: {
123-
command: ['gnatprove'],
128+
command: ['gnatprove', '-j0'],
124129
extra: limitSubp,
125130
title: 'Prove subprogram',
126131
},
127132
proveRegion: {
128-
command: ['gnatprove', '-u', '${fileBasename}'],
133+
command: ['gnatprove', '-j0', '-u', '${fileBasename}'],
129134
extra: limitRegion,
130135
title: 'Prove selected region',
131136
},
132137
proveLine: {
133138
command: getGnatArgs([
134139
'gnatprove',
140+
'-j0',
135141
'-u',
136142
'${fileBasename}',
137143
'--limit-line=${fileBasename}:${lineNumber}',

0 commit comments

Comments
 (0)