search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.87k stars 255 forks source link

Confusing error message regarding `dafny test` #3378

Open davidcok opened 1 year ago

davidcok commented 1 year ago

Dafny version

3.10.0+dev

Code to produce this issue

method {:extern} m(i: int, ghost j: int)
  requires j == 1
{
}

Command to run and resulting output

dafny test --test-assumptions:Externs text.dfy

What happened?

text.dfy(2,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.

Dafny program verifier finished with 0 verified, 0 errors Errors compiling program: (5006,17): error CS0501: '__default.m(BigInteger)' must declare a body because it is not marked abstract, extern, or partial

The warning is fine, but the subsequent error is confusing: a body is declared and it is marked extern. ??

What type of operating system are you experiencing the problem on?

Mac

MikaelMayer commented 1 year ago

This is a C# error message on which we have no control, so I'm closing this issue. Extern methods in C# do exist.

davidcok commented 1 year ago

Regardless of whether it comes from C# - that is an internal implementation detail for Dafny -- we should not emit confusing error messages to users. At minimum Dafny should not try to compile programs it can anticipate will fail to compile.

MikaelMayer commented 1 year ago

we should not emit confusing error messages to users

If we replaced "Errors compiling program:" by "Errors returned by the dotnet compiler when trying to compile the cs code generated by Dafny", would that solve your concern? Although I hate internal error messages, I don't want to hide them from the user, otherwise it makes things hard to replicate and debug for us.

davidcok commented 1 year ago

I have two points: 1) Dafny should not be sending code to the C# compiler that does not copmpile - that is a Dafny bug. 2) If it does, I agree that the error message from the C# compiler is "internal", but we should at least wrap it in a way that the user understands it is an internal defensive report that should be reported as a bug.