search

dafny-lang / dafny

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

test fails: DafnyTests/TestAttribute.dfy #1571

Open hmijail opened 3 years ago

hmijail commented 3 years ago

Dafny 3.3 (commit 88cf232) macOS 11.6

$ dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy
[...]
Test run for /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/IntegrationTests.dll (.NETCoreApp,Version=v5.0)
Microsoft (R) Test Execution Command Line Tool Version 16.11.0
Copyright (c) Microsoft Corporation.  All rights reserved.

Starting test execution, please wait...
A total of 1 test files matched the specified pattern.
[xUnit.net 00:00:00.00] xUnit.net VSTest Adapter v2.4.3+1b45f5407b (64-bit .NET 5.0.11)
[xUnit.net 00:00:00.98]   Discovering: IntegrationTests
[xUnit.net 00:00:01.39]   Discovered:  IntegrationTests
[xUnit.net 00:00:01.40]   Starting:    IntegrationTests
[xUnit.net 00:00:05.26]     DafnyTests/TestAttribute.dfy [FAIL]
[xUnit.net 00:00:05.27]       System.Exception : Command returned non-zero exit code (1): diff TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy.expect /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
[xUnit.net 00:00:05.27]       Output:
[xUnit.net 00:00:05.27]       4,8d3
[xUnit.net 00:00:05.27]       <      _module.__default.FailingTest_CheckForFailureForXunit [FAIL]
[xUnit.net 00:00:05.27]       <      _module.__default.FailingTestUsingExpectWithMessage [FAIL]
[xUnit.net 00:00:05.27]       <      _module.__default.FailingTestUsingExpect [FAIL]
[xUnit.net 00:00:05.27]       <      _module.__default.FailingTestUsingNoLHSAssignOrHalt [FAIL]
[xUnit.net 00:00:05.27]       <      _module.__default.FailingTestUsingAssignOrHalt [FAIL]
[xUnit.net 00:00:05.27]
[xUnit.net 00:00:05.27]       Error:
[xUnit.net 00:00:05.27]
[xUnit.net 00:00:05.27]       Stack Trace:
[xUnit.net 00:00:05.27]         /Users/mija/repos/dafny/dafny/Source/XUnitExtensions/Lit/LitTestCase.cs(80,0): at XUnitExtensions.Lit.LitTestCase.Execute(ITestOutputHelper outputHelper)
[xUnit.net 00:00:05.27]         /Users/mija/repos/dafny/dafny/Source/XUnitExtensions/Lit/LitTestCase.cs(50,0): at XUnitExtensions.Lit.LitTestCase.Run(String filePath, LitTestConfiguration config, ITestOutputHelper outputHelper)
[xUnit.net 00:00:05.27]         /Users/mija/repos/dafny/dafny/Source/IntegrationTests/LitTests.cs(106,0): at IntegrationTests.LitTests.LitTest(String path)
[xUnit.net 00:00:05.27]       Output:
[xUnit.net 00:00:05.27]         Executing command: dotnet /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/Dafny.dll /countVerificationErrors:0 /useBaseNameForFileName /compileVerbose:0 /errorTrace:0 /timeLimit:300 /compileVerbose:1 /compile:0 /spillTargetCode:3 /noVerify TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy > /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
[xUnit.net 00:00:05.27]         Executing command: dotnet test -v:q -noLogo /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests 2> /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp.testresults.raw || true
[xUnit.net 00:00:05.27]         Executing command: sed s/[^]]*\]// /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp.testresults.raw >> /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
[xUnit.net 00:00:05.27]         Executing command: diff TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy.expect /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
[xUnit.net 00:00:05.28]   Finished:    IntegrationTests
  Failed DafnyTests/TestAttribute.dfy [3 s]
  Error Message:
   System.Exception : Command returned non-zero exit code (1): diff TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy.expect /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
