-
Notifications
You must be signed in to change notification settings - Fork 260
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
test fails: DafnyTests/TestAttribute.dfy #1571
Comments
What are your environment variables? Try to run with |
I ran it with
Not sure if that answers your question about environment variables. If not, please let me know which ones you're interested in; a whole dump would probably include things that shouldn't be public. |
Just in case, I just upgraded to Dafny's latest commit (1fc7bff) and repeated the test:
|
FYI, potentially related to #1540 - the same test was stubbornly failing on Windows until @MikaelMayer figured out an environment variable wasn't being passed through when this test invoked |
The thing is, my environment is over 200K, and contains things like access tokens, so I can't just publish it all. And sanitizing all of that would be difficult and uncertain. Is there any subset that is of interest? Is it helpful if I clear most of the environment and repeat the test? |
On Wednesday I just fixed a bug of the same test failing on Windows. |
There's no LOCALAPPDATA in my environment. |
Interestingly, though there is no |
I looked at your trace and just figured out I forgot to mention something. |
I upgraded to Dafny commit 6f23068, modified TestAttribute.dfy as requested and ran again: $ dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy > log.txt
[xUnit.net 00:00:04.93] DafnyTests/TestAttribute.dfy [FAIL]
Test Run Failed. |
Can you remove the temporary files in /Output (like Output/DafnyMain.cs) and start again? |
I see a lot of Output directories, none at the root of the Dafny directory. Which one do you mean? Is it enough if I do something like |
(I see that Anyway, I guess that you mean (repo root)/Test/DafnyTests/Output, which does contain a DafnyMain.cs. I deleted that directory and reran. $ dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy > log2.txt
[xUnit.net 00:00:07.80] DafnyTests/TestAttribute.dfy [FAIL]
Test Run Failed. |
Great, deleting that file actually seems to have solved the problem. I see in the log that it correctly outputs what was expected:
. Now ensure the Output/ folder is empty again, remove the extra dotnet line that I made you add with the diagnostics, and run the test again. It should work. |
Something strange is happening... At my first try at following your instructions, I found that the Output folder was no longer there at all, and the test (reverted to its original form) still failed anyway. $ ls -la Test/DafnyTests
total 176
drwxr-xr-x 9 mija staff 288 Dec 1 12:37 .
drwxr-xr-x 47 mija staff 1504 Nov 5 14:23 ..
-rw-r--r--@ 1 mija staff 6148 Dec 1 12:37 .DS_Store
-rw-r--r-- 1 mija staff 420 Aug 16 14:55 DafnyTests.csproj
-rw-r--r-- 1 mija staff 68056 Nov 25 17:21 TestAttribute.cs
-rw-r--r--@ 1 mija staff 1631 Dec 2 08:51 TestAttribute.dfy
-rw-r--r--@ 1 mija staff 416 Nov 5 13:11 TestAttribute.dfy.expect
drwxr-xr-x 3 mija staff 96 Aug 16 14:56 bin
drwxr-xr-x 8 mija staff 256 Nov 5 14:14 obj
$ dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy > log3.txt
[xUnit.net 00:00:06.00] DafnyTests/TestAttribute.dfy [FAIL]
Test Run Failed. I thought to run $ make exe
(cd /Users/mija/repos/dafny/dafny/ ; dotnet build Source/Dafny.sln ) ## includes parser
Microsoft (R) Build Engine version 16.11.1+3e40a09f8 for .NET
Copyright (C) Microsoft Corporation. All rights reserved.
Determining projects to restore...
All projects are up-to-date for restore.
DafnyPipeline -> /Users/mija/repos/dafny/dafny/Source/Dafny/bin/Debug/net5.0/DafnyPipeline.dll
XUnitExtensions -> /Users/mija/repos/dafny/dafny/Source/XUnitExtensions/bin/Debug/net5.0/XUnitExtensions.dll
Compiling DafnyRuntimeJava to DafnyRuntimeJava/build/libs/DafnyRuntime.jar...
DafnyServer -> /Users/mija/repos/dafny/dafny/Binaries/DafnyServer.dll
DafnyTestGeneration -> /Users/mija/repos/dafny/dafny/Source/DafnyTestGeneration/bin/Debug/net5.0/DafnyTestGeneration.dll
DafnyTestGeneration.Test -> /Users/mija/repos/dafny/dafny/Source/DafnyTestGeneration.Test/bin/Debug/net5.0/DafnyTestGeneration.Test.dll
DafnyRuntime -> /Users/mija/repos/dafny/dafny/Binaries/net5.0/DafnyRuntime.dll
Compiling DafnyRuntimeJava to DafnyRuntimeJava/build/libs/DafnyRuntime.jar...
DafnyDriver -> /Users/mija/repos/dafny/dafny/Binaries/Dafny.dll
DafnyPipeline.Test -> /Users/mija/repos/dafny/dafny/Source/DafnyPipeline.Test/bin/Debug/net5.0/DafnyPipeline.Test.dll
/usr/local/share/dotnet/sdk/5.0.402/Microsoft.Common.CurrentVersion.targets(4966,5): error MSB3030: Could not copy the file "/Users/mija/repos/dafny/dafny/Source/DafnyRuntime/DafnyRuntimeJava/build/libs/DafnyRuntime.jar" because it was not found. [/Users/mija/repos/dafny/dafny/Source/DafnyLanguageServer/DafnyLanguageServer.csproj]
Successfully created package '/Users/mija/repos/dafny/dafny/Binaries/DafnyRuntime.1.1.0.nupkg'.
IntegrationTests -> /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/IntegrationTests.dll
Build FAILED.
/usr/local/share/dotnet/sdk/5.0.402/Microsoft.Common.CurrentVersion.targets(4966,5): error MSB3030: Could not copy the file "/Users/mija/repos/dafny/dafny/Source/DafnyRuntime/DafnyRuntimeJava/build/libs/DafnyRuntime.jar" because it was not found. [/Users/mija/repos/dafny/dafny/Source/DafnyLanguageServer/DafnyLanguageServer.csproj]
0 Warning(s)
1 Error(s)
Time Elapsed 00:00:15.33
make: *** [exe] Error 1 (Note: I am not using Java at the moment, I haven't touched the DafnyRuntime.jar file, and my git client didn't show any change regarding that file!) Thinking I was blocked, I tried $ make clean
(cd /Users/mija/repos/dafny/dafny/; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin )
(cd /Users/mija/repos/dafny/dafny/ ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
Build succeeded.
0 Warning(s)
0 Error(s)
Time Elapsed 00:00:06.59
make -C /Users/mija/repos/dafny/dafny//Source/Dafny -f Makefile.Linux clean
(cd /Users/mija/repos/dafny/dafny//Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
Deprecated Gradle features were used in this build, making it incompatible with Gradle 7.0.
Use '--warning-mode all' to show the individual deprecation warnings.
See https://docs.gradle.org/6.3/userguide/command_line_interface.html#sec:command_line_warnings
BUILD SUCCESSFUL in 629ms
1 actionable task: 1 executed
make -C /Users/mija/repos/dafny/dafny//docs/DafnyRef clean
(cd /Users/mija/repos/dafny/dafny/; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin )
echo Source/*/bin Source/*/obj
Source/DafnyLanguageServer.Test/bin Source/DafnyPipeline.Test/bin Source/DafnyTestGeneration.Test/bin Source/DafnyTestGeneration/bin Source/IntegrationTests/bin Source/XUnitExtensions/bin Source/DafnyLanguageServer.Test/obj Source/DafnyLanguageServer/obj Source/DafnyPipeline.Test/obj Source/DafnyTestGeneration.Test/obj Source/DafnyTestGeneration/obj Source/IntegrationTests/obj Source/XUnitExtensions/obj
$ make exe
(cd /Users/mija/repos/dafny/dafny/ ; dotnet build Source/Dafny.sln ) ## includes parser
Microsoft (R) Build Engine version 16.11.1+3e40a09f8 for .NET
Copyright (C) Microsoft Corporation. All rights reserved.
Determining projects to restore...
Restored /Users/mija/repos/dafny/dafny/Source/Dafny/DafnyPipeline.csproj (in 229 ms).
Restored /Users/mija/repos/dafny/dafny/Source/DafnyRuntime/DafnyRuntime.csproj (in 229 ms).
Restored /Users/mija/repos/dafny/dafny/Source/DafnyServer/DafnyServer.csproj (in 229 ms).
Restored /Users/mija/repos/dafny/dafny/Source/DafnyDriver/DafnyDriver.csproj (in 262 ms).
7 of 11 projects are up-to-date for restore.
Tool 'cocor' (version '2014.12.23') was restored. Available commands: coco
Tool 'dotnet-format' (version '5.1.225507') was restored. Available commands: dotnet-format
Restore was successful.
XUnitExtensions -> /Users/mija/repos/dafny/dafny/Source/XUnitExtensions/bin/Debug/net5.0/XUnitExtensions.dll
Compiling DafnyRuntimeJava to DafnyRuntimeJava/build/libs/DafnyRuntime.jar...
.NET SDK (reflecting any global.json):
Version: 5.0.402
Commit: e9d3381880
Runtime Environment:
OS Name: Mac OS X
OS Version: 11.0
OS Platform: Darwin
RID: osx.11.0-x64
Base Path: /usr/local/share/dotnet/sdk/5.0.402/
Host (useful for support):
Version: 5.0.11
Commit: f431858f8b
.NET SDKs installed:
5.0.402 [/usr/local/share/dotnet/sdk]
.NET runtimes installed:
Microsoft.AspNetCore.App 5.0.11 [/usr/local/share/dotnet/shared/Microsoft.AspNetCore.App]
Microsoft.NETCore.App 5.0.11 [/usr/local/share/dotnet/shared/Microsoft.NETCore.App]
To install additional .NET runtimes or SDKs:
https://aka.ms/dotnet-download
Coco/R (Apr 19, 2011)
checking
OldSemi deletable
ParameterDefaultValue deletable
IteratorSpec deletable
MethodSpec deletable
OptGenericInstantiation deletable
FunctionSpec deletable
LoopSpec deletable
LambdaSpec deletable
LL1 warning in ModuleExport: least is start & successor of deletable structure
LL1 warning in ModuleExport: greatest is start & successor of deletable structure
parser + scanner generated
0 errors detected
DafnyPipeline -> /Users/mija/repos/dafny/dafny/Source/Dafny/bin/Debug/net5.0/DafnyPipeline.dll
Successfully created package '/Users/mija/repos/dafny/dafny/Source/Dafny/bin/Debug/DafnyPipeline.1.1.0.nupkg'.
DafnyRuntime -> /Users/mija/repos/dafny/dafny/Binaries/net5.0/DafnyRuntime.dll
DafnyServer -> /Users/mija/repos/dafny/dafny/Binaries/DafnyServer.dll
Compiling DafnyRuntimeJava to DafnyRuntimeJava/build/libs/DafnyRuntime.jar...
DafnyTestGeneration -> /Users/mija/repos/dafny/dafny/Source/DafnyTestGeneration/bin/Debug/net5.0/DafnyTestGeneration.dll
Successfully created package '/Users/mija/repos/dafny/dafny/Source/DafnyTestGeneration/bin/Debug/DafnyTestGeneration.1.1.0.nupkg'.
DafnyTestGeneration.Test -> /Users/mija/repos/dafny/dafny/Source/DafnyTestGeneration.Test/bin/Debug/net5.0/DafnyTestGeneration.Test.dll
Successfully created package '/Users/mija/repos/dafny/dafny/Binaries/DafnyRuntime.1.1.0.nupkg'.
DafnyDriver -> /Users/mija/repos/dafny/dafny/Binaries/Dafny.dll
DafnyPipeline.Test -> /Users/mija/repos/dafny/dafny/Source/DafnyPipeline.Test/bin/Debug/net5.0/DafnyPipeline.Test.dll
DafnyLanguageServer -> /Users/mija/repos/dafny/dafny/Binaries/DafnyLanguageServer.dll
DafnyLanguageServer.Test -> /Users/mija/repos/dafny/dafny/Source/DafnyLanguageServer.Test/bin/Debug/net5.0/DafnyLanguageServer.Test.dll
IntegrationTests -> /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/IntegrationTests.dll
Build succeeded.
0 Warning(s)
0 Error(s)
Time Elapsed 00:00:16.24
$ ls -la Test/DafnyTests
total 176
drwxr-xr-x 9 mija staff 288 Dec 1 12:37 .
drwxr-xr-x 47 mija staff 1504 Nov 5 14:23 ..
-rw-r--r--@ 1 mija staff 6148 Dec 1 12:37 .DS_Store
-rw-r--r-- 1 mija staff 420 Aug 16 14:55 DafnyTests.csproj
-rw-r--r-- 1 mija staff 68056 Nov 25 17:21 TestAttribute.cs
-rw-r--r--@ 1 mija staff 1590 Dec 2 08:57 TestAttribute.dfy
-rw-r--r--@ 1 mija staff 416 Nov 5 13:11 TestAttribute.dfy.expect
drwxr-xr-x 3 mija staff 96 Aug 16 14:56 bin
drwxr-xr-x 8 mija staff 256 Nov 5 14:14 obj
$ dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy > log3.txt
$ So, in summary: yes, the test now passes, but it's sounding like the makefile / build process needs some scrubbing, and maybe it was even the original reason for the test failure? |
What is the content of It looks like the first I'm wondering what went wrong here. |
Ugh, sorry, I overwrote that log3.txt file with the last successful run! If I find myself in that situation again I'll make sure to save it. About the missing jar - this is not the first time I run |
I suspect that the jar got deleted when at some point I started running the full set of tests by mistake and interrupted it with ^C while it was still building. I can see that during that building process, the jar is deleted and copied or rebuilt, so interrupting at that point might cause that problem maybe? Since then I ran only the TestAttribute test. Looks like the tests and the general Dafny project have different or overlapping build systems, so maybe one of them can leave things in a state that the other doesn't understand, and Relatedly, I just realized that if I try running the tests with the deprecated All together, given that it looks like my tree is accumulating cruft because of deprecations and whatnot and that |
Oh I did not realize that the lit command was creating these undesirable files for the dotnet test command. |
Dafny 3.3 (commit 88cf232)
macOS 11.6
The text was updated successfully, but these errors were encountered: