Skip to content

Commit

Permalink
Revert "Retry LSP tests in case of error (#5342)" (#5361)
Browse files Browse the repository at this point in the history
This reverts commit 44ca1b2.

### Description
The recently merged PR #5342
argues that we should automatically retry failing IDE tests, because
that's what we manually do anyways. However, we only do that in some
cases. Specifically, when any of us make changes that may create
unstable tests, such as changes in the IDE, then failing IDE tests
should not be retried, manually or automatically. PR5342 makes it so
that such a retry happens automatically, thereby making it much easier
to introduce non-deterministic bugs either in IDE code or tests. That's
why this PR is reverting that one.

IMO there is little difference between a test that fails 100% of the
time and one that fails <100% of the time. Retrying a failing test that
fails <100% of the time is similar to saying "I believe my PR is not at
fault for this test failing, please ignore it". A similar situation
occurs when a PR gets merged that causes nightly to fail. However then
we don't have a way for new PRs to say "please ignore nightly failing",
and we explicitly block all PR until nightly is fixed again. A similar
approach to unstable tests would be to not to retry failing builds until
the instability is resolved, but instead to wait until an instability
fix PR is merged.

### How has this been tested?
It's a revert.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer committed Apr 30, 2024
1 parent 0b629ea commit ba7ac85
Showing 1 changed file with 12 additions and 12 deletions.
24 changes: 12 additions & 12 deletions .github/workflows/xunit-tests-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,10 @@ jobs:
uses: actions/setup-dotnet@v4
with:
dotnet-version: 6.0.x
- name: Install dependencies
run: |
dotnet restore ${{env.solutionPath}}
dotnet tool install dotnet-coverage
- name: Load Z3
shell: pwsh
run: |
Expand All @@ -60,21 +64,17 @@ jobs:
run: |
chmod +x Binaries/z3/bin/z3*
- name: Build
run: dotnet build ${{env.solutionPath}}
run: dotnet build --no-restore ${{env.solutionPath}}
- name: Run DafnyCore Tests
run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyCore.Test/coverlet.runsettings Source/DafnyCore.Test
# Retry LSP tests 3 times because there are some spurious errors
# Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package
- name: Run DafnyLanguageServer Tests
uses: nick-fields/retry@v3
with:
timeout_minutes: 45
max_attempts: 3
command: |
cd dafny
dotnet restore ${{env.solutionPath}}
dotnet tool install dotnet-coverage
dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test
run: |
## Run twice to catch unstable code (Issue #2673)
dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test
## On the second run, collect test coverage data
## Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package
dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test
- name: Run DafnyDriver Tests
run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyDriver.Test/coverlet.runsettings Source/DafnyDriver.Test
- name: Run DafnyPipeline Tests
Expand Down

0 comments on commit ba7ac85

Please sign in to comment.