Output:
4,8d3
<      _module.__default.FailingTest_CheckForFailureForXunit [FAIL]
<      _module.__default.FailingTestUsingExpectWithMessage [FAIL]
<      _module.__default.FailingTestUsingExpect [FAIL]
<      _module.__default.FailingTestUsingNoLHSAssignOrHalt [FAIL]
<      _module.__default.FailingTestUsingAssignOrHalt [FAIL]

Error:

  Stack Trace:
     at XUnitExtensions.Lit.LitTestCase.Execute(ITestOutputHelper outputHelper) in /Users/mija/repos/dafny/dafny/Source/XUnitExtensions/Lit/LitTestCase.cs:line 80
   at XUnitExtensions.Lit.LitTestCase.Run(String filePath, LitTestConfiguration config, ITestOutputHelper outputHelper) in /Users/mija/repos/dafny/dafny/Source/XUnitExtensions/Lit/LitTestCase.cs:line 50
   at IntegrationTests.LitTests.LitTest(String path) in /Users/mija/repos/dafny/dafny/Source/IntegrationTests/LitTests.cs:line 106
  Standard Output Messages:
 Executing command: dotnet /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/Dafny.dll /countVerificationErrors:0 /useBaseNameForFileName /compileVerbose:0 /errorTrace:0 /timeLimit:300 /compileVerbose:1 /compile:0 /spillTargetCode:3 /noVerify TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy > /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
 Executing command: dotnet test -v:q -noLogo /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests 2> /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp.testresults.raw || true
 Executing command: sed s/[^]]*\]// /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp.testresults.raw >> /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp
 Executing command: diff TestFiles/LitTests/LitTest/DafnyTests/TestAttribute.dfy.expect /Users/mija/repos/dafny/dafny/Source/IntegrationTests/bin/Debug/net5.0/TestFiles/LitTests/LitTest/DafnyTests/Output/TestAttribute.dfy.tmp

Test Run Failed.
Total tests: 1
     Failed: 1
 Total time: 6.0709 Seconds
     1>Done Building Project "/Users/mija/repos/dafny/dafny/Source/IntegrationTests/IntegrationTests.csproj" (VSTest target(s)) -- FAILED.

Build FAILED.
    0 Warning(s)
    0 Error(s)

Time Elapsed 00:00:23.78
MikaelMayer commented 3 years ago

What are your environment variables?

Try to run with -v:d and share with me the trace so that I can compare with a Windows machine.

hmijail commented 3 years ago

I ran it with -v:d : 

$ dotnet test -v:d Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy | gistit
[xUnit.net 00:00:06.09]     DafnyTests/TestAttribute.dfy [FAIL]
Test Run Failed.
Gist URL: https://gist.github.com/ac5e99cf29512327f824c1872dd2e53a

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.

hmijail commented 3 years ago

Just in case, I just upgraded to Dafny's latest commit (1fc7bff2ccaf1b30297efc9bc2c6c9fa26b1a493) and repeated the test:

$ dotnet test -v:d Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy | gistit
[xUnit.net 00:00:04.33]     DafnyTests/TestAttribute.dfy [FAIL]
Test Run Failed.
Gist URL: https://gist.github.com/8f2396fdf66c0cc2cba82c2fda40e536
robin-aws commented 3 years ago

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 dotnet test itself. There could be something similar going on here even though you're on macOS.

hmijail commented 3 years ago

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?

MikaelMayer commented 3 years ago

On Wednesday I just fixed a bug of the same test failing on Windows. I had to add -v:diag (this is a very long diagnostic process) and found out that an exception was thrown, and with this level of detail I also had access to the precise stack track of the exception being thrown. It turned out, it was part of the NuGET package manager environment and it was missing the environment variable LOCALAPPDATA which we had to pass through. The trace helped me to identify where null was dereferenced and figure out this missing environment variable. Let us know if this helps.

hmijail commented 3 years ago

There's no LOCALAPPDATA in my environment.
In case it helps, I removed the environment variables that looked to me most suspicious security-wise and ran again the test with -v:diag instead of the previously mentioned -v:d. The resulting log is 98MB; it's too big for a gist so I'm attaching it here. diag2.txt.zip

