-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add verification loggers and report generator #38
Changes from 39 commits
aed044e
59bb5ad
7f246e0
8781a8d
c6c0764
13cf6c2
7906775
2c3bd36
30a8c34
d6a2aaf
6013e6e
0c527a2
0d0649e
6c5d6ec
03d2c9e
caf667a
1fc5c6d
0d19733
6460f3d
0f2e495
089c493
043a867
e56325b
b52462d
f1c4890
045408a
3be0e51
f675930
9bc2e6d
aa1927e
12426a0
548a9df
717d820
f6ad164
5fc4b19
94f9189
27c350c
ab26e78
519f1c9
a410700
feedfa8
48340eb
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
name: 'Test Report' | ||
on: | ||
workflow_run: | ||
workflows: ['tests'] # runs after CI workflow | ||
types: | ||
- completed | ||
jobs: | ||
report: | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: dorny/test-reporter@v1 | ||
with: | ||
artifact: verification-results | ||
name: Verification Tests | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why are we using the name "test" here? Isn't it reporting verification metrics? Or is it related to Dafny's There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Nope, I just did a poor job of editing the template. :) I'm changing it to "Verification Results" |
||
path: '*.trx' | ||
reporter: dotnet-trx |
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
|
@@ -18,10 +18,20 @@ jobs: | |||||
with: | ||||||
dafny-version: "3.4.2" | ||||||
|
||||||
- uses: actions/setup-python@v1 | ||||||
- name: Install Dafny report generator | ||||||
run: dotnet tool install --global dafny-reportgenerator | ||||||
|
||||||
- name: Install lit | ||||||
run: pip install lit OutputCheck | ||||||
|
||||||
- name: Verify/Test Dafny code | ||||||
run: lit --time-tests -v . | ||||||
- name: Verify Dafny Code | ||||||
run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' . | ||||||
|
||||||
- name: Generate Report | ||||||
run: find . -name '*.csv' | xargs -t dafny-reportgenerator summarize-csv-results --max-duration-seconds 10 | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What happens if there are too many There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah I'm a bit concerned that will be an issue in the future and cut an issue here: dafny-lang/dafny-reportgenerator#4. The current command length is 1505 so we've got a fair bit of headroom under the 4K limit at least (if it applies to the commands that xargs generates). |
||||||
|
||||||
- uses: actions/upload-artifact@v2 # upload test results | ||||||
if: success() || failure() # run this step even if previous step failed | ||||||
with: | ||||||
name: verification-results | ||||||
path: 'TestResults/*.trx' | ||||||
atomb marked this conversation as resolved.
Show resolved
Hide resolved
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,2 @@ | ||
**/Output/ | ||
**/TestResults/ |
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Test
sounds like a verb here to me. MaybeGenerate test report
? Same in the file name.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fair point! This is from the template at https://github.com/dorny/test-reporter so I opened a PR to fix it there too. :)