Skip to content
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

Unstable CLI test git-issues/git-issue-697j.dfy, related to Rust backend #5537

Open
Tracked by #5561
keyboardDrummer opened this issue Jun 6, 2024 · 5 comments
Open
Tracked by #5561
Labels
kind: language development speed Slows down development of Dafny the language, flaky tests part: ci Issue is with Dafny's CI infrastructure priority: not yet Will reconsider working on this when we're looking for work

Comments

@keyboardDrummer
Copy link
Member

https://github.com/dafny-lang/dafny/actions/runs/9399349297/job/25886601888

[xUnit.net 00:19:37.60]   Finished:    IntegrationTests
  Failed git-issues/git-issue-697j.dfy [11 m 28 s]
  Error Message:
   System.AggregateException : One or more errors occurred. (Command returned non-zero exit code (255): dotnet /Users/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestDafny.dll for-each-compiler --dafny /Users/runner/work/dafny/dafny/unzippedRelease/dafny/dafny --refresh-exit-code=0 TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy -- --allow-warnings
Output:
Using legacy resolver and verifying...
Using refresh resolver and verifying...
Executing on C#...
Executing on C# (with --include-runtime:false)...
Executing on JavaScript...
Executing on Go...
Executing on Java...
Executing on Python...
Executing on C++...
Executing on Rust...
OutputCheck on TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check failed. Output was:

Executing on ResolvedDesugaredExecutableDafny...

Error:
ERROR: Could not find any match for CheckLiteral Directive (TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.rs.check:1 Literal: 'Unhandled exception: System.InvalidOperationException: Operation is not valid due to the current state of the object.'). The output is above.
@keyboardDrummer keyboardDrummer added the kind: language development speed Slows down development of Dafny the language, flaky tests label Jun 6, 2024
@MikaelMayer
Copy link
Member

One of the things I've observed is that the Rust backend downloads a lot of dependencies and sometimes fails if one of these dependencies cannot be downloaded. This might be one of the case. It's going to slow us down.

@stefan-aws
Copy link
Collaborator

@robin-aws
Copy link
Member

One of the things I've observed is that the Rust backend downloads a lot of dependencies and sometimes fails if one of these dependencies cannot be downloaded. This might be one of the case. It's going to slow us down.

Is that the root cause here though? It seems unlikely given the failure.

If it is a problem, there are caching tools that might help:

@robin-aws
Copy link
Member

@stefan-aws
Copy link
Collaborator

@stefan-aws stefan-aws added priority: not yet Will reconsider working on this when we're looking for work and removed priority: unknown labels Jun 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: language development speed Slows down development of Dafny the language, flaky tests part: ci Issue is with Dafny's CI infrastructure priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Development

No branches or pull requests

4 participants