hmijail commented 3 years ago

Interestingly, though there is no LOCALAPPDATA (with any case) in my environment, I see that the log does mention a LocalAppData. No idea when it appears nor where it comes from.

MikaelMayer commented 2 years ago

I looked at your trace and just figured out I forgot to mention something. Instead of putting the diagnostics in the command dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy because this test is actually spawning another test, please insert just before the line // RUN: dotnet test -v:q -noLogo %S 2> %t.testresults.raw || true the line: // RUN: dotnet test -v:diag -noLogo %S There, you should see more clearly the error made by this test.

hmijail commented 2 years ago

I upgraded to Dafny commit 6f23068dd6ac5b93f64cfe6d7d01e360ee5f47d6, 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.

log.txt.zip

MikaelMayer commented 2 years ago

Can you remove the temporary files in /Output (like Output/DafnyMain.cs) and start again?

hmijail commented 2 years ago

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 make clean && dotnet test -v:n Source/IntegrationTests --filter DisplayName~DafnyTests/TestAttribute.dfy > log.txt ?

hmijail commented 2 years ago

(I see that make clean still leaves Output directories with files inside, which sounds problematic - by the way, this might be related: https://github.com/dafny-lang/dafny/issues/1584 )

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.

log2.txt.zip

MikaelMayer commented 2 years ago

Great, deleting that file actually seems to have solved the problem. I see in the log that it correctly outputs what was expected:

[xUnit.net 00:00:11.50]       Error:
[xUnit.net 00:00:11.50]       [xUnit.net 00:00:00.60]     _module.__default.FailingTest_CheckForFailureForXunit [FAIL]
[xUnit.net 00:00:11.50]       [xUnit.net 00:00:00.61]     _module.__default.FailingTestUsingExpectWithMessage [FAIL]
[xUnit.net 00:00:11.50]       [xUnit.net 00:00:00.61]     _module.__default.FailingTestUsingExpect [FAIL]
[xUnit.net 00:00:11.50]       [xUnit.net 00:00:00.61]     _module.__default.FailingTestUsingNoLHSAssignOrHalt [FAIL]
[xUnit.net 00:00:11.50]       [xUnit.net 00:00:00.61]     _module.__default.FailingTestUsingAssignOrHalt [FAIL]

. 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.

hmijail commented 2 years ago

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 and see if would make the Output folder reappear. But it failed too!

$ 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, though not seeing how it could help. But it worked! Then make exe. It worked too - no Output folder appeared, anyway. Then the test again. And it worked!

$ 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?

MikaelMayer commented 2 years ago

What is the content of log3.txt that you created above? It contained the reason why it failed.

It looks like the first make exe was assuming that the jar runtime existed and because it failed to copy, that's what the test error was about. Now it looks like make clean triggered something so that it forced make exe to regenerate the JAR.

I'm wondering what went wrong here.

hmijail commented 2 years ago

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 make exe in the repo, so if it was ever created, it should still be there. I guess the question is, how did it get deleted?

hmijail commented 2 years ago

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 make clean brought the state to a point common to both?

Relatedly, I just realized that if I try running the tests with the deprecated lit command, the problematic Output folder gets created again. So I guess those Output folders in my tree are remains from when lit was still the way to go.

All together, given that it looks like my tree is accumulating cruft because of deprecations and whatnot and that make clean doesn't do a deep clean, maybe I should just nuke the tree and clone the repo again?

MikaelMayer commented 2 years ago

Oh I did not realize that the lit command was creating these undesirable files for the dotnet test command. That's why I got these errors on the first place too on my machine that were not in the CI, because I was working on both. I think if it works and you are not using the lit test for this file again, you should be fine. I can't think yet of other things that might break. Of course, if you clone the repo again, you'll have problems that are easier to reproduce, but I don't think it's a viable long-term solution.