-
Notifications
You must be signed in to change notification settings - Fork 260
185 lines (167 loc) · 7.99 KB
/
msbuild.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
name: Build and Test
on:
workflow_dispatch:
pull_request:
branches: [ master, main-* ]
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
env:
dotnet-version: 6.0.x # SDK Version for building Dafny
jobs:
check-deep-tests:
uses: ./.github/workflows/check-deep-tests-reusable.yml
singletons:
needs: check-deep-tests
if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
runs-on: ubuntu-20.04
steps:
- name: Setup dotnet
uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{env.dotnet-version}}
- name: Checkout Dafny
uses: actions/checkout@v4
with:
path: dafny
submodules: recursive
- name: Restore tools
working-directory: dafny
run: dotnet tool restore
- name: Check whitespace and style
working-directory: dafny
run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
- name: Get Boogie Version
run: |
sudo apt-get update
sudo apt-get install -qq libxml2-utils
echo "boogieVersion=`xmllint --xpath "//PackageReference[@Include='Boogie.ExecutionEngine']/@Version" dafny/Source/DafnyCore/DafnyCore.csproj | grep -Po 'Version="\K.*?(?=")'`" >> $GITHUB_ENV
- name: Attempt custom Boogie patch
working-directory: dafny
run: git apply customBoogie.patch
- name: Checkout Boogie
uses: actions/checkout@v4
with:
repository: boogie-org/boogie
path: dafny/boogie
ref: v${{ env.boogieVersion }}
- name: Build Dafny with local Boogie
working-directory: dafny
run: dotnet build Source/Dafny.sln
- name: Create NuGet package (just to make sure it works)
run: dotnet pack dafny/Source/Dafny.sln
- name: Check uniformity of integration tests that exercise backends
run: DAFNY_INTEGRATION_TESTS_MODE=uniformity-check dotnet test dafny/Source/IntegrationTests
xunit-tests:
needs: check-deep-tests
if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
uses: ./.github/workflows/xunit-tests-reusable.yml
integration-tests:
needs: check-deep-tests
if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
uses: ./.github/workflows/integration-tests-reusable.yml
with:
ref: ${{ github.ref }}
# By default run only on one platform, but run on all platforms if the PR has the "run-deep-tests"
# label, and skip checking the nightly build above.
# This is the best way to fix an issue in master that was only caught by the nightly build.
all_platforms: ${{ contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')}}
num_shards: 5
test-coverage-analysis:
runs-on: ubuntu-20.04
# Don't include in run-deep-tests, because those tests run on
# release builds instead of source packages.
if: ${{ !contains(github.event.pull_request.labels.*.name, 'run-deep-tests') && !contains(github.event.push.labels.*.name, 'run-deep-tests')}}))
needs: [xunit-tests, integration-tests]
steps:
# Check out Dafny so that highlighted source is possible
- name: Checkout Dafny
uses: actions/checkout@v4
with:
path: dafny
submodules: recursive
- name: Setup dotnet
uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{env.dotnet-version}}
- name: Install dotnet-reportgenerator and coverage
run: |
dotnet tool install --global dotnet-reportgenerator-globaltool
dotnet tool install --global dotnet-coverage
- name: Install and run Coco
run: |
# Run coco to ensure that all source code is available. It's faster to do this alone than to rebuild everything.
cd dafny
dotnet tool restore
dotnet tool run coco "Source/DafnyCore/Dafny.atg" -namespace Microsoft.Dafny -frames "Source/DafnyCore/Coco"
- name: Download integration test artifacts
uses: actions/download-artifact@v4
with:
pattern: integration-test-results-ubuntu-20.04-*
merge-multiple: true
- name: Download unit test artifacts
uses: actions/download-artifact@v4
with:
name: unit-test-results-ubuntu-20.04
- name: Merge reports
run: |
# Convert the coverage data from the language server to Cobertura format
dotnet coverage merge DafnyLanguageServer.Test.coverage -o DafnyLanguageServer.Test.Cobertura.xml -f cobertura
# Generate a combined report, including xUnit results but not
# LSP results
reportgenerator \
-reports:"./**/coverage.cobertura.xml" \
-reporttypes:Cobertura -targetdir:coverage-cobertura \
-classfilters:"-Microsoft.Dafny.*PreType*;-Microsoft.Dafny.ResolverPass;-Microsoft.Dafny.*Underspecification*;-Microsoft.Dafny.DetectUnderspecificationVisitor;-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector;-Microsoft.Dafny.Compilers.DafnyCompiler;-DAST.*;-DCOMP.*"
# Generate HTML from combined report, leaving out XUnitExtensions
reportgenerator \
-reports:"coverage-cobertura/Cobertura.xml" \
-assemblyfilters:"-XUnitExtensions" \
-reporttypes:HTML -targetdir:coverage-html
# Generate HTML from LSP report, including only LSP stuff
reportgenerator \
-reports:"DafnyLanguageServer.Test.Cobertura.xml" \
-assemblyfilters:"+dafnylanguageserver" \
-reporttypes:HTML -targetdir:lsp-html
# Generate new Cobertura from LSP report, including only LSP stuff
reportgenerator \
-reports:"DafnyLanguageServer.Test.Cobertura.xml" \
-assemblyfilters:"+dafnylanguageserver" \
-reporttypes:Cobertura -targetdir:.
mv Cobertura.xml coverage-cobertura/LSP-Cobertura.xml
- name: Code coverage report (non-LSP)
uses: irongut/[email protected]
with:
filename: ./coverage-cobertura/Cobertura.xml
badge: true
fail_below_min: true
format: markdown
hide_branch_rate: false
hide_complexity: true
indicators: true
output: both
# Fail if less than 86% total coverage, measured across all packages combined.
# Report "yellow" status if less than 90% total coverage.
thresholds: '86 90'
- name: Code coverage report (LSP)
uses: irongut/[email protected]
with:
filename: ./coverage-cobertura/LSP-Cobertura.xml
badge: true
fail_below_min: true
format: markdown
hide_branch_rate: false
hide_complexity: true
indicators: true
output: both
# Fail if less than 86% total coverage, measured across all packages combined.
# Report "yellow" status if less than 90% total coverage.
thresholds: '86 90'
- uses: actions/upload-artifact@v4
if: always() # Upload results even if the job fails
with:
name: test-coverage-results
path: |
coverage-cobertura
coverage-html
lsp